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

On Tue, Jul 22, 2025 at 05:43:16PM -0700, Paul E. McKenney wrote:
> On Mon, Jan 06, 2025 at 10:40:03PM +0100, Jonas Oberhauser wrote:
> > The current LKMM allows out-of-thin-air (OOTA), as evidenced in the following
> > example shared on this list a few years ago:
> 
> Apologies for being slow, but I have finally added the litmus tests in
> this email thread to the https://github.com/paulmckrcu/litmus repo.
> 
> It is quite likely that I have incorrectly intuited the missing portions
> of the litmus tests, especially the two called out in the commit log
> below.  If you have time, please do double-check.

I didn't look very closely when this first came out...

> --- /dev/null
> +++ b/manual/oota/C-AS-OOTA-2.litmus
> @@ -0,0 +1,33 @@
> +C C-AS-OOTA-2
> +
> +(*
> + * Result: Always
> + *
> + * If we were using C-language relaxed atomics instead of volatiles,
> + * the compiler *could* eliminate the first WRITE_ONCE() in each process,
> + * then also each process's local variable, thus having an undefined value
> + * for each of those local variables.  But this cannot happen given that
> + * we are using Linux-kernel _ONCE() primitives.
> + *
> + * https://lore.kernel.org/all/[email protected]/
> + *)
> +
> +{}
> +
> +P0(int *a, int *b)
> +{
> +	int r0 = READ_ONCE(*a);
> +
> +	WRITE_ONCE(*b, r0);
> +	WRITE_ONCE(*b, 2);
> +}
> +
> +P1(int *a, int *b)
> +{
> +	int r1 = READ_ONCE(*b);
> +
> +	WRITE_ONCE(*a, r0);

This should be r1 instead of r0.

> +	WRITE_ONCE(*a, 2);
> +}
> +
> +exists ((0:r0=0 \/ 0:r0=2) /\ (1:r1=0 \/ 1:r1=2))

Alan