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: <a0887a91-468c-43ff-872e-c4c4e23b26dd@rowland.harvard.edu>
Date: Thu, 19 Jun 2025 13:56:58 -0400
From: Alan Stern <stern@...land.harvard.edu>
To: Thomas Haas <t.haas@...bs.de>
Cc: Andrea Parri <parri.andrea@...il.com>,
	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 Thu, Jun 19, 2025 at 04:59:38PM +0200, Thomas Haas wrote:
> 
> 
> On 19.06.25 16:32, Alan Stern wrote:
> > On Thu, Jun 19, 2025 at 04:27:56PM +0200, Thomas Haas wrote:
> > > 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.
> > 
> > To me, it doesn't feel all that easy.  I'm not even sure where to start
> > changing the LKMM.\
> > 
> > Probably the best way to keep things organized would be to begin with
> > changes to the informal operational model and then figure out how to
> > formalize them.  But what changes are needed to the operational model?
> > 
> > Alan
> 
> Of course, the difficult part is to get the model right. Maybe I shouldn't
> have said that we are "just" missing the model :).
> I'm only saying that we already have some tooling to validate changes to the
> formal model.
> 
> I think it makes sense to first play around with the tooling and changes to
> the formal model to just get a feeling of what can go wrong and what needs
> to go right. Then it might become more clear on how the informal operational
> model needs to change.
> 
> A good starting point might be to lift the existing ARM8 MSA litmus tests to
> corresponding C/LKMM litmus tests and go from there.
> If the informal operational model fails to explain them, then it needs to
> change. This goes only one way though: if ARM permits a behavior then so
> should LKMM. If ARM does not, then it is not so clear if LKMM should or not.

Okay, that seems reasonable.

BTW, I don't want to disagree with what you wrote ... but doesn't your 
last paragraph contradict the paragraph before it?  Is starting with the 
various MSA litmus tests and seeing how the operational model fails to 
explain them not the opposite of first playing around with the tooling 
and changes to the formal model?

Alan