Messages in this thread | | | Date | Wed, 18 Jan 2023 21:28:28 -0500 | From | Alan Stern <> | Subject | Re: Internal vs. external barriers (was: Re: Interesting LKMM litmus test) |
| |
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
| |