lkml.org 
[lkml]   [2017]   [Nov]   [27]   [last100]   RSS Feed
Views: [wrap][no wrap]   [headers]  [forward] 
 
Messages in this thread
/
Date
From
SubjectUnlock-lock questions and the Linux Kernel Memory Model
This is essentially a repeat of an email I sent out before the
Thanksgiving holiday, the assumption being that lack of any responses
was caused by the holiday break. (And this time the message is CC'ed
to LKML, so there will be a public record of it.)

A few people have said they believe the Linux Kernel Memory Model
should make unlock followed by lock (of the same variable) act as a
write memory barrier. In other words, they want the memory model to
forbid the following litmus test:


C unlock-lock-write-ordering-1

{}

P0(int *x, int *y, spinlock_t *s)
{
spin_lock(s);
WRITE_ONCE(*x, 1);
spin_unlock(s);
spin_lock(s);
WRITE_ONCE(*y, 1);
spin_unlock(s);
}

P1(int *x, int *y)
{
r1 = READ_ONCE(*y);
smp_rmb();
r2 = READ_ONCE(*x);
}

exists (1:r1=1 /\ 1:r2=0)


Judging from this, it seems likely that they would want the memory
model to forbid the next two litmus tests as well (since there's never
any guarantee that some other CPU won't interpose a critical section
between a given unlock and a following lock):


C unlock-lock-write-ordering-2

{}

P0(int *x, spinlock_t *s)
{
spin_lock(s);
WRITE_ONCE(*x, 1);
spin_unlock(s);
}

P1(int *x, int *y, spinlock_t *s)
{
spin_lock(s);
r1 = READ_ONCE(*x);
WRITE_ONCE(*y, 1);
spin_unlock(s);
}

P2(int *x, int *y)
{
r2 = READ_ONCE(*y);
smp_rmb();
r3 = READ_ONCE(*x);
}

exists (1:r1=1 /\ 2:r2=1 /\ 2:r3=0)


C unlock-lock-write-ordering-3

{}

P0(int *x, int *y, int *z, spinlock_t *s)
{
spin_lock(s);
WRITE_ONCE(*x, 1);
spin_unlock(s);
spin_lock(s);
r1 = READ_ONCE(*z);
WRITE_ONCE(*y, 1);
spin_unlock(s);
}

P1(int *x, int *z, spinlock_t *s)
{
spin_lock(s);
r2 = READ_ONCE(*x);
WRITE_ONCE(*z, 1);
spin_unlock(s);
}

P2(int *x, int *y)
{
r3 = READ_ONCE(*y);
smp_rmb();
r4 = READ_ONCE(*x);
}

exists (0:r1=1 /\ 1:r2=1 /\ 2:r3=1 /\ 2:r4=0)


The general justification is that all the architectures currently
supported by the kernel do forbid these tests, and there is code in the
kernel that depends on this behavior. Thus the model should forbid
them. (Currently the model allows them, on the principle that ordering
induced by a lock is visible only to CPUs that take the lock.)

On the other hand, whether RISC-V would forbid these tests is not
clear. Basically, it comes down to using an RCsc versus an RCpc
approach for the locking primitives.

Given that spin_lock() and spin_unlock() derive many of their
properties from acting as an acquire and a release respectively, we can
ask if the memory model should forbid the analogous release-acquire
litmus test:


C rel-acq-write-ordering-3

{}

P0(int *x, int *s, int *y)
{
WRITE_ONCE(*x, 1);
smp_store_release(s, 1);
r1 = smp_load_acquire(s);
WRITE_ONCE(*y, 1);
}

P1(int *x, int *y)
{
r2 = READ_ONCE(*y);
smp_rmb();
r3 = READ_ONCE(*x);
}

exists (1:r2=1 /\ 1:r3=0)


For that matter, what if we take the initial write to be the
store-release itself rather than something coming before it?


C rel-acq-write-ordering-1

{}

P0(int *s, int *y)
{
smp_store_release(s, 1);
r1 = smp_load_acquire(s);
WRITE_ONCE(*y, 1);
}

P1(int *s, int *y)
{
r2 = READ_ONCE(*y);
smp_rmb();
r3 = READ_ONCE(*s);
}

exists (1:r2=1 /\ 1:r3=0)


And going to extremes, what if the load-acquire reads from a different
variable, not the one written by the store-release? This would be
like unlocking s and then locking t:


C rel-acq-write-ordering-2

{}

P0(int *s, int *t, int *y)
{
smp_store_release(s, 1);
r1 = smp_load_acquire(t);
WRITE_ONCE(*y, 1);
}

P1(int *s, int *y)
{
r2 = READ_ONCE(*y);
smp_rmb();
r3 = READ_ONCE(*s);
}

exists (1:r2=1 /\ 1:r3=0)


The architectures currently supported by the kernel all forbid this
last test, but whether we want the model to forbid it is a lot more
questionable.

I (and others!) would like to know people's opinions on these matters.

Alan Stern

\
 
 \ /
  Last update: 2017-11-27 22:18    [W:0.083 / U:4.616 seconds]
©2003-2018 Jasper Spaans|hosted at Digital Ocean and TransIP|Read the blog|Advertise on this site