linux-yocto/Documentation/litmus-tests
Paul E. McKenney 2ba5b4130e Documentation/litmus-tests: Make cmpxchg() tests safe for klitmus
The four litmus tests in Documentation/litmus-tests/atomic do not
declare all of their local variables.  Although this is just fine for LKMM
analysis by herd7, it causes build failures when run in-kernel by klitmus.
This commit therefore adjusts these tests to declare all local variables.

Reported-by: Andrea Parri <parri.andrea@gmail.com>
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
Acked-by: Andrea Parri <parri.andrea@gmail.com>
2024-05-06 14:29:21 -07:00
..
atomic Documentation/litmus-tests: Make cmpxchg() tests safe for klitmus 2024-05-06 14:29:21 -07:00
locking tools/memory-model: Document locking corner cases 2023-03-24 10:22:25 -07:00
rcu
README Documentation/litmus-tests: Demonstrate unordered failing cmpxchg 2024-05-06 14:28:54 -07:00

============ LITMUS TESTS

Each subdirectory contains litmus tests that are typical to describe the semantics of respective kernel APIs. For more information about how to "run" a litmus test or how to generate a kernel test module based on a litmus test, please see tools/memory-model/README.

atomic (/atomic directory)

Atomic-RMW+mb__after_atomic-is-stronger-than-acquire.litmus Test that an atomic RMW followed by a smp_mb__after_atomic() is stronger than a normal acquire: both the read and write parts of the RMW are ordered before the subsequential memory accesses.

Atomic-RMW-ops-are-atomic-WRT-atomic_set.litmus Test that atomic_set() cannot break the atomicity of atomic RMWs. NOTE: Require herd7 7.56 or later which supports "(void)expr".

cmpxchg-fail-ordered-1.litmus Demonstrate that a failing cmpxchg() operation acts as a full barrier when followed by smp_mb__after_atomic().

cmpxchg-fail-ordered-2.litmus Demonstrate that a failing cmpxchg() operation acts as an acquire operation when followed by smp_mb__after_atomic().

cmpxchg-fail-unordered-1.litmus Demonstrate that a failing cmpxchg() operation does not act as a full barrier.

cmpxchg-fail-unordered-2.litmus Demonstrate that a failing cmpxchg() operation does not act as an acquire operation.

locking (/locking directory)

DCL-broken.litmus Demonstrates that double-checked locking needs more than just the obvious lock acquisitions and releases.

DCL-fixed.litmus Demonstrates corrected double-checked locking that uses smp_store_release() and smp_load_acquire() in addition to the obvious lock acquisitions and releases.

RM-broken.litmus Demonstrates problems with "roach motel" locking, where code is freely moved into lock-based critical sections. This example also shows how to use the "filter" clause to discard executions that would be excluded by other code not modeled in the litmus test. Note also that this "roach motel" optimization is emulated by physically moving P1()'s two reads from x under the lock.

What is a roach motel?  This is from an old advertisement for
a cockroach trap, much later featured in one of the "Men in
Black" movies.  "The roaches check in.  They don't check out."

RM-fixed.litmus The counterpart to RM-broken.litmus, showing P0()'s two loads from x safely outside of the critical section.

RCU (/rcu directory)

MP+onceassign+derefonce.litmus (under tools/memory-model/litmus-tests/) Demonstrates the use of rcu_assign_pointer() and rcu_dereference() to ensure that an RCU reader will not see pre-initialization garbage.

RCU+sync+read.litmus RCU+sync+free.litmus Both the above litmus tests demonstrate the RCU grace period guarantee that an RCU read-side critical section can never span a grace period.