b9a6e87a | 25-Jun-2024 |
Akira Yokosawa <akiyks@gmail.com> |
tools/memory-model: simple.txt: Fix stale reference to recipes-pairs.txt
There has never been recipes-paris.txt at least since v5.11. Fix the typo.
Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
tools/memory-model: simple.txt: Fix stale reference to recipes-pairs.txt
There has never been recipes-paris.txt at least since v5.11. Fix the typo.
Signed-off-by: Akira Yokosawa <akiyks@gmail.com> Acked-by: Andrea Parri <parri.andrea@gmail.com> Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
show more ...
|
9bc931e9 | 25-Jun-2024 |
Akira Yokosawa <akiyks@gmail.com> |
tools/memory-model: Add locking.txt and glossary.txt to README
locking.txt and glossary.txt have been in LKMM's documentation for quite a while.
Add them in README's introduction of docs and the li
tools/memory-model: Add locking.txt and glossary.txt to README
locking.txt and glossary.txt have been in LKMM's documentation for quite a while.
Add them in README's introduction of docs and the list of docs at the bottom. Add access-marking.txt in the former as well.
Signed-off-by: Akira Yokosawa <akiyks@gmail.com> Acked-by: Andrea Parri <parri.andrea@gmail.com> Cc: Marco Elver <elver@google.com> Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
show more ...
|
ea6ee1ba | 06-Jun-2024 |
Alan Stern <stern@rowland.harvard.edu> |
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 <stern@rowland.harvard.edu> Tested-by: Andrea Parri <parri.andrea@gmail.com> Acked-by: Andrea Parri <parri.andrea@gmail.com> Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
show more ...
|
4c830eef | 06-Jun-2024 |
Alan Stern <stern@rowland.harvard.edu> |
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 <stern@rowland.harvard.edu> Reported-by: Andrea Parri <parri.andrea@gmail.com> Closes: https://lore.kernel.org/linux-arch/ZlC0IkzpQdeGj+a3@andrea/ Tested-by: Andrea Parri <parri.andrea@gmail.com> Acked-by: Andrea Parri <parri.andrea@gmail.com> Fixes: 15553dcbca06 ("tools/memory-model: Add model support for spin_is_locked()") CC: <stable@vger.kernel.org> Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
show more ...
|
520c637b | 05-Jun-2024 |
Paul E. McKenney <paulmck@kernel.org> |
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 <akiyks@gmail.com> 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 <akiyks@gmail.com> Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
show more ...
|
cc4a2981 | 23-Mar-2023 |
Andrea Parri <parri.andrea@gmail.com> |
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 <parri.andrea@gmail.com> Reviewed-by: Joel Fernandes (Google) <joel@joelfernandes.org> Acked-by: Alan Stern <stern@rowland.harvard.edu> Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
show more ...
|
05dc8470 | 27-Jan-2023 |
Paul E. McKenney <paulmck@kernel.org> |
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 <paulmck@kernel.org>
show more ...
|
2a8ec611 | 21-Nov-2022 |
Tiezhu Yang <yangtiezhu@loongson.cn> |
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 <yangtiezhu@loongson.cn> Reviewed-by: Akira Yokosawa <akiyks@gmail.com> Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
show more ...
|
719bef0c | 25-Jun-2019 |
Paul E. McKenney <paulmck@kernel.org> |
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 <luc.maranget@inria.fr> Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
show more ...
|
72b5f102 | 06-Jun-2019 |
Paul E. McKenney <paulmck@kernel.org> |
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 <paulmck@kernel.org>
show more ...
|
68f7bcab | 03-May-2019 |
Paul E. McKenney <paulmck@kernel.org> |
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 <paulmck@kernel.org>
show more ...
|
df0f6750 | 02-May-2019 |
Paul E. McKenney <paulmck@kernel.org> |
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 <paulmck@kernel.org>
show more ...
|
8b99521f | 02-May-2019 |
Paul E. McKenney <paulmck@kernel.org> |
tools/memory-model: Add "--" to parseargs.sh for additional arguments
Currently, parseargs.sh expects to consume all the command-line arguments, which prevents the calling script from having any of
tools/memory-model: Add "--" to parseargs.sh for additional arguments
Currently, parseargs.sh expects to consume all the command-line arguments, which prevents the calling script from having any of its own arguments. This commit therefore causes parseargs.sh to stop consuming arguments when it encounters a "--" argument, leaving any remaining arguments for the calling script.
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
show more ...
|
75eee921 | 08-Apr-2019 |
Paul E. McKenney <paulmck@kernel.org> |
tools/memory-model: Make history-check scripts use mselect7
The history-check scripts currently use grep to ignore non-C-language litmus tests, which is a bit fragile. This commit therefore enlists
tools/memory-model: Make history-check scripts use mselect7
The history-check scripts currently use grep to ignore non-C-language litmus tests, which is a bit fragile. This commit therefore enlists the aid of "mselect7 -arch C", given Luc Maraget's recent modifications that allow mselect7 to operate in filter mode.
This change requires herdtools 7.52-32-g1da3e0e50977 or later.
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
show more ...
|
2ac8cbee | 08-Apr-2019 |
Paul E. McKenney <paulmck@kernel.org> |
tools/memory-model: Make checkghlitmus.sh use mselect7
The checkghlitmus.sh script currently uses grep to ignore non-C-language litmus tests, which is a bit fragile. This commit therefore enlists t
tools/memory-model: Make checkghlitmus.sh use mselect7
The checkghlitmus.sh script currently uses grep to ignore non-C-language litmus tests, which is a bit fragile. This commit therefore enlists the aid of "mselect7 -arch C", given Luc Maraget's recent modifications that allow mselect7 to operate in filter mode.
This change requires herdtools 7.52-32-g1da3e0e50977 or later.
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
show more ...
|
6e6586b0 | 27-Mar-2019 |
Paul E. McKenney <paulmck@kernel.org> |
tools/memory-model: Fix scripting --jobs argument
The parseargs.sh regular expression for the --jobs argument incorrectly requires that the number of jobs be at least 10, that is, have at least two
tools/memory-model: Fix scripting --jobs argument
The parseargs.sh regular expression for the --jobs argument incorrectly requires that the number of jobs be at least 10, that is, have at least two digits. This commit therefore adjusts this regular expression to allow single-digit numbers of jobs to be specified.
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
show more ...
|
69d476c5 | 23-Mar-2019 |
Paul E. McKenney <paulmck@kernel.org> |
tools/memory-model: Implement --hw support for checkghlitmus.sh
This commits enables the "--hw" argument for the checkghlitmus.sh script, causing it to convert any applicable C-language litmus tests
tools/memory-model: Implement --hw support for checkghlitmus.sh
This commits enables the "--hw" argument for the checkghlitmus.sh script, causing it to convert any applicable C-language litmus tests to the specified flavor of assembly language, to verify these assembly-language litmus tests, and checking compatibility of the outcomes.
Note that the conversion does not yet handle locking, RCU, SRCU, plain C-language memory accesses, or casts.
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
show more ...
|
d9313e05 | 05-Apr-2019 |
Paul E. McKenney <paulmck@kernel.org> |
tools/memory-model: Add -v flag to jingle7 runs
Adding the -v flag to jingle7 invocations gives much useful information on why jingle7 didn't like a given litmus test. This commit therefore adds th
tools/memory-model: Add -v flag to jingle7 runs
Adding the -v flag to jingle7 invocations gives much useful information on why jingle7 didn't like a given litmus test. This commit therefore adds this flag and saves off any such information into a .err file.
Suggested-by: Luc Maranget <luc.maranget@inria.fr> Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
show more ...
|
a9504aaa | 26-Mar-2019 |
Paul E. McKenney <paulmck@kernel.org> |
tools/memory-model: Make runlitmus.sh check for jingle errors
It turns out that the jingle7 tool is currently a bit picky about the litmus tests it is willing to process. This commit therefore ensu
tools/memory-model: Make runlitmus.sh check for jingle errors
It turns out that the jingle7 tool is currently a bit picky about the litmus tests it is willing to process. This commit therefore ensures that jingle7 failures are reported.
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
show more ...
|