diff options
author | Alan Stern <stern@rowland.harvard.edu> | 2024-06-06 15:59:01 +0200 |
---|---|---|
committer | Paul E. McKenney <paulmck@kernel.org> | 2024-06-06 20:24:58 +0200 |
commit | ea6ee1bac6034cb4e91bcc229ed1354ca1a024d5 (patch) | |
tree | 2becc764127af9315b63812cd688c64a290bebf3 | |
parent | tools/memory-model: Fix bug in lock.cat (diff) | |
download | linux-ea6ee1bac6034cb4e91bcc229ed1354ca1a024d5.tar.xz linux-ea6ee1bac6034cb4e91bcc229ed1354ca1a024d5.zip |
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>
-rw-r--r-- | tools/memory-model/lock.cat | 56 |
1 files changed, 35 insertions, 21 deletions
diff --git a/tools/memory-model/lock.cat b/tools/memory-model/lock.cat index 21ba65086938..03c12efed66a 100644 --- a/tools/memory-model/lock.cat +++ b/tools/memory-model/lock.cat @@ -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 +(* + * 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 *) 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 *) 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 = (* - * Given an LF event r, compute the possible rfe edges for that event - * (all those starting from LKW events in other threads), - * and then convert that relation to a set of single-edge relations. + * Convert the possible-rfe-noncrit-lf relation for e + * to a set of single edges *) - let possible-rfe-lf r = - let pair-to-relation p = p ++ 0 - in map pair-to-relation ((LKW * {r}) & loc & ext) - (* Do this for each LF event r that isn't in rfi-lf *) - in map possible-rfe-lf (LF \ range(rfi-lf)) + let set-of-singleton-rfe-lf e = + map pair-to-relation (possible-rfe-noncrit-lf e) + (* Do this for each LF event e that isn't in rfi-lf *) + in map set-of-singleton-rfe-lf (LF \ range(rfi-lf)) (* Generate all rf relations for LF events *) with rfe-lf from cross(all-possible-rfe-lf) let rf-lf = rfe-lf | rfi-lf (* - * RU, i.e., spin_is_locked() returning False, is slightly different. - * We rely on the memory model to rule out cases where spin_is_locked() - * within one of the lock's critical sections returns False. + * A given RU event e may read internally from the last po-previous UL, + * or it may read from a UL event in another thread or the initial write. + * 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) -(* - * rf for RU events: an RU may read from an external UL or the initial write, - * or from the last po-previous UL - *) +(* Compute set of sets of possible rf edges for RU events *) let all-possible-rf-ru = - let possible-rf-ru r = - let pair-to-relation p = p ++ 0 - in map pair-to-relation ((((UL | IW) * {r}) & loc & ext) | - (((UL * {r}) & po-loc) \ ([UL] ; po-loc ; [LKW] ; po-loc))) - in map possible-rf-ru RU + (* Convert the possible-rf-ru relation for e to a set of single edges *) + let set-of-singleton-rf-ru e = + map pair-to-relation (possible-rf-ru e) + (* Do this for each RU event e *) + in map set-of-singleton-rf-ru RU (* Generate all rf relations for RU events *) with rf-ru from cross(all-possible-rf-ru) |