[PATCH] icpp remedy

Wed Sep 14 22:06:48 UTC 2022

On Tue, Sep 13, 2022 at 12:42 PM Kuan-Hsun Chen <c0066c at gmail.com> wrote:
>
> Thanks for the prompt reply. Yes, I will guide Junjie to make a ticket and go through the issue.
>
> >Is there a test case for this?
> Yes, a test case is also ready to be reviewed and can be part of the testsuite to test out ICPP (MrsP should also pass).
>
> > If it applies to 5 or 4.11, there needs to be another ticket to get the fix back ported.
> So each release version with one ticket? We only check 5.1 in this work. My intuitive guess is that if the functionality does not change over the versions, the remedy should be similar.
> Let us figure it out.
>
> On Tue, Sep 13, 2022 at 8:21 PM Joel Sherrill <joel at rtems.org> wrote:
>>
>>
>>
>> On Tue, Sep 13, 2022, 1:14 PM Kuan-Hsun Chen <c0066c at gmail.com> wrote:
>>>
>>> (Oh, I just noticed that the patch was submitted faster than my mail to share this patch :P).
>>
>>
>> No problem. That's why I asked what the issue was.
>>
>> It needs at least a much better log message. It needs a ticket given the gravity of the issue. That ticket can explain the situation and include links. Probably needs a comment above the change explaining what's going on.
>>
>> Is there a test case for this?
>>
>> If it applies to 5 or 4.11, there needs to be another ticket to get the fix back ported.
>>
>> Great catch. Just need to do a good job on the log, test, ticket(s), etc
>>
>> --joel
>>
>>>
>>> Hi Joel,
>>>
>>> Let me clarify what happened here. In our recent study, we adopt Frama-C to formally verify the implementation of ICPP (also MrsP) and note that the current flow may lead to a deadlock. The patch is a simple remedy to fix the issue.
>>>
>>> The resource’s ceiling is not checked against the thread’s base priority, but against its current dynamic priority derived from the task’s priority aggregation. However, a resource’s ceiling is required to be set as the highest base priority of all tasks that are requesting it. This mismatch may lead to a deadlock by denying legitimate nested resource access if resources are requested in descending order of priority. So this adaption is needed to resolve the issue. A similar issue can also be found in MrsP due to the usage of this function. A detailed explanation can be found at the end of Section V in the attached preprint, and a toy example is provided there to reveal the issue.
>>>

By changing this to check the base priority instead of the dynamic
priority, the mutex seize will now allow a task to acquire a ceiling
mutex even though its dynamic priority is higher than the ceiling. The
specification to check against the base priority of tasks comes from
the ICPP without nested lock behavior as I recall, and I'm not 100%
sure where the requirement comes from that "a resource’s ceiling is
required to be set as the highest base priority of all tasks that are
requesting it" -- is that requirement proved anywhere for ICPP with
nested resources? I'm a little concerned about making this kind of
fundamental change deep within the (shared) locking protocol code,
especially since it primarily seems to cater to a uniprocessor corner
case.

This is a tricky situation, and clearly a lot of work has already gone
into discovering it. I think we need to discuss this patch a bit more.
If I understood correctly, this deadlock can't happen if locks are
always acquired in the increasing priority order. Changing this code
allows for applications to acquire locks in arbitrary priority order.
I'm not sure that is permissible in multiprocessor systems to still
ensure correctness of the locking protocol correctness. It would be
therefore also valid to state this as an explicit requirement for
applications to make correct use of ICPP. The same thing is also true
for MrsP, and for multiprocessor locking protocols in general I
believe it is required for locks to be acquired in priority order? I'd
be inclined to instead say that we should confirm that locks are
acquired in the proper priority ordering as a way to avoid the
identified deadlock situation.

Either way this discussion/patch goes, we should document these issues
in https://docs.rtems.org/branches/master/c-user/key_concepts.html#priorityceiling

>>> The verification framework will be presented in EMSOFT this year, which is publicly available here: https://github.com/tu-dortmund-ls12-rt/Resource-Synchronization-Protocols-Verification-RTEMS

Congrats on the paper. I'll read through it more thoroughly later. For
now I focused only on the outcome of the verification (Section V) and
the discussion of the ICPP / MrsP concerns.

>>> *I notice that Andrew today also sent a patch for a chapter on formal verification. Since our result is relevant, I plan to respond to the previous thread (https://lists.rtems.org/pipermail/devel/2022-July/072167.html).
>>>

Thanks. It's great to see some kind of community forming around this.
I wonder if it would make sense to look at stimulating a community
focused on formal verification for real-time systems with RTEMS as a
proof-of-concept "playground" -- then again, it's hard to grok some of
the results.

>>> Best regards,
>>> Kuan-Hsun
>>>
>>> On Tue, Sep 13, 2022 at 3:35 PM Joel Sherrill <joel at rtems.org> wrote:
>>>>
>>>> What is this a remedy for?
>>>>
>>>> Why isn't the helper method OK to use?
>>>>
>>>> --joel
>>>>
>>>> On Tue, Sep 13, 2022 at 7:41 AM Strange369 <junjie.shi at tu-dortmund.de> wrote:
>>>>>
>>>>> ---
>>>>>  cpukit/include/rtems/score/coremuteximpl.h | 2 +-
>>>>>  1 file changed, 1 insertion(+), 1 deletion(-)
>>>>>
>>>>> diff --git a/cpukit/include/rtems/score/coremuteximpl.h b/cpukit/include/rtems/score/coremuteximpl.h
>>>>> index d489a0d946..72d32f8030 100644
>>>>> --- a/cpukit/include/rtems/score/coremuteximpl.h
>>>>> +++ b/cpukit/include/rtems/score/coremuteximpl.h
>>>>> @@ -445,7 +445,7 @@ RTEMS_INLINE_ROUTINE Status_Control _CORE_ceiling_mutex_Set_owner(
>>>>>    scheduler_node = _Thread_Scheduler_get_home_node( owner );
>>>>>
>>>>>    if (
>>>>> -    _Priority_Get_priority( &scheduler_node->Wait.Priority )
>>>>> +    owner->Real_priority.priority
>>>>>        < the_mutex->Priority_ceiling.priority
>>>>>    ) {
>>>>>      _Thread_Wait_release_default_critical( owner, &lock_context );
>>>>> --
>>>>> 2.25.1
>>>>>
>>>>> _______________________________________________
>>>>> devel mailing list
>>>>> devel at rtems.org
>>>>> http://lists.rtems.org/mailman/listinfo/devel
>>>>
>>>> _______________________________________________
>>>> devel mailing list
>>>> devel at rtems.org
>>>> http://lists.rtems.org/mailman/listinfo/devel
>>>
>>>
>>>
>>> --
>>> Diese Mail wurde mobil geschrieben. Etwaige Rechtschreibfehler sind volle Absicht und als großzügiges Geschenk zu verstehen.
>
>
>
> --
> Diese Mail wurde mobil geschrieben. Etwaige Rechtschreibfehler sind volle Absicht und als großzügiges Geschenk zu verstehen.