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
