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

[Thomas Haas <t.haas@tu-bs.de>]

On 19.06.25 19:56, Alan Stern wrote:
> 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

I would rather see the approaches as complementary.
If you lift ARM tests to LKMM tests, you can use them to reason about 
both the informal operational model and the formal axiomatic model.
I mean, there are going to be litmus tests that show behavior that 
should reasonably be forbidden on all platforms, and trying to adapt the 
formal LKMM to also forbid them seems like a good exercise.
Even if it turns out that the changes are unsound, I think you will end 
up with better understanding, no?

Either way, I'm just suggesting possible ways to start but I myself 
don't have the time (right now) to get this project going.

Thomas