Re: [RFC] LKMM: Add volatile_if()

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