Priority inversion

see Wikipedia.

I will deal with the problem in the following steps:

1. Model the problem on SyncStitch.
2. Observe the problem by simulation.
3. Define the safety specificaion againt the problem.
4. Implement priority-inheritance protocol.
5. Check the safety.

Warming up

Using SyncStitch, you can easily realize and test your ideas rapidly.
Before challenging the priority inversion problem, build a simple model as warming-up.

A simple RTOS can be modelled on which processes has the following state-transitions.

The kernel can be modelled like this: (just a sketch, this may be the smallest rtos in the world?)

Then, you can perform simulations for it:

You can see that a process of lower priority is preempted by a higher one.

Implement locks

Like this:

Of course there is possibilities for processes to be preempted in locks.
In fact, you can observe the following sequence:

1. Process 2 wakes up (the bigger number, the lower priority).
2. Process 2 locks.
3. Process 0 wakes up.
4. Process 2 is preempted.
5. Process 0 runs. try to lock, but failed since it is already owned by Process 2.
6. Process 1 wakes up. It can run as long as it wants though the higher Process 0 is waiting for the lock.

This phenomenon is what is called the priority-inversion problem. This can be show as a diagram:

Safety specification

We observed the problem by simulation above. Next, we make a specification which enable the tool automatically detect the problem or make sure there is no problem.

This type of specifications are called safety specifications, which can be described as a state-transition which accepts only possible sequecens and does not include any harmful sequence.

We can define the safety specification for the priority-inversion protocol like this:

SyncStitch is one of what they call refinement checkers, and it has the ability to compare the given specification and the given implementation model and check the correctness relation between them.

The result of the check is this; a violation is found:

Then, you can thoroughly investigate the violation using the analyzing tools provided by SyncStitch.

You can see the same sequence we saw above for the violation:

Priority-inheritance protocol

One of the solutions for the priority-inversion problem is the priority-inheritance protocol. The idea is simple: when schedule the processes, select the process which blocks the process of highest priority.

The function for the selection is like this:

Putting it into the model, you will see the problem is resolved.