On the Verification Problem for Weak Memory Models

Mohamed Faouzi Atig, Ahmed Bouajjani, Sebastian Burckhardt, and Madanlal Musuvathi

Abstract

We address the verification problem of finite-state concurrent programs

running under weak memory models. These models capture

the reordering of program (read and write) operations done by modern

multi-processor architectures for performance. The verification

problem we study is crucial for the correctness of concurrency libraries

and other performance-critical system services employing

lock-free synchronization, as well as for the correctness of compiler

backends that generate code targeted to run on such architectures.

We consider in this paper combinations of three well-known

program order relaxations. We consider first the “write to read”

relaxation, which corresponds to the TSO (Total Store Ordering)

model. This relaxation is used in most hardware architectures available

today. Then, we consider models obtained by adding either (1)

the “write to write” relaxation, leading to a model which is essentially

PSO (Partial Store Ordering), or (2) the “read to read/write”

relaxation, or (3) both of them, as it is done in the RMO (Relaxed

Memory Ordering) model for instance.

We define abstract operational models for these weak memory

models based on state machines with (potentially unbounded) FIFO

buffers, and we investigate the decidability of their reachability and

their repeated reachability problems.

We prove that the reachability problem is decidable for the TSO

model, as well as for its extension with “write to write” relaxation

(PSO). Furthermore, we prove that the reachability problem

becomes undecidable when the “read to read/write” relaxation is

added to either of these two memory models, and we give a condition

under which this addition preserves the decidability of the

reachability problem. We show also that the repeated reachability

problem is undecidable for all the considered memory models.

Details

Publication typeInproceedings
Published inProceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
PublisherAssociation for Computing Machinery, Inc.
> Publications > On the Verification Problem for Weak Memory Models