Here is the companion material for the paper: Untangling the Intricacies of Thread Synchronization in the PREEMPT_RT Linux Kernel by Daniel Bristot de Oliveira, Rômulo Silva de Oliveira, and Tommaso Cucinotta, to be presented at the ISORC 2019.
NOTE: The latest version of the model and patches can be found here!
The model was developed using the Supremica tool. You can find more information about Supremica here.
The source code of the model can be found here. It can be opened with Supremica. From Supremica it is possible to visualize, edit, analyze, simulate and export the model.
In the Linux part, you can find the patch with perf task_model and tracepoints here. It applies in the version v4.14.15-rt13 of the development tree of the PREEMPT RT.
It is possible to use a virtual machine to run the experiments. Here is the definition of a QEMU/KVM virtual machine and the kernel config file that works with this VM.
ERRATA: Prof. Martin Fabian, found that despite the minimized model was “non-blocking” the non-minimized was not. The problem was caused by two missing events (sched_switch_in, sched_switch_in_o) in the state any_thread_running in the specification s19. This difference causes a change in the number of states from 13906 to 13786, and in the transitions from 31708 to 31221. This problem was already resolved, in a version earlier than the submission of the paper. But I (Daniel) forgot to update Table II and the reference model. This error does not change any of the results. The link above points to the correct model. The broken model is here.
