From bf28ae5627442355dbb8d99238da4fb95c2dd4ec Mon Sep 17 00:00:00 2001 From: Alan Stern Date: Tue, 20 Feb 2018 15:25:12 -0800 Subject: tools/memory-model: Remove rb-dep, smp_read_barrier_depends, and lockless_dereference Since commit 76ebbe78f739 ("locking/barriers: Add implicit smp_read_barrier_depends() to READ_ONCE()") was merged for the 4.15 kernel, it has not been necessary to use smp_read_barrier_depends(). Similarly, commit 59ecbbe7b31c ("locking/barriers: Kill lockless_dereference()") removed lockless_dereference() from the kernel. Since these primitives are no longer part of the kernel, they do not belong in the Linux Kernel Memory Consistency Model. This patch removes them, along with the internal rb-dep relation, and updates the revelant documentation. Signed-off-by: Alan Stern Signed-off-by: Paul E. McKenney Acked-by: Peter Zijlstra Cc: Linus Torvalds Cc: Thomas Gleixner Cc: akiyks@gmail.com Cc: boqun.feng@gmail.com Cc: dhowells@redhat.com Cc: j.alglave@ucl.ac.uk Cc: linux-arch@vger.kernel.org Cc: luc.maranget@inria.fr Cc: nborisov@suse.com Cc: npiggin@gmail.com Cc: parri.andrea@gmail.com Cc: will.deacon@arm.com Link: http://lkml.kernel.org/r/1519169112-20593-12-git-send-email-paulmck@linux.vnet.ibm.com Signed-off-by: Ingo Molnar --- tools/memory-model/linux-kernel.cat | 7 ++----- 1 file changed, 2 insertions(+), 5 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 f0d27f813ec2..df97db03b6c2 100644 --- a/tools/memory-model/linux-kernel.cat +++ b/tools/memory-model/linux-kernel.cat @@ -25,7 +25,6 @@ include "lock.cat" (*******************) (* Fences *) -let rb-dep = [R] ; fencerel(Rb_dep) ; [R] let rmb = [R \ Noreturn] ; fencerel(Rmb) ; [R \ Noreturn] let wmb = [W] ; fencerel(Wmb) ; [W] let mb = ([M] ; fencerel(Mb) ; [M]) | @@ -61,11 +60,9 @@ let dep = addr | data let rwdep = (dep | ctrl) ; [W] let overwrite = co | fr let to-w = rwdep | (overwrite & int) -let rrdep = addr | (dep ; rfi) -let strong-rrdep = rrdep+ & rb-dep -let to-r = strong-rrdep | rfi-rel-acq +let to-r = addr | (dep ; rfi) | rfi-rel-acq let fence = strong-fence | wmb | po-rel | rmb | acq-po -let ppo = rrdep* ; (to-r | to-w | fence) +let ppo = to-r | to-w | fence (* Propagation: Ordering from release operations and strong fences. *) let A-cumul(r) = rfe? ; r -- cgit v1.2.3