From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: (majordomo@vger.kernel.org) by vger.kernel.org via listexpand id S933335AbcI3J5s (ORCPT ); Fri, 30 Sep 2016 05:57:48 -0400 Received: from bombadil.infradead.org ([198.137.202.9]:32920 "EHLO bombadil.infradead.org" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with ESMTP id S932413AbcI3J5l (ORCPT ); Fri, 30 Sep 2016 05:57:41 -0400 Date: Fri, 30 Sep 2016 11:57:38 +0200 From: Peter Zijlstra To: "Paul E. McKenney" Cc: Will Deacon , linux-kernel@vger.kernel.org, mingo@kernel.org, dhowells@redhat.com, stern@rowland.harvard.edu Subject: Re: [PATCH locking/Documentation 1/2] Add note of release-acquire store vulnerability Message-ID: <20160930095738.GG5016@twins.programming.kicks-ass.net> References: <20160929155401.GA5097@linux.vnet.ibm.com> <20160929155817.GB5016@twins.programming.kicks-ass.net> <20160929160307.GT13862@arm.com> <20160929164353.GX14933@linux.vnet.ibm.com> <20160929171036.GV13862@arm.com> <20160929172322.GZ14933@linux.vnet.ibm.com> <20160929180444.GA22882@linux.vnet.ibm.com> <20160929181015.GB22882@linux.vnet.ibm.com> <20160929184439.GD5016@twins.programming.kicks-ass.net> <20160929191858.GD14933@linux.vnet.ibm.com> MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline In-Reply-To: <20160929191858.GD14933@linux.vnet.ibm.com> User-Agent: Mutt/1.5.23.1 (2014-03-12) Sender: linux-kernel-owner@vger.kernel.org List-ID: X-Mailing-List: linux-kernel@vger.kernel.org On Thu, Sep 29, 2016 at 12:18:58PM -0700, Paul E. McKenney wrote: > On Thu, Sep 29, 2016 at 08:44:39PM +0200, Peter Zijlstra wrote: > > How about something like so on PPC? > > > > P0(int *x, int *y) > > { > > WRITE_ONCE(*x, 1); > > smp_store_release(y, 1); > > } > > > > P1(int *x, int *y) > > { > > WRITE_ONCE(x, 2); > > Need "WRITE_ONCE(*x, 2)" here. > > > smp_store_release(y, 2); > > } > > > > P2(int *x, int *y) > > { > > r1 = smp_load_acquire(y); > > r2 = READ_ONCE(*x); > > } > > > > (((x==1 && y==2) | (x==2 && y==1)) && (r1==1 || r1==2) && r2==0) > > That exists-clause is quite dazzling... So if each of P0 and P1 > win, but on different stores, and if P2 follows one or the other > of P0 or P1, can r2 get the pre-initialization value for x? > > > If you execute P0 and P1 concurrently and one store of each 'wins' the > > LWSYNC of either is null and void, and therefore P2 is unordered and can > > observe r2==0. > > That vaguely resembles the infamous Z6.3, but only vaguely. The Linux-kernel > memory model says "forbidden" to this: https://www.cl.cam.ac.uk/~pes20/ppc-supplemental/ppc710.html That one, right? Hmm, I seem to remember something else.. /me goes poke through history and comes up with: https://lkml.kernel.org/r/20160115215853.GC3818@linux.vnet.ibm.com So what was that about then? I remember it being a completely nonsensical case, but a weird one. > So let's try PPCMEM. If PPCMEM allows it, then the kernel model is > clearly broken. > > PPC PeterZijlstra+o-r+o-r+a-o-SB.litmus > { > 0:r1=1; 0:r2=2; 0:r3=x; 0:r4=y; > 1:r1=1; 1:r2=2; 1:r3=x; 1:r4=y; > 2:r3=x; 2:r4=y; > } > P0 | P1 | P2 ; > stw r1,0(r3) | stw r2,0(r3) | lwz r1,0(r4) ; > lwsync | lwsync | lwsync ; > stw r1,0(r4) | stw r2,0(r4) | lwz r2,0(r3) ; > exists > (((x=1 /\ y=2) \/ (x=2 /\ y=1)) /\ (2:r1=1 \/ 2:r1=2) /\ 2:r2=0) > Or did I incorrectly translate your litmus test? Looks about right. Still not seeing how that is prohibited though. My reasoning is as follows: - P0 and P1 both store to x, one looses (say P0). Effectively only P1 does a store. - P0 and P1 both store to y, one looses (say P1). Effectively only P0 does a store. - P2 reads y, sees the value from P0. - P2 does lwsync, which constraints P2 to not issue the load of x before this. It also forms a (local) sync-point with P0 for having seen its store or y. - P2 reads x, sees the initial value because the store from P1 hasn't been propagated yet. It will not see the store P0 did to x, since that didn't happen. Assuming I'm wrong on that last part, is then the following possible? (x=2 /\ y=1 /\ 2:r1=1 /\ 2:r2=1) Where we see a store that didn't happen?