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

On 6/17/2025 4:23 PM, Thomas Haas wrote:
> 
> 
> 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.

Yes, my bad. I was using the generic header rather than the aarch64 
specific one and then the changes to the model were having not effect 
(as they should).

Now I am using the aarch64 specific ones and I can confirm dartagnan 
still reports the violations with the current model and making the 
change proposed by Thomas (adding ;si just to the second part seems to 
be enough) indeed removes all violations.

Hernan

> 
>>
>>> 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.
>