On Fri, Jun 26, 2015 at 9:42 AM, Sebastian Huber <sebastian.hu...@embedded-brains.de> 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 > PGP : Public key available on request. > > Diese Nachricht ist keine geschäftliche Mitteilung im Sinne des EHUG. > > _______________________________________________ > 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
