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: Windows password security audit tool. GUI, reports in PDF.

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

Date:   Tue, 22 Jan 2019 11:19:13 -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>,
        <linux-kernel@...r.kernel.org>
Subject: Re: Plain accesses and data races in the Linux Kernel Memory Model

On Tue, 22 Jan 2019, Andrea Parri wrote:

> > @@ -131,7 +159,7 @@ let rec rcu-fence = rcu-gp | srcu-gp |
> >  	(rcu-fence ; rcu-link ; rcu-fence)
> >  
> >  (* rb orders instructions just as pb does *)
> > -let rb = prop ; po ; rcu-fence ; po? ; hb* ; pb*
> > +let rb = prop ; po ; rcu-fence ; po? ; hb* ; pb* ; [marked]
> 
> Testing has revealed some subtle semantics changes for some RCU tests
> _without_ unmarked memory accesses; an example is reported at the end
> of this email.  I suspect that the improvements you mentioned in this
> thread can restore the original semantics but I'm reporting this here
> for further reference.
> 
> With the above definition of 'rb', we're losing links which originate
> or target RCU fences, so that this definition is in fact a relaxation
> w.r.t. the current semantics (even when limiting to marked accesses).
> The test below, for example, is currently forbidden by the LKMM, but
> it becomes allowed with this patch.
> 
> FWIW, I checked that including the RCU fences in 'marked' can restore
> the original semantics of these tests; I'm still not sure whether this
> change can make sense though....
> 
> Thoughts?

Ah, a very good discovery.  I think changing marked to ~plain in a few
places would be a better solution.  Or maybe allowing plain accesses in
those places will also be okay -- it's hard to judge at this point.

> Oh, one last (and unrelated) nit before I forget: IIUC, we used to
> upper-case set names, so I'd also suggest s/marked/Marked, s/plain/Plain
> and similarly for the other sets to be introduced.

Okay, I'll follow that convention.

Alan