linux.git/tools/memory-model/linux-kernel.def, branch v6.12.80

tools/memory-model: Provide exact SRCU semantics

2023-03-22T19:02:21+00:00

LKMM has long provided only approximate handling of SRCU read-side
critical sections.  This has not been a pressing problem because LKMM's
traditional handling is correct for the common cases of non-overlapping
and properly nested critical sections.  However, LKMM's traditional
handling of partially overlapping critical sections incorrectly fuses
them into one large critical section.

For example, consider the following litmus test:

------------------------------------------------------------------------

C C-srcu-nest-5

(*
 * Result: Sometimes
 *
 * This demonstrates non-nested overlapping of SRCU read-side critical
 * sections.  Unlike RCU, SRCU critical sections do not unconditionally
 * nest.
 *)

{}

P0(int *x, int *y, struct srcu_struct *s1)
{
        int r1;
        int r2;
        int r3;
        int r4;

        r3 = srcu_read_lock(s1);
        r2 = READ_ONCE(*y);
        r4 = srcu_read_lock(s1);
        srcu_read_unlock(s1, r3);
        r1 = READ_ONCE(*x);
        srcu_read_unlock(s1, r4);
}

P1(int *x, int *y, struct srcu_struct *s1)
{
        WRITE_ONCE(*y, 1);
        synchronize_srcu(s1);
        WRITE_ONCE(*x, 1);
}

locations [0:r1]
exists (0:r1=1 /\ 0:r2=0)

------------------------------------------------------------------------

Current mainline incorrectly flattens the two critical sections into
one larger critical section, giving "Never" instead of the correct
"Sometimes":

------------------------------------------------------------------------

$ herd7 -conf linux-kernel.cfg C-srcu-nest-5.litmus
Test C-srcu-nest-5 Allowed
States 3
0:r1=0; 0:r2=0;
0:r1=0; 0:r2=1;
0:r1=1; 0:r2=1;
No
Witnesses
Positive: 0 Negative: 3
Flag srcu-bad-nesting
Condition exists (0:r1=1 /\ 0:r2=0)
Observation C-srcu-nest-5 Never 0 3
Time C-srcu-nest-5 0.01
Hash=e692c106cf3e84e20f12991dc438ff1b

------------------------------------------------------------------------

To its credit, it does complain about bad nesting.  But with this
commit we get the following result, which has the virtue of being
correct:

------------------------------------------------------------------------

$ herd7 -conf linux-kernel.cfg C-srcu-nest-5.litmus
Test C-srcu-nest-5 Allowed
States 4
0:r1=0; 0:r2=0;
0:r1=0; 0:r2=1;
0:r1=1; 0:r2=0;
0:r1=1; 0:r2=1;
Ok
Witnesses
Positive: 1 Negative: 3
Condition exists (0:r1=1 /\ 0:r2=0)
Observation C-srcu-nest-5 Sometimes 1 3
Time C-srcu-nest-5 0.05
Hash=e692c106cf3e84e20f12991dc438ff1b

------------------------------------------------------------------------

In addition, there are new srcu_down_read() and srcu_up_read()
functions on their way to mainline.  Roughly speaking, these are to
srcu_read_lock() and srcu_read_unlock() as down() and up() are to
mutex_lock() and mutex_unlock().  The key point is that
srcu_down_read() can execute in one process and the matching
srcu_up_read() in another, as shown in this litmus test:

------------------------------------------------------------------------

C C-srcu-nest-6

(*
 * Result: Never
 *
 * This would be valid for srcu_down_read() and srcu_up_read().
 *)

{}

P0(int *x, int *y, struct srcu_struct *s1, int *idx, int *f)
{
        int r2;
        int r3;

        r3 = srcu_down_read(s1);
        WRITE_ONCE(*idx, r3);
        r2 = READ_ONCE(*y);
        smp_store_release(f, 1);
}

P1(int *x, int *y, struct srcu_struct *s1, int *idx, int *f)
{
        int r1;
        int r3;
        int r4;

        r4 = smp_load_acquire(f);
        r1 = READ_ONCE(*x);
        r3 = READ_ONCE(*idx);
        srcu_up_read(s1, r3);
}

P2(int *x, int *y, struct srcu_struct *s1)
{
        WRITE_ONCE(*y, 1);
        synchronize_srcu(s1);
        WRITE_ONCE(*x, 1);
}

locations [0:r1]
filter (1:r4=1)
exists (1:r1=1 /\ 0:r2=0)

------------------------------------------------------------------------

When run on current mainline, this litmus test gets a complaint about
an unknown macro srcu_down_read().  With this commit:

------------------------------------------------------------------------

