Re: [RFC] tools/memory-model: Rule out OOTA

On Thu, Jan 09, 2025 at 09:54:28AM -0800, Paul E. McKenney wrote:
> > P0(int *a, int *b, int *x, int *y) {
> > 	int r1;
> > 	int r2 = 0;
> > 	r1 = READ_ONCE(*x);
> > 	smp_rmb();
> > 	if (r1 == 1) {
> > 		r2 = *b;
> > 	}
> > 	WRITE_ONCE(*a, r2);
> > 	smp_wmb();
> > 	WRITE_ONCE(*y, 1);
> > }
> > 
> > P1(int *a, int *b, int *x, int *y) {
> > 	int r1;
> > 
> > 	int r2 = 0;
> > 
> > 	r1 = READ_ONCE(*y);
> > 	smp_rmb();
> > 	if (r1 == 1) {
> > 		r2 = *a;
> > 	}
> > 	WRITE_ONCE(*b, r2);
> > 	smp_wmb();
> > 	WRITE_ONCE(*x, 1);
> > }
> > 
> > 
> > The reason that the WRITE_ONCE helps in the speculative store case is that
> > both its ctrl dependency and the wmb provide ordering, which together
> > creates ordering between *x and *y.
> 
> Ah, and that is because LKMM does not enforce control dependencies past
> the end of the "if" statement.  Cute!

I think the reason we hesitated on that was CMOV and similar conditional
instructions. If the body of the branch is a CMOV, then there no
conditionality on the common path after the body.