API Documentation: https://mirkootter.github.io/lean-mt-doc/Mt.html
Multithreaded algorithms can be very hard to reason about. For simple problems, many developers are able to somehow "see" that the code is correct, but precise argumentation or even formal proofs are much more difficult, even for the simplest of problems.
Let us consider the following very simple example
let x : atomic<int> = 0; // Assuming sequential consistency
let y : atomic<int> = 0; // Assuming sequential consistency
function thread1() {
++x; // atomic increment
++y; // atomic increment
const py = y; // atomic read
const px = x; // atomic read
assert(px ≥ py);
}
The above code is correct: Spawning a (reasonable) number of those threads in parallel will never panic. Obviously, spawning several billion of those threads might panic due to new cases introduced by integer overflow.
We can make the sample above a little more complicated by adding a second type of thread. It is supposed to be spawned alongside thread1
function thread2() {
++x;
++x;
++y;
++x;
++y;
++y;
const py = y; // atomic read
const px = x; // atomic read
assert(px ≥ py);
}
We can spawn any number of thread1
and thread2
and none of them will panic (again, ignoring integer overflows for now)
Assuming sequential consistency, thread1
can be cut intro 5 steps and interleaved with the steps of all other threads. If we spawn this method one time, we have exactly one possible combination. If we spawn it two times, we have
combinations. If we spawn it three times, we have 756,756 combinations. For four threads, we get already 11,732,745,024 combinations. If we use also thread2
, it gets even worse. Obviously, naive cases analysis is not a good idea.
We provide a powerful and easy to use framework using Lean 4. Assuming the sequential consistent memory model, we follow the intuitive model of treating threads as iterable systems. In each time step, one thread is chosen and iterated. One iteration corresponds to one atomic operation. We develop a system based on invariants: Designing some rules, we use the following simple idea:
If all threads are following the same rules, we can focus our reasoning on one thread at a time. We have to prove that the current thread respects the rules, assuming the other threads do the same.
This idea is formalized. We develop a very general type of invariant and provide tools to specify threads and reason about them. We provide a central soundness theorem to justify the intuition above: Given any number of threads which respects a given invariant, the whole system will respect it.
Reservations are our way to reason about the thread's past actions without needing to manage its full history. Often, we find situations that a given thread may perform a certain action only if he has performed a different action first.
Consider the line ++y
in thread1
. This line is only sound
because the thread has called ++x
before.
This poses an additional challenge for writing thread specifications.
Without the line ++y
, we could simply demand that x ≥ y
holds
at all time and use a simple inductive argument (induction over time).
However, the knowledge that a previous thread only ensured x ≥ y
is not enough to reason that ++y
is an allowed operation. We need
the stronger guarantee x ≥ y + 1
for that.
Our solution to this problems are reservations. Reservations are a certain kind of thread local variables. Since they are thread local, they cannot be modifed by other threads. However, the specification may demand certain properties of the reservations which we can use as foundation for reasoning.
Going back to our example, we follow the intuitive approach
that ++x
creates some "luft" between x
and y
to prepare
++y
. This luft is stored as reservation. The next time this
thread becomes active, the reservation will still be valid
and we conclude y ≥ x + 1
.
Have a look at our revised example, which is much easier to reason about:
let x : atomic<int> = 0;
let y : atomic<int> = 0;
[@threadlocal] let luft : uint = 0;
void thread1b() {
atomic { ++x; luft = 1; }
atomic { ++y; luft = 0; }
// ...
}
Using the invariant
we can now use a simple inductive approach to reason that
we have indeed x ≥ y
at all times.
Note that we have omitted the assertion in the code above. This is
because the reservation above is not enough to prove that the
assertion will succeed. We read x
and y
at different points in
time. To reason about that, we need a second reservation:
let x : atomic<int> = 0;
let y : atomic<int> = 0;
[@threadlocal] let luft : uint = 0;
[@threadlocal] let min_x : int = 0;
void thread1b() {
atomic { ++x; luft = 1; }
atomic { ++y; luft = 0; }
const py = atomic { min_x = y ; y }
const px = x;
assert (px ≥ py);
}
with the two invariants
In fact, we can remove the
Using this form, we can combine both reservations into one reservation
with
Note that the operator
For our reasoning framework, we want to decouple threads from each other as much as possible. We want to focus on one given thread at a time, and refer to everything outside as "the environment".
It should not matter how many other threads they are. Only what they do (or could do, potentially). If each of the other threads has made reservations which we need to respect, it should not matter whether one very complex threads has done a huge reservation or if there are thousands of threads out there.
Additionally, it is reasonable to assume that the order of the reservations does not matter, since the other threads could be called in any order. In general, this assumption should not be a problem. On the other hand, it greatly simplifies the framework: We only have to reason about two reservations at a time: The reservation of the environment, and the reservation of our own thread. We can change our own reservation, but we have no control at all about the reservation of the environment.
Our main goal is to reason about a multithreaded system by decoupling the threads from each other. Reasoning about the system becomes reasoning about one thread at a time, even one line at a time.
To do that, we know that after each iteration the situation may have completely changed. If the other threads may do virtually everything, we would not be able to reason about anything. That's what the specification is for. It describes precisely what a thread can do and what not. If all threads of a given system follow the same specification, we can use this information for reasoning.
In this project, the specification provides (among other things) the following:
- The type
State
which represents the shared memory - The type
Reservation
which represents the threadlocal reservations - A validation predicate
Reservation → State → Prop
. For a valid system, this predicate must hold at all times