linux-kernel - Question about DEC Alpha memory ordering

lists.openwall.net		lists / announce owl-users owl-dev john-users john-dev passwdqc-users yescrypt popa3d-users / oss-security kernel-hardening musl sabotage tlsify passwords / crypt-dev xvendor / Bugtraq Full-Disclosure linux-kernel linux-netdev linux-ext4 linux-hardening linux-cve-announce PHC
Open Source and information security mailing list archives

Hash Suite: Windows password security audit tool. GUI, reports in PDF.

[<prev] [next>] [thread-next>] [day] [month] [year] [list]

Date:   Mon, 13 Feb 2017 10:39:20 -0800
From:   "Paul E. McKenney" <paulmck@...ux.vnet.ibm.com>
To:     rth@...ddle.net, ink@...assic.park.msu.ru, mattst88@...il.com
Cc:     stern@...land.harvard.edu, j.alglave@....ac.uk,
        luc.maranget@...ia.fr, parri.andrea@...il.com, will.deacon@....com,
        linux-alpha@...r.kernel.org, linux-kernel@...r.kernel.org
Subject: Question about DEC Alpha memory ordering

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)