<div dir="ltr"><div class="gmail_default" style="font-family:verdana,sans-serif">Thanks for the prompt reply. Yes, I will guide Junjie to make a ticket and go through the issue.</div><div class="gmail_default" style="font-family:verdana,sans-serif"><br></div><div class="gmail_default" style="font-family:verdana,sans-serif">>Is there a test case for this?</div><div class="gmail_default" style="font-family:verdana,sans-serif">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).</div><div class="gmail_default" style="font-family:verdana,sans-serif"><br></div><div class="gmail_default" style="font-family:verdana,sans-serif">> If it applies to 5 or 4.11, there needs to be another ticket to get the fix back ported.</div><div class="gmail_default" style="font-family:verdana,sans-serif">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. <br>Let us figure it out.</div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Tue, Sep 13, 2022 at 8:21 PM Joel Sherrill <<a href="mailto:joel@rtems.org" target="_blank">joel@rtems.org</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="auto"><div><br><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Tue, Sep 13, 2022, 1:14 PM Kuan-Hsun Chen <<a href="mailto:c0066c@gmail.com" target="_blank">c0066c@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr"><div class="gmail_default" style="font-family:verdana,sans-serif">(Oh, I just noticed that the patch was submitted faster than my mail to share this patch :P).</div></div></blockquote></div></div><div dir="auto"><br></div><div dir="auto">No problem. That's why I asked what the issue was.</div><div dir="auto"><br></div><div dir="auto">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.</div><div dir="auto"><br></div><div dir="auto">Is there a test case for this?</div><div dir="auto"><br></div><div dir="auto">If it applies to 5 or 4.11, there needs to be another ticket to get the fix back ported.</div><div dir="auto"><br></div><div dir="auto">Great catch. Just need to do a good job on the log, test, ticket(s), etc</div><div dir="auto"><br></div><div dir="auto">--joel</div><div dir="auto"><br></div><div dir="auto"><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr"><div class="gmail_default" style="font-family:verdana,sans-serif"> </div><div class="gmail_default" style="font-family:verdana,sans-serif"><br></div><div class="gmail_default" style="font-family:verdana,sans-serif">Hi Joel, <br></div><div class="gmail_default" style="font-family:verdana,sans-serif"><br></div><div class="gmail_default" style="font-family:verdana,sans-serif">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.</div><div class="gmail_default" style="font-family:verdana,sans-serif"><br></div><div class="gmail_default" style="font-family:verdana,sans-serif">The <span style="font-family:Arial,Helvetica,sans-serif">resource’s ceiling is not checked against the thread’s base </span><span style="font-family:Arial,Helvetica,sans-serif">priority, but against its current dynamic priority derived from </span><span style="font-family:Arial,Helvetica,sans-serif">the task’s priority aggregation. </span>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.</div><div class="gmail_default" style="font-family:verdana,sans-serif"><br></div><div class="gmail_default" style="font-family:verdana,sans-serif">The verification framework will be presented in EMSOFT this year, which is publicly available here: <a href="https://github.com/tu-dortmund-ls12-rt/Resource-Synchronization-Protocols-Verification-RTEMS" rel="noreferrer" target="_blank">https://github.com/tu-dortmund-ls12-rt/Resource-Synchronization-Protocols-Verification-RTEMS</a></div><div class="gmail_default" style="font-family:verdana,sans-serif">*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 (<a href="https://lists.rtems.org/pipermail/devel/2022-July/072167.html" rel="noreferrer" target="_blank">https://lists.rtems.org/pipermail/devel/2022-July/072167.html</a>).</div><div class="gmail_default" style="font-family:verdana,sans-serif"><br></div><div class="gmail_default" style="font-family:verdana,sans-serif">Best regards,<br>Kuan-Hsun</div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Tue, Sep 13, 2022 at 3:35 PM Joel Sherrill <<a href="mailto:joel@rtems.org" rel="noreferrer" target="_blank">joel@rtems.org</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr">What is this a remedy for?<div><br></div><div>Why isn't the helper method OK to use?</div><div><br></div><div>--joel</div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Tue, Sep 13, 2022 at 7:41 AM Strange369 <<a href="mailto:junjie.shi@tu-dortmund.de" rel="noreferrer" target="_blank">junjie.shi@tu-dortmund.de</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">---<br>
 cpukit/include/rtems/score/coremuteximpl.h | 2 +-<br>
 1 file changed, 1 insertion(+), 1 deletion(-)<br>
<br>
diff --git a/cpukit/include/rtems/score/coremuteximpl.h b/cpukit/include/rtems/score/coremuteximpl.h<br>
index d489a0d946..72d32f8030 100644<br>
--- a/cpukit/include/rtems/score/coremuteximpl.h<br>
+++ b/cpukit/include/rtems/score/coremuteximpl.h<br>
@@ -445,7 +445,7 @@ RTEMS_INLINE_ROUTINE Status_Control _CORE_ceiling_mutex_Set_owner(<br>
   scheduler_node = _Thread_Scheduler_get_home_node( owner );<br>
<br>
   if (<br>
-    _Priority_Get_priority( &scheduler_node->Wait.Priority )<br>
+    owner->Real_priority.priority<br>
       < the_mutex->Priority_ceiling.priority<br>
   ) {<br>
     _Thread_Wait_release_default_critical( owner, &lock_context );<br>
-- <br>
2.25.1<br>
<br>
_______________________________________________<br>
devel mailing list<br>
<a href="mailto:devel@rtems.org" rel="noreferrer" target="_blank">devel@rtems.org</a><br>
<a href="http://lists.rtems.org/mailman/listinfo/devel" rel="noreferrer noreferrer" target="_blank">http://lists.rtems.org/mailman/listinfo/devel</a><br>
</blockquote></div>
_______________________________________________<br>
devel mailing list<br>
<a href="mailto:devel@rtems.org" rel="noreferrer" target="_blank">devel@rtems.org</a><br>
<a href="http://lists.rtems.org/mailman/listinfo/devel" rel="noreferrer noreferrer" target="_blank">http://lists.rtems.org/mailman/listinfo/devel</a></blockquote></div><br clear="all"><div><br></div>-- <br><div dir="ltr"><div dir="ltr">Diese Mail wurde mobil geschrieben. Etwaige Rechtschreibfehler sind volle Absicht und als großzügiges Geschenk zu verstehen.<br></div></div>
</blockquote></div></div></div>
</blockquote></div><br clear="all"><div><br></div>-- <br><div dir="ltr"><div dir="ltr">Diese Mail wurde mobil geschrieben. Etwaige Rechtschreibfehler sind volle Absicht und als großzügiges Geschenk zu verstehen.<br></div></div>