Messages in this thread | | | Date | Thu, 15 Nov 2018 14:12:44 -0500 (EST) | From | Alan Stern <> | Subject | Re: [PATCH 2/3] tools/memory-model: Refactor some RCU relations |
| |
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
| |