| dcc51978 | 05-Nov-2024 |
Jonas Oberhauser <[email protected]> |
tools/memory-model: Distinguish between syntactic and semantic tags
Not all annotated accesses provide the semantics their syntactic tags
would imply. For example, an 'acquire tag on a write does no
tools/memory-model: Distinguish between syntactic and semantic tags
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 <[email protected]>
Signed-off-by: Jonas Oberhauser <[email protected]>
Reviewed-by: Boqun Feng <[email protected]>
Tested-by: Boqun Feng <[email protected]>
Signed-off-by: Paul E. McKenney <[email protected]>
Tested-by: Akira Yokosawa <[email protected]> # herdtools7.7.58
show more ...
|
| fafa1806 | 30-Sep-2024 |
Jonas Oberhauser <[email protected]> |
tools/memory-model: Switch to softcoded herd7 tags
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
tools/memory-model: Switch to softcoded herd7 tags
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 <[email protected]>
Signed-off-by: Hernan Ponce de Leon <[email protected]>
Signed-off-by: Jonas Oberhauser <[email protected]>
Signed-off-by: Paul E. McKenney <[email protected]>
Reviewed-by: Boqun Feng <[email protected]>
Tested-by: Boqun Feng <[email protected]>
Tested-by: Akira Yokosawa <[email protected]> # herdtools7.7.58
show more ...
|
| 29279349 | 30-Sep-2024 |
Jonas Oberhauser <[email protected]> |
tools/memory-model: Define effect of Mb tags on RMWs in tools/...
Herd7 transforms successful RMW with Mb tags by inserting smp_mb() fences
around them. We emulate this by considering imaginary po-e
tools/memory-model: Define effect of Mb tags on RMWs in tools/...
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 <[email protected]>
Suggested-by: Alan Stern <[email protected]>
Signed-off-by: Jonas Oberhauser <[email protected]>
Signed-off-by: Paul E. McKenney <[email protected]>
Reviewed-by: Boqun Feng <[email protected]>
Tested-by: Boqun Feng <[email protected]>
show more ...
|
| 723177d7 | 30-Sep-2024 |
Jonas Oberhauser <[email protected]> |
tools/memory-model: Define applicable tags on operation in tools/...
Herd7 transforms reads, writes, and read-modify-writes by eliminating
'acquire tags from writes, 'release tags from reads, and 'a
tools/memory-model: Define applicable tags on operation in tools/...
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 <[email protected]>
Signed-off-by: Paul E. McKenney <[email protected]>
Reviewed-by: Boqun Feng <[email protected]>
Tested-by: Boqun Feng <[email protected]>
show more ...
|
| de6f9972 | 30-Sep-2024 |
Jonas Oberhauser <[email protected]> |
tools/memory-model: Legitimize current use of tags in LKMM macros
The current macros in linux-kernel.def reference instructions such as
__xchg{mb} or __cmpxchg{acquire}, which are invalid combinatio
tools/memory-model: Legitimize current use of tags in LKMM macros
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 <[email protected]>
Signed-off-by: Paul E. McKenney <[email protected]>
Reviewed-by: Boqun Feng <[email protected]>
Tested-by: Boqun Feng <[email protected]>
show more ...
|
| e176ebff | 14-May-2024 |
Puranjay Mohan <[email protected]> |
tools/memory-model: Add atomic_andnot() with its variants
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 varia
tools/memory-model: Add atomic_andnot() with its variants
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 <[email protected]>
Acked-by: Andrea Parri <[email protected]>
Signed-off-by: Paul E. McKenney <[email protected]>
Cc: Alan Stern <[email protected]>
Cc: Will Deacon <[email protected]>
Cc: Peter Zijlstra <[email protected]>
Cc: Boqun Feng <[email protected]>
Cc: Nicholas Piggin <[email protected]>
Cc: David Howells <[email protected]>
Cc: Jade Alglave <[email protected]>
Cc: Luc Maranget <[email protected]>
Cc: Akira Yokosawa <[email protected]>
Cc: Daniel Lustig <[email protected]>
Cc: Joel Fernandes <[email protected]>
Cc: <[email protected]>
show more ...
|
| ea6ee1ba | 06-Jun-2024 |
Alan Stern <[email protected]> |
tools/memory-model: Code reorganization in lock.cat
Code reorganization for the lock.cat file in tools/memory-model:
Improve the efficiency by ruling out right at the start RU events
(spin_is_locke
tools/memory-model: Code reorganization in lock.cat
Code reorganization for the lock.cat file in tools/memory-model:
Improve the efficiency by ruling out right at the start RU events
(spin_is_locked() calls that return False) inside a critical section
for the same lock.
Improve the organization of the code for handling LF and RU events by
pulling the definitions of the pair-to-relation macro out from two
different complicated compound expressions, using a single standalone
definition instead.
Rewrite the calculations of the rf relation for LF and RU events, for
greater clarity.
Signed-off-by: Alan Stern <[email protected]>
Tested-by: Andrea Parri <[email protected]>
Acked-by: Andrea Parri <[email protected]>
Signed-off-by: Paul E. McKenney <[email protected]>
show more ...
|
| 4c830eef | 06-Jun-2024 |
Alan Stern <[email protected]> |
tools/memory-model: Fix bug in lock.cat
Andrea reported that the following innocuous litmus test:
C T
{}
P0(spinlock_t *x)
{
int r0;
spin_lock(x);
spin_unlock(x);
r0 = spin_is_locked(x);
}
tools/memory-model: Fix bug in lock.cat
Andrea reported that the following innocuous litmus test:
C T
{}
P0(spinlock_t *x)
{
int r0;
spin_lock(x);
spin_unlock(x);
r0 = spin_is_locked(x);
}
gives rise to a nonsensical empty result with no executions:
$ herd7 -conf linux-kernel.cfg T.litmus
Test T Required
States 0
Ok
Witnesses
Positive: 0 Negative: 0
Condition forall (true)
Observation T Never 0 0
Time T 0.00
Hash=6fa204e139ddddf2cb6fa963bad117c0
The problem is caused by a bug in the lock.cat part of the LKMM. Its
computation of the rf relation for RU (read-unlocked) events is
faulty; it implicitly assumes that every RU event must read from
either a UL (unlock) event in another thread or from the lock's
initial state. Neither is true in the litmus test above, so the
computation yields no possible executions.
The lock.cat code tries to make up for this deficiency by allowing RU
events outside of critical sections to read from the last po-previous
UL event. But it does this incorrectly, trying to keep these rfi links
separate from the rfe links that might also be needed, and passing only
the latter to herd7's cross() macro.
The problem is fixed by merging the two sets of possible rf links for
RU events and using them all in the call to cross().
Signed-off-by: Alan Stern <[email protected]>
Reported-by: Andrea Parri <[email protected]>
Closes: https://lore.kernel.org/linux-arch/ZlC0IkzpQdeGj+a3@andrea/
Tested-by: Andrea Parri <[email protected]>
Acked-by: Andrea Parri <[email protected]>
Fixes: 15553dcbca06 ("tools/memory-model: Add model support for spin_is_locked()")
CC: <[email protected]>
Signed-off-by: Paul E. McKenney <[email protected]>
show more ...
|
| 520c637b | 05-Jun-2024 |
Paul E. McKenney <[email protected]> |
tools/memory-model: Add access-marking.txt to README
Given that access-marking.txt exists, this commit makes it easier to find.
Reported-by: Akira Yokosawa <[email protected]>
Signed-off-by: Paul E.
tools/memory-model: Add access-marking.txt to README
Given that access-marking.txt exists, this commit makes it easier to find.
Reported-by: Akira Yokosawa <[email protected]>
Signed-off-by: Paul E. McKenney <[email protected]>
show more ...
|
| cc4a2981 | 23-Mar-2023 |
Andrea Parri <[email protected]> |
tools/memory-model: Remove out-of-date SRCU documentation
Commit 6cd244c87428 ("tools/memory-model: Provide exact SRCU semantics")
changed the semantics of partially overlapping SRCU read-side criti
tools/memory-model: Remove out-of-date SRCU documentation
Commit 6cd244c87428 ("tools/memory-model: Provide exact SRCU semantics")
changed the semantics of partially overlapping SRCU read-side critical
sections (among other things), making such documentation out-of-date.
The new, semantic changes are discussed in explanation.txt. Remove the
out-of-date documentation.
Signed-off-by: Andrea Parri <[email protected]>
Reviewed-by: Joel Fernandes (Google) <[email protected]>
Acked-by: Alan Stern <[email protected]>
Signed-off-by: Paul E. McKenney <[email protected]>
show more ...
|
| 05dc8470 | 26-Jan-2023 |
Paul E. McKenney <[email protected]> |
tools/memory-model: Document LKMM test procedure
This commit documents how to run the various scripts in order to test
a potentially pervasive change to the memory model.
Signed-off-by: Paul E. McK
tools/memory-model: Document LKMM test procedure
This commit documents how to run the various scripts in order to test
a potentially pervasive change to the memory model.
Signed-off-by: Paul E. McKenney <[email protected]>
show more ...
|
| 2a8ec611 | 21-Nov-2022 |
Tiezhu Yang <[email protected]> |
tools/memory-model: Use "grep -E" instead of "egrep"
The latest version of grep claims the egrep is now obsolete so the build
now contains warnings that look like:
egrep: warning: egrep is obsolesc
tools/memory-model: Use "grep -E" instead of "egrep"
The latest version of grep claims the egrep is now obsolete so the build
now contains warnings that look like:
egrep: warning: egrep is obsolescent; using grep -E
fix this up by moving the related file to use "grep -E" instead.
sed -i "s/egrep/grep -E/g" `grep egrep -rwl tools/memory-model`
Here are the steps to install the latest grep:
wget http://ftp.gnu.org/gnu/grep/grep-3.8.tar.gz
tar xf grep-3.8.tar.gz
cd grep-3.8 && ./configure && make
sudo make install
export PATH=/usr/local/bin:$PATH
Signed-off-by: Tiezhu Yang <[email protected]>
Reviewed-by: Akira Yokosawa <[email protected]>
Signed-off-by: Paul E. McKenney <[email protected]>
show more ...
|
| 719bef0c | 25-Jun-2019 |
Paul E. McKenney <[email protected]> |
tools/memory-model: Use "-unroll 0" to keep --hw runs finite
Litmus tests involving atomic operations produce LL/SC loops on a number
of architectures, and unrolling these loops can result in excess
tools/memory-model: Use "-unroll 0" to keep --hw runs finite
Litmus tests involving atomic operations produce LL/SC loops on a number
of architectures, and unrolling these loops can result in excessive
verification times or even stack overflows. This commit therefore uses
the "-unroll 0" herd7 argument to avoid unrolling, on the grounds that
additional passes through an LL/SC loop should not change the verification.
Note however, that certain bugs in the mapping of the LL/SC loop to
machine instructions may go undetected. On the other hand, herd7 might
not be the best vehicle for finding such bugs in any case. (You do
stress-test your architecture-specific code, don't you?)
Suggested-by: Luc Maranget <[email protected]>
Signed-off-by: Paul E. McKenney <[email protected]>
show more ...
|
| 72b5f102 | 06-Jun-2019 |
Paul E. McKenney <[email protected]> |
tools/memory-model: Make judgelitmus.sh handle scripted Result: tag
The scripts that generate the litmus tests in the "auto" directory of
the https://github.com/paulmckrcu/litmus archive place the "
tools/memory-model: Make judgelitmus.sh handle scripted Result: tag
The scripts that generate the litmus tests in the "auto" directory of
the https://github.com/paulmckrcu/litmus archive place the "Result:"
tag into a single-line ocaml comment, which judgelitmus.sh currently
does not recognize. This commit therefore makes judgelitmus.sh
recognize both the multiline comment format that it currently does
and the automatically generated single-line format.
Signed-off-by: Paul E. McKenney <[email protected]>
show more ...
|
| 68f7bcab | 03-May-2019 |
Paul E. McKenney <[email protected]> |
tools/memory-model: Add data-race capabilities to judgelitmus.sh
This commit adds functionality to judgelitmus.sh to allow it to handle
both the "DATARACE" markers in the "Result:" comments in litmu
tools/memory-model: Add data-race capabilities to judgelitmus.sh
This commit adds functionality to judgelitmus.sh to allow it to handle
both the "DATARACE" markers in the "Result:" comments in litmus tests
and the "Flag data-race" markers in LKMM output. For C-language tests,
if either marker is present, the other must also be as well, at least for
litmus tests having a "Result:" comment. If the LKMM output indicates
a data race, then failures of the Always/Sometimes/Never portion of the
"Result:" prediction are forgiven.
The reason for forgiving "Result:" mispredictions is that data races can
result in "interesting" compiler optimizations, so that all bets are off
in the data-race case.
[ paulmck: Apply Akira Yokosawa feedback. ]
Signed-off-by: Paul E. McKenney <[email protected]>
show more ...
|
| df0f6750 | 02-May-2019 |
Paul E. McKenney <[email protected]> |
tools/memory-model: Add checktheselitmus.sh to run specified litmus tests
This commit adds a checktheselitmus.sh script that runs the litmus tests
specified on the command line. This is useful for
tools/memory-model: Add checktheselitmus.sh to run specified litmus tests
This commit adds a checktheselitmus.sh script that runs the litmus tests
specified on the command line. This is useful for verifying fixes to
specific litmus tests.
Signed-off-by: Paul E. McKenney <[email protected]>
show more ...
|