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
