From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: (majordomo@vger.kernel.org) by vger.kernel.org via listexpand id S1752269AbdBMSj0 (ORCPT ); Mon, 13 Feb 2017 13:39:26 -0500 Received: from mx0a-001b2d01.pphosted.com ([148.163.156.1]:33743 "EHLO mx0a-001b2d01.pphosted.com" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with ESMTP id S1751665AbdBMSjZ (ORCPT ); Mon, 13 Feb 2017 13:39:25 -0500 Date: Mon, 13 Feb 2017 10:39:20 -0800 From: "Paul E. McKenney" To: rth@twiddle.net, ink@jurassic.park.msu.ru, mattst88@gmail.com Cc: stern@rowland.harvard.edu, j.alglave@ucl.ac.uk, luc.maranget@inria.fr, parri.andrea@gmail.com, will.deacon@arm.com, linux-alpha@vger.kernel.org, linux-kernel@vger.kernel.org Subject: Question about DEC Alpha memory ordering Reply-To: paulmck@linux.vnet.ibm.com MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline User-Agent: Mutt/1.5.21 (2010-09-15) X-TM-AS-GCONF: 00 X-Content-Scanned: Fidelis XPS MAILER x-cbid: 17021318-8235-0000-0000-00000AF18A6F X-IBM-SpamModules-Scores: X-IBM-SpamModules-Versions: BY=3.00006610; HX=3.00000240; KW=3.00000007; PH=3.00000004; SC=3.00000203; SDB=6.00821441; UDB=6.00401752; IPR=6.00598894; BA=6.00005133; NDR=6.00000001; ZLA=6.00000005; ZF=6.00000009; ZB=6.00000000; ZP=6.00000000; ZH=6.00000000; ZU=6.00000002; MB=3.00014268; XFM=3.00000011; UTC=2017-02-13 18:39:20 X-IBM-AV-DETECTION: SAVI=unused REMOTE=unused XFE=unused x-cbparentid: 17021318-8236-0000-0000-0000398D4ACB Message-Id: <20170213183920.GA25191@linux.vnet.ibm.com> X-Proofpoint-Virus-Version: vendor=fsecure engine=2.50.10432:,, definitions=2017-02-13_10:,, 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-1612050000 definitions=main-1702130180 Sender: linux-kernel-owner@vger.kernel.org List-ID: X-Mailing-List: linux-kernel@vger.kernel.org Hello! We have a question about DEC Alpha memory ordering. Given the litmus test shown at the end of this email, some of us believe that DEC Alpha won't ever have both P0()'s and P1()'s READ_ONCE() calls return 1, but others believe otherwise. Our current Linux-kernel memory model assumes that it cannot, though we are not aware of any Linux-kernel code that cares. In this litmus test, the "C auto/C-LB-LRW+OB-Ov" and the empty pair of curly braces can be ignored. P0() and P1() run concurrently, and are passed pointer to the two shared variables that they are accessing (u0 and x1, and yes, this test was automatically generated -- why do you ask?). The "exists" clause at the end is evaluated at the end of time, after all the dust has settled. Note that the undeclared "r1" variables are local to their respective functions, and that "0:r1" in the "exists" clause accesses P0()'s instance of "r1", and that "1:r1" similarly accesses P1()'s "r1". So, can real DEC Alpha hardware end up with both instances of "r1" having the value 1? Thanx, Paul ------------------------------------------------------------------------ C auto/C-LB-LRW+OB-Ov { } P0(int *u0, int *x1) { r1 = READ_ONCE(*u0); smp_mb(); WRITE_ONCE(*x1, 1); } P1(int *u0, int *x1) { r1 = READ_ONCE(*x1); WRITE_ONCE(*u0, r1); } exists (0:r1=1 /\ 1:r1=1)