herd7 -conf linux-kernel.cfg C-srcu-nest-6.litmus
Test C-srcu-nest-6 Allowed
States 3
0:r1=0; 0:r2=0; 1:r1=0;
0:r1=0; 0:r2=1; 1:r1=0;
0:r1=0; 0:r2=1; 1:r1=1;
No
Witnesses
Positive: 0 Negative: 3
Condition exists (1:r1=1 /\ 0:r2=0)
Observation C-srcu-nest-6 Never 0 3
Time C-srcu-nest-6 0.02
Hash=c1f20257d052ca5e899be508bedcb2a1

------------------------------------------------------------------------

Note that the user must supply the flag "f" and the "filter" clause,
similar to what must be done to emulate call_rcu().

The commit works by treating srcu_read_lock()/srcu_down_read() as
loads and srcu_read_unlock()/srcu_up_read() as stores.  This allows us
to determine which unlock matches which lock by looking for a data
dependency between them.  In order for this to work properly, the data
dependencies have to be tracked through stores to intermediate
variables such as "idx" in the litmus test above; this is handled by
the new carry-srcu-data relation.  But it's important here (and in the
existing carry-dep relation) to avoid tracking the dependencies
through SRCU unlock stores.  Otherwise, in situations resembling:

	A: r1 = srcu_read_lock(s);
	B: srcu_read_unlock(s, r1);
	C: r2 = srcu_read_lock(s);
	D: srcu_read_unlock(s, r2);

it would look as if D was dependent on both A and C, because "s" would
appear to be an intermediate variable written by B and read by C.
This explains the complications in the definitions of carry-srcu-dep
and carry-dep.

As a debugging aid, the commit adds a check for errors in which the
value returned by one call to srcu_read_lock()/srcu_down_read() is
passed to more than one instance of srcu_read_unlock()/srcu_up_read().

Finally, since these SRCU-related primitives are now treated as
ordinary reads and writes, we have to add them into the lists of
marked accesses (i.e., not subject to data races) and lock-related
accesses (i.e., one shouldn't try to access an srcu_struct with a
non-lock-related primitive such as READ_ONCE() or a plain write).

Portions of this approach were suggested by Boqun Feng and Jonas
Oberhauser.

[ paulmck: Fix space-before-tab whitespace nit. ]

Reported-by: Paul E. McKenney 
Signed-off-by: Alan Stern 
Reviewed-by: Jonas Oberhauser 
Signed-off-by: Paul E. McKenney

tools/memory-model: Add smp_mb__after_srcu_read_unlock()

2023-03-22T19:02:21+00:00

This commit adds support for smp_mb__after_srcu_read_unlock(), which,
when combined with a prior srcu_read_unlock(), implies a full memory
barrier.  No ordering is guaranteed to accesses between the two, and
placing accesses between is bad practice in any case.

Tests may be found at https://github.com/paulmckrcu/litmus in files
matching manual/kernel/C-srcu-mb-*.litmus.

Signed-off-by: Paul E. McKenney

tools/memory-model: Add data-race detection

2019-05-28T15:18:21+00:00

This patch adds data-race detection to the Linux-Kernel Memory Model.
As part of this effort, support is added for:

	compiler barriers (the barrier() function), and

	a new Preserved Program Order term: (addr ; [Plain] ; wmb)

Data races are marked with a special Flag warning in herd.  It is
not guaranteed that the model will provide accurate predictions when a
data race is present.

The patch does not include documentation for the data-race detection
facility.  The basic design has been explained in various emails, and
a separate documentation patch will be submitted later.

This work is based on an earlier formulation of data races for the
LKMM by Andrea Parri.

Signed-off-by: Alan Stern 
Reviewed-by: Andrea Parri 
Signed-off-by: Paul E. McKenney

tools/memory-model: Add support for synchronize_srcu_expedited()

2019-04-04T20:48:34+00:00

Given that synchronize_rcu_expedited() is supported, this commit adds
support for synchronize_srcu_expedited().

Signed-off-by: Paul E. McKenney 
Acked-by: Andrea Parri

tools/memory-model: Dynamically check SRCU lock-to-unlock matching

2019-03-18T17:27:52+00:00

This commit checks that the return value of srcu_read_lock() is passed
to the matching srcu_read_unlock(), where "matching" is determined by
nesting.  This check operates as follows:

   1. srcu_read_lock() creates an integer token, which is stored into
      the generated events.
   2. srcu_read_unlock() records its second (token) argument into the
      generated event.
   3. A new herd primitive 'different-values' filters out pairs of events
      with identical values from the relation passed as its argument.
   4. The bell file applies the above primitive to the (srcu)
      read-side-critical-section relation 'srcu-rscs' and flags non-empty
      results.

BEWARE: Works only with herd version 7.51+6 and onwards.

