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)?
Now you see why this stuff is so difficult... At the moment, I don't
know how to fix this.
> (In part., similar considerations hold for the following litmus test:
>
> C MP1
>
> {}
>
> P0(int *x, int *y)
> {
> *x = 1;
> smp_store_release(y, 1);
> }
>
> P1(int *x, int *y)
> {
> int r0;
> int r1 = -1;
>
> r0 = smp_load_acquire(y);
> if (r0)
> r1 = *x;
> }
>
> exists (1:r0=1 /\ 1:r1=0)
>
> )
>
> I wonder whether you actually intended to introduce these "races"...?
No, I did not.
Alan
