On Tue, Jul 16, 2019 at 02:53:09PM +0200, Andrea Parri wrote: > C daniel-padata > > { } > > P0(atomic_t *reorder_objects, spinlock_t *pd_lock) > { > int r0; > > spin_lock(pd_lock); > spin_unlock(pd_lock); > smp_mb(); > r0 = atomic_read(reorder_objects); > } > > P1(atomic_t *reorder_objects, spinlock_t *pd_lock, spinlock_t *reorder_lock) > { > int r1; > > spin_lock(reorder_lock); > atomic_inc(reorder_objects); > spin_unlock(reorder_lock); > //smp_mb(); > r1 = spin_trylock(pd_lock); > } > > exists (0:r0=0 /\ 1:r1=0) > > It seems worth noticing that this test's "exists" clause is satisfiable > according to the (current) memory consistency model. (Informally, this > can be explained by noticing that the RELEASE from the spin_unlock() in > P1 does not provide any order between the atomic increment and the read > part of the spin_trylock() operation.) FWIW, uncommenting the smp_mb() > in P1 would suffice to prevent this clause from being satisfiable; I am > not sure, however, whether this approach is feasible or ideal... (sorry, > I'm definitely not too familiar with this code... ;/) Urgh, that one again. Yes, you need the smp_mb(); although a whole bunch of architectures can live without it. IIRC it is part of the eternal RCsc/RCpc debate. Paul/RCU have their smp_mb__after_unlock_lock() that is about something similar, although we've so far confinsed that to the RCU code, because of how confusing that all is.