<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">c0066c@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;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:0 0 0 .8ex;border-left:1px #ccc solid;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" target="_blank" rel="noreferrer">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" target="_blank" rel="noreferrer">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" target="_blank" rel="noreferrer">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" target="_blank" rel="noreferrer">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" target="_blank" rel="noreferrer">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" target="_blank" rel="noreferrer">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>