Re: Internal vs. external barriers (was: Re: Interesting LKMM litmus test)
From: Jonas Oberhauser
Date: Mon Jan 23 2023 - 11:17:15 EST
On 1/19/2023 5:41 PM, Alan Stern wrote:
On Thu, Jan 19, 2023 at 12:22:50PM +0100, Jonas Oberhauser wrote:
I mean that if you have a cycle that is formed by having two adjacent actual
`gp` edges, like .... ; gp;gp ; .... with gp= po ; rcu-gp ; po?,
(not like your example, where the cycle uses two *rcu*-gp but no gp edges)
Don't forget that I had in mind a version of the model where rcu-gp did
not exist.
and assume we define gp' = po ; rcu-gp ; po and hb' and pb' to use gp'
instead of gp,
then there are two cases for how that cycle came to be, either 1) as
... ; hb;hb ; ....
but then you can refactor as
... ; po;rcu-gp;po;rcu-gp;po ; ...
... ; po;rcu-gp; po ; ...
... ; gp' ; ...
... ; hb' ; ...
which again creates a cycle, or 2) as
... ; pb ; hb ; ...
coming from
... ; prop ; gp ; gp ; ....
which you can similarly refactor as
... ; prop ; po;rcu-gp;po ; ....
... ; prop ; gp' ; ....
and again get a cycle with
... ; pb' ; ....
Therefore, gp = po;rcu-gp;po should be equivalent.
The point is that in P1, we have Write ->(gp;gp) Read, but we do not
have Write ->(gp';gp') Read. Only Write ->gp' Read. So if you're using
gp' instead of gp, you'll analyze the litmus test as if it had only one
grace period but two critical sections, getting a wrong answer.
Are you writing about the old model? Otherwise I don't see how this can
give a wrong answer.
gp' isn't used to count the grace periods (anymore?). the po<=rcu-link
allows using both grace periods to create rcu-order between the two read
side critical sections.
For the old model I believe it.
Here's a totally different way of thinking about these things, which may
prove enlightening. These thoughts originally occurred to me years ago,
and I had forgotten about them until last night.
If G is a grace period, let's write t1(G) for the time when G starts and
t2(G) for the time when G ends.
Likewise, if C is a read-side critical section, let's write t2(C) for
the time when C starts (or the lock executes if you prefer) and t1(C)
for the time when C ends (or the unlock executes). This terminology
reflects the "backward" role that critical sections play in the memory
model.
Now we can can characterize rcu-order and rcu-link in operational terms.
Let A and B each be either a grace period or a read-side critical
section. Then:
A ->rcu-order B means t1(A) < t2(B), and
A ->rcu-link B means t2(A) <= t1(B).
That's a really elegant notation! I have thought about rcu-link and
rcu-order as ordering ends or starts depending on which events are being
ordered, but it quickly got out of hand because of all the different
cases. With this notation it becomes quite trivial.
(Of course, we always have t1(X) < t2(X) for any grace period or
critical section X.)
This explains quite a lot. For example, we can justify including
C ->rcu-link G
into rcu-order as follows. From C ->rcu-link G we get that t2(C) <=
t1(G), in other words, C starts when or before G starts. Then the
Fundamental Law of RCU says that C must end before G ends, since
otherwise C would span all of G. Thus t1(C) < t2(G), which is C
->rcu-order G.
The case of G ->rcu-link C is similar.
This also explains why rcu-link can be extended by appending (rcu-order
; rcu-link)*.
Indeed, by similar (but more clumsy) reasoning I observed that rcu-order
can be thought of as "extending" rcu-link.
From X ->rcu-order Y ->rcu-link Z we get that t1(X) <
t2(Y) <= t1(Z) and thus t1(X) <= t1(Z). So if
A ->rcu-link B ->(rcu-order ; rcu-link)* C
then t2(A) <= t1(B) <= t1(C), which justifies A ->rcu-link C.
The same sort of argument shows that rcu-order should be extendable by
appending (rcu-link ; rcu-order)* -- but not (rcu-order ; rcu-link)*.
This also justifies why a lone gp belongs in rcu-order: G ->rcu-order G
holds because t1(G) < t2(G). But for critical sections we have t2(C) <
t1(C) and so C ->rcu-order C does not hold.
I don't think that it justifies why it belongs there. It justifies that
it could be included.
Neither rcu-order nor rcu-link exactly capture the temporal ordering,
they just imply it.
For example, if you have L1 U1 and L2 U2 forming two read side critical
sections C1 and C2, and
U1 ->(hb|pb)+ L2
then I would say you would have
t1(C1) < t2(C2)
but no rcu-order relation between any of the four events.
And for rcu-link this is even more obvious, because
(rcu-order;rcu-link)* does not currently actually extend rcu-link (but
it could based on the above reasoning).
In fact it seems we shouldn't even define a relation that is precisely
ordering t1(A) < t2(B) because that should be a total order on all grace
periods. As far as "observable" t1(A) < t2(B) is concerned, gp belongs
in that definition but I think it already is there through hb and/or pb.
Assuming ordinary memory accesses occur in a single instant, you see why
it makes sense to consider (po ; rcu-order ; po) an ordering.
Do you mean "execute" in a single instant?
But when you're comparing grace periods or critical sections to each other,
things get a little ambiguous. Should G1 be considered to come before
G2 when t1(G1) < t1(G2), when t2(G1) < t2(G2), or when t2(G1) < t1(G2)?
Springing for (po ; rcu-order ; po?) amounts to choosing the second
alternative.
Aha, I see! Powerful notation indeed.
Keeping that in mind, wouldn't it make sense for pb also be changed to
`...;po?` ?
Mathematically it ends up making no difference (so far), because any
cycle of
... ;(pb';po?); (rb | (pb';po?) | hb);...
(where pb' is pb but where things have been redefined so that the final
po is dropped)
can be trivially turned into a (pb | hb | rb) cycle except if it is
... ; pb' ; rcu-order ; po ; ...
But in this case we can use pb' <= prop ; po
... ; prop ; po ; rcu-order ; po ; ...
which is
... ; rb ; ...
and thus we get again a (pb | hb | rb) cycle.
But it would be more uniform and lets us define
xyz-order = po ; ... ; po?
pb = prop ; ...-order
rb = prop ; ...-order
Thanks for the insights,
jonas