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

lists.openwall.net		lists / announce owl-users owl-dev john-users john-dev passwdqc-users yescrypt popa3d-users / oss-security kernel-hardening musl sabotage tlsify passwords / crypt-dev xvendor / Bugtraq Full-Disclosure linux-kernel linux-netdev linux-ext4 linux-hardening linux-cve-announce PHC
Open Source and information security mailing list archives

Hash Suite: Windows password security audit tool. GUI, reports in PDF.

[<prev] [next>] [<thread-prev] [thread-next>] [day] [month] [year] [list]

Message-ID: <595209ed-2074-46da-8f57-be276c2e383b@tu-bs.de>
Date: Thu, 19 Jun 2025 16:27:56 +0200
From: Thomas Haas <t.haas@...bs.de>
To: Andrea Parri <parri.andrea@...il.com>, Alan Stern
	<stern@...land.harvard.edu>
CC: Peter Zijlstra <peterz@...radead.org>, Will Deacon <will@...nel.org>,
	Boqun Feng <boqun.feng@...il.com>, Nicholas Piggin <npiggin@...il.com>, David
 Howells <dhowells@...hat.com>, Jade Alglave <j.alglave@....ac.uk>, Luc
 Maranget <luc.maranget@...ia.fr>, "Paul E. McKenney" <paulmck@...nel.org>,
	Akira Yokosawa <akiyks@...il.com>, Daniel Lustig <dlustig@...dia.com>, Joel
 Fernandes <joelagnelf@...dia.com>, <linux-kernel@...r.kernel.org>,
	<linux-arch@...r.kernel.org>, <lkmm@...ts.linux.dev>,
	<hernan.poncedeleon@...weicloud.com>, <jonas.oberhauser@...weicloud.com>,
	"r.maseli@...bs.de" <r.maseli@...bs.de>
Subject: 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

t.haas@...braunschweig.de
https://www.tu-braunschweig.de/tcs/team/thomas-haas