public inbox for linux-kernel@vger.kernel.org
 help / color / mirror / Atom feed
* Question about DEC Alpha memory ordering
@ 2017-02-13 18:39 Paul E. McKenney
  2017-02-13 18:53 ` bob smith
  0 siblings, 1 reply; 13+ messages in thread
From: Paul E. McKenney @ 2017-02-13 18:39 UTC (permalink / raw)
  To: rth, ink, mattst88
  Cc: stern, j.alglave, luc.maranget, parri.andrea, will.deacon,
	linux-alpha, linux-kernel

Hello!

We have a question about DEC Alpha memory ordering.  Given the litmus test
shown at the end of this email, some of us believe that DEC Alpha won't
ever have both P0()'s and P1()'s READ_ONCE() calls return 1, but others
believe otherwise.  Our current Linux-kernel memory model assumes that
it cannot, though we are not aware of any Linux-kernel code that cares.

In this litmus test, the "C auto/C-LB-LRW+OB-Ov" and the empty pair
of curly braces can be ignored.  P0() and P1() run concurrently, and
are passed pointer to the two shared variables that they are accessing
(u0 and x1, and yes, this test was automatically generated -- why do
you ask?).  The "exists" clause at the end is evaluated at the end of
time, after all the dust has settled.  Note that the undeclared "r1"
variables are local to their respective functions, and that "0:r1" in
the "exists" clause accesses P0()'s instance of "r1", and that "1:r1"
similarly accesses P1()'s "r1".

So, can real DEC Alpha hardware end up with both instances of "r1"
having the value 1?

							Thanx, Paul

------------------------------------------------------------------------

C auto/C-LB-LRW+OB-Ov
{
}

P0(int *u0, int *x1)
{
	r1 = READ_ONCE(*u0);
	smp_mb();
	WRITE_ONCE(*x1, 1);
}


P1(int *u0, int *x1)
{
	r1 = READ_ONCE(*x1);
	WRITE_ONCE(*u0, r1);
}

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

^ permalink raw reply	[flat|nested] 13+ messages in thread

end of thread, other threads:[~2017-02-14 20:13 UTC | newest]

Thread overview: 13+ messages (download: mbox.gz follow: Atom feed
-- links below jump to the message on this page --
2017-02-13 18:39 Question about DEC Alpha memory ordering Paul E. McKenney
2017-02-13 18:53 ` bob smith
2017-02-13 19:08   ` Will Deacon
2017-02-13 19:09   ` Paul E. McKenney
2017-02-13 19:14     ` Tobias Klausmann
2017-02-13 20:28       ` Paul E. McKenney
2017-02-13 21:06         ` Alan Stern
2017-02-13 21:24           ` Paul E. McKenney
2017-02-14 11:35             ` Andrea Parri
2017-02-14 19:26               ` Michael Cree
2017-02-14 20:12                 ` Andrea Parri
2017-02-13 19:23     ` Michael Cree
2017-02-13 20:32       ` Paul E. McKenney

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox