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:   Thu, 1 Mar 2018 20:50:15 -0800
From:   "Paul E. McKenney" <paulmck@linux.vnet.ibm.com>
To:     Boqun Feng <boqun.feng@gmail.com>
Cc:     Alan Stern <stern@rowland.harvard.edu>,
        LKMM Maintainers -- Akira Yokosawa <akiyks@gmail.com>,
        Andrea Parri <parri.andrea@gmail.com>,
        David Howells <dhowells@redhat.com>,
        Jade Alglave <j.alglave@ucl.ac.uk>,
        Luc Maranget <luc.maranget@inria.fr>,
        Nicholas Piggin <npiggin@gmail.com>,
        Peter Zijlstra <peterz@infradead.org>,
        Will Deacon <will.deacon@arm.com>,
        Kernel development list <linux-kernel@vger.kernel.org>
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>
 <Pine.LNX.4.44L0.1803011027120.1394-100000@iolanthe.rowland.org>
 <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)
Message-Id: <20180302045015.GO3777@linux.vnet.ibm.com>
Sender: linux-kernel-owner@vger.kernel.org
Precedence: bulk

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 <boqun.feng@gmail.com>

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*
> >