From: Thomas Haas <t.haas@tu-bs.de>
To: Will Deacon <will@kernel.org>,
Hernan Ponce de Leon <hernan.poncedeleon@huaweicloud.com>
Cc: Peter Zijlstra <peterz@infradead.org>,
Alan Stern <stern@rowland.harvard.edu>,
Andrea Parri <parri.andrea@gmail.com>,
Boqun Feng <boqun.feng@gmail.com>,
Nicholas Piggin <npiggin@gmail.com>,
David Howells <dhowells@redhat.com>,
Jade Alglave <j.alglave@ucl.ac.uk>,
Luc Maranget <luc.maranget@inria.fr>,
"Paul E. McKenney" <paulmck@kernel.org>,
Akira Yokosawa <akiyks@gmail.com>,
Daniel Lustig <dlustig@nvidia.com>,
Joel Fernandes <joelagnelf@nvidia.com>,
<linux-kernel@vger.kernel.org>, <linux-arch@vger.kernel.org>,
<lkmm@lists.linux.dev>, <jonas.oberhauser@huaweicloud.com>,
"r.maseli@tu-bs.de" <r.maseli@tu-bs.de>
Subject: Re: [RFC] Potential problem in qspinlock due to mixed-size accesses
Date: Tue, 17 Jun 2025 16:23:11 +0200 [thread overview]
Message-ID: <7a20b873-3c26-4a52-b118-c816ede7298d@tu-bs.de> (raw)
In-Reply-To: <20250617141704.GB19021@willie-the-truck>
On 17.06.25 16:17, Will Deacon wrote:
> On Tue, Jun 17, 2025 at 10:42:04AM +0200, Hernan Ponce de Leon wrote:
>> On 6/17/2025 8:19 AM, Thomas Haas wrote:
>>> On 16.06.25 16:23, Will Deacon wrote:
>>>> I'm half inclined to think that the Arm memory model should be tightened
>>>> here; I can raise that with Arm and see what they say.
>>>>
>>>> Although the cited paper does give examples of store-forwarding from a
>>>> narrow store to a wider load, the case in qspinlock is further
>>>> constrained by having the store come from an atomic rmw and the load
>>>> having acquire semantics. Setting aside the MSA part, that specific case
>>>> _is_ ordered in the Arm memory model (and C++ release sequences rely on
>>>> it iirc), so it's fair to say that Arm CPUs don't permit forwarding from
>>>> an atomic rmw to an acquire load.
>>>>
>>>> Given that, I don't see how this is going to occur in practice.
>>>
>>> You are probably right. The ARM model's atomic-ordered-before relation
>>>
>>> let aob = rmw | [range(rmw)]; lrs; [A | Q]
>>>
>>> clearly orders the rmw-store with subsequent acquire loads (lrs = local-
>>> read-successor, A = acquire).
>>> If we treat this relation (at least the second part) as a "global
>>> ordering" and extend it by "si" (same-instruction), then the problematic
>>> reordering under MSA should be gone.
>>> I quickly ran Dartagnan on the MSA litmus tests with this change to the
>>> ARM model and all the tests still pass.
>>
>> Even with this change I still get violations (both safety and termination)
>> for qspinlock with dartagnan.
>
> Please can you be more specific about the problems you see?
I talked to Hernán personally and it turned out that he used the generic
implementation of smp_cond_acquire (not sure if the name is correct)
which uses a relaxed load followed by a barrier. In that case, replacing
aob by aob;si does not change anything.
Indeed, even in the reported problem we used the generic implementation
(I was unaware of this), though it is easy to check that changing the
relaxed load to acquire does not give sufficient orderings.
>
>> I think the problem is actually with the Internal visibility axiom, because
>> only making that one stronger seems to remove the violations.
>
> That sounds surprising to me, as there's nothing particularly weird about
> Arm's coherence requirements when compared to other architectures, as far
> as I'm aware.
>
I agree. The internal visibility axiom is not the issue I think.
--
=====================================
Thomas Haas
Technische Universität Braunschweig
Institut für Theoretische Informatik
Mühlenpfordtstr. 23, Raum IZ 343
38106 Braunschweig | Germany
t.haas@tu-braunschweig.de
https://www.tu-braunschweig.de/tcs/team/thomas-haas
next prev parent reply other threads:[~2025-06-17 14:31 UTC|newest]
Thread overview: 23+ messages / expand[flat|nested] mbox.gz Atom feed top
2025-06-12 14:55 [RFC] Potential problem in qspinlock due to mixed-size accesses Thomas Haas
2025-06-13 7:55 ` Peter Zijlstra
2025-06-13 11:17 ` Andrea Parri
[not found] ` <9264df13-36db-4b25-b2c4-7a9701df2f4d@tu-bs.de>
2025-06-16 6:21 ` Andrea Parri
2025-06-16 14:11 ` Alan Stern
2025-06-17 14:09 ` Andrea Parri
2025-06-19 14:27 ` Thomas Haas
2025-06-19 14:32 ` Alan Stern
2025-06-19 14:59 ` Thomas Haas
2025-06-19 17:56 ` Alan Stern
2025-06-19 18:21 ` Thomas Haas
2025-06-16 14:23 ` Will Deacon
2025-06-17 6:19 ` Thomas Haas
2025-06-17 8:42 ` Hernan Ponce de Leon
2025-06-17 14:17 ` Will Deacon
2025-06-17 14:23 ` Thomas Haas [this message]
2025-06-17 19:00 ` Hernan Ponce de Leon
2025-06-19 12:30 ` Will Deacon
2025-06-19 14:11 ` Thomas Haas
2025-06-18 6:51 ` Paul E. McKenney
2025-06-18 12:11 ` Paul E. McKenney
2025-12-17 19:05 ` Thomas Haas
2025-12-18 22:02 ` Andrea Parri
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=7a20b873-3c26-4a52-b118-c816ede7298d@tu-bs.de \
--to=t.haas@tu-bs.de \
--cc=akiyks@gmail.com \
--cc=boqun.feng@gmail.com \
--cc=dhowells@redhat.com \
--cc=dlustig@nvidia.com \
--cc=hernan.poncedeleon@huaweicloud.com \
--cc=j.alglave@ucl.ac.uk \
--cc=joelagnelf@nvidia.com \
--cc=jonas.oberhauser@huaweicloud.com \
--cc=linux-arch@vger.kernel.org \
--cc=linux-kernel@vger.kernel.org \
--cc=lkmm@lists.linux.dev \
--cc=luc.maranget@inria.fr \
--cc=npiggin@gmail.com \
--cc=parri.andrea@gmail.com \
--cc=paulmck@kernel.org \
--cc=peterz@infradead.org \
--cc=r.maseli@tu-bs.de \
--cc=stern@rowland.harvard.edu \
--cc=will@kernel.org \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).