| 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 ...
|