Re: [PATCH kcsan 9/9] tools/memory-model: Document locking corner cases

[Alan Stern]

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