You can configure the test environment according to your needs but 3 mutex are sufficient to cover all test cases and we can have multiple threads using verify() of JPF.
Thanks, Saurabh Gadia On Thu, Jun 25, 2015 at 6:37 PM, Saurabh Gadia <ga...@usc.edu> wrote: > Hi all, > For time being I have cleaned up the code. I have also attached the trace > files where our JPF-Model can reproduce the RTEMS unbounded priority > inheritance problem(TraceWupi). And after running it through solution model > we are able to demonstrate that there are no assertion errors and it runs > to completion. > > *Model Description: * > > #. Number of threads under test: 2 > #. Number of mutex under test: 2 > #. JPF-Github Link:https://github.com/saurabhgadia4/lock-model > #. Wiki-Link: https://devel.rtems.org/wiki/GSoC/2015/NestedMutex > > #. sanity test function for detecting unbounded priority inheritance > problem: > > https://github.com/saurabhgadia4/lock-model/blob/master/rtems/Mutex.java#L119 > /* > Validator() checks that after stepping down the priority, on unlock() > operation, there should be no higher priority thread contending on any of > the mutex still held by holder. > */ > > Unbounded Priority inheritance demonstrating trace file: > > https://github.com/saurabhgadia4/lock-model/blob/master/TraceWupi#L83 > > Test Scenario: > 1. Thread 1 which have *priority=3* acquires mutex l1, l2. > 2. Thread 2 with priority=1 tries to acquire mutex l1. So with current > RTEMS we just increase the priority of thread 1. > 3. So thread 1 currentPriority becomes 1. and thread 2 sits in waitqueue > of mutex l1 whose holder is thread1. > 4. Now thread 1 happen to release mutex l2 and its priority is stepped > down to 3 again from 1 which was raised by thread 2. > !!!Bingo this is our unbounded priority inheritance problem which we can > successfully catch in our validator function which raises assertion error!!! > so line 83, 84, 85 in TraceWupi > > > > > *Holder Thread: 1, after stepdown operation -->current priority: 3 while > releasing mutex: 2--->Mutex: 1 (has this mutex in its stack > yet)------>Thread-id: 2 priority: 1 (Thread 2 is contending on mutex 1 > which is higer priority than the holder which is Thread 1)* > > *#. Sanity test passes for our solution of handling unbounded priority > Inheritance(UPI). * > tracefile: > https://github.com/saurabhgadia4/lock-model/blob/master/TraceW_O_upi > > > *Highlighting points of this JPF-Model test:* > > Potential present problems in RTEMS: > *problem 1: > Test Case: > Thread 3 with priority=2 acquires mutex l2. Thread 1 of > priority=3 is waiting on waitqueue of mutex2 and simultaneously holds > mutex1 on which thread 2 is contending. thread 2 raises priority of thread > 1 from 3 to 1 and waits in l1 waitqueue. Thread 1 was already waiting in > queue for mutex 2 which is acquired by thread 3 whose priority is 2. So > again we got unbounded priority inheritance problem with thread 1 with > raised priority=1(waiting) and thread 3 with priority=3 is running. > >>>> Correct Behavior: after raising thread 1 priority we reEnqueue > thread1 if it is waiting with the updated priority. We should immediately > update the priority of thread 3 on which thread 1 waits<<<< > > *problem 2: > When mutex is held by a thread and some other thread tries to > acquire the same mutex. The updatePriority() in lock() and > waitqueue.Remove() happens simultaneously. We solved this by having the > global lock() for each mutex. (May be Cyrille can elaborate on this) > > > > Thanks, > > Saurabh Gadia > > On Thu, Jun 25, 2015 at 5:43 PM, Saurabh Gadia <ga...@usc.edu> wrote: > >> O(n) is the least that we can have!! >> >> Thanks, >> >> Saurabh Gadia >> >> On Thu, Jun 25, 2015 at 5:39 PM, Saurabh Gadia <ga...@usc.edu> wrote: >> >>> I mean not recursion. just looping till top of stack of held mutexes. >>> check this out: >>> https://github.com/saurabhgadia4/lock-model/blob/master/rtems/Mutex.java >>> -->updateRecPriority() line 143 >>> >>> Thanks, >>> >>> Saurabh Gadia >>> >>> On Thu, Jun 25, 2015 at 5:35 PM, Joel Sherrill < >>> joel.sherr...@oarcorp.com> wrote: >>> >>>> >>>> >>>> On June 25, 2015 7:33:24 PM CDT, Saurabh Gadia <ga...@usc.edu> wrote: >>>> >@joel: It essentially means finding out the highest priority thread (or >>>> >ceiling) of any remaining mutex held, right? >>>> > >>>> >If you are talking this in context of nested mutex problem ---> >>>> > >>>> >We never go and find the highest priority thread waiting on held mutex. >>>> >Inversely highest priority thread will recursively make changes to top >>>> >of stack of held mutexes by the holder. We don't search. >>>> >>>> True recursion? Or implemented with loop? >>>> >>>> Ok. Still an O(n) operation. Discuss locking on devel@ >>>> >>>> > >>>> >Thanks, >>>> > >>>> > >>>> >Saurabh Gadia >>>> > >>>> > >>>> >On Thu, Jun 25, 2015 at 5:27 PM, Joel Sherrill >>>> ><joel.sherr...@oarcorp.com> wrote: >>>> > >>>> > >>>> > >>>> >On June 25, 2015 7:23:06 PM CDT, Cyrille Artho >>>> ><cyrille.ar...@gmail.com> wrote: >>>> >>Hi Gedare and all, >>>> >>Good news: >>>> >>In this morning's discussion, we fixed some remaining issues in the >>>> >>model and now got results. >>>> >> >>>> >>The current model shows a case of priority inversion with a simple >>>> >>priority reset mechanism and the absence of that problem with the >>>> >>proposed strategy. >>>> >> >>>> >>There is only one flaw: We had to use a global lock in the model >>>> >>(essentially making the entire "lock" and "unlock" operations atomic), >>>> >>because so far we couldn't find a way to secure lock the operations on >>>> >>a lower level. The model uses a list of locks held (by a thread) and a >>>> >>list of threads waiting on a lock (in the lock data structure), so >>>> >>these aspects are essentially cross-cutting and very hard to get right >>>> >>without a global lock. >>>> >> >>>> >>The RTEMS code uses different macros inside these operations (_Seize, >>>> >>_Surrender), which do not seem to use a global lock (but I may have >>>> >>missed something). It is possible that a data race occurs for a >>>> >>complex lock update strategy, if we don't use a global lock. >>>> >> >>>> >>Saurabh will clean up the model and provide documentation with >>>> >details. >>>> >> >>>> >>In the meantime, can you maybe answer these questions for us: >>>> >> >>>> >>(1) Did you have any issues with race conditions in the current RTEMS >>>> >>code (especially recent changes)? >>>> > >>>> >We haven't observed any but that doesn't mean there aren't any >>>> >undiscovered. >>>> > >>>> >>(2) Is a fix using a global lock acceptable? Correctness-wise it's the >>>> >>safest thing, but of course performance-wise it's a bottleneck. >>>> > >>>> >The locking strategy needs to be discussed. On a uniprocessor system, >>>> >these issues tend to be minor and cause delays. On smp systems, they >>>> >become more complex and performance problems. >>>> > >>>> >It essentially means finding out the highest priority thread (or >>>> >ceiling) of any remaining mutex held, right? >>>> > >>>> >Bring this up on devel@ >>>> > >>>> > >>>> >--joel >>>> >>>> --joel >>>> >>> >>> >> >
_______________________________________________ devel mailing list devel@rtems.org http://lists.rtems.org/mailman/listinfo/devel
