DEV Community

loading...

Priority inversion and priority inheritance

Hisabumi Hatsugai
・3 min read

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.

sd1

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

ker0

Then, you can perform simulations for it:

pe0

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

Implement locks

Like this:

sd2

kernel

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.

pe2

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

pi

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:

safety

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:

assert1

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:

seq

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.

pi

The function for the selection is like this:

sp

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

assert2

Discussion (0)