Priority inversion and priority inheritance

Hisabumi Hatsugai — Sun, 22 Jul 2018 00:49:42 +0000

Priority inversion

I will deal with the problem in the following steps:

Model the problem on SyncStitch.
Observe the problem by simulation.
Define the safety specificaion againt the problem.
Implement priority-inheritance protocol.
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:

Process 2 wakes up (the bigger number, the lower priority).
Process 2 locks.
Process 0 wakes up.
Process 2 is preempted.
Process 0 runs. try to lock, but failed since it is already owned by Process 2.
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.

Safety verification of a spin lock used in Linux kernel based on x86-TSO memory model by using SyncStitch

Hisabumi Hatsugai — Fri, 20 Jul 2018 00:13:06 +0000

Memory model

A memory model describes the interactions of threads through memory and their shared use of the data. It is generally defined in programing language specifications or CPU manuals.

x86-TSO

When you write multi-threading programs on x86 processors, you are supposed to assume the memory model described in the x86 manuals, and should not base on the actual behaviour of CPU you use because it varies from CPU model to model, it may be change in the future.

However, unfortunatelly, the memory model is described in natural language and it is often ambiguous and even inconsistent.

To deal with this issue, researchers built a programmer's model. There is a paper titied:

x86-TSO: A Rigorous and Usable Programmer’s Model for x86 Multiprocessors

In this paper, the memory model is rigorously formalized in a mathematical language.

I investigated the behaviours of the model with a model checker (more strictly, a refinement checker) called SyncStitch by modeling (modeling a model!) the memory model in the paper and composing it with thread models executing a sequence of read/write instructions.

The x86-TSO memory model consists of a memory, a lock-state for LOCK-prefix, and for each processor, a set of registers and a writer buffer (a queue which element is a pair of address and a value to be written).

(from the paper)

This model is translated into the SyncStitch model like this (just a sketch):

Once you model a CPU, you can investigate all of possible behaviours of the code like this:

(from the paper)

Or this:

(from the paper)

The results are shown like this.

When you find an allowed final state, you can consult the detailed path from the initial state to the final state with looking into values of the memory, the registers, and the writer buffers, which cannot be observed on the actual CPU.

Spin lock in Linux kernel

According to the paper, there was a discussion about the correctness and the safety of an implementation of a spin lock code in Linux kernel. The code is as follows:

(from the paper)

I modeled this code on SyncStitch with x86-TSO model, and also built a safety specification for it. Then check the safety on the tool.

I successfuly confirmed the safety. This is what a refinement checker can do (one of them).

Since the model I built this time supports LOCK-prefix and MFENCE instruction, you can investigate broad type of x86 instruction sequences intended for multi-threading. I guess programmers working on operating systems and/or embeded systems are insterested in this model and tool.

DEV Community: Hisabumi Hatsugai

Priority inversion and priority inheritance

Priority inversion

Warming up

Implement locks

Safety specification

Priority-inheritance protocol

Safety verification of a spin lock used in Linux kernel based on x86-TSO memory model by using SyncStitch

Memory model

x86-TSO

Spin lock in Linux kernel