linux-kernel - Re: Unlock-lock questions and the Linux Kernel Memory Model

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-prev] [thread-next>] [day] [month] [year] [list]

Date:   Mon, 27 Nov 2017 15:28:03 -0800
From:   Daniel Lustig <dlustig@...dia.com>
To:     Alan Stern <stern@...land.harvard.edu>,
        "Paul E. McKenney" <paulmck@...ux.vnet.ibm.com>,
        Andrea Parri <parri.andrea@...il.com>,
        Luc Maranget <luc.maranget@...ia.fr>,
        Jade Alglave <j.alglave@....ac.uk>,
        Boqun Feng <boqun.feng@...il.com>,
        Nicholas Piggin <npiggin@...il.com>,
        Peter Zijlstra <peterz@...radead.org>,
        Will Deacon <will.deacon@....com>,
        David Howells <dhowells@...hat.com>,
        Palmer Dabbelt <palmer@...belt.com>
CC:     Kernel development list <linux-kernel@...r.kernel.org>
Subject: Re: Unlock-lock questions and the Linux Kernel Memory Model

On 11/27/2017 1:16 PM, Alan Stern wrote:> 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)
> 
<snip>
> 
> And going to extremes...

Sorry if I'm missing something obvious, but before going to extremes...
what about this one?

"SB+rel-acq" (or please rename if you have a different scheme)

{}

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

P1(int *x, int *y)
{
	WRITE_ONCE(*y, 1);
	smp_store_release(s, 2);
	r3 = smp_load_acquire(s);
	r4 = READ_ONCE(*x);
}

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

If smp_store_release() and smp_load_acquire() map to normal TSO loads
and stores on x86, then this test can't be forbidden, can it?

Similar question for the other tests, but this is probably the
easiest one to analyze.

Dan