Skip to Main content Skip to Navigation
Conference papers

From Array Domains to Abstract Interpretation Under Store-Buffer-Based Memory Models

Thibault Suzanne 1 Antoine Miné 2
1 ANTIQUE - Analyse Statique par Interprétation Abstraite
DI-ENS - Département d'informatique de l'École normale supérieure, Inria Paris-Rocquencourt
2 APR - Algorithmes, Programmes et Résolution
LIP6 - Laboratoire d'Informatique de Paris 6
Abstract : We address the problem of verifying concurrent programs under store-buffer-based weakly consistent memory models, such as TSO or PSO. Using the abstract interpretation framework, we adapt existing domains for arrays to model store buffers and obtain a sound abstraction of program states (including the case of programs with infinite state space) parameterised by a numerical domain. Whereas the usual method for this kind of programs implements a program transformation to come back to an analysis under a sequentially consistent model, the novelty of our work consists in applying abstract interpretation directly on the source program, setting a clean foundation for special dedicated domains keeping information difficult to express with program transformations. We demonstrate the precision of this method on a few examples, tar-getting the TSO model and incidentally being also sound for PSO due to some specific abstraction choice. We discuss an application to fence removal and show that our implementation is usually able to remove as many or more fences, with respect to the state of the art, on concurrent algorithms designed for sequential consistency while still remaining precise enough to verify them.
Document type :
Conference papers
Complete list of metadata

Cited literature [20 references]  Display  Hide  Download
Contributor : Antoine Miné Connect in order to contact the contributor
Submitted on : Tuesday, September 6, 2016 - 10:10:09 AM
Last modification on : Wednesday, November 17, 2021 - 12:32:17 PM
Long-term archiving on: : Wednesday, December 7, 2016 - 12:35:27 PM


Files produced by the author(s)



Thibault Suzanne, Antoine Miné. From Array Domains to Abstract Interpretation Under Store-Buffer-Based Memory Models. SAS 2016 - 23rd Static Analysis Symposium, Sep 2016, Edinburgh, United Kingdom. pp.469-488, ⟨10.1007/978-3-662-53413-7_23⟩. ⟨hal-01360566⟩



Record views


Files downloads