lkml.org 
[lkml]   [2020]   [Aug]   [31]   [last100]   RSS Feed
Views: [wrap][no wrap]   [headers]  [forward] 
 
Messages in this thread
    /
    Date
    From
    SubjectRe: [PATCH kcsan 9/9] tools/memory-model: Document locking corner cases
    On Mon, Aug 31, 2020 at 11:20:37AM -0700, paulmck@kernel.org 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

    \
     
     \ /
      Last update: 2020-08-31 22:17    [W:3.768 / U:0.076 seconds]
    ©2003-2020 Jasper Spaans|hosted at Digital Ocean and TransIP|Read the blog|Advertise on this site