On the Verification Problem for Weak Memory Models

14 years 1 months ago
On the Verification Problem for Weak Memory Models
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 re...
Ahmed Bouajjani, Madanlal Musuvathi, Mohamed Faouz
Added 01 Mar 2010
Updated 02 Mar 2010
Type Conference
Year 2010
Where POPL
Authors Ahmed Bouajjani, Madanlal Musuvathi, Mohamed Faouzi Atig, Sebastian Burckhardt
Comments (0)