Re: [RFC] LKMM: Add volatile_if()

Alan Stern
2021-08-04T20:09:54Z

On Mon, Aug 02, 2021 at 04:31:56PM -0700, Paul E. McKenney wrote:
> o Section 2 I leave in Alan's capable hands.

Here goes, although I'm not sure how important this is, given that
section 2 is presented as merely a "straw man" argument for something
that ARM decided to abandon.

While reading this section (and the paper in general), it was annoying
that the terms "down-one-leg" and "down-two-legs" are never explained or
motivated. Even after reading section 2, I'm still not sure what they
are really intended to mean. My impression is that "down-one-leg" is an
attempt to express the idea that control dependencies apply to accesses
occurring along one leg of a conditional but not to accesses occurring
after the two legs have rejoined. Is that right?

P.17: "The drawback of this approach is that it would require order for
the “independent” case" -- this doesn't seem like a drawback to me.
Particularly since no existing architecture attempts to avoid ordering
the independent case.

Def. of "points of divergence": This is not very precise. What exactly
is a "branching decision"? Do the two paths of a CAS or CSEL
instruction count? What if the decision doesn't involve whether or not
to take the branch but rather where to branch to (as in a computed
branch or even just a call through a function pointer)?

Def. of "address dependency": How could there be a Dependency through
registers from D4 to R2? It's not at all easy to untangle the
definitions to see what this might mean. What would be an example? At
any rate, the case where RW2 is a Memory read doesn't seem right. It
says that:

R0 = Load
R1 = Load([R0])

is an address dependency but

R0 = Load
// Branching decision that depends on the value of R0 and
// carries a Dependency through registers to a new value for
// R0 (whatever that may mean) which is always equal to the
// existing value
R1 = Load([R0])

isn't. Is this really what you mean? If so, what is the motivation for
this definition? How does it relate to the discussion earlier in this
section?

Def. of antecedent: What is a Local read successor or an immediate Local
write successor? These terms aren't defined, and without knowing what
they mean it is impossible to understand what an antecedent is.

Def. of pre-equivalent effects and related terms: I don't understand how
you can have effects on different branches of a Point of divergence. By
definition, only one of the branches is executed -- how can there be any
effects on the speculated branch?

With all these concepts being so unclear, I was completely unable to
figure out what the definition of control dependency means. The text
doesn't help at all, because it doesn't contain any examples or
explanations to make these things more comprehensible.

The formalization in cat may have some historical interest, but it
conveys no information to a reader who isn't prepared to spend hours or
days trying to decipher it. Honestly, do you know _anybody_ who could
tell what Figures 22 - 25 mean and what they do just from reading them?
You pretty much have to be an expert in cat just to tell what some of
the recursive functions in Figs. 23 and 24 do.

(As just one very minor example, the "bisimulation" function in the
fourth-to-last line of Figure 25 isn't mentioned anywhere else. How are
people supposed to understand it?)

Alan