Received-SPF: pass (google.com: best guess record for domain of linux-kernel-owner@vger.kernel.org designates 209.132.180.67 as permitted sender) client-ip=209.132.180.67;
Date:   Wed, 16 Jan 2019 12:57:52 +0100
From:   Peter Zijlstra <peterz@infradead.org>
To:     Alan Stern <stern@rowland.harvard.edu>
Cc:     Andrea Parri <andrea.parri@amarulasolutions.com>,
        LKMM Maintainers -- Akira Yokosawa <akiyks@gmail.com>,
        Boqun Feng <boqun.feng@gmail.com>,
        Daniel Lustig <dlustig@nvidia.com>,
        David Howells <dhowells@redhat.com>,
        Jade Alglave <j.alglave@ucl.ac.uk>,
        Luc Maranget <luc.maranget@inria.fr>,
        Nicholas Piggin <npiggin@gmail.com>,
        "Paul E. McKenney" <paulmck@linux.ibm.com>,
        Will Deacon <will.deacon@arm.com>,
        Dmitry Vyukov <dvyukov@google.com>,
        linux-kernel@vger.kernel.org
Subject: Re: Plain accesses and data races in the Linux Kernel Memory Model
Message-ID: <20190116115752.GB10803@hirez.programming.kicks-ass.net>
References: <20190115142545.GA9255@andrea>
 <Pine.LNX.4.44L0.1901151003470.1408-100000@iolanthe.rowland.org>
MIME-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Content-Disposition: inline
In-Reply-To: <Pine.LNX.4.44L0.1901151003470.1408-100000@iolanthe.rowland.org>
User-Agent: Mutt/1.10.1 (2018-07-13)
Sender: linux-kernel-owner@vger.kernel.org
Precedence: bulk

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.