I will try to model this test case environment soon and get back to you. @gedare - you are absolutely correct about the description of project
On Friday, June 26, 2015, Gedare Bloom <ged...@gwu.edu> wrote: > On Fri, Jun 26, 2015 at 9:42 AM, Sebastian Huber > <sebastian.hu...@embedded-brains.de <javascript:;>> wrote: > > On 26/06/15 15:28, Gedare Bloom wrote: > >> > >> Since this thread got migrated to devel a bit prematurely, I'll > >> back-stop some of the details and how I understand the state of this > >> project. > >> > >> Saurabh is working toward solving https://devel.rtems.org/ticket/2124 > >> (so yes there is a ticket already, and it should be referenced by > >> patches accordingly). As a first step he has proposed a modified way > >> to step-down inherited priorities when multiple mutexes are acquired > >> simultaneously by one thread and contended by others, i.e. nested > >> mutex access. We wanted assurance the proposal is sound, so we had him > >> implement a model of the current thread synchronization of RTEMS > >> within a Java-based model-checking framework, called Java Path Finder, > >> or JPF. His model shows the existing error with the current > >> STRICT_ORDER option, and then does not show a problem using his > >> proposed method for solving nested mutex acquisition. > >> > >> However, validating the proposed method apparently required adding a > >> global lock around the two linked lists that are used in Saurabh's > >> proposed solution. My intuition is that the global lock to protect > >> these lists is not a big problem for uniprocessor, and for SMP we > >> should prefer to find other solutions at any rate. The lists should > >> not be long, and we should be able to find their bounds. One list is > >> bounded by the number of mutexes a thread may hold, and the other by > >> the number of threads that may contend a specific mutex. > > > > > > Does this new approach address the problem here: > > > > https://git.rtems.org/rtems/tree/testsuites/sptests/spsem03/init.c > > > Perhaps Saurabh can comment and model this problem too, and then we > can see. As I understood the test, a low-priority task holding > semaphore A blocks a mid-priority task holding semaphore B (contending > A), and then a high-priority task blocks on semaphore B, elevating the > priority of mid, but not low => a priority inversion occurs. > > If Saurabh's solution iterates the mutexes held by mid when elevating > its priority, then this inversion also should be fixed. > > Gedare > > > > > -- > > Sebastian Huber, embedded brains GmbH > > > > Address : Dornierstr. 4, D-82178 Puchheim, Germany > > Phone : +49 89 189 47 41-16 > > Fax : +49 89 189 47 41-09 > > E-Mail : sebastian.hu...@embedded-brains.de <javascript:;> > > PGP : Public key available on request. > > > > Diese Nachricht ist keine geschäftliche Mitteilung im Sinne des EHUG. > > > > _______________________________________________ > > devel mailing list > > devel@rtems.org <javascript:;> > > http://lists.rtems.org/mailman/listinfo/devel > _______________________________________________ > devel mailing list > devel@rtems.org <javascript:;> > http://lists.rtems.org/mailman/listinfo/devel -- Thanks, Saurabh Gadia
_______________________________________________ devel mailing list devel@rtems.org http://lists.rtems.org/mailman/listinfo/devel
