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

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

> My question is: Do we have enough general knowledge at this point about 
> how the various types of hardware handle mixed-size accesses to come up 
> with a memory model everyone can agree one?

You know, I can imagine a conversation along the following line if I
were to turn this question to certain "hardware people":

  [Me/LKMM] People, how do you order such and those MSAs?
   [RTL/DV] What are Linux's uses and requirements?

that is to say that the work mentioned is probably more "interactive"
and more dynamic than how your question may suggest.  ;)

Said this, I do like to think that we (LKMM supporters and followers)
have enough knowledge to approach that effort.  It would require some
changes to herd7 (and klitmus7), starting from teaching the tools the
new MSAs syntax and how to generate rf, co and other basic relations
(while monitoring potential non-MSA regressions).  Non-trivial maybe,
but seems doable.  Suffice it to say that herd7 can't currently parse
the following C test, but it can run its "lowerings"/assembly against
a bunch of hardware models and implementations, including arm64, x86,
powerpc and riscv!  Any volunteers with ocaml expertise interested in
contributing to the LKMM?  ;)

C C-thomas-haas

{
u32 x;
u16 *x_lh = x; // herd7 dialect for "... = &x;"
}

P0(u32 *x)
{
	WRITE_ONCE(*x, 0x10001);
}

P1(u16 **x_lh, u32 *x)
{
	u16 r0;
	u32 r1;

	r0 = xchg_relaxed(*x_lh, 0x2);
	r1 = smp_load_acquire(x);
}

exists (1:r0=0x1 /\ 1:r1=0x2)