Re: [PATCH] misra: address Rule 11.3 in spin_unlock_common()

[Nicola Vetrini <nicola.vetrini@bugseng.com>]

On 2025-11-03 12:26, Andrew Cooper wrote:
> On 03/11/2025 10:11 am, Dmytro Prokopchuk1 wrote:
>> diff --git a/xen/common/spinlock.c b/xen/common/spinlock.c
>> index 0389293b09..d9dc9998e6 100644
>> --- a/xen/common/spinlock.c
>> +++ b/xen/common/spinlock.c
>> @@ -367,7 +367,8 @@ static void always_inline 
>> spin_unlock_common(spinlock_tickets_t *t,
>>      LOCK_PROFILE_REL;
>>      rel_lock(debug);
>>      arch_lock_release_barrier();
>> -    add_sized(&t->head, 1);
>> +    BUILD_BUG_ON(sizeof(t->head) != sizeof(uint16_t));
>> +    add_u16_sized(&t->head, 1);
> 
> This is an example where MISRA's opinions actively making the logic 
> less
> safe.
> 
> It's not possible for add_sized() to use the wrong type (as it
> calculates it internally), whereas it's quite possible to update the
> BUILD_BUG_ON() and fail to adjust the add.
> 

I agree, we should devise a way to argue that the casts are safe and 
write a proper deviation. If I recall correctly, {read,write}_atomic 
have exactly the same issues.

> Specifically, you've made it more complicated to reason about, and
> created an opportunity to make an unsafe change where that opportunity
> does not exist in the code as-is.
> 
> Furthermore, read and write atomic have exactly the same internal
> pattern as add_sized(), so how does this not just kick the can down the
> road?
> 
> ~Andrew

-- 
Nicola Vetrini, B.Sc.
Software Engineer
BUGSENG (https://bugseng.com)
LinkedIn: https://www.linkedin.com/in/nicola-vetrini-a42471253