On Fri, Jul 30, 2021 at 06:20:22PM +0100, Jade Alglave wrote: > Dear all, > Sincere apologies in taking so long to reply. I attach a technical > report which describes the status of dependencies in the Arm memory > model. > > I have also released the corresponding cat files and a collection of > interesting litmus tests over here: > https://github.com/herd/herdtools7/commit/f80bd7c2e49d7d3adad22afc62ff4768d65bf830 > > I hope this material can help inform this conversation and I would love > to hear your thoughts. Jade: Here are a few very preliminary reactions (I haven't finished reading the entire paper yet). P.2: Typo: "the register X1 contains the address x" should be "the register X1 contains the address of x". P.4 and later: Several complicated instructions (including CSEL, CAS, and SWP) are mentioned but not explained; the text assumes that the reader already understands what these instructions do. A brief description of their effects would help readers like me who aren't very familiar with the ARM instruction set. P.4: The text describing Instrinsic dependencies in CSEL instructions says that if cond is true then there is an Intrinsic control dependencies from the read of PSTATE.NZCV to the read of Xm. Why is this so? Can't the CPU read Xm unconditionally before it knows whether the value will be used? P.17: The definition of "Dependency through registers" uses the acronym "PE", but the acronym isn't defined anywhere. P.14: In the description of Figure 18, I wasn't previously aware -- although perhaps I should have been -- that ARM could speculatively place a Store in a local store buffer, allowing it to be forwarded to a po-later Read. Why doesn't the same mechanism apply to Figure 20, allowing the Store in D to be speculatively placed in a local store buffer and forwarded to E? Is this because conditional branches are predicted but loads aren't? If so, that is a significant difference. More to come... Alan
