Re: [RFC] LKMM: Add volatile_if()

Alan Stern
2021-07-30T20:35:45Z

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