Messages in this thread | | | Date | Fri, 18 Jan 2019 10:10:22 -0500 (EST) | From | Alan Stern <> | Subject | Re: Plain accesses and data races in the Linux Kernel Memory Model |
| |
On Thu, 17 Jan 2019, Andrea Parri wrote:
> > Can the compiler (maybe, it does?) transform, at the C or at the "asm" > > level, LB1's P0 in LB2's P0 (LB1 and LB2 are reported below)? > > > > C LB1 > > > > { > > int *x = &a; > > } > > > > P0(int **x, int *y) > > { > > int *r0; > > > > r0 = rcu_dereference(*x); > > *r0 = 0; > > smp_wmb(); > > WRITE_ONCE(*y, 1); > > } > > > > P1(int **x, int *y, int *b) > > { > > int r0; > > > > r0 = READ_ONCE(*y); > > rcu_assign_pointer(*x, b); > > } > > > > exists (0:r0=b /\ 1:r0=1) > > > > > > C LB2 > > > > { > > int *x = &a; > > } > > > > P0(int **x, int *y) > > { > > int *r0; > > > > r0 = rcu_dereference(*x); > > if (*r0) > > *r0 = 0; > > smp_wmb(); > > WRITE_ONCE(*y, 1); > > } > > > > P1(int **x, int *y, int *b) > > { > > int r0; > > > > r0 = READ_ONCE(*y); > > rcu_assign_pointer(*x, b); > > } > > > > exists (0:r0=b /\ 1:r0=1) > > > > LB1 and LB2 are data-race free, according to the patch; LB1's "exists" > > clause is not satisfiable, while LB2's "exists" clause is satisfiable.
A relatively simple solution to this problem would be to say that smp_wmb doesn't order plain writes.
I think the rest of the memory model would then be okay. However, I am open to arguments that this approach is too complex and we should insist on the same kind of strict ordering for race avoidance that the C11 standard uses (i.e., conflicting accesses separated by full memory barriers or release & acquire barriers or locking).
Alan
| |