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

On 17.06.25 16:09, Andrea Parri wrote:
>> 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)

I support this endeavor, but from the Dartagnan side :).
We already support MSA in real C/Linux code and so extending our 
supported Litmus fragment to MSA does not sound too hard to me.
We are just missing a LKMM cat model that supports MSA.

We cannot automatically generate and run tests on real hardware though, 
so the support in herd7 and co. is definitely needed.


-- 
=====================================

Thomas Haas

Technische Universität Braunschweig
Institut für Theoretische Informatik
Mühlenpfordtstr. 23, Raum IZ 343
38106 Braunschweig | Germany

[email protected]
https://www.tu-braunschweig.de/tcs/team/thomas-haas