Results

[Saurabh Gadia]

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 <gedare at gwu.edu> wrote:

> On Fri, Jun 26, 2015 at 9:42 AM, Sebastian Huber
> <sebastian.huber at 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.huber at 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 at rtems.org <javascript:;>
> > http://lists.rtems.org/mailman/listinfo/devel
> _______________________________________________
> devel mailing list
> devel at rtems.org <javascript:;>
> http://lists.rtems.org/mailman/listinfo/devel



-- 
Thanks,

Saurabh Gadia
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.rtems.org/pipermail/devel/attachments/20150626/6eac0004/attachment-0002.html>