> DCL-broken.litmus
> - Demonstrates that double-checked locking needs more than just
> - the obvious lock acquisitions and releases.
> + 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.
> + 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.
> + 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."
> + 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.
> + The counterpart to RM-broken.litmus, showing P0()'s two loads from
> + x safely outside of the critical section.
AFAIU, the changes above belong to patch #1. Looks like you realigned
the text, but forgot to integrate the changes in #1?
> +C cmpxchg-fail-ordered-1
> +
> +(*
> + * Result: Never
> + *
> + * Demonstrate that a failing cmpxchg() operation will act as a full
> + * barrier when followed by smp_mb__after_atomic().
> + *)
> +
> +{}
> +
> +P0(int *x, int *y, int *z)
> +{
> + int r0;
> + int r1;
> +
> + WRITE_ONCE(*x, 1);
> + r1 = cmpxchg(z, 1, 0);
> + smp_mb__after_atomic();
> + r0 = READ_ONCE(*y);
> +}
> +
> +P1(int *x, int *y, int *z)
> +{
> + int r0;
> +
> + WRITE_ONCE(*y, 1);
> + r1 = cmpxchg(z, 1, 0);
P1's r1 is undeclared (so klitmus7 will complain).
The same observation holds for cmpxchg-fail-unordered-1.litmus.
> + smp_mb__after_atomic();
> + r0 = READ_ONCE(*x);
> +}
> +
> +locations[0:r1;1:r1]
> +exists (0:r0=0 /\ 1:r0=0)
> +C cmpxchg-fail-ordered-2
> +
> +(*
> + * Result: Never
> + *
> + * Demonstrate use of smp_mb__after_atomic() to make a failing cmpxchg
> + * operation have acquire ordering.
> + *)
> +
> +{}
> +
> +P0(int *x, int *y)
> +{
> + int r0;
> + int r1;
> +
> + WRITE_ONCE(*x, 1);
> + r1 = cmpxchg(y, 0, 1);
> +}
> +
> +P1(int *x, int *y)
> +{
> + int r0;
> +
> + r1 = cmpxchg(y, 0, 1);
> + smp_mb__after_atomic();
> + r2 = READ_ONCE(*x);
P1's r1 and r2 are undeclared. P0's r0 and P1's r0 are unused.
Same for cmpxchg-fail-unordered-2.litmus.
Andrea
