Re: "Verifying and Optimizing Compact NUMA-Aware Locks on Weak Memory Models"

[Andrea Parri <parri.andrea@gmail.com>]

> Here is a litmus test showing the problem (I hope the comment are enough to relate it back to qspinlock)
> 
> C Liveness
> {
>   atomic_t x = ATOMIC_INIT(0);
>   atomic_t y = ATOMIC_INIT(0);
> }
> 
> P0(atomic_t *x) {
>   // clear_pending_set_locked
>   int r0 = atomic_fetch_add(2,x) ;
> }
> 
> P1(atomic_t *x, int *z) {
>   // queued_spin_trylock
>   int r0 = atomic_read(x);
>   // barrier after the initialization of nodes
>   smp_wmb();
>   // xchg_tail
>   int r1 = atomic_cmpxchg_relaxed(x,r0,42);
>   // link node into the waitqueue
>   WRITE_ONCE(*z, 1);
> }
> 
> P2(atomic_t *x,atomic_t *z) {
>   // node initialization
>   WRITE_ONCE(*z, 2);
>   // queued_spin_trylock
>   int r0 = atomic_read(x);
>   // barrier after the initialization of nodes
>   smp_wmb();
>   // xchg_tail
>   int r1 = atomic_cmpxchg_relaxed(x,r0,24);
> }
> 
> exists (0:r0 = 24 /\ 1:r0 = 26 /\ z=2)
> 
> herd7 says that the behavior is observable. 
> However if you change wmb by mb, it is not observable anymore.

Indeed.  For more context, this is a 3-threads extension of the 2+2W
test/behavior, cf.

  https://github.com/paulmckrcu/litmus/blob/master/manual/lwn573436/C-2+2w+o-wb-o+o-wb-o.litmus

which is also allowed by the LKMM.  The basic rationale for allowing
such behaviors was that we "don't think we need to care" (cf. the
comment in the link above), except that it seems the developers of the
code at stake disagreed.  ;-)  So this does look like a good time to
review that design choice/code.

  Andrea