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]

Date:   Wed, 16 Jan 2019 05:11:50 -0800
From:   "Paul E. McKenney" <paulmck@...ux.ibm.com>
To:     Peter Zijlstra <peterz@...radead.org>
Cc:     Alan Stern <stern@...land.harvard.edu>,
        Andrea Parri <andrea.parri@...rulasolutions.com>,
        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>,
        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 Wed, Jan 16, 2019 at 12:57:52PM +0100, Peter Zijlstra wrote:
> On Tue, Jan 15, 2019 at 10:19:10AM -0500, Alan Stern wrote:
> > On Tue, 15 Jan 2019, Andrea Parri wrote:
> > 
> > > Unless I'm mis-reading/-applying this definition, this will flag the
> > > following test (a variation on your "race.litmus") with "data-race":
> > > 
> > > C no-race
> > > 
> > > {}
> > > 
> > > P0(int *x, spinlock_t *s)
> > > {
> > > 	spin_lock(s);
> > >         WRITE_ONCE(*x, 1);	/* A */
> > > 	spin_unlock(s);	/* B */
> > > }
> > > 
> > > P1(int *x, spinlock_t *s)
> > > {
> > >         int r1;
> > > 
> > > 	spin_lock(s); /* C */
> > >         r1 = *x;	/* D */
> > > 	spin_unlock(s);
> > > }
> > > 
> > > exists (1:r1=1)
> > > 
> > > Broadly speaking, this is due to the fact that the modified "happens-
> > > before" axiom does not forbid the execution with the (MP-) cycle
> > > 
> > > 	A ->po-rel B ->rfe C ->acq-po D ->fre A
> > > 
> > > and then to the link "D ->race-from-r A" here defined.
> > 
> > Yes, that cycle certainly should be forbidden.  On the other hand, we
> > don't want to insist that C happens before D, given that D may not
> > happen at all.
> > 
> > This is a real problem.  Can we solve it by adding a modified
> > "happens-before" which says essentially that _if_ D is preserved _then_
> > C happens before D?  But then what about cycles involving more than one
> > possibly preserved access?  Or maybe a relation which says that D
> > cannot execute before C (so if D executes at all, it has to come after
> > C)?
> 
> The latter; there is a compiler barrier implied at the end of
> spin_lock() such that anything later (in PO) must indeed be later.
> 
> > Now you see why this stuff is so difficult...  At the moment, I don't
> > know how to fix this.

In the spirit of cutting the Gordian Knot...

Given that we are flagging data races, how much do we really lose by
simply ignoring the possibility of removed accesses?

							Thanx, Paul