Signed-off-by: Luc Maranget 
Signed-off-by: Paul E. McKenney 
[ paulmck: Apply Andrea Parri's off-list feedback. ]
Acked-by: Alan Stern

tools/memory-model: Add SRCU support

2019-03-18T17:27:52+00:00

Add support for SRCU.  Herd creates srcu events and linux-kernel.def
associates them with three possible annotations (srcu-lock,
srcu-unlock, and sync-srcu) corresponding to the API routines
srcu_read_lock(), srcu_read_unlock(), and synchronize_srcu().

The linux-kernel.bell file now declares the annotations
and determines matching lock/unlock pairs delimiting SRCU read-side
critical sections, and it also checks for synchronize_srcu() calls
inside an RCU critical section (which would generate a "sleeping in
atomic context" error in real kernel code).  The linux-kernel.cat file
now adds SRCU-induced ordering, analogous to the existing RCU-induced
ordering, to the gp and rcu-fence relations.

Curiously enough, these small changes to the model's .cat code are all
that is needed to describe SRCU.

Portions of this patch (linux-kernel.def and the first hunk in
linux-kernel.bell) were written by Luc Maranget.

Signed-off-by: Alan Stern 
CC: Luc Maranget 
Signed-off-by: Paul E. McKenney 
Tested-by: Andrea Parri

tools/memory-model: Model smp_mb__after_unlock_lock()

2019-01-21T10:06:55+00:00

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 
Signed-off-by: Paul E. McKenney 
Cc: Akira Yokosawa 
Cc: Alan Stern 
Cc: Boqun Feng 
Cc: Daniel Lustig 
Cc: David Howells 
Cc: Jade Alglave 
Cc: Linus Torvalds 
Cc: Luc Maranget 
Cc: Nicholas Piggin 
Cc: Peter Zijlstra 
Cc: Thomas Gleixner 
Cc: Will Deacon 
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

tools/memory-model: Update ASPLOS information

2018-05-15T06:11:18+00:00

ASPLOS 2018 was held in March: make sure this is reflected in
header comments and references.

Signed-off-by: Andrea Parri 
Signed-off-by: Paul E. McKenney 
Cc: Akira Yokosawa 
Cc: Alan Stern 
Cc: Andrew Morton 
Cc: Boqun Feng 
Cc: David Howells 
Cc: Jade Alglave 
Cc: Linus Torvalds 
Cc: Luc Maranget 
Cc: Nicholas Piggin 
Cc: Peter Zijlstra 
Cc: Thomas Gleixner 
Cc: Will Deacon 
Cc: linux-arch@vger.kernel.org
Cc: parri.andrea@gmail.com
Link: http://lkml.kernel.org/r/1526340837-12222-18-git-send-email-paulmck@linux.vnet.ibm.com
Signed-off-by: Ingo Molnar

tools/memory-model: Add model support for spin_is_locked()

2018-05-15T06:11:17+00:00

This commit first adds a trivial macro for spin_is_locked() to
linux-kernel.def.

It also adds cat code for enumerating all possible matches of lock
write events (set LKW) with islocked events returning true (set RL,
for Read from Lock), and unlock write events (set UL) with islocked
events returning false (set RU, for Read from Unlock).  Note that this
intentionally does not model uniprocessor kernels (CONFIG_SMP=n) built
with CONFIG_DEBUG_SPINLOCK=n, in which spin_is_locked() unconditionally
returns zero.

It also adds a pair of litmus tests demonstrating the minimal ordering
provided by spin_is_locked() in conjunction with spin_lock().  Will Deacon
noted that this minimal ordering happens on ARMv8:
https://lkml.kernel.org/r/20180226162426.GB17158@arm.com

Notice that herd7 installations strictly older than version 7.49
do not handle the new constructs.

Signed-off-by: Luc Maranget 
Signed-off-by: Paul E. McKenney 
Reviewed-by: Alan Stern 
Cc: Akira Yokosawa 
Cc: Andrea Parri 
Cc: Andrew Morton 
Cc: Boqun Feng 
Cc: David Howells 
Cc: Jade Alglave 
Cc: Linus Torvalds 
Cc: Luc Maranget 
Cc: Nicholas Piggin 
Cc: Peter Zijlstra 
Cc: Thomas Gleixner 
Cc: Will Deacon 
Cc: linux-arch@vger.kernel.org
Link: http://lkml.kernel.org/r/1526340837-12222-10-git-send-email-paulmck@linux.vnet.ibm.com
Signed-off-by: Ingo Molnar

tools/memory-model: Fix coding style in 'linux-kernel.def'

2018-05-15T06:11:17+00:00

This commit fixes white spaces around semicolons.

Signed-off-by: Andrea Parri 
Signed-off-by: Paul E. McKenney 
Cc: Andrew Morton 
Cc: Linus Torvalds 
Cc: Peter Zijlstra 
Cc: Thomas Gleixner 
Cc: Will Deacon 
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: npiggin@gmail.com
Cc: parri.andrea@gmail.com
Cc: stern@rowland.harvard.edu
Link: http://lkml.kernel.org/r/1526340837-12222-8-git-send-email-paulmck@linux.vnet.ibm.com
Signed-off-by: Ingo Molnar