From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: (majordomo@vger.kernel.org) by vger.kernel.org via listexpand id S1422815AbeCBEuB (ORCPT ); Thu, 1 Mar 2018 23:50:01 -0500 Received: from mx0a-001b2d01.pphosted.com ([148.163.156.1]:33728 "EHLO mx0a-001b2d01.pphosted.com" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with ESMTP id S1164978AbeCBEtx (ORCPT ); Thu, 1 Mar 2018 23:49:53 -0500 Date: Thu, 1 Mar 2018 20:50:15 -0800 From: "Paul E. McKenney" To: Boqun Feng Cc: Alan Stern , LKMM Maintainers -- Akira Yokosawa , Andrea Parri , David Howells , Jade Alglave , Luc Maranget , Nicholas Piggin , Peter Zijlstra , Will Deacon , Kernel development list Subject: Re: [PATCH 2/2 v2 RFC] tools/memory-model: redefine rb in terms of rcu-fence Reply-To: paulmck@linux.vnet.ibm.com References: <20180301015531.olvuu5g35eta5xhr@tardis> <20180301174906.GC3777@linux.vnet.ibm.com> <20180301183758.GA31761@linux.vnet.ibm.com> <20180302043141.fgmjyysrws55pi7q@tardis> MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline In-Reply-To: <20180302043141.fgmjyysrws55pi7q@tardis> User-Agent: Mutt/1.5.21 (2010-09-15) X-TM-AS-GCONF: 00 x-cbid: 18030204-0044-0000-0000-000003ED013B X-IBM-SpamModules-Scores: X-IBM-SpamModules-Versions: BY=3.00008609; HX=3.00000241; KW=3.00000007; PH=3.00000004; SC=3.00000254; SDB=6.00997107; UDB=6.00506974; IPR=6.00776425; MB=3.00019811; MTD=3.00000008; XFM=3.00000015; UTC=2018-03-02 04:49:47 X-IBM-AV-DETECTION: SAVI=unused REMOTE=unused XFE=unused x-cbparentid: 18030204-0045-0000-0000-0000081D0280 Message-Id: <20180302045015.GO3777@linux.vnet.ibm.com> X-Proofpoint-Virus-Version: vendor=fsecure engine=2.50.10432:,, definitions=2018-03-02_02:,, signatures=0 X-Proofpoint-Spam-Details: rule=outbound_notspam policy=outbound score=0 priorityscore=1501 malwarescore=0 suspectscore=0 phishscore=0 bulkscore=0 spamscore=0 clxscore=1015 lowpriorityscore=0 impostorscore=0 adultscore=0 classifier=spam adjust=0 reason=mlx scancount=1 engine=8.0.1-1709140000 definitions=main-1803020054 Sender: linux-kernel-owner@vger.kernel.org List-ID: X-Mailing-List: linux-kernel@vger.kernel.org On Fri, Mar 02, 2018 at 12:31:41PM +0800, Boqun Feng wrote: > On Thu, Mar 01, 2018 at 10:37:58AM -0800, Paul E. McKenney wrote: > > On Thu, Mar 01, 2018 at 09:49:06AM -0800, Paul E. McKenney wrote: [ . . . ] > > And as Andrea pointed out off-list, I did indeed mess up Boqun's change. > > I forgot to change the "irreflexive" into "acyclic". Applying that change > > makes everything work. > > > > Please accept my apologies for my confusion! > > > > np, also I should have provided a proper patch for your testing. > > For this Alan's patch, feel free to add: > > Reviewed-by: Boqun Feng Alan's last submission was still RFC, so I have not yet queued it. So this ball is still in Alan's court. Thanx, Paul > Regards, > Boqun > > > Thanx, Paul > > > > > > > I prefer this because we already treat "gp" as "strong-fence", which > > > > > already is a "rcu-link". > > > > > > > > That's a good point; it had not occurred to me. > > > > > > And if I remove the "gp" but leave the last line, it does properly > > > classify the two new litmus tests. > > > > > > Thanx, Paul > > > > > > > > Also, recurisively extending rcu-fence with > > > > > itself is exactly calculating the transitive closure, which we can avoid > > > > > by using a "acycle" rule. Besides, it looks more consistent with hb and > > > > > pb. > > > > > > > > That _had_ occurred to me. But I couldn't see any way to do it while > > > > still defining rcu-fence correctly. > > > > > > ------------------------------------------------------------------------ > > > > > > diff --git a/tools/memory-model/linux-kernel.cat b/tools/memory-model/linux-kernel.cat > > > index 1e5c4653dd12..75d3c225146c 100644 > > > --- a/tools/memory-model/linux-kernel.cat > > > +++ b/tools/memory-model/linux-kernel.cat > > > @@ -106,12 +106,11 @@ let rcu-link = hb* ; pb* ; prop > > > * Any sequence containing at least as many grace periods as RCU read-side > > > * critical sections (joined by rcu-link) acts as a generalized strong fence. > > > *) > > > -let rec rcu-fence = gp | > > > +let rec rcu-fence = > > > (gp ; rcu-link ; rscs) | > > > (rscs ; rcu-link ; gp) | > > > (gp ; rcu-link ; rcu-fence ; rcu-link ; rscs) | > > > - (rscs ; rcu-link ; rcu-fence ; rcu-link ; gp) | > > > - (rcu-fence ; rcu-link ; rcu-fence) > > > + (rscs ; rcu-link ; rcu-fence ; rcu-link ; gp) > > > > > > (* rb orders instructions just as pb does *) > > > let rb = prop ; rcu-fence ; hb* ; pb* > >