linux-toradex.git/tools/memory-model/linux-kernel.cat, branch v5.19-rc7

tools/memory-model: Provide extra ordering for unlock+lock pair on the same CPU

2021-12-01T01:47:08+00:00

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: Fix data race detection for unordered store and load

2019-10-05T18:58:14+00:00

Currently the Linux Kernel Memory Model gives an incorrect response
for the following litmus test:

C plain-WWC

{}

P0(int *x)
{
	WRITE_ONCE(*x, 2);
}

P1(int *x, int *y)
{
	int r1;
	int r2;
	int r3;

	r1 = READ_ONCE(*x);
	if (r1 == 2) {
		smp_rmb();
		r2 = *x;
	}
	smp_rmb();
	r3 = READ_ONCE(*x);
	WRITE_ONCE(*y, r3 - 1);
}

P2(int *x, int *y)
{
	int r4;

	r4 = READ_ONCE(*y);
	if (r4 > 0)
		WRITE_ONCE(*x, 1);
}

exists (x=2 /\ 1:r2=2 /\ 2:r4=1)

The memory model says that the plain read of *x in P1 races with the
WRITE_ONCE(*x) in P2.

The problem is that we have a write W and a read R related by neither
fre or rfe, but rather W ->coe W' ->rfe R, where W' is an intermediate
write (the WRITE_ONCE() in P0).  In this situation there is no
particular ordering between W and R, so either a wr-vis link from W to
R or an rw-xbstar link from R to W would prove that the accesses
aren't concurrent.

But the LKMM only looks for a wr-vis link, which is equivalent to
assuming that W must execute before R.  This is not necessarily true
on non-multicopy-atomic systems, as the WWC pattern demonstrates.

This patch changes the LKMM to accept either a wr-vis or a reverse
rw-xbstar link as a proof of non-concurrency.

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

tools/memory-model: Improve data-race detection

2019-06-24T16:08:54+00:00

Herbert Xu recently reported a problem concerning RCU and compiler
barriers. In the course of discussing the problem, he put forth a
litmus test which illustrated a serious defect in the Linux Kernel
Memory Model's data-race-detection code [1].

The defect was that the LKMM assumed visibility and executes-before
ordering of plain accesses had to be mediated by marked accesses. In
Herbert's litmus test this wasn't so, and the LKMM claimed the litmus
test was allowed and contained a data race although neither is true.

In fact, plain accesses can be ordered by fences even in the absence
of marked accesses. In most cases this doesn't matter, because most
fences only order accesses within a single thread. But the rcu-fence
relation is different; it can order (and induce visibility between)
accesses in different threads -- events which otherwise might be
concurrent. This makes it relevant to data-race detection.

This patch makes two changes to the memory model to incorporate the
new insight:

If a store is separated by a fence from another access,
the store is necessarily visible to the other access (as
reflected in the ww-vis and wr-vis relations). Similarly,
if a load is separated by a fence from another access then
the load necessarily executes before the other access (as
reflected in the rw-xbstar relation).

If a store is separated by a strong fence from a marked access
then it is necessarily visible to any access that executes
after the marked access (as reflected in the ww-vis and wr-vis
relations).

With these changes, the LKMM gives the desired result for Herbert's
litmus test and other related ones [2].

[1] https://lore.kernel.org/lkml/Pine.LNX.4.44L0.1906041026570.1731-100000@iolanthe.rowland.org/

[2] https://github.com/paulmckrcu/litmus/blob/master/manual/plain/C-S-rcunoderef-1.litmus
https://github.com/paulmckrcu/litmus/blob/master/manual/plain/C-S-rcunoderef-2.litmus
https://github.com/paulmckrcu/litmus/blob/master/manual/plain/C-S-rcunoderef-3.litmus
https://github.com/paulmckrcu/litmus/blob/master/manual/plain/C-S-rcunoderef-4.litmus
https://github.com/paulmckrcu/litmus/blob/master/manual/plain/strong-vis.litmus

Reported-by: Herbert Xu
Signed-off-by: Alan Stern
Acked-by: Andrea Parri
Signed-off-by: Paul E. McKenney
Tested-by: Akira Yokosawa

tools/memory-model: Change definition of rcu-fence

2019-06-21T23:20:49+00:00

The rcu-fence relation in the Linux Kernel Memory Model is not well
named.  It doesn't act like any other fence relation, in that it does
not relate events before a fence to events after that fence.  All it
does is relate certain RCU events to one another (those that are
ordered by the RCU Guarantee); this induces an actual
strong-fence-like relation linking events preceding the first RCU
event to those following the second.

This patch renames rcu-fence, now called rcu-order.  It adds a new
definition of rcu-fence, something which should have been present all
along because it is used in the rb relation.  And it modifies the
fence and strong-fence relations by making them incorporate the new
rcu-fence.

As a result of this change, there is no longer any need to define
full-fence in the section for detecting data races.  It can simply be
replaced by the updated strong-fence relation.

This change should have no effect on the operation of the memory model.

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

tools/memory-model: Expand definition of barrier

2019-06-21T23:18:45+00:00

Commit 66be4e66a7f4 ("rcu: locking and unlocking need to always be at
least barriers") added compiler barriers back into rcu_read_lock() and
rcu_read_unlock().  Furthermore, srcu_read_lock() and
srcu_read_unlock() have always contained compiler barriers.

The Linux Kernel Memory Model ought to know about these barriers.
This patch adds them into the memory model.

Signed-off-by: Alan Stern 
Acked-by: Andrea Parri 
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 definitions of plain and marked accesses

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

This patch adds definitions for marked and plain accesses to the
Linux-Kernel Memory Model.  It also modifies the definitions of the
existing parts of the model (including the cumul-fence, prop, hb, pb,
and rb relations) so as to make them apply only to marked accesses.

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

tools/memory-model: Prepare for data-race detection

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

This patch makes some slight alterations to linux-kernel.cat in
preparation for adding support for data-race detection to the
Linux-Kernel Memory Model.

	The definitions of relations involved in Acquire, Release, and
	unlock-lock ordering are moved up earlier in the source file.

	The rmb relation is factored through the new R4rmb class: the
	class of reads to which rmb will apply.

	The definition of the fence relation is moved earlier, and it
	is split up into read- and write-fences (rmb and wmb) and all
	the others.

This should not make any functional changes.

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

tools/memory-model: Avoid duplicating herdtools versions

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

Currently, herdtools version information appears no fewer than three
times in the LKMM source, which is difficult to maintain.  This commit
therefore places the required version in one place, namely the
tools/memory-model/README file.

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

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