Re: Internal vs. external barriers (was: Re: Interesting LKMM litmus test)

Alan Stern
2023-01-19T02:28:34Z

Jonas, each of your emails introduces too many new thoughts and ideas!
I can't keep up. So in this reply I'm going to skip over most of what
you wrote. If you think any of the items I have elided are worth
pursuing, you can bring them up in a new thread -- hopefully with just
one main thought per email! :-)

On Wed, Jan 18, 2023 at 12:25:05PM +0100, Jonas Oberhauser wrote:
>
>
> On 1/17/2023 10:19 PM, Alan Stern wrote:
> > On Tue, Jan 17, 2023 at 06:48:12PM +0100, Jonas Oberhauser wrote:
> > > On 1/14/2023 5:42 PM, Alan Stern wrote:

> > > Pretending for simplicity that rscs and grace periods aren't reads&writes
> > They aren't. You don't have to pretend.
>
> rscs are reads& writes in herd. That's how the data dependency works in your
> patch, right?

No, you're mixing up RCU and SRCU. The RCU operations rcu_read_lock()
and rcu_read_unlock() are not loads or stores; they're just fences. In
the current form of the LKMM the same is true for the SRCU operations
srcu_read_lock() and srcu_read_unlock(), but in the patch I submitted
they are indeed loads and stores.

> I consider that a hack though and don't like it.

It _is_ a bit of a hack, but not a huge one. srcu_read_lock() really
is a lot like a load, in that it returns a value obtained by reading
something from memory (along with some other operations, though, so it
isn't a simple straightforward read -- perhaps more like an
atomic_inc_return_relaxed).

srcu_read_unlock() is somewhat less like a store, but it does have one
notable similarity: It takes an input value and therefore can be the
target of a data dependency. The biggest difference is that an
srcu_read_unlock() can't really be read-from. It would be nice if herd
had an event type that behaved this way.

Also, herd doesn't have any way of saying that the value passed to a
store is an unmodified copy of the value obtained by a load. In our
case that doesn't matter much -- nobody should be writing litmus tests
in which the value returned by srcu_read_lock() is incremented and then
decremented again before being passed to srcu_write_lock()!

> > > > There was also something about what should happen when you have two
> > > > grace periods in a row.
> > > Note that two grace periods in a row are a subset of po;rcu-gp;po and thus
> > > gp, and so there's nothing to be done.
> > That is not stated carefully, but it probably is wrong. Consider this:
> >
> > P0 P1 P2
> > --------------- -------------- -----------------
> > rcu_read_lock Wy=1 rcu_read_lock
> > Wx=1 synchronize_rcu Wz=1
> > Ry=0 synchronize_rcu Rx=0
> > rcu_read_unlock Rz=0 rcu_read_unlock
> >
> > (W stands for Write and R for Read.) This execution is forbidden by the
> > counting rule: Its cycle has two grace periods and two critical
> > sections. But if we changed the definition of gp to be
> >
> > let gp = po ; [Sync-rcu | Sync-srcu] ; po
> >
> > then the memory model would allow the execution. So having the po? at
> > the end of gp is vital.
>
> I hadn't thought yet about the effect of modifying the definition of gp, but
> I don't think this example relies on gp at all.
> The model would forbid this even if rcu-fence and gp were both changed from
> po? to po.
> From Rz=0 we know
>     second sync() ->rcu-gp;po Rz ->prop Wz ->po P2 unlock() ->rcu-rscsi P2
> lock()
> From Ry=0 we know
>   P1 unlock() ->rcu-rsci P1 lock() ->po Ry ->prop Wy ->po;rcu-gp first
> sync()
>
> which are both rcu-order.
> Then from Rx=0 we have
>   Rx ->prop Wx ->po P1 unlock() ->rcu-order  first sync() ->po second sync()
> ->rcu-order P2 lock() ->po Rx
> of course since po is one case of rcu-link, we get
>   Rx ->prop Wx ->po P1 unlock() ->rcu-order P2 lock() ->po Rx
> and hence
>   Rx ->prop Wx ->rcu-fence Rx
> which is supposed to be irreflexive (even with rcu-fence=po;rcu-order;po).

By golly, you're right! I'm still thinking in terms of an older
version of the memory model, which used gp in place of rcu-gp. In
that version, P1's write and read would be linked by gp but not by
(gp ; rcu-link ; gp) if the po? at the end of the definition of gp
was replaced by po.

> Note that if your ordering relies on actually using gp twice in a row, then
> these must come from strong-fence, but you should be able to just take the
> shortcut by merging them into a single gp.
>   po;rcu-gp;po;rcu-gp;po <= gp <= strong-fence <= hb & strong-order

I don't know what you mean by this. The example above does rely on
having two synchronize_rcu() calls; with only one it would be allowed.

> > > I don't think rcu-order is necessary at all to define LKMM, and one can
> > > probably just use rcu-extend instead of rcu-order (and in fact even a
> > > version of rcu-extend without any lone rcu-gps).
> > Sure, you could do that, but it wouldn't make sense. Why would anyone
> > want to define an RCU ordering relation that includes
> >
> > gp ... rscs ... gp ... rscs
> >
> > but not
> >
> > gp ... rscs ... rscs ... gp
> >
> > ?
>
> Because the the RCU Grace Period Guarantee doesn't say "if a gp happens
> before a gp, with some rscs in between, ...".
> So I think even the picture is not the best picture to draw for RCU
> ordering. I think the right picture to draw for RCU ordering is something
> like this:
>     case (1): C ends before G does:
>
> rcsc ... ... ... ... ... gp
>
> case (2): G ends before C does:
>
> gp ... ... ... ... ... rscs
>
> where the dots are some relation that means "happens before".

Okay. So we could define rcu-order by:

let rec rcu-order = (rcu-gp ; rcu-link ; (rcu-order ; rcu-link)* ; rcu-rscsi) |
(rcu-rscsi ; rcu-link ; (rcu-order ; rcu-link)* ; rcu-gp)

(ignoring the SRCU cases). That is a little awkward; it might make
sense to factor out (rcu-link ; (rcu-order ; rcu-link)*) as a separate
relation and do a simultaneous recursion on both relations.

But either way, rcu-fence would have to be defined as (po ; rcu-order+ ; po?),
which looks a little odd.

Alan