Notice: We have migrated to GitLab launching 2024-05-01 see here: https://gitlab.rtems.org/

Changes between Version 20 and Version 21 of GSoC/2015/NestedMutex


Ignore:
Timestamp:
08/29/15 16:25:50 (9 years ago)
Author:
Saurabh Gadia
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • GSoC/2015/NestedMutex

    v20 v21  
    44
    55'''Participant:''' Saurabh Gadia
    6 
    7 '''Status:''' Currently working on configuring and designing the nested mutex validation model in JPF environment for proposed solution.
    86
    97'''Introduction:''' The strict order mutexes in RTEMS is based on LIFO ordering. So whenever thread tries to acquire mutex lock, its priority before acquiring the lock is pushed to that mutex’s thread queue. So whenever thread release any lock then that lock’s queue is consulted and thread’s priority is restored. So this mechanism of restoring priority may induce unbounded priority inversion if higher priority thread is contending for a lock still hold by our candidate thread. This project deals with solving this problem and developing validation methods using JPF.
     
    6664    [http://babelfish.arc.nasa.gov/trac/jpf/wiki/install/start Installation]
    6765
     66= Status =
    6867
     68Development repositories developed during the GSoC project duration:
     69
     701. uniproc-new1 [https://github.com/saurabhgadia4/lock-model/tree/uniproc-new1 link] - JPF branch successfully solving priority inversion problem for Uniprocessor architecture. We have a extra lock over executing thread which avoids data race. We need to confirm this for RTEMS. All test cases passes for this branch
     71
     722. rtemsjpf-0.6-b2 [https://github.com/saurabhgadia4/lock-model/tree/rtemsjpf-0.6-b2 link] - JPF branch successfully solving priority inversion problem for SMP architecture. We have a extra lock over executing thread which avoids data race. We need to confirm this for RTEMS. All test cases passes for this branch
     73
     743. nested-mutex [https://github.com/saurabhgadia4/rtems/tree/nested-mutex link] - RTEMS implementation of priority inversion problem for uniprocessor target. This branch passes all spsem test cases.
     75
     76
     77There are two places in our JPF implementation where we have used locks over executing thread to avoid data races for SMP targets which RTEMS does not uses. So we have analysed the test case results after removing the lock  over executing thread. With the help of failing test cases we want to reproduce the same data race problem as detected by JPF in RTEMS and resolve the issue for SMP as well. These branches are created rtemsjpf-0.6-b2 and then we have removed the lock over executing thread.
     78
     794. without_exec_lock [https://github.com/saurabhgadia4/lock-model/tree/without_exec_lock link] - removing lock over executing thread in lock() when mutex is not available. Because of this we get data race issues in this branch which are detected by the subset of good test cases.
     80
     815. without_exec_lock-1 [https://github.com/saurabhgadia4/lock-model/tree/without_exec_lock-1 link] - removing lock over executing thread in lock() when mutex is available. Because of this we get data race issues in this branch which are detected by the subset of good test cases.
     82
     83Our next goal is to prove/reproduce that there exists a data race in RTEMS for SMP target by taking help from above 2 branches and their failing test cases.