On Thu, 17 Jan 2019, Andrea Parri wrote:
> > > There is a special case (data;rfi) that doesn't
> > > provide ordering in itself but can contribute to other
> > > orderings. A data;rfi link corresponds to situations
> > > where a value is stored in a temporary shared variable
> > > and then loaded back again. Since the compiler might
> > > choose to eliminate the temporary, its accesses can't
> > > be said to be ordered -- but the accesses around it
> > > might be. As a simple example, consider:
> > >
> > > r1 = READ_ONCE(ptr);
> > > tmp = r1;
> > > r2 = tmp;
> > > WRITE_ONCE(*r2, 5);
> > >
> > > The plain accesses involving tmp don't have any
> > > particular ordering requirements, but we do know that
> > > the READ_ONCE must be ordered before the WRITE_ONCE.
> > > The chain of relations is:
> > >
> > > [marked] ; data ; rfi ; addr ; [marked]
> > >
> > > showing that a data;rfi has been inserted into an
> > > address dependency from a marked read to a marked
> > > write. In general, any number of data;rfi links can
> > > be inserted in each of the other kinds of dependencies.
>
> As a more general comment (disclaimer), I'm not sure we want to/can add
> all the constraints above. On one hand, for some of them, I ignore the
> existence of current use cases in the source (and I don't quite see my-
> self encouraging their adoption...); on the other hand, these certainly
> do not make the model "simpler" or easier to maintain (in a sound way).
>
> Moreover, I doubt that runtime checkers a la KTSan will ever be able to
> assist the developer by supporting these "dependency orderings". [1]
>
> Maybe we could start by adding those orderings that we know are "widely"
> relied upon _and_ used by the developers, and later add more/strengthen
> the model as needed (where feasible).
>
> Thoughts?
Right now I'm inclined to give up on all dependency orderings other
than address dependency from a marked read. But this would mean
missing things like
MR ->addr PR ->data MW
which ought to be a valid ordering (MR stands for "marked read", "PR"
for "plain read", and "MW" for "marked write"). Is that going to be
okay? Or should I also include data and control dependencies from
plain reads to marked writes?
Also, should this still include "[marked] ; (data ; rfi)* ; addr"?
Without it, we wouldn't be able to tell that the following test does
not race:
C non-race4
{
int *x = a;
}
P0(int **x, int *b)
{
*b = 1;
smp_wmb();
rcu_assign_pointer(*x, b);
}
P1(int **x, int **tmp)
{
int *r1;
int *r2;
int r3;
r1 = rcu_dereference(*x);
tmp = r1;
r2 = tmp;
r3 = *r2;
}
exists (1:r1=b /\ 1:r3=0)
And it seems reasonable that this pattern could be used in the kernel.
Although, I admit, in this scenario it's much more likely that tmp
would be a non-shared variable.
Alan
