Re: [RFC] LKMM: Add volatile_if()

Alan Stern
2021-08-07T00:51:35Z

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 4...

The definition of Pick Basic dependency is phrased incorrectly. The
"all of the following apply" in the first paragraph refers only to first
bullet point, which in turn refers to the following two bullet points.
The "all of the following apply" phrase should be removed and the first
bullet point should be merged into the main text.

The definition of Pick dependency is redundant, because each Pick
Address and Pick Data dependency is itself already a Pick Basic
dependency. The same is true of the cat formalization.

In the cat code, the definition of Reg looks wrong. It is:

let Reg=~M | ~BR

Since (I presume) no event falls into both the M and BR classes, this
definition includes all events. It probably should be:

let Reg=~(M | BR)

or

let Reg=~M & ~BR

It's now clear that my original understanding of the underlying basis of
Intrinsic control dependencies was wrong. They aren't separated out
because CPUs can speculate through conditional branches; rather they are
separated out because they are the things which give rise to Pick
dependencies. It would have been nice if the text had explained this at
the start instead of leaving it up to me to figure out for myself.

Alan