Re: Current LKMM patch disposition

[Alan Stern]

On Sat, Feb 11, 2023 at 03:49:39PM +0000, Joel Fernandes wrote:
> Hi Alan, all,
> 
> One thing I noticed: Shouldn't the model have some notion of fences with the
> srcu lock primitive? SRCU implementation in the kernel does an unconditional
> memory barrier on srcu_read_lock() (which it has to do for a number of
> reasons including correctness), but currently both with/without this patch,
> the following returns "Sometimes", instead of "Never". Sorry if this was
> discussed before:
> 
> C MP+srcu
> 
> (*
>  * Result: Sometimes
>  *
>  * If an srcu_read_unlock() is called between 2 stores, they should propogate
>  * in order.
>  *)
> 
> {}
> 
> P0(struct srcu_struct *s, int *x, int *y)
> {
> 	int r1;
> 
> 	r1 = srcu_read_lock(s);
> 	WRITE_ONCE(*x, 1);
> 	srcu_read_unlock(s, r1); // replace with smp_mb() makes Never.
> 	WRITE_ONCE(*y, 1);
> }
> 
> P1(struct srcu_struct *s, int *x, int *y)
> {
> 	int r1;
> 	int r2;
> 
> 	r1 = READ_ONCE(*y);
> 	smp_rmb();
> 	r2 = READ_ONCE(*x);
> }
> 
> exists (1:r1=1 /\ 1:r2=0)

As far as I know, the SRCU API does not guarantee this behavior.  The 
current implementation behaves this way, but future implementations 
might not.  Therefore we don't want to put it in the memory model.

> Also, one more general (and likely silly) question about reflexive-transitive closures.
> 
> Say you have 2 relations, R1 and R2. Except that R2 is completely empty.
> 
> What does (R1; R2)* return?

It returns the identity relation, that is, a relation which links each 
event with itself.  Remember, R* is defined as linking A to B if there 
is a series of R links, of _any_ length (including 0!), going from A to 
B.  Since there is always a series of length 0 linking A to itself, R* 
always contains the identity relation.

> I expect (R1; R2) to be empty, since there does not exist a tail in R1, that
> is a head in R2.

Correct.  But for any relation R, R* always contains the identity 
relation -- even when R is empty.  R+, on the other hand, does not.  
That's the difference between R* and R+: In R* the series of links can 
be of any length, whereas in R+ there must be at least one link.

In your example, both R2+ and (R1 ; R2)+ would be empty.

> However, that does not appear to be true like in the carry-srcu-data relation
> in Alan's patch. For instance, if I have a simple litmus test with a single
> reader on a single CPU, and an updater on a second CPU, I see that
> carry-srcu-data is a bunch of self-loops on all individual loads and stores
> on all CPUs, including the loads and stores surrounding the updater's
> synchronize_srcu() call, far from being an empty relation!

Yep, that's the identity relation.

Alan