linux/Documentation/litmus-tests/locking/RM-fixed.litmus
Paul E. McKenney 7e7eb5ae4e tools/memory-model: Document locking corner cases
Most Linux-kernel uses of locking are straightforward, but there are
corner-case uses that rely on less well-known aspects of the lock and
unlock primitives.  This commit therefore adds a locking.txt and litmus
tests in Documentation/litmus-tests/locking to explain these corner-case
uses.

[ paulmck: Apply Andrea Parri feedback for klitmus7. ]
[ paulmck: Apply Akira Yokosawa example-consistency feedback. ]

Reviewed-by: Akira Yokosawa <akiyks@gmail.com>
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
2023-03-24 10:22:25 -07:00

42 lines
640 B
Plaintext

C RM-fixed
(*
* Result: Never
*
* This litmus test demonstrates that the old "roach motel" approach
* to locking, where code can be freely moved into critical sections,
* cannot be used in the Linux kernel.
*)
{
int x;
atomic_t y;
}
P0(int *x, atomic_t *y, spinlock_t *lck)
{
int r2;
spin_lock(lck);
r2 = atomic_inc_return(y);
WRITE_ONCE(*x, 1);
spin_unlock(lck);
}
P1(int *x, atomic_t *y, spinlock_t *lck)
{
int r0;
int r1;
int r2;
r0 = READ_ONCE(*x);
r1 = READ_ONCE(*x);
spin_lock(lck);
r2 = atomic_inc_return(y);
spin_unlock(lck);
}
locations [x;0:r2;1:r0;1:r1;1:r2]
filter (1:r0=0 /\ 1:r1=1)
exists (1:r2=1)