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
