[PATCH] icpp remedy

[Joel Sherrill]

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.
>
> 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
> *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).
>
> 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.
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.rtems.org/pipermail/devel/attachments/20220913/62fef142/attachment.htm>