On Mon, Aug 31, 2020 at 11:20:37AM -0700, paulmck@xxxxxxxxxx wrote:
> +No Roach-Motel Locking!
> +-----------------------
> +
> +This example requires familiarity with the herd7 "filter" clause, so
> +please read up on that topic in litmus-tests.txt.
> +
> +It is tempting to allow memory-reference instructions to be pulled
> +into a critical section, but this cannot be allowed in the general case.
> +For example, consider a spin loop preceding a lock-based critical section.
> +Now, herd7 does not model spin loops, but we can emulate one with two
> +loads, with a "filter" clause to constrain the first to return the
> +initial value and the second to return the updated value, as shown below:
> +
> + /* See Documentation/litmus-tests/locking/RM-fixed.litmus. */
> + P0(int *x, int *y, int *lck)
> + {
> + int r2;
> +
> + spin_lock(lck);
> + r2 = atomic_inc_return(y);
> + WRITE_ONCE(*x, 1);
> + spin_unlock(lck);
> + }
> +
> + P1(int *x, int *y, int *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);
> + }
> +
> + filter (y=2 /\ 1:r0=0 /\ 1:r1=1)
> + exists (1:r2=1)
> +
> +The variable "x" is the control variable for the emulated spin loop.
> +P0() sets it to "1" while holding the lock, and P1() emulates the
> +spin loop by reading it twice, first into "1:r0" (which should get the
> +initial value "0") and then into "1:r1" (which should get the updated
> +value "1").
> +
> +The purpose of the variable "y" is to reject deadlocked executions.
> +Only those executions where the final value of "y" have avoided deadlock.
> +
> +The "filter" clause takes all this into account, constraining "y" to
> +equal "2", "1:r0" to equal "0", and "1:r1" to equal 1.
> +
> +Then the "exists" clause checks to see if P1() acquired its lock first,
> +which should not happen given the filter clause because P0() updates
> +"x" while holding the lock. And herd7 confirms this.
> +
> +But suppose that the compiler was permitted to reorder the spin loop
> +into P1()'s critical section, like this:
> +
> + /* See Documentation/litmus-tests/locking/RM-broken.litmus. */
> + P0(int *x, int *y, int *lck)
> + {
> + int r2;
> +
> + spin_lock(lck);
> + r2 = atomic_inc_return(y);
> + WRITE_ONCE(*x, 1);
> + spin_unlock(lck);
> + }
> +
> + P1(int *x, int *y, int *lck)
> + {
> + int r0;
> + int r1;
> + int r2;
> +
> + spin_lock(lck);
> + r0 = READ_ONCE(*x);
> + r1 = READ_ONCE(*x);
> + r2 = atomic_inc_return(y);
> + spin_unlock(lck);
> + }
> +
> + locations [x;lck;0:r2;1:r0;1:r1;1:r2]
> + filter (y=2 /\ 1:r0=0 /\ 1:r1=1)
> + exists (1:r2=1)
> +
> +If "1:r0" is equal to "0", "1:r1" can never equal "1" because P0()
> +cannot update "x" while P1() holds the lock. And herd7 confirms this,
> +showing zero executions matching the "filter" criteria.
> +
> +And this is why Linux-kernel lock and unlock primitives must prevent
> +code from entering critical sections. It is not sufficient to only
> +prevnt code from leaving them.
Is this discussion perhaps overkill?
Let's put it this way: Suppose we have the following code:
P0(int *x, int *lck)
{
spin_lock(lck);
WRITE_ONCE(*x, 1);
do_something();
spin_unlock(lck);
}
P1(int *x, int *lck)
{
while (READ_ONCE(*x) == 0)
;
spin_lock(lck);
do_something_else();
spin_unlock(lck);
}
It's obvious that this test won't deadlock. But if P1 is changed to:
P1(int *x, int *lck)
{
spin_lock(lck);
while (READ_ONCE(*x) == 0)
;
do_something_else();
spin_unlock(lck);
}
then it's equally obvious that the test can deadlock. No need for
fancy memory models or litmus tests or anything else.
Alan
