RE: [PATCH] tools: memory-model: Add rmw-sequences to the LKMM

[Jonas Oberhauser <jonas.oberhauser@huawei.com>]

	
> -----Original Message-----
> From: Alan Stern [mailto:stern@rowland.harvard.edu] 
> Sent: Monday, November 14, 2022 6:26 PM

Hi Alan,
thanks for preparing this!

> Jonas has pointed out a weakness in the Linux Kernel Memory Model.
> Namely, the memory ordering properties of atomic operations are not
> monotonic: An atomic op with full-barrier semantics does not always provide ordering as strong as one with release-barrier semantics.

Note that I believe it was Viktor who originally pointed out this weakness to me
in private communication. My contribution (besides chatting with you) is to
check that the solution does indeed restore the monotonicity (not just on some
litmus tests but in general).

So I would change the wording to "Viktor has pointed out a weakness in the Linux
Kernel Memory Model."


> +let rmw-sequence = (rf ; rmw)*

I would perhaps suggest to only consider external read-from in rmw-sequences, as
below:
+let rmw-sequence = (rfe ; rmw)*

The reason I (slightly) prefer this is that this is sufficient to imply
monotonicity.
Also there is some minor concern that the patch that results in the stricter
model (i.e., rmw-sequence = (rf ; rmw)*) might be incorrect on some hypothetical
future architecture in which RMWs can be merged in the store coalescing queue
with earlier stores to the same location. This is exemplified in the following
litmus test:

C atomics-not-monotonic-2

{}

P0(int *x, atomic_t *y)
{
    int r1;
	WRITE_ONCE(*x, 1);
	smp_store_release(y, 0);
	r1 = atomic_inc_return_relaxed(y);
}

P1(atomic_t *y)
{
	int r1;

	r1 = atomic_inc_return(y);
}

P2(int *x, atomic_t *y)
{
	int r2;
	int r3;

	r2 = atomic_read(y);
	smp_rmb();
	r3 = READ_ONCE(*x);
}

exists (2:r2=2 /\ 2:r3=0)

Here such a hypothetical future architecture could merge the operations to *y by
P0 into a single store, effectively turning the code of P0 into

P0(int *x, atomic_t *y)
{
    int r1;
	WRITE_ONCE(*x, 1);
	WRITE_ONCE(*y, 1);
	r1 = 0;
}

The stricter patch would not be sound with this hypothetical architecture, while
the more relaxed patch should be.

I don't think such a future architecture is likely since I don't expect there to
be any practical performance impact. At the same time I also don't currently see
any advantage of the stricter model.

For this reason I would slightly prefer the more relaxed model.



> +Rmw sequences have a special property in the LKMM: They can extend the 
> +cumul-fence relation.  That is, if we have:
> +
> +	U ->cumul-fence X -> rmw-sequence Y
> +
> +then also U ->cumul-fence Y.  Thinking about this in terms of the 
> +operational model, U ->cumul-fence X says that the store U propagates 
> +to each CPU before the store X does.  Then the fact that X and Y are 
> +linked by an rmw sequence means that U also propagates to each CPU 
> +before Y does.
> +

Here I would add that the rmw sequences also play a similar role in the
w-post-bounded relation. For example as follows:

+Rmw sequences have a special property in the LKMM: They can extend the 
+cumul-fence and w-post-bounded relations.  That is, if we have:
+
+	U ->cumul-fence X -> rmw-sequence Y
+
+then also U ->cumul-fence Y, and analogously if we have
+
+	U ->w-post-bounded X -> rmw-sequence Y
+
+then also U ->w-post-bounded Y. Thinking about this in terms of the 
+operational model, U ->cumul-fence X says that the store U propagates 
+to each CPU before the store X does.  Then the fact that X and Y are 
+linked by an rmw sequence means that U also propagates to each CPU 
+before Y does.
+


Best wishes,
jonas