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

[Hernan Luis Ponce de Leon <hernanl.leon@huawei.com>]

What they mean seems to be that a prop relation followed only by wmb (not mb) doesn't enforce the order of some writes to the same location, leading to the claimed hang in qspinlock (at least as far as LKMM is concerned). 

What we mean is that wmb does not give the same propagation properties as mb.
The claim is based on these relations from the memory model

let strong-fence = mb | gp
...
let cumul-fence = [Marked] ; (A-cumul(strong-fence | po-rel) | wmb |
	po-unlock-lock-po) ; [Marked]
let prop = [Marked] ; (overwrite & ext)? ; cumul-fence* ;
	[Marked] ; rfe? ; [Marked]

From an engineering perspective, I think the only issue is that cat *currently* does not have any syntax for this, nor does herd currently implement the await model checking techniques proposed in those works (c.f. Theorem 5.3. in the "making weak memory models fair" paper, which says that for this kind of loop, iff the mo-maximal reads in some graph are read in a loop iteration that does not exit the loop, the loop can run forever). However GenMC and I believe also Dat3M and recently also Nidhugg support such techniques. It may not even be too much effort to implement something like this in herd if desired.

The Dartagnan model checker uses the Theorem 5.3 from above to detect liveness violations.

We did not try to come up with a litmus test about the behavior because herd7 cannot reason about liveness.
However, if anybody is interested, the violating execution is shown here
	https://github.com/huawei-drc/cna-verification/blob/master/verification-output/BUG1.png

Hernan