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
