Received-SPF: pass (google.com: best guess record for domain of linux-kernel-owner@vger.kernel.org designates 209.132.180.67 as permitted sender) client-ip=209.132.180.67;
Date:   Mon, 27 Nov 2017 16:16:47 -0500 (EST)
From:   Alan Stern <stern@rowland.harvard.edu>
To:     "Paul E. McKenney" <paulmck@linux.vnet.ibm.com>,
        Andrea Parri <parri.andrea@gmail.com>,
        Luc Maranget <luc.maranget@inria.fr>,
        Jade Alglave <j.alglave@ucl.ac.uk>,
        Boqun Feng <boqun.feng@gmail.com>,
        Nicholas Piggin <npiggin@gmail.com>,
        Peter Zijlstra <peterz@infradead.org>,
        Will Deacon <will.deacon@arm.com>,
        David Howells <dhowells@redhat.com>,
        Daniel Lustig <dlustig@nvidia.com>,
        Palmer Dabbelt <palmer@dabbelt.com>
cc:     Kernel development list <linux-kernel@vger.kernel.org>
Subject: Unlock-lock questions and the Linux Kernel Memory Model
In-Reply-To: <4118cdbe-c396-08b9-a3e3-a0a6491b82fa@nvidia.com>
Message-ID: <Pine.LNX.4.44L0.1711271553490.1424-100000@iolanthe.rowland.org>
MIME-Version: 1.0
Content-Type: TEXT/PLAIN; charset=US-ASCII
Sender: linux-kernel-owner@vger.kernel.org
Precedence: bulk

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


From 1585510294555705936@xxx Thu Nov 30 16:47:26 +0000 2017
X-GM-THRID: 1585506351213539491
X-Gmail-Labels: Inbox,Category Forums,HistoricalUnread