tools/memory-model: Code reorganization in lock.cat
Code reorganization for the lock.cat file in tools/memory-model: Improve the efficiency by ruling out right at the start RU events (spin_is_locked() calls that return False) inside a critical section for the same lock. Improve the organization of the code for handling LF and RU events by pulling the definitions of the pair-to-relation macro out from two different complicated compound expressions, using a single standalone definition instead. Rewrite the calculations of the rf relation for LF and RU events, for greater clarity. Signed-off-by: Alan Stern <stern@rowland.harvard.edu> Tested-by: Andrea Parri <parri.andrea@gmail.com> Acked-by: Andrea Parri <parri.andrea@gmail.com> Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
This commit is contained in:
parent
4c830eef80
commit
ea6ee1bac6
@ -54,6 +54,12 @@ flag ~empty LKR \ domain(lk-rmw) as unpaired-LKR
|
|||||||
*)
|
*)
|
||||||
empty ([LKW] ; po-loc ; [LKR]) \ (po-loc ; [UL] ; po-loc) as lock-nest
|
empty ([LKW] ; po-loc ; [LKR]) \ (po-loc ; [UL] ; po-loc) as lock-nest
|
||||||
|
|
||||||
|
(*
|
||||||
|
* In the same way, spin_is_locked() inside a critical section must always
|
||||||
|
* return True (no RU events can be in a critical section for the same lock).
|
||||||
|
*)
|
||||||
|
empty ([LKW] ; po-loc ; [RU]) \ (po-loc ; [UL] ; po-loc) as nested-is-locked
|
||||||
|
|
||||||
(* The final value of a spinlock should not be tested *)
|
(* The final value of a spinlock should not be tested *)
|
||||||
flag ~empty [FW] ; loc ; [ALL-LOCKS] as lock-final
|
flag ~empty [FW] ; loc ; [ALL-LOCKS] as lock-final
|
||||||
|
|
||||||
@ -79,39 +85,47 @@ empty ([UNMATCHED-LKW] ; loc ; [UNMATCHED-LKW]) \ id as unmatched-locks
|
|||||||
(* rfi for LF events: link each LKW to the LF events in its critical section *)
|
(* rfi for LF events: link each LKW to the LF events in its critical section *)
|
||||||
let rfi-lf = ([LKW] ; po-loc ; [LF]) \ ([LKW] ; po-loc ; [UL] ; po-loc)
|
let rfi-lf = ([LKW] ; po-loc ; [LF]) \ ([LKW] ; po-loc ; [UL] ; po-loc)
|
||||||
|
|
||||||
(* rfe for LF events *)
|
(* Utility macro to convert a single pair to a single-edge relation *)
|
||||||
|
let pair-to-relation p = p ++ 0
|
||||||
|
|
||||||
|
(*
|
||||||
|
* If a given LF event e is outside a critical section, it cannot read
|
||||||
|
* internally but it may read from an LKW event in another thread.
|
||||||
|
* Compute the relation containing these possible edges.
|
||||||
|
*)
|
||||||
|
let possible-rfe-noncrit-lf e = (LKW * {e}) & loc & ext
|
||||||
|
|
||||||
|
(* Compute set of sets of possible rfe edges for LF events *)
|
||||||
let all-possible-rfe-lf =
|
let all-possible-rfe-lf =
|
||||||
(*
|
(*
|
||||||
* Given an LF event r, compute the possible rfe edges for that event
|
* Convert the possible-rfe-noncrit-lf relation for e
|
||||||
* (all those starting from LKW events in other threads),
|
* to a set of single edges
|
||||||
* and then convert that relation to a set of single-edge relations.
|
|
||||||
*)
|
*)
|
||||||
let possible-rfe-lf r =
|
let set-of-singleton-rfe-lf e =
|
||||||
let pair-to-relation p = p ++ 0
|
map pair-to-relation (possible-rfe-noncrit-lf e)
|
||||||
in map pair-to-relation ((LKW * {r}) & loc & ext)
|
(* Do this for each LF event e that isn't in rfi-lf *)
|
||||||
(* Do this for each LF event r that isn't in rfi-lf *)
|
in map set-of-singleton-rfe-lf (LF \ range(rfi-lf))
|
||||||
in map possible-rfe-lf (LF \ range(rfi-lf))
|
|
||||||
|
|
||||||
(* Generate all rf relations for LF events *)
|
(* Generate all rf relations for LF events *)
|
||||||
with rfe-lf from cross(all-possible-rfe-lf)
|
with rfe-lf from cross(all-possible-rfe-lf)
|
||||||
let rf-lf = rfe-lf | rfi-lf
|
let rf-lf = rfe-lf | rfi-lf
|
||||||
|
|
||||||
(*
|
(*
|
||||||
* RU, i.e., spin_is_locked() returning False, is slightly different.
|
* A given RU event e may read internally from the last po-previous UL,
|
||||||
* We rely on the memory model to rule out cases where spin_is_locked()
|
* or it may read from a UL event in another thread or the initial write.
|
||||||
* within one of the lock's critical sections returns False.
|
* Compute the relation containing these possible edges.
|
||||||
*)
|
*)
|
||||||
|
let possible-rf-ru e = (((UL * {e}) & po-loc) \
|
||||||
|
([UL] ; po-loc ; [UL] ; po-loc)) |
|
||||||
|
(((UL | IW) * {e}) & loc & ext)
|
||||||
|
|
||||||
(*
|
(* Compute set of sets of possible rf edges for RU events *)
|
||||||
* rf for RU events: an RU may read from an external UL or the initial write,
|
|
||||||
* or from the last po-previous UL
|
|
||||||
*)
|
|
||||||
let all-possible-rf-ru =
|
let all-possible-rf-ru =
|
||||||
let possible-rf-ru r =
|
(* Convert the possible-rf-ru relation for e to a set of single edges *)
|
||||||
let pair-to-relation p = p ++ 0
|
let set-of-singleton-rf-ru e =
|
||||||
in map pair-to-relation ((((UL | IW) * {r}) & loc & ext) |
|
map pair-to-relation (possible-rf-ru e)
|
||||||
(((UL * {r}) & po-loc) \ ([UL] ; po-loc ; [LKW] ; po-loc)))
|
(* Do this for each RU event e *)
|
||||||
in map possible-rf-ru RU
|
in map set-of-singleton-rf-ru RU
|
||||||
|
|
||||||
(* Generate all rf relations for RU events *)
|
(* Generate all rf relations for RU events *)
|
||||||
with rf-ru from cross(all-possible-rf-ru)
|
with rf-ru from cross(all-possible-rf-ru)
|
||||||
|
Loading…
Reference in New Issue
Block a user