Hi Alan,
On Sat, Feb 11, 2023 at 9:59 PM Alan Stern <stern@xxxxxxxxxxxxxxxxxxx> wrote:
>
[...]
>
> Would you like to post a few examples showing some of the most difficult
> points you encountered? Maybe explanation.txt can be improved.
One additional feedback I wanted to mention, regarding this paragraph
under "WARNING":
===========
The protections provided by READ_ONCE(), WRITE_ONCE(), and others are
not perfect; and under some circumstances it is possible for the
compiler to undermine the memory model. Here is an example. Suppose
both branches of an "if" statement store the same value to the same
location:
r1 = READ_ONCE(x);
if (r1) {
WRITE_ONCE(y, 2);
... /* do something */
} else {
WRITE_ONCE(y, 2);
... /* do something else */
}
===========
I tried lots of different compilers with varying degrees of
optimization, in all cases I find that the conditional instruction
always appears in program order before the stores inside the body of
the conditional. So I am not sure if this is really a valid concern on
current compilers, if not - could you provide an example of a compiler
and options that cause it?
In any case, if it is a theoretical concern, it could be clarified
that this is a theoretical possibility in the text. And if it is a
real/practical concern, then it could be mentioned the specific
compiler/arch this was seen in.
Thanks!
- Joel
>
> > > I'm not sure that breaking this relation up into pieces will make it any
> > > easier to understand.
> >
> > Yes, but I tried. I will keep trying to understand your last patch
> > more. Especially I am still not sure, why in the case of an SRCU
> > reader on a single CPU, the following does not work:
> > let srcu-rscs = ([Srcu-lock]; data; [Srcu-unlock]).
>
> You have to understand that herd7 does not track dependencies through
> stores and subsequent loads. That is, if you have something like:
>
> r1 = READ_ONCE(*x);
> WRITE_ONCE(*y, r1);
> r2 = READ_ONCE(*y);
> WRITE_ONCE(*z, r2);
>
> then herd7 will realize that the write to y depends on the value read
> from x, and it will realize that the write to z depends on the value
> read from y. But it will not realize that the write to z depends on the
> value read from x; it loses track of that dependency because of the
> intervening store/load from y.
>
> More to the point, if you have:
>
> r1 = srcu_read_lock(lock);
> WRITE_ONCE(*y, r1);
> r2 = READ_ONCE(*y);
> srcu_read_unlock(lock, r2);
>
> then herd7 will not realize that the value of r2 depends on the value of
> r1. So there will be no data dependency from the srcu_read_lock() to
> the srcu_read_unlock().
>
> Alan
