linux-kernel - Re: Plain accesses and data races in 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 for Android: free password hash cracker in your pocket

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

Message-ID: <Pine.LNX.4.44L0.1901181005110.1425-100000@iolanthe.rowland.org>
Date:   Fri, 18 Jan 2019 10:10:22 -0500 (EST)
From:   Alan Stern <stern@...land.harvard.edu>
To:     Andrea Parri <andrea.parri@...rulasolutions.com>
cc:     LKMM Maintainers -- Akira Yokosawa <akiyks@...il.com>,
        Boqun Feng <boqun.feng@...il.com>,
        Daniel Lustig <dlustig@...dia.com>,
        David Howells <dhowells@...hat.com>,
        Jade Alglave <j.alglave@....ac.uk>,
        Luc Maranget <luc.maranget@...ia.fr>,
        Nicholas Piggin <npiggin@...il.com>,
        "Paul E. McKenney" <paulmck@...ux.ibm.com>,
        Peter Zijlstra <peterz@...radead.org>,
        Will Deacon <will.deacon@....com>,
        Dmitry Vyukov <dvyukov@...gle.com>,
        Nick Desaulniers <ndesaulniers@...gle.com>,
        <linux-kernel@...r.kernel.org>
Subject: Re: Plain accesses and data races in the Linux Kernel Memory Model

On Thu, 17 Jan 2019, Andrea Parri wrote:

> > Can the compiler (maybe, it does?) transform, at the C or at the "asm"
> > level, LB1's P0 in LB2's P0 (LB1 and LB2 are reported below)?
> > 
> > C LB1
> > 
> > {
> > 	int *x = &a;
> > }
> > 
> > P0(int **x, int *y)
> > {
> > 	int *r0;
> > 
> > 	r0 = rcu_dereference(*x);
> > 	*r0 = 0;
> > 	smp_wmb();
> > 	WRITE_ONCE(*y, 1);
> > }
> > 
> > P1(int **x, int *y, int *b)
> > {
> > 	int r0;
> > 
> > 	r0 = READ_ONCE(*y);
> > 	rcu_assign_pointer(*x, b);
> > }
> > 
> > exists (0:r0=b /\ 1:r0=1)
> > 
> > 
> > C LB2
> > 
> > {
> > 	int *x = &a;
> > }
> > 
> > P0(int **x, int *y)
> > {
> > 	int *r0;
> > 
> > 	r0 = rcu_dereference(*x);
> > 	if (*r0)
> > 		*r0 = 0;
> > 	smp_wmb();
> > 	WRITE_ONCE(*y, 1);
> > }
> > 
> > P1(int **x, int *y, int *b)
> > {
> > 	int r0;
> > 
> > 	r0 = READ_ONCE(*y);
> > 	rcu_assign_pointer(*x, b);
> > }
> > 
> > exists (0:r0=b /\ 1:r0=1)
> > 
> > LB1 and LB2 are data-race free, according to the patch; LB1's "exists"
> > clause is not satisfiable, while LB2's "exists" clause is satisfiable.

A relatively simple solution to this problem would be to say that 
smp_wmb doesn't order plain writes.

I think the rest of the memory model would then be okay.  However, I am
open to arguments that this approach is too complex and we should
insist on the same kind of strict ordering for race avoidance that the
C11 standard uses (i.e., conflicting accesses separated by full memory
barriers or release & acquire barriers or locking).

Alan