Re: [RFC] LKMM: Add volatile_if()

[Alan Stern]

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