Skip to Main content Skip to Navigation
Conference papers

Relational Thread-Modular Abstract Interpretation Under Relaxed Memory Models

Abstract : We address the verification problem of numeric properties in many-threaded concurrent programs under weakly consistent memory models, especially TSO. We build on previous work that proposed an abstract interpretation method to analyse these programs with rela-tional domains. This method was not sufficient to analyse more than two threads in a decent time. Our contribution here is to rely on a rely-guarantee framework with automatic inference of thread interferences to design an analysis with a thread-modular approach and describe re-lational abstractions of both thread states and interferences. We show how to adapt the usual computing procedure of interferences to the additional issues raised by weakly consistent memories. We demonstrate the precision and the performance of our method on a few examples, operating a prototype analyser that verifies safety properties like mutual exclusion. We discuss how weak memory models affect the scalability results compared to a sequentially consistent environment.
Document type :
Conference papers
Complete list of metadata

Cited literature [20 references]  Display  Hide  Download
Contributor : Thibault Suzanne Connect in order to contact the contributor
Submitted on : Wednesday, December 12, 2018 - 7:29:57 PM
Last modification on : Wednesday, June 8, 2022 - 12:50:03 PM
Long-term archiving on: : Wednesday, March 13, 2019 - 3:53:51 PM


Files produced by the author(s)



Thibault Suzanne, Antoine Miné. Relational Thread-Modular Abstract Interpretation Under Relaxed Memory Models. APLAS 2018 - 16th Asian Symposium on Programming Languages and Systems, Dec 2018, Wellington, New Zealand. pp.109-128, ⟨10.1007/978-3-030-02768-1_6⟩. ⟨hal-01953358⟩



Record views


Files downloads