Messages in this thread | | | Date | Fri, 2 Mar 2018 12:31:41 +0800 | From | Boqun Feng <> | Subject | Re: [PATCH 2/2 v2 RFC] tools/memory-model: redefine rb in terms of rcu-fence |
| |
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: > > On Thu, Mar 01, 2018 at 10:49:05AM -0500, Alan Stern wrote: > > > On Thu, 1 Mar 2018, Boqun Feng wrote: > > > > > > > > +let rec rcu-fence = gp | > > > > > + (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) > > > > > + > > > > > +(* rb orders instructions just as pb does *) > > > > > +let rb = prop ; rcu-fence ; hb* ; pb* > > > > > > > > > > irreflexive rb as rcu > > > > > > > > I wonder whether we can simplify things as: > > > > > > > > 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) > > > > > > > > (* gp and rcu-fence; rcu-link; rcu-fence removed *) > > > > > > > > let rb = prop; rcu-fence; hb*; pb* > > > > > > > > acycle rb as rcu > > > > > > > > In this way, "rcu-fence" is defined as "any sequence containing as many > > > > grace periods as RCU read-side critical sections (joined by rcu-link)." > > > > Note that "rcu-link" contains "gp", so we don't miss the case where > > > > there are more grace periods. And since we use "acycle" now, so we don't > > > > need "rcu-fence; rcu-link; rcu-fence" to build "rcu-fence" recursively. > > > > > > Would this definition of rcu-fence work for a sequence such as (leaving > > > out the intermediate rcu-link parts): > > > > > > gp gp gp rscs rscs gp rscs rscs > > > > > > ? I don't think it would. Yes, if you had a cycle of that form then
Right.
> > > your "rcu" axiom would detect it, but at some point we might want to > > > use rcu-fence for some other purpose, one that doesn't involve cycles.
OK, and I've not yet found another simple way to express rcu-fence for purposes other than cycle-checking. So I'm OK to leave it as it is except removing the redundant "gp" in rcu-fence definition.
But I will continue to search for a easier and sufficient way to define these things ;-)
> > > > Let's see, that would map to this: > > > > auto/RW-G+RW-G+RW-G+RW-R+RW-R+RW-G+RW-R+RW-R.litmus > > > > And no, there is no such automatically generated litmus test. Let's > > try reversing the "gp" and "rscs", which should have the same effect > > courtesy of symmetry: > > > > auto/RW-R+RW-R+RW-R+RW-G+RW-G+RW-R+RW-G+RW-G.litmus > > > > And that one doesn't exist, either. So much for random test generation! :-/ > > > > Clearly time to add them. And here is what herd has to say about them: > > > > l$ sh scripts/checklitmus.sh /tmp/auto/C-RW-G+RW-G+RW-G+RW-R+RW-R+RW-G+RW-R+RW-R.litmus > > Herd options: -conf linux-kernel.cfg > > Observation /tmp/auto/C-RW-G+RW-G+RW-G+RW-R+RW-R+RW-G+RW-R+RW-R Sometimes 1 255 > > ^^^ Unexpected non-Never verification > > 0inputs+32outputs (0major+2605minor)pagefaults 0swaps > > $ sh scripts/checklitmus.sh /tmp/auto/C-RW-R+RW-R+RW-R+RW-G+RW-G+RW-R+RW-G+RW-G.litmus > > Herd options: -conf linux-kernel.cfg > > Observation /tmp/auto/C-RW-R+RW-R+RW-R+RW-G+RW-G+RW-R+RW-G+RW-G Sometimes 1 255 > > ^^^ Unexpected non-Never verification > > 0inputs+32outputs (0major+2620minor)pagefaults 0swaps > > > > In other words, they are in fact misclassified as "Sometimes" when they > > should be "Never". I have my diffs below in case I misapplied Boqun's > > change. > > > > With Alan's original formulation, these two litmus tests are correctly > > handled: > > > > $ sh scripts/checklitmus.sh /tmp/auto/C-RW-G+RW-G+RW-G+RW-R+RW-R+RW-G+RW-R+RW-R.litmus > > Herd options: -conf linux-kernel.cfg > > Observation /tmp/auto/C-RW-G+RW-G+RW-G+RW-R+RW-R+RW-G+RW-R+RW-R Never 0 255 > > 1.61user 0.00system 0:01.63elapsed 98%CPU (0avgtext+0avgdata 9572maxresident)k > > $ sh scripts/checklitmus.sh /tmp/auto/C-RW-R+RW-R+RW-R+RW-G+RW-G+RW-R+RW-G+RW-G.litmus > > Herd options: -conf linux-kernel.cfg > > Observation /tmp/auto/C-RW-R+RW-R+RW-R+RW-G+RW-G+RW-R+RW-G+RW-G Never 0 255 > > 1.84user 0.01system 0:01.92elapsed 96%CPU (0avgtext+0avgdata 10112maxresident)k > > 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>
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* > [unhandled content-type:application/pgp-signature] | |