= 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 [https://docs.rtems.org/rsb link] from 1.0 to 2.4 Building step(inclusive). I have used spark-sis configuration. * Now clone the RTEMS repository from [https://github.com/saurabhgadia4/rtems 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 [http://babelfish.arc.nasa.gov/trac/jpf/wiki/install/start link] * Clone JPF latest repository. [http://babelfish.arc.nasa.gov/trac/jpf/wiki/install/repositories 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.[https://github.com/saurabhgadia4/lock-model 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. * Till now we are able to reproduce the RTEMS locking model and have finished coding for proposed solution to resolve unbounded priority inheritance problem. = 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] * Working on validation of RTEMS-JPF models. = Resources = * Complete Documentation and status of project [https://docs.google.com/document/d/1eQ1pkziaitgnjeaH6shT0Hi_QmnxpjUL4AJ-blWn-rk/edit?usp=sharing link] * Project Blog [https://rejuvinatewithme.wordpress.com/ link] * RTEMS-JPF Model code repository [https://github.com/saurabhgadia4/lock-model link] * Documentation (Annotation) of RTEMS-JPF model [https://docs.google.com/document/d/1_okTNAewI6NO6EcR1oCv-BIIgdkaZa3qm9kByv0tLdI/edit?usp=sharing link] * Nested Mutex related test cases [https://github.com/RTEMS/rtems/blob/master/testsuites/sptests/spsem02/init.c Test Case] * JPF Related Resources:[[BR]] [http://babelfish.arc.nasa.gov/trac/jpf/wiki/install/start Installation]