Version 19 (modified by Saurabh Gadia, on Aug 24, 2015 at 7:54:34 AM) (diff)


Nested Mutex

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

Participant: Saurabh Gadia

Status: Currently working on configuring and designing the nested mutex validation model in JPF environment for proposed solution.

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)


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


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
  • 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 as per requirement. After making changes compile and run it.
  • Till now we are able to reproduce the RTEMS locking model and have finished coding for proposed solution to resolve unbounded priority inheritance problem.


  • 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]
  • Working on validation of RTEMS-JPF models.


Attachments (1)

Download all attachments as: .zip