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, 15 Nov 2018 14:12:44 -0500 (EST)
From:   Alan Stern <stern@rowland.harvard.edu>
To:     Boqun Feng <boqun.feng@gmail.com>
cc:     "Paul E. McKenney" <paulmck@linux.ibm.com>,
        LKMM Maintainers -- Akira Yokosawa <akiyks@gmail.com>,
        Andrea Parri <andrea.parri@amarulasolutions.com>,
        Daniel Lustig <dlustig@nvidia.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/3] tools/memory-model: Refactor some RCU relations
In-Reply-To: <20181115175420.GA3227@tardis>
Message-ID: <Pine.LNX.4.44L0.1811151406580.1308-100000@iolanthe.rowland.org>
MIME-Version: 1.0
Content-Type: TEXT/PLAIN; charset=US-ASCII
Sender: linux-kernel-owner@vger.kernel.org
Precedence: bulk

On Fri, 16 Nov 2018, Boqun Feng wrote:

> > -let rcu-rscsi = po ; rcu-rscs^-1 ; po?
> > +let rcu-gp = [Sync-rcu]		(* Compare with gp *)
> > +let rcu-rscsi = rcu-rscs^-1
> 
> Isn't it more straight-forward to use "rcu-rscs^-1" other than
> "rcu-rscsi" in the definition of "rcu-fence", is it?

It's a matter of personal preference.  I prefer to store the inverse
relation in a separate variable rather than recomputing it multiple
times.  (Maybe OCaml is smart enough to recognize when a value has 
already been computed and avoid computing it again; I don't know.)

> The introduction of "rcu-rscsi" makes sense in the first patch, but with
> this refactoring, I think it's better we just don't use it.

In the end this probably doesn't make much difference.

Alan