On Wed, 11 Jul 2018, Andrea Parri wrote: > > > Does something like "po; [UL]; rf; [LKR]; po" fit in with the rest > > > of the model? If so, maybe that solves the asymmetry and also > > > legalizes the approach of putting fence.tso in front? > > > > That would work just as well. For this version of the patch it > > doesn't make any difference, because nothing that comes po-after the > > LKR is able to directly read the value stored by the UL. > > Consider: > > C v2-versus-v3 > > {} > > P0(spinlock_t *s, int *x) > { > spin_lock(s); /* A */ > spin_unlock(s); > spin_lock(s); > WRITE_ONCE(*x, 1); /* B */ > spin_unlock(s); > } > > P1(spinlock_t *s, int *x) > { > int r0; > int r1; > > r0 = READ_ONCE(*x); /* C */ > smp_rmb(); > r1 = spin_is_locked(s); /* D */ > } > > With v3, it's allowed that C reads from B and D reads from (the LKW of) A; > this is not allowed with v2 (unless I mis-applied/mis-read v2).
Correct. But it doesn't affect the end result, because both versions allow C to read from B while D reads from the second spin_lock(), and there's no way to distinguish that from the case where D reads from A. If we were talking about arbitrary integers and rmw-acquire updates, there _would_ be a difference. But not with spinlocks. Alan