linux-toradex.git/tools/memory-model, branch v6.15-rc7

tools/memory-model: glossary.txt: Fix indents

2025-02-25T18:22:34+00:00

There are a couple of inconsistent indents around code/literal blocks.
Adjust them to make this file easier to parse.

Signed-off-by: Akira Yokosawa 
Signed-off-by: Paul E. McKenney

tools/memory-model/README: Fix typo

2025-02-25T18:22:34+00:00

Fix a trivial typo.

Signed-off-by: Akira Yokosawa 
Signed-off-by: Paul E. McKenney

tools/memory-model: Distinguish between syntactic and semantic tags

2025-02-25T18:17:39+00:00

Not all annotated accesses provide the semantics their syntactic tags
would imply. For example, an 'acquire tag on a write does not imply that
the write is finally in the Acquire set and provides acquire ordering.

To distinguish in those cases between the syntactic tags and actual
sets, we capitalize the former, so 'ACQUIRE tags may be present on both
reads and writes, but only reads will appear in the Acquire set.

For tags where the two concepts are the same we do not use specific
capitalization to make this distinction.

Reported-by: Boqun Feng 
Signed-off-by: Jonas Oberhauser 
Reviewed-by: Boqun Feng 
Tested-by: Boqun Feng 
Signed-off-by: Paul E. McKenney 
Tested-by: Akira Yokosawa  # herdtools7.7.58

tools/memory-model: Switch to softcoded herd7 tags

2025-02-25T18:16:57+00:00

A new version of herd7 provides a -lkmmv2 switch which overrides the old herd7
behavior of simply ignoring any softcoded tags in the .def and .bell files. We
port LKMM to this version of herd7 by providing the switch in linux-kernel.cfg
and reporting an error if the LKMM is used without this switch.

To preserve the semantics of LKMM, we also softcode the Noreturn tag on atomic
RMW which do not return a value and define atomic_add_unless with an Mb tag in
linux-kernel.def.

We update the herd-representation.txt accordingly and clarify some of the
resulting combinations.

Co-developed-by: Hernan Ponce de Leon 
Signed-off-by: Hernan Ponce de Leon 
Signed-off-by: Jonas Oberhauser 
Signed-off-by: Paul E. McKenney 
Reviewed-by: Boqun Feng 
Tested-by: Boqun Feng 
Tested-by: Akira Yokosawa  # herdtools7.7.58

tools/memory-model: Define effect of Mb tags on RMWs in tools/...

2025-02-20T15:40:23+00:00

Herd7 transforms successful RMW with Mb tags by inserting smp_mb() fences
around them. We emulate this by considering imaginary po-edges before the
RMW read and before the RMW write, and extending the smp_mb() ordering
rule, which currently only applies to real po edges that would be found
around a really inserted smp_mb(), also to cases of the only imagined po
edges.

Reported-by: Viktor Vafeiadis 
Suggested-by: Alan Stern 
Signed-off-by: Jonas Oberhauser 
Signed-off-by: Paul E. McKenney 
Reviewed-by: Boqun Feng 
Tested-by: Boqun Feng

tools/memory-model: Define applicable tags on operation in tools/...

2025-02-20T15:40:23+00:00

Herd7 transforms reads, writes, and read-modify-writes by eliminating
'acquire tags from writes, 'release tags from reads, and 'acquire,
'release, and 'mb tags from failed read-modify-writes. We emulate this
behavior by redefining Acquire, Release, and Mb sets in linux-kernel.bell
to explicitly exclude those combinations.

Herd7 furthermore adds 'noreturn tag to certain reads. Currently herd7
does not allow specifying the 'noreturn tag manually, but such manual
declaration (e.g., through a syntax __atomic_op{noreturn}) would add
invalid 'noreturn tags to writes; in preparation, we already also exclude
this combination.

Signed-off-by: Jonas Oberhauser 
Signed-off-by: Paul E. McKenney 
Reviewed-by: Boqun Feng 
Tested-by: Boqun Feng

tools/memory-model: Legitimize current use of tags in LKMM macros

2025-02-20T15:40:23+00:00

The current macros in linux-kernel.def reference instructions such as
__xchg{mb} or __cmpxchg{acquire}, which are invalid combinations of tags
and instructions according to the declarations in linux-kernel.bell.
This works with current herd7 because herd7 removes these tags anyways
and does not actually enforce validity of combinations at all.

If a future herd7 version no longer applies these hardcoded
transformations, then all currently invalid combinations will actually
appear on some instruction.

We therefore adjust the declarations to make the resulting combinations
valid, by adding the 'mb tag to the set of Accesses and allowing all
Accesses to appear on all read, write, and RMW instructions.

Signed-off-by: Jonas Oberhauser 
Signed-off-by: Paul E. McKenney 
Reviewed-by: Boqun Feng 
Tested-by: Boqun Feng

tools/memory-model: Add atomic_andnot() with its variants

2025-02-20T15:40:23+00:00

Pull-855[1] added the support of atomic_andnot() to the herd tool. Use
this to add the implementation in the LKMM. All of the ordering variants
are also added.

Here is a small litmus-test that uses this operation:

C andnot

{
atomic_t u = ATOMIC_INIT(7);
}

P0(atomic_t *u)
{

        r0 = atomic_fetch_andnot(3, u);
        r1 = READ_ONCE(*u);
}

exists (0:r0=7 /\ 0:r1=4)

Test andnot Allowed
States 1
0:r0=7; 0:r1=4;
Ok
Witnesses
Positive: 1 Negative: 0
Condition exists (0:r0=7 /\ 0:r1=4)
Observation andnot Always 1 0
Time andnot 0.00
Hash=78f011a0b5a0c65fa1cf106fcd62c845

[1] https://github.com/herd/herdtools7/pull/855

Signed-off-by: Puranjay Mohan 
Acked-by: Andrea Parri 
Signed-off-by: Paul E. McKenney 
Cc: Alan Stern 
Cc: Will Deacon 
Cc: Peter Zijlstra 
Cc: Boqun Feng 
Cc: Nicholas Piggin 
Cc: David Howells 
Cc: Jade Alglave 
Cc: Luc Maranget 
Cc: Akira Yokosawa 
Cc: Daniel Lustig 
Cc: Joel Fernandes 
Cc:

tools/memory-model: Add atomic_and()/or()/xor() and add_negative

2025-02-20T15:40:23+00:00

Pull-849[1] added the support of '&', '|', and '^' to the herd7 tool's
atomics operations.

Use these in linux-kernel.def to implement atomic_and()/or()/xor() with
all their ordering variants.

atomic_add_negative() is already available so add its acquire, release,
and relaxed ordering variants.

[1] https://github.com/herd/herdtools7/pull/849

Signed-off-by: Puranjay Mohan 
Acked-by: Andrea Parri 
Reviewed-by: Boqun Feng 
Signed-off-by: Paul E. McKenney 
Cc: Alan Stern 
Cc: Will Deacon 
Cc: Peter Zijlstra 
Cc: Nicholas Piggin 
Cc: David Howells 
Cc: Jade Alglave 
Cc: Luc Maranget 
Cc: Akira Yokosawa 
Cc: Daniel Lustig 
Cc: Joel Fernandes 
Cc:

tools/memory-model: simple.txt: Fix stale reference to recipes-pairs.txt

2024-09-14T06:56:44+00:00

There has never been recipes-paris.txt at least since v5.11.
Fix the typo.

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