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.