Mohamed Faouzi Atig, Ahmed Bouajjani, Sebastian Burckhardt, and Madanlal Musuvathi
20 January 2010
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.
In Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
Publisher Association for Computing Machinery, Inc.
Copyright © 2007 by the Association for Computing Machinery, Inc. Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, to republish, to post on servers, or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from Publications Dept, ACM Inc., fax +1 (212) 869-0481, or email@example.com. The definitive version of this paper can be found at ACM’s Digital Library --http://www.acm.org/dl/.