From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: (majordomo@vger.kernel.org) by vger.kernel.org via listexpand id S1755931AbcI2U0s (ORCPT ); Thu, 29 Sep 2016 16:26:48 -0400 Received: from mx0b-001b2d01.pphosted.com ([148.163.158.5]:36205 "EHLO mx0a-001b2d01.pphosted.com" rhost-flags-OK-OK-OK-FAIL) by vger.kernel.org with ESMTP id S1755499AbcI2U0o (ORCPT ); Thu, 29 Sep 2016 16:26:44 -0400 Date: Thu, 29 Sep 2016 13:26:41 -0700 From: "Paul E. McKenney" To: Alan Stern Cc: Peter Zijlstra , Will Deacon , linux-kernel@vger.kernel.org, mingo@kernel.org, dhowells@redhat.com Subject: Re: [PATCH locking/Documentation 1/2] Add note of release-acquire store vulnerability Reply-To: paulmck@linux.vnet.ibm.com References: <20160929191858.GD14933@linux.vnet.ibm.com> MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline In-Reply-To: User-Agent: Mutt/1.5.21 (2010-09-15) X-TM-AS-GCONF: 00 X-Content-Scanned: Fidelis XPS MAILER x-cbid: 16092920-0016-0000-0000-000004CF295D X-IBM-SpamModules-Scores: X-IBM-SpamModules-Versions: BY=3.00005826; HX=3.00000240; KW=3.00000007; PH=3.00000004; SC=3.00000186; SDB=6.00762817; UDB=6.00363634; IPR=6.00537940; BA=6.00004771; NDR=6.00000001; ZLA=6.00000005; ZF=6.00000009; ZB=6.00000000; ZP=6.00000000; ZH=6.00000000; ZU=6.00000002; MB=3.00012825; XFM=3.00000011; UTC=2016-09-29 20:26:41 X-IBM-AV-DETECTION: SAVI=unused REMOTE=unused XFE=unused x-cbparentid: 16092920-0017-0000-0000-00003361016A Message-Id: <20160929202641.GE14933@linux.vnet.ibm.com> X-Proofpoint-Virus-Version: vendor=fsecure engine=2.50.10432:,, definitions=2016-09-29_13:,, signatures=0 X-Proofpoint-Spam-Details: rule=outbound_notspam policy=outbound score=0 spamscore=0 suspectscore=0 malwarescore=0 phishscore=0 adultscore=0 bulkscore=0 classifier=spam adjust=0 reason=mlx scancount=1 engine=8.0.1-1609280000 definitions=main-1609290353 Sender: linux-kernel-owner@vger.kernel.org List-ID: X-Mailing-List: linux-kernel@vger.kernel.org On Thu, Sep 29, 2016 at 03:36:38PM -0400, Alan Stern wrote: > On Thu, 29 Sep 2016, 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? > > In fact, this is more than you need. It's enough to specify > > exists (2:r1=1 \/ 2:r1=2) /\ 2:r2=0 > > This much already is forbidden. For the sake of argument, say r1=1. > Then P2 has read from P1's store-release. By definition, P1's write to > x is visible to P2, so r2 will get the value from that write or from > one that is later in x's coherence order. In other words, r2 will end > up equal to either 1 or 2, but not 0. > > > > 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. > > Not so. lwsync instructions cannot be "voided". > > > That vaguely resembles the infamous Z6.3, but only vaguely. The Linux-kernel > > memory model says "forbidden" to this: > > > > C C-WillDeacon-AcqRelStore.litmus > > > > { > > } > > > > P0(int *x, int *y) > > { > > WRITE_ONCE(*x, 1); > > smp_store_release(y, 1); > > } > > > > P1(int *x, int *y) > > { > > WRITE_ONCE(*x, 2); > > smp_store_release(y, 2); > > } > > > > P2(int *x, int *y) > > { > > r1 = smp_load_acquire(y); > > r2 = READ_ONCE(*x); > > } > > > > exists > > (((x=1 /\ y=2) \/ (x=2 /\ y=1)) /\ (2:r1=1 \/ 2:r1=2) /\ 2:r2=0) > > As above, you can leave out the part about the final values for x and > y. The test will still be forbidden. > > On the other hand, there's no guarantee that if r1=1 at the end then r2 > will also be 1. It's quite possible that r1=1 and r2=2, or vice versa. And herd agrees for both the kernel model and the powerpc translation. I killed PPCMEM, which was up to 1.2G of state space. So is this a case where "herd -cat ppc.cat" can be trusted? ;-) And the web ppcmem does not allow the exists clause, from what I could see. Thanx, Paul