Messages in this thread | | | Date | Wed, 16 Jan 2019 12:57:52 +0100 | From | Peter Zijlstra <> | Subject | Re: Plain accesses and data races in the Linux Kernel Memory Model |
| |
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.
| |