Nested Mutex

Mentors: Cyrille Artho, Daniel Ramirez, Joel Sherrill, Gedare Bloom, Chris Johns

Participant: Saurabh Gadia

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.

RTEMS Environment Setup Steps from sratch for STRICT ORDER MUTEX configuration

• Build RSB by following this ​link from 1.0 to 2.4 Building step(inclusive). I have used spark-sis configuration.
• Now clone the RTEMS repository from ​Personal Github Link

sudo apt-get install pax    (you require it for compiling libtests from testsuite) This step should be performed before bootstraping.

cd rtems

export PATH=/opt/rtems/4.11/bin:$PATH

export PATH=~/devlopment/rtems/4.11/bin:$PATH    (RSB tools path)

./bootstrap

cd ..

mkdir b-sis

cd b-sis

../rtems/configure --target=sparc-rtems4.11 --enable-rtemsbsp=sis --enable-tests --disable-posix ENABLE_STRICT_ORDER_MUTEX=1

make

sudo PATH=/opt/rtems/4.11/bin:${PATH} make install

• Above steps if performed correctly will compile your RTEMS code and you can go ahead with your test suites. path of compiled testsuites: b-sis/sparc-rtems4.11/c/sis/testsuites/sptests

JPF Setup

• You can either download snapshots or build JPF from source. Building from source is recommended as they contain latest changeset and our project runs under latest compiled source code.
• You can find detailed JPF installation guide at ​link
• Clone JPF latest repository. ​link
• Make sure you fulfil all the requirement mentioned on above link especially use JDK 8 or later version to compile.
• If you want to check with RTEMS JPF code please clone this repository.​link
• Set the path of jpf-core which you cloned from JPF site under JPF_HOME. export JPF_HOME=Path-To-jpf-core-Directory.
• For compiling just run compile script present under cloned RTEMS lock-model repository.
• For running the JPF code just run jpf script.
• We are using 3 threads and 3 mutex to demonstrate the RTEMS behavior. It takes far more time to run for this test configuration. You can go ahead and modify Environment.java as per requirement. After making changes compile and run it.

Progress

• Proposed solution for the existing problem. You can find presentation which also contains test cases in attachment section.
• Compiled RTEMS for running Strict Mutex test cases. [Setup from scratch]
• We modelled our solution in JPF for bith uniprocessor as well as SMP architecture.
• Developed all the test case suite for validating the solution.
• Implemented the JPF solution for uniprocessor target in legacy RTEMS and all test cases were passing successfully.

Resources

• Complete Documentation and status of project ​link
• Project Blog ​link
• RTEMS-JPF Model code repository ​link
• Documentation (Annotation) of RTEMS-JPF model ​link
• Nested Mutex related test cases ​Test Case
• JPF Related Resources:
  ​Installation

Status

Development repositories developed during the GSoC project duration:

1. 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

2. 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

3. nested-mutex ​link - RTEMS implementation of priority inversion problem for uniprocessor target. This branch passes all spsem test cases.

There 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.

4. 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.

5. 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.

Our 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.