On Tue, Jan 15, 2019 at 10:19:10AM -0500, Alan Stern wrote:
> On Tue, 15 Jan 2019, Andrea Parri wrote:
>
> > Unless I'm mis-reading/-applying this definition, this will flag the
> > following test (a variation on your "race.litmus") with "data-race":
> >
> > C no-race
> >
> > {}
> >
> > P0(int *x, spinlock_t *s)
> > {
> > spin_lock(s);
> > WRITE_ONCE(*x, 1); /* A */
> > spin_unlock(s); /* B */
> > }
> >
> > P1(int *x, spinlock_t *s)
> > {
> > int r1;
> >
> > spin_lock(s); /* C */
> > r1 = *x; /* D */
> > spin_unlock(s);
> > }
> >
> > exists (1:r1=1)
> >
> > Broadly speaking, this is due to the fact that the modified "happens-
> > before" axiom does not forbid the execution with the (MP-) cycle
> >
> > A ->po-rel B ->rfe C ->acq-po D ->fre A
> >
> > and then to the link "D ->race-from-r A" here defined.
>
> Yes, that cycle certainly should be forbidden. On the other hand, we
> don't want to insist that C happens before D, given that D may not
> happen at all.
>
> This is a real problem. Can we solve it by adding a modified
> "happens-before" which says essentially that _if_ D is preserved _then_
> C happens before D? But then what about cycles involving more than one
> possibly preserved access? Or maybe a relation which says that D
> cannot execute before C (so if D executes at all, it has to come after
> C)?
The latter; there is a compiler barrier implied at the end of
spin_lock() such that anything later (in PO) must indeed be later.
> Now you see why this stuff is so difficult... At the moment, I don't
> know how to fix this.
