From 9d036883a17969caf8796d1fce813af0ab016986 Mon Sep 17 00:00:00 2001 From: Alan Stern Date: Mon, 14 May 2018 16:33:40 -0700 Subject: 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 Signed-off-by: Paul E. McKenney Reviewed-by: Boqun Feng Reviewed-by: Andrea Parri Cc: Andrew Morton Cc: Linus Torvalds Cc: Peter Zijlstra Cc: Thomas Gleixner Cc: Will Deacon 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 --- tools/memory-model/linux-kernel.cat | 33 ++++++++++++++++++++------------- 1 file changed, 20 insertions(+), 13 deletions(-) (limited to 'tools/memory-model/linux-kernel.cat') 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 + *) -- cgit v1.2.3