From ddfe12944e84830fe7dc490992e55b4fa773555e Mon Sep 17 00:00:00 2001 From: Boqun Feng Date: Mon, 25 Oct 2021 22:54:14 +0800 Subject: tools/memory-model: Provide extra ordering for unlock+lock pair on the same CPU A recent discussion[1] shows that we are in favor of strengthening the ordering of unlock + lock on the same CPU: a unlock and a po-after lock should provide the so-called RCtso ordering, that is a memory access S po-before the unlock should be ordered against a memory access R po-after the lock, unless S is a store and R is a load. The strengthening meets programmers' expection that "sequence of two locked regions to be ordered wrt each other" (from Linus), and can reduce the mental burden when using locks. Therefore add it in LKMM. [1]: https://lore.kernel.org/lkml/20210909185937.GA12379@rowland.harvard.edu/ Co-developed-by: Alan Stern Signed-off-by: Alan Stern Signed-off-by: Boqun Feng Reviewed-by: Michael Ellerman (powerpc) Acked-by: Palmer Dabbelt (RISC-V) Acked-by: Peter Zijlstra (Intel) Signed-off-by: Paul E. McKenney --- tools/memory-model/linux-kernel.cat | 6 +++--- 1 file changed, 3 insertions(+), 3 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 2a9b4fe4a84e..d70315fddef6 100644 --- a/tools/memory-model/linux-kernel.cat +++ b/tools/memory-model/linux-kernel.cat @@ -27,7 +27,7 @@ include "lock.cat" (* Release Acquire *) let acq-po = [Acquire] ; po ; [M] let po-rel = [M] ; po ; [Release] -let po-unlock-rf-lock-po = po ; [UL] ; rf ; [LKR] ; po +let po-unlock-lock-po = po ; [UL] ; (po|rf) ; [LKR] ; po (* Fences *) let R4rmb = R \ Noreturn (* Reads for which rmb works *) @@ -70,12 +70,12 @@ let rwdep = (dep | ctrl) ; [W] let overwrite = co | fr let to-w = rwdep | (overwrite & int) | (addr ; [Plain] ; wmb) let to-r = addr | (dep ; [Marked] ; rfi) -let ppo = to-r | to-w | fence | (po-unlock-rf-lock-po & int) +let ppo = to-r | to-w | fence | (po-unlock-lock-po & int) (* Propagation: Ordering from release operations and strong fences. *) let A-cumul(r) = (rfe ; [Marked])? ; r let cumul-fence = [Marked] ; (A-cumul(strong-fence | po-rel) | wmb | - po-unlock-rf-lock-po) ; [Marked] + po-unlock-lock-po) ; [Marked] let prop = [Marked] ; (overwrite & ext)? ; cumul-fence* ; [Marked] ; rfe? ; [Marked] -- cgit v1.2.3-70-g09d2