Samuel Grahn: Concurrency: Models, Algorithms, and Verification

Abstract

Concurrent programs are everywhere, as are the systems they run on. They can be found in everything, from watches to airplanes and medical devices. Ensuring that these programs and systems behave as intended is crucial, as any failures can have devastating consequences. Verifying programs on concurrent hardware is tricky, since the order in which operations are performed can be considered nondeterministic from the point of view of the programmer. Moreover, the intuitive notions of causality may or may not apply to memory accesses, due to sacrifices made by cache protocols designed to optimize these accesses. This thesis presents work on the verification of concurrent programs and systems.

In the first contribution, we focus on linearizability, a correctness condition for concurrent objects. In particular, we develop efficient monitoring algorithms --- checking whether single executions are linearizable --- for stacks, queues, and (multi)sets. Our stack algorithm runs in quadratic time, our queue algorithm runs in linearithmic time, and our (multi)set algorithm runs in linear time. We also implement these algorithms in a tool, LiMo, and mechanize the stack algorithm and its correctness proof in a theorem prover.

In the second contribution, we cover the consistency problem for event-driven traces. An event-driven trace, in addition to shared-memory concurrency, contains a message-passing component: handlers execute messages from their mailboxes and can send messages to each other. We expect these messages to be delivered and handled in an order consistent with queue semantics: first-in-first-out (FIFO). We check, for a given trace, whether there is an order of sent and received messages that satisfies the semantics. Modern model checking solutions like dynamic partial order reduction (DPOR) can use these results to extend their tools to the event-driven model.

We provide a restatement of the problem that is suitable for extending existing model checking algorithms to support event-driven models. We show that the problem is NP-complete. We also present and implement an algorithm.

In the third contribution, we focus on the concurrent systems themselves. Memory systems such as cache protocols or distributed memory protocols rarely implement the conceptually simple model of sequential consistency: that a concurrent program acts equivalently to executing one operation at a time, interleaving the operations of each thread. Rather, they implement much weaker memory models. We consider a family of models known from the C11 memory model: Release-Acquire. This family consists of a relaxed version named Weak Release-Acquire (WRA), the standard version (RA), and a strong version (SRA). We consider the system verification problem for these models: given a memory system modeled as a register machine, do all executions of all programs executing on this system satisfy the corresponding memory semantics? We show that the problem can be solved in polynomial time for WRA, and PSPACE-complete for RA and SRA.