mirror of
https://mirrors.bfsu.edu.cn/git/linux.git
synced 2024-11-16 08:44:21 +08:00
bf28ae5627
Since commit76ebbe78f7("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, commit59ecbbe7b3("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 <stern@rowland.harvard.edu> Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com> Acked-by: Peter Zijlstra <peterz@infradead.org> Cc: Linus Torvalds <torvalds@linux-foundation.org> Cc: Thomas Gleixner <tglx@linutronix.de> 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 <mingo@kernel.org>
122 lines
3.4 KiB
Plaintext
122 lines
3.4 KiB
Plaintext
// SPDX-License-Identifier: GPL-2.0+
|
|
(*
|
|
* Copyright (C) 2015 Jade Alglave <j.alglave@ucl.ac.uk>,
|
|
* Copyright (C) 2016 Luc Maranget <luc.maranget@inria.fr> for Inria
|
|
* Copyright (C) 2017 Alan Stern <stern@rowland.harvard.edu>,
|
|
* Andrea Parri <parri.andrea@gmail.com>
|
|
*
|
|
* An earlier version of this file appears in the companion webpage for
|
|
* "Frightening small children and disconcerting grown-ups: Concurrency
|
|
* in the Linux kernel" by Alglave, Maranget, McKenney, Parri, and Stern,
|
|
* which is to appear in ASPLOS 2018.
|
|
*)
|
|
|
|
"Linux-kernel memory consistency model"
|
|
|
|
(*
|
|
* File "lock.cat" handles locks and is experimental.
|
|
* It can be replaced by include "cos.cat" for tests that do not use locks.
|
|
*)
|
|
|
|
include "lock.cat"
|
|
|
|
(*******************)
|
|
(* Basic relations *)
|
|
(*******************)
|
|
|
|
(* Fences *)
|
|
let rmb = [R \ Noreturn] ; fencerel(Rmb) ; [R \ Noreturn]
|
|
let wmb = [W] ; fencerel(Wmb) ; [W]
|
|
let mb = ([M] ; fencerel(Mb) ; [M]) |
|
|
([M] ; fencerel(Before-atomic) ; [RMW] ; po? ; [M]) |
|
|
([M] ; po? ; [RMW] ; fencerel(After-atomic) ; [M]) |
|
|
([M] ; po? ; [LKW] ; fencerel(After-spinlock) ; [M])
|
|
let gp = po ; [Sync-rcu] ; po?
|
|
|
|
let strong-fence = mb | gp
|
|
|
|
(* Release Acquire *)
|
|
let acq-po = [Acquire] ; po ; [M]
|
|
let po-rel = [M] ; po ; [Release]
|
|
let rfi-rel-acq = [Release] ; rfi ; [Acquire]
|
|
|
|
(**********************************)
|
|
(* Fundamental coherence ordering *)
|
|
(**********************************)
|
|
|
|
(* Sequential Consistency Per Variable *)
|
|
let com = rf | co | fr
|
|
acyclic po-loc | com as coherence
|
|
|
|
(* Atomic Read-Modify-Write *)
|
|
empty rmw & (fre ; coe) as atomic
|
|
|
|
(**********************************)
|
|
(* Instruction execution ordering *)
|
|
(**********************************)
|
|
|
|
(* Preserved Program Order *)
|
|
let dep = addr | data
|
|
let rwdep = (dep | ctrl) ; [W]
|
|
let overwrite = co | fr
|
|
let to-w = rwdep | (overwrite & int)
|
|
let to-r = addr | (dep ; rfi) | rfi-rel-acq
|
|
let fence = strong-fence | wmb | po-rel | rmb | acq-po
|
|
let ppo = to-r | to-w | fence
|
|
|
|
(* Propagation: Ordering from release operations and strong fences. *)
|
|
let A-cumul(r) = rfe? ; r
|
|
let cumul-fence = A-cumul(strong-fence | po-rel) | wmb
|
|
let prop = (overwrite & ext)? ; cumul-fence* ; rfe?
|
|
|
|
(*
|
|
* Happens Before: Ordering from the passage of time.
|
|
* No fences needed here for prop because relation confined to one process.
|
|
*)
|
|
let hb = ppo | rfe | ((prop \ id) & int)
|
|
acyclic hb as happens-before
|
|
|
|
(****************************************)
|
|
(* Write and fence propagation ordering *)
|
|
(****************************************)
|
|
|
|
(* Propagation: Each non-rf link needs a strong fence. *)
|
|
let pb = prop ; strong-fence ; hb*
|
|
acyclic pb as propagation
|
|
|
|
(*******)
|
|
(* RCU *)
|
|
(*******)
|
|
|
|
(*
|
|
* Effect of read-side critical section proceeds from the rcu_read_lock()
|
|
* onward on the one hand and from the rcu_read_unlock() backwards on the
|
|
* other hand.
|
|
*)
|
|
let rscs = po ; crit^-1 ; po?
|
|
|
|
(*
|
|
* The synchronize_rcu() strong fence is special in that it can order not
|
|
* one but two non-rf relations, but only in conjunction with an RCU
|
|
* read-side critical section.
|
|
*)
|
|
let link = hb* ; pb* ; prop
|
|
|
|
(* Chains that affect the RCU grace-period guarantee *)
|
|
let gp-link = gp ; link
|
|
let rscs-link = rscs ; link
|
|
|
|
(*
|
|
* A cycle containing at least as many grace periods as RCU read-side
|
|
* critical sections is forbidden.
|
|
*)
|
|
let rec rcu-path =
|
|
gp-link |
|
|
(gp-link ; rscs-link) |
|
|
(rscs-link ; gp-link) |
|
|
(rcu-path ; rcu-path) |
|
|
(gp-link ; rcu-path ; rscs-link) |
|
|
(rscs-link ; rcu-path ; gp-link)
|
|
|
|
irreflexive rcu-path as rcu
|