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

Message-ID: <Pine.LNX.4.44L0.1901151003470.1408-100000@iolanthe.rowland.org>
Date:   Tue, 15 Jan 2019 10:19:10 -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, 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)?

Now you see why this stuff is so difficult...  At the moment, I don't
know how to fix this.

> (In part., similar considerations hold for the following litmus test:
> 
> C MP1
> 
> {}
> 
> P0(int *x, int *y)
> {
> 	*x = 1;
> 	smp_store_release(y, 1);
> }
> 
> P1(int *x, int *y)
> {
> 	int r0;
> 	int r1 = -1;
> 
> 	r0 = smp_load_acquire(y);
> 	if (r0)
> 		r1 = *x;
> }
> 
> exists (1:r0=1 /\ 1:r1=0)
> 
> )
> 
> I wonder whether you actually intended to introduce these "races"...?

No, I did not.

Alan