Re: [RFC] LKMM: Add volatile_if()

[Alan Stern <stern@rowland.harvard.edu>]

On Fri, Jul 30, 2021 at 06:20:22PM +0100, Jade Alglave wrote:
> I hope this material can help inform this conversation and I would love
> to hear your thoughts.

Thoughts on section 3...

The paragraph on Branching Effect is pretty meager.  Exactly what 
effects does a conditional branch instruction generate?  I imagine 
there's a register read of the flags register, to see whether the branch 
should be taken.  And evidently there's a branch effect, which may take 
the register read as input but doesn't have any obvious outputs.  
Anything else? -- there don't seem to be any register writes.

Why are Store Exclusive instructions explicitly disallowed in the 
definition of dependency through registers?  Is this because ARM CPUs 
don't forward values written by such instructions to po-later reads?  If 
so, why don't they?  (Paul asked a similar question.)

Since the recursive definition of dependency through registers starts 
with either a register write or intrinsic order of events in an 
instruction, it appears that there cannot be any dependency through 
registers starting from a branching effect.  So why does the definition 
of address dependency talk about a dependency through registers from B4 
(a branching effect) to R2?  (Paul also asked about this -- does writing 
to the program counter get treated as a register write?  But almost no 
instructions explicitly read from the program counter.)

What is the whole point of the special handling of branching effects in 
the definition of address dependencies?  It isn't obvious and the text 
doesn't explain it.

Figure 26 includes a lot of terms that seem like herd primitives.  They 
must be relatively new, because they aren't mentioned in the 
documentation that I've got.  (I'm referring to such terms as iico_data, 
iico_ctrl, intrinsic, same-instance, DATA, and NDATA.)  Are they 
explained anywhere?

Way back in Section 1, various Intrinsic dependency relations were 
introduced.  The reason for treating Intrinsic control dependencies 
specially seems to be that the CPU can speculate past such dependencies 
(though it would be nice if the text made this point explicitly).  But 
why do you differentiate between data and order Intrinsic dependencies?  
Is this also related to some specific behavior of ARM CPUs?

Alan