| 5c9e0062 | 22-Apr-2025 |
Uladzislau Rezki (Sony) <urezki@gmail.com> |
tools/memory-model/Documentation: Fix SRCU section in explanation.txt
The SRCU read-side critical sections describes the difference between
srcu_down_read()/srcu_up_read() and srcu_read_lock()/srcu_
tools/memory-model/Documentation: Fix SRCU section in explanation.txt
The SRCU read-side critical sections describes the difference between
srcu_down_read()/srcu_up_read() and srcu_read_lock()/srcu_read_unlock()
in a way that a last pair must occur on the same CPU.
This is not true, the srcu_read_unlock() can happen on any CPU, but it
must be performed by the same task that invoked srcu_read_lock().
Signed-off-by: Uladzislau Rezki (Sony) <urezki@gmail.com>
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
show more ...
|
| 730c0a8e | 14-Mar-2025 |
Akira Yokosawa <akiyks@gmail.com> |
tools/memory-model: docs/references: Remove broken link to imgtec.com
MIPS documents are not provided at imgtec.com any more.
Get rid of useless link.
Signed-off-by: Akira Yokosawa <akiyks@gmail.co
tools/memory-model: docs/references: Remove broken link to imgtec.com
MIPS documents are not provided at imgtec.com any more.
Get rid of useless link.
Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
Acked-by: Andrea Parri <parri.andrea@gmail.com>
show more ...
|
| f0a83980 | 14-Mar-2025 |
Akira Yokosawa <akiyks@gmail.com> |
tools/memory-model: docs/ordering: Fix trivial typos
Fix trivial typos including:
- Repeated "a call to"
- Inconsistent forms of referencing functions of rcu_dereference()
and rcu_assign_po
tools/memory-model: docs/ordering: Fix trivial typos
Fix trivial typos including:
- Repeated "a call to"
- Inconsistent forms of referencing functions of rcu_dereference()
and rcu_assign_pointer()
- Past tense used in describing normal behavior
and other minor ones.
[ paulmck: Wordsmith plus recent LWN RCU API URL. ]
Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
Acked-by: Andrea Parri <parri.andrea@gmail.com>
show more ...
|
| 366b88f6 | 14-Mar-2025 |
Akira Yokosawa <akiyks@gmail.com> |
tools/memory-model: docs/simple.txt: Fix trivial typos
Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
Acked-by: Andrea Parri <parri.andrea@gmai
tools/memory-model: docs/simple.txt: Fix trivial typos
Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
Acked-by: Andrea Parri <parri.andrea@gmail.com>
show more ...
|
| a2bfbf84 | 25-Feb-2025 |
Akira Yokosawa <akiyks@gmail.com> |
tools/memory-model: glossary.txt: Fix indents
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 <ak
tools/memory-model: glossary.txt: Fix indents
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 <akiyks@gmail.com>
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
show more ...
|
| dcc51978 | 05-Nov-2024 |
Jonas Oberhauser <jonas.oberhauser@huaweicloud.com> |
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 <boqun.feng@gmail.com>
Signed-off-by: Jonas Oberhauser <jonas.oberhauser@huaweicloud.com>
Reviewed-by: Boqun Feng <boqun.feng@gmail.com>
Tested-by: Boqun Feng <boqun.feng@gmail.com>
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
Tested-by: Akira Yokosawa <akiyks@gmail.com> # herdtools7.7.58
show more ...
|
| fafa1806 | 30-Sep-2024 |
Jonas Oberhauser <jonas.oberhauser@huaweicloud.com> |
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 <hernan.poncedeleon@huaweicloud.com>
Signed-off-by: Hernan Ponce de Leon <hernan.poncedeleon@huaweicloud.com>
Signed-off-by: Jonas Oberhauser <jonas.oberhauser@huaweicloud.com>
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
Reviewed-by: Boqun Feng <boqun.feng@gmail.com>
Tested-by: Boqun Feng <boqun.feng@gmail.com>
Tested-by: Akira Yokosawa <akiyks@gmail.com> # herdtools7.7.58
show more ...
|
| 29279349 | 30-Sep-2024 |
Jonas Oberhauser <jonas.oberhauser@huaweicloud.com> |
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 <viktor@mpi-sws.org>
Suggested-by: Alan Stern <stern@rowland.harvard.edu>
Signed-off-by: Jonas Oberhauser <jonas.oberhauser@huaweicloud.com>
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
Reviewed-by: Boqun Feng <boqun.feng@gmail.com>
Tested-by: Boqun Feng <boqun.feng@gmail.com>
show more ...
|
| 723177d7 | 30-Sep-2024 |
Jonas Oberhauser <jonas.oberhauser@huaweicloud.com> |
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 <jonas.oberhauser@huaweicloud.com>
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
Reviewed-by: Boqun Feng <boqun.feng@gmail.com>
Tested-by: Boqun Feng <boqun.feng@gmail.com>
show more ...
|
| de6f9972 | 30-Sep-2024 |
Jonas Oberhauser <jonas.oberhauser@huaweicloud.com> |
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 <jonas.oberhauser@huaweicloud.com>
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
Reviewed-by: Boqun Feng <boqun.feng@gmail.com>
Tested-by: Boqun Feng <boqun.feng@gmail.com>
show more ...
|
| e176ebff | 14-May-2024 |
Puranjay Mohan <puranjay@kernel.org> |
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 <puranjay@kernel.org>
Acked-by: Andrea Parri <parri.andrea@gmail.com>
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
Cc: Alan Stern <stern@rowland.harvard.edu>
Cc: Will Deacon <will@kernel.org>
Cc: Peter Zijlstra <peterz@infradead.org>
Cc: Boqun Feng <boqun.feng@gmail.com>
Cc: Nicholas Piggin <npiggin@gmail.com>
Cc: David Howells <dhowells@redhat.com>
Cc: Jade Alglave <j.alglave@ucl.ac.uk>
Cc: Luc Maranget <luc.maranget@inria.fr>
Cc: Akira Yokosawa <akiyks@gmail.com>
Cc: Daniel Lustig <dlustig@nvidia.com>
Cc: Joel Fernandes <joel@joelfernandes.org>
Cc: <linux-arch@vger.kernel.org>
show more ...
|
| 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 ...
|