forked from Minki/linux
5b735eb1ce
The kernel documents smp_mb__after_unlock_lock() the following way:
"Place this after a lock-acquisition primitive to guarantee that
an UNLOCK+LOCK pair acts as a full barrier. This guarantee applies
if the UNLOCK and LOCK are executed by the same CPU or if the
UNLOCK and LOCK operate on the same lock variable."
Formalize in LKMM the above guarantee by defining (new) mb-links according
to the law:
([M] ; po ; [UL] ; (co | po) ; [LKW] ;
fencerel(After-unlock-lock) ; [M])
where the component ([UL] ; co ; [LKW]) identifies "UNLOCK+LOCK pairs on
the same lock variable" and the component ([UL] ; po ; [LKW]) identifies
"UNLOCK+LOCK pairs executed by the same CPU".
In particular, the LKMM forbids the following two behaviors (the second
litmus test below is based on:
Documentation/RCU/Design/Memory-Ordering/Tree-RCU-Memory-Ordering.html
c.f., Section "Tree RCU Grace Period Memory Ordering Building Blocks"):
C after-unlock-lock-same-cpu
(*
* Result: Never
*)
{}
P0(spinlock_t *s, spinlock_t *t, int *x, int *y)
{
int r0;
spin_lock(s);
WRITE_ONCE(*x, 1);
spin_unlock(s);
spin_lock(t);
smp_mb__after_unlock_lock();
r0 = READ_ONCE(*y);
spin_unlock(t);
}
P1(int *x, int *y)
{
int r0;
WRITE_ONCE(*y, 1);
smp_mb();
r0 = READ_ONCE(*x);
}
exists (0:r0=0 /\ 1:r0=0)
C after-unlock-lock-same-lock-variable
(*
* Result: Never
*)
{}
P0(spinlock_t *s, int *x, int *y)
{
int r0;
spin_lock(s);
WRITE_ONCE(*x, 1);
r0 = READ_ONCE(*y);
spin_unlock(s);
}
P1(spinlock_t *s, int *y, int *z)
{
int r0;
spin_lock(s);
smp_mb__after_unlock_lock();
WRITE_ONCE(*y, 1);
r0 = READ_ONCE(*z);
spin_unlock(s);
}
P2(int *z, int *x)
{
int r0;
WRITE_ONCE(*z, 1);
smp_mb();
r0 = READ_ONCE(*x);
}
exists (0:r0=0 /\ 1:r0=0 /\ 2:r0=0)
Signed-off-by: Andrea Parri <andrea.parri@amarulasolutions.com>
Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com>
Cc: Akira Yokosawa <akiyks@gmail.com>
Cc: Alan Stern <stern@rowland.harvard.edu>
Cc: Boqun Feng <boqun.feng@gmail.com>
Cc: Daniel Lustig <dlustig@nvidia.com>
Cc: David Howells <dhowells@redhat.com>
Cc: Jade Alglave <j.alglave@ucl.ac.uk>
Cc: Linus Torvalds <torvalds@linux-foundation.org>
Cc: Luc Maranget <luc.maranget@inria.fr>
Cc: Nicholas Piggin <npiggin@gmail.com>
Cc: Peter Zijlstra <peterz@infradead.org>
Cc: Thomas Gleixner <tglx@linutronix.de>
Cc: Will Deacon <will.deacon@arm.com>
Cc: linux-arch@vger.kernel.org
Cc: parri.andrea@gmail.com
Link: http://lkml.kernel.org/r/20181203230451.28921-1-paulmck@linux.ibm.com
Signed-off-by: Ingo Molnar <mingo@kernel.org>
131 lines
3.9 KiB
Plaintext
131 lines
3.9 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 appeared 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 appeared 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]) |
|
|
([M] ; po ; [UL] ; (co | po) ; [LKW] ;
|
|
fencerel(After-unlock-lock) ; [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 po-unlock-rf-lock-po = po ; [UL] ; rf ; [LKR] ; po
|
|
|
|
(**********************************)
|
|
(* 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)
|
|
let fence = strong-fence | wmb | po-rel | rmb | acq-po
|
|
let ppo = to-r | to-w | fence | (po-unlock-rf-lock-po & int)
|
|
|
|
(* Propagation: Ordering from release operations and strong fences. *)
|
|
let A-cumul(r) = rfe? ; r
|
|
let cumul-fence = A-cumul(strong-fence | po-rel) | wmb | po-unlock-rf-lock-po
|
|
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 rcu-link = hb* ; pb* ; prop
|
|
|
|
(*
|
|
* 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 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
|
|
*)
|