Automated Verification of Algorithms under Weak Memory Models

Motivation

Shared-memory multiprocessor architectures are now ubiquitous. For performance reasons, most contemporary multiprocessors implement relaxed memory consistency models. Such memory models relax the ordering guarantees of memory accesses. For example, the most common relaxation is that writes to shared memory may be delayed past subsequent reads from memory. This write-to-read relaxation is commonly attributed to store buffers between each processor and the main memory. The corresponding memory model is historically called TSO, for Total-Store-Order. Similarly, many models relax under certain conditions read-to-read order, read-to-write order, and write-to-write order.

Programmers usually assume that program instructions from different threads will be executed in an interleaved manner, all accesses to the shared memory are performed instantaneously and atomically, which is guaranteed only by the strongest memory model, Sequential Consistency (SC). Nevertheless, this assumption is in fact safe for most programs. The reason is that the recommended methodology for programming shared memory (namely, to use threads and locks in such a manner as to avoid data races) is usually sufficient to hide the effect of memory ordering relaxations. This effect is known as the DRF guarantee, because it applies to data-race-free programs.

However, while very useful for mainstream programs, the DRF guarantee does not apply in all situations. For one, the implementors of the synchronization operations need to be fully aware of the hardware relaxations to ensure sufficient ordering guarantees (it is their responsibility to uphold the DRF guarantee). For example, Dekker's mutual exclusion protocol does not function correctly on TSO architectures. Secondly, many concurrency libraries and other performance-critical system services (such as garbage collectors) bypass conventional locking protocol and employ lock-free synchronization techniques instead. Such algorithms need to be aware of the memory model. They may either be immune to the relaxations by design, or contain explicit memory ordering fences to prevent them. Most algorithms choose the latter option; however, two recent implementations of a work-stealing queue are using algorithms that are specifically written to perform well on TSO architectures without requiring fences.

Reasoning about the behavior of such algorithms on relaxed memory models is much more difficult than for sequentially consistent memory, and it is not clear how to apply standard reasoning techniques or finite-state abstractions. Furthermore bugs introduced by weak memory model instruction reordering are frequently very hard to find by testing, since their manifestations may be rare and unpredictable. This highlights the need (1) for more research on automatic verification techniques for programs on relaxed memory models and (2) for automated tools that can prove correctness (or incorrectness) of algorithms under weak memory models!

Long Term Goal

The goals of the project is developing formal semantics for various weak memory models and solving their verification problems. Indeed, there are a variety of memory models, and a formal framework for defining their semantics and studying the decidability of their verification problems is necessary.

A long-term challenge is the development of tools for the automatic verification and correction for various memory models. This tool should be based on the use of scalable techniques for the exact or approximative analysis of the verification problems for weak memory models.

Achievements

In [Atig et al., POPL 2010], we showed that the reachability problem is decidable for TSO and for an extension of TSO with the write-to-write order relaxation, but beyond these models nothing is known to be decidable. Moreover, we proved that relaxing the program order by allowing reads or writes to overtake reads leads to undecidability. Furthermore, we showed that the the repeated reachability problem for TSO, PSO and RMO are all undecidable.

In [Leonardsson, M.Sc. Thesis], we developed an efficient but incomplete method for model checking programs under TSO in a thread-modular fashion. The method models the reorderings of TSO by a successive rewriting of the program source code, rather than explicitly modelling write buffers.

In [Atig et al. CAV'2011], we proposed an approach for reducing the TSO reachability analysis of concurrent programs to their SC reachability analysis, under some conditions on the explored behaviors. First, we proposed a linear code-to-code translation that takes as input a concurrent program P and produces a concurrent program P' such that, running P' under SC yields the same set of reachable (shared) states as running P under TSO with at most k context-switches for each thread, for a fixed k. Experimental results show that bugs due to TSO can be detected with small bounds, using off-the-shelf SC analysis tools.

Current Work

We developed a prototype for the reachability analysis of concurrent programs running under the weak memory model TSO. We used a scalable verification technique for concurrent programs under TSO to automatically infer a minimal set of memory barriers necessary for ensuring particular safety properties for the analyzed algorithms. We are aiming towards extending our work to handle weaker memory models such as RMO and PowerPC by developing scalable verification techniques based on accurate upper or under approximations.

We are also working on include extensions that concern algorithms working with unbounded data (e.g. counters, dynamic memory management, ...) or an unbounded number of threads.

On the other side, we are working on defining formal semantics for various weak memory models and refining the results of [Atig et al., POPL 2010] by sharpening the (un)decidability frontiers.

Approach

The reordering of a weak memory model is a source of infinity for the state space of an algorithm. I.e., even an algorithm which under sequential consistency has a finite state space may (and in most cases will) have an infinite state space under a weak memory model. To address this problem we make use of the well-structured transition systems framework. In order for this to work we have defined an alternative model (the SB model) which is equivalent to TSO with respect to reachability, but has a natural ordering which is monotonic with respect to the program transitions.

Publications

Staff

Senior: Parosh Abdulla (Contact), Bengt Jonsson, Mohamed Faouzi Atig,
Ph.D. students: Carl Leonardsson