lkml.org 
[lkml]   [2018]   [Mar]   [1]   [last100]   RSS Feed
Views: [wrap][no wrap]   [headers]  [forward] 
 
Messages in this thread
/
Date
From
SubjectRe: [PATCH 2/2 v2 RFC] tools/memory-model: redefine rb in terms of rcu-fence
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
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.

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

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

Alan

\
 
 \ /
  Last update: 2018-03-01 16:49    [W:0.769 / U:0.080 seconds]
©2003-2020 Jasper Spaans|hosted at Digital Ocean and TransIP|Read the blog|Advertise on this site