[PATCH] icpp remedy

[Kuan-Hsun Chen]

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.
>>
>> 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.
>>
>

-- 
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/727c9d78/attachment-0001.htm>