Re: [RFC] Potential problem in qspinlock due to mixed-size accesses

[Andrea Parri]

> ARM has recently fixed the issue on their side by strengthening the memory
> model (see https://github.com/herd/herdtools7/commit/2b7921a44a61766e23a1234767d28af696b436a0)
> 
> With the updated ARM-MSA model, Dartagnan does no longer find violations in
> qspinlock. No patches needed :)

Thanks for the heads-up, Thomas.

This reminds me:  After your post, I wrote some script/files to test MSA
against the LKMM by leveraging the MSA support for AArch64 available in
herd7 and requiring no changes to herd7 internals.  I've put these files
in the repository:

  https://github.com/andrea-parri/lkmm-msa.git

in case someone here feels particularly bored during the Christmas holi-
days and desire to have a look!  ;-)

I am hoping to be able to resume this study (and to write a proper README)
soonish - but the starting point was to "lift" ARMv8 execution graphs to
(corresponding) LKMM graphs, cf. the file cats/lkmm-from-armv8.cat; then
the usual "test, model and iterate" process, with unmarked accesses still
needing several iterations I'm afraid.  Any feedback's welcome.

  Andrea