diff options
| author | Alan Stern <stern@rowland.harvard.edu> | 2018-05-14 16:33:40 -0700 |
|---|---|---|
| committer | Ingo Molnar <mingo@kernel.org> | 2018-05-15 08:11:16 +0200 |
| commit | 9d036883a17969caf8796d1fce813af0ab016986 (patch) | |
| tree | 5c9bcd17f62f63a8a3d85cb5abb9bf33a6d4cceb /tools/memory-model/linux-kernel.cat | |
| parent | 1ee2da5f9b5a8e814b397b77a08d44fed5f96a4a (diff) | |
tools/memory-model: Redefine rb in terms of rcu-fence
This patch reorganizes the definition of rb in the Linux Kernel Memory
Consistency Model. The relation is now expressed in terms of
rcu-fence, which consists of a sequence of gp and rscs links separated
by rcu-link links, in which the number of occurrences of gp is >= the
number of occurrences of rscs.
Arguments similar to those published in
http://diy.inria.fr/linux/long.pdf show that rcu-fence behaves like an
inter-CPU strong fence. Furthermore, the definition of rb in terms of
rcu-fence is highly analogous to the definition of pb in terms of
strong-fence, which can help explain why rcu-path expresses a form of
temporal ordering.
This change should not affect the semantics of the memory model, just
its internal organization.
Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
Reviewed-by: Boqun Feng <boqun.feng@gmail.com>
Reviewed-by: Andrea Parri <parri.andrea@gmail.com>
Cc: Andrew Morton <akpm@linux-foundation.org>
Cc: Linus Torvalds <torvalds@linux-foundation.org>
Cc: Peter Zijlstra <peterz@infradead.org>
Cc: Thomas Gleixner <tglx@linutronix.de>
Cc: Will Deacon <will.deacon@arm.com>
Cc: akiyks@gmail.com
Cc: dhowells@redhat.com
Cc: j.alglave@ucl.ac.uk
Cc: linux-arch@vger.kernel.org
Cc: luc.maranget@inria.fr
Cc: npiggin@gmail.com
Link: http://lkml.kernel.org/r/1526340837-12222-2-git-send-email-paulmck@linux.vnet.ibm.com
Signed-off-by: Ingo Molnar <mingo@kernel.org>
Diffstat (limited to 'tools/memory-model/linux-kernel.cat')
| -rw-r--r-- | tools/memory-model/linux-kernel.cat | 33 |
1 files changed, 20 insertions, 13 deletions
diff --git a/tools/memory-model/linux-kernel.cat b/tools/memory-model/linux-kernel.cat index cdf682859d4e..1e5c4653dd12 100644 --- a/tools/memory-model/linux-kernel.cat +++ b/tools/memory-model/linux-kernel.cat @@ -102,20 +102,27 @@ let rscs = po ; crit^-1 ; po? *) let rcu-link = hb* ; pb* ; prop -(* Chains that affect the RCU grace-period guarantee *) -let gp-link = gp ; rcu-link -let rscs-link = rscs ; rcu-link - (* - * A cycle containing at least as many grace periods as RCU read-side - * critical sections is forbidden. + * Any sequence containing at least as many grace periods as RCU read-side + * critical sections (joined by rcu-link) acts as a generalized strong fence. *) -let rec rb = - gp-link | - (gp-link ; rscs-link) | - (rscs-link ; gp-link) | - (rb ; rb) | - (gp-link ; rb ; rscs-link) | - (rscs-link ; rb ; gp-link) +let rec rcu-fence = gp | + (gp ; rcu-link ; rscs) | + (rscs ; rcu-link ; gp) | + (gp ; rcu-link ; rcu-fence ; rcu-link ; rscs) | + (rscs ; rcu-link ; rcu-fence ; rcu-link ; gp) | + (rcu-fence ; rcu-link ; rcu-fence) + +(* rb orders instructions just as pb does *) +let rb = prop ; rcu-fence ; hb* ; pb* irreflexive rb as rcu + +(* + * The happens-before, propagation, and rcu constraints are all + * expressions of temporal ordering. They could be replaced by + * a single constraint on an "executes-before" relation, xb: + * + * let xb = hb | pb | rb + * acyclic xb as executes-before + *) |