On Mon, Jan 23, 2023 at 08:33:42PM +0100, Jonas Oberhauser wrote:
And yet you complained about the reasoning needed to understand that
On 1/23/2023 6:28 PM, Alan Stern wrote:
I suppose it's true that Y being a load would be an exception, but that
I guess one would have to put
(cumul-fence+ ; [W])?
or something like it in the definition.
would only be if the cumul-fence+ sequence either ends in a strong-fence, or
in po-unlock-lock-po.
We can ignore the first case (and the ordering would be provided anyways
through pb at that point).
For the po-unlock-lock-po, you can just take Y:=the LKW event of the unlock
and repeat the argument.
(pb ; hb) <= pb!
Not to mention the brittleness of this argument; what
if in the future cumul-fence gets another term ending in a load?
Let's at this point in time not get started on the overwrite part being optional :D (see, this is me successfully holding myself back from opening another discussion! I can do it!).So I don't think the [W] is necessary. (and if it was maybe it would also beWell, consider that maybe they aren't the same. :-)
necessary in the definition of prop/cumul-fence itself, to account for all
the non-A-cumulative fences in there).
I think part of my weird feeling comes from this asymmetry between A-cumul()
putting the rfe? to the left and prop putting the rfe? to the right. Or more
precisely, that the latter is sometimes in anticipation of an A-cumulative
fence (where the A-cumul would normally take it to the left of that fence)
and sometimes just to express the idea of propagation, and that these are
the same, which should somehow lead to a simpler definition but doesn't.
The definition of prop is a little more complicated than one might
expect, because the overwrite and cumul-fence parts are both optional.
Leaving one or both of them out is valid, but it requires a little extra
thought to see why.
Sorry, I meant the prop-related non-ppo parts of hb and pb.Surely not, since prop doesn't usually provide ordering by itself.I'm not against this partially overlapping kind of redundancy, but I dislikeConsider: Could we remove all propagation-ordering fences from ppo
subsuming kind of redundancy where some branches of the logic just never
need to be used.
because they are subsumed by prop? (Or is that just wrong?)
Ok, but why not just use (pb|hb)* and (pb|hb|rb)* and not worry about having to explain anything?This can be mentioned explicitly as a comment or in explanation.txt.I think that's an improvement. It's obvious that (hb | pb)* is right and soI'm not so sure that's a good idea. For instance, it would require theIn fact, I wouldn't mind removing the happens-before, propagation, andI was planning to propose the same thing, however, I would also propose to
rcu axioms from LKMM entirely, replacing them with the single
executes-before axiom.
redefine hb and rb by dropping the hb/pb parts at the end of these
relations.
hb = ....
pb = prop ; strong-fence ; [Marked]
rb = prop ; rcu-fence ; [Marked]
xb = hb|pb|rb
acyclic xb
definitions of rcu-link and rb to be changed from having (hb* ; pb*) to
having (hb | pb)*.
is (pb | hb)*.
For (hb* ; pb*), the first reaction is "why do all the hb edges need to be
before the pb edges?", until one realizes that pb actually allows hb* at the
end, so in a sense this is hb* ; (pb ; hb*)*, and then one has to
understand that this means that the prop;strong-fence edges can appear any
number of times at arbitrary locations. It just seems like defining (pb |
hb)* with extra steps.
Note that in that alternative universe,The order of nesting seems to be also somewhat a matter of preference,You can't define hb that way, because the definition of hb appears
perhaps in some weird alternative universe the LKMM says pb = (prop\id)&int
| prop;strong-fence and hb = (rfe | ppo);pb*. (Personally I think the
current way is more reasonable than this one, but that might be because our
preferences happen to align in this instance.)
before the definition of pb. And it has to be this way, because hb is
used in the definition of pb.