On Tue, Sep 13, 2022, 1:14 PM Kuan-Hsun Chen <c00...@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 <j...@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....@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@rtems.org >>> http://lists.rtems.org/mailman/listinfo/devel >>> >> _______________________________________________ >> devel mailing list >> devel@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. >
_______________________________________________ devel mailing list devel@rtems.org http://lists.rtems.org/mailman/listinfo/devel
