Re: [RFC] LKMM: Add volatile_if()

Alan Stern
2021-08-05T19:47:53Z

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