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

On 6/17/2025 8:19 AM, Thomas Haas wrote:
> 
> 
> On 16.06.25 16:23, Will Deacon wrote:
>> On Fri, Jun 13, 2025 at 09:55:01AM +0200, Peter Zijlstra wrote:
>>> On Thu, Jun 12, 2025 at 04:55:28PM +0200, Thomas Haas wrote:
>>>> We have been taking a look if mixed-size accesses (MSA) can affect the
>>>> correctness of qspinlock.
>>>> We are focusing on aarch64 which is the only memory model with MSA 
>>>> support
>>>> [1].
>>>> For this we extended the dartagnan [2] tool to support MSA and now it
>>>> reports liveness, synchronization, and mutex issues.
>>>> Notice that we did something similar in the past for LKMM, but we were
>>>> ignoring MSA [3].
>>>>
>>>> The culprit of all these issues is that atomicity of single load
>>>> instructions is not guaranteed in the presence of smaller-sized stores
>>>> (observed on real hardware according to [1] and Fig. 21/22)
>>>> Consider the following pseudo code:
>>>>
>>>>      int16 old = xchg16_rlx(&lock, 42);
>>>>      int32 l = load32_acq(&lock);
>>>>
>>>> Then the hardware can treat the code as (likely due to store- 
>>>> forwarding)
>>>>
>>>>      int16 old = xchg16_rlx(&lock, 42);
>>>>      int16 l1 = load16_acq(&lock);
>>>>      int16 l2 = load16_acq(&lock + 2); // Assuming byte-precise pointer
>>>> arithmetic
>>>>
>>>> and reorder it to
>>>>
>>>>      int16 l2 = load16_acq(&lock + 2);
>>>>      int16 old = xchg16_rlx(&lock, 42);
>>>>      int16 l1 = load16_acq(&lock);
>>>>
>>>> Now another thread can overwrite "lock" in between the first two 
>>>> accesses so
>>>> that the original l (l1 and l2) ends up containing
>>>> parts of a lock value that is older than what the xchg observed.
>>>
>>> Oops :-(
>>>
>>> (snip the excellent details)
>>>
>>>> ### Solutions
>>>>
>>>> The problematic executions rely on the fact that T2 can move half of 
>>>> its
>>>> load operation (1) to before the xchg_tail (3).
>>>> Preventing this reordering solves all issues. Possible solutions are:
>>>>      - make the xchg_tail full-sized (i.e, also touch lock/pending 
>>>> bits).
>>>>        Note that if the kernel is configured with >= 16k cpus, then 
>>>> the tail
>>>> becomes larger than 16 bits and needs to be encoded in parts of the 
>>>> pending
>>>> byte as well.
>>>>        In this case, the kernel makes a full-sized (32-bit) access 
>>>> for the
>>>> xchg. So the above bugs are only present in the < 16k cpus setting.
>>>
>>> Right, but that is the more expensive option for some.
>>>
>>>>      - make the xchg_tail an acquire operation.
>>>>      - make the xchg_tail a release operation (this is an odd 
>>>> solution by
>>>> itself but works for aarch64 because it preserves REL->ACQ 
>>>> ordering). In
>>>> this case, maybe the preceding "smp_wmb()" can be removed.
>>>
>>> I think I prefer this one, it move a barrier, not really adding
>>> additional overhead. Will?
>>
>> 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.
>>
>> Will
> 
> 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.

I think the problem is actually with the Internal visibility axiom, 
because only making that one stronger seems to remove the violations.

Hernan

> 
> We should definitely ask ARM about this. I did sent an email to Jade 
> before writing about this issue here, but she was (and still is) busy 
> and told me to ask at [email protected] .
> I will ask them.
> 
>