Parameterized Model Checking on the TSO Weak Memory Model
- PDF / 624,747 Bytes
- 24 Pages / 439.37 x 666.142 pts Page_size
- 31 Downloads / 215 Views
Parameterized Model Checking on the TSO Weak Memory Model Sylvain Conchon1,2 · David Declerck3
· Fatiha Zaïdi1
Received: 5 May 2020 / Accepted: 11 May 2020 © Springer Nature B.V. 2020
Abstract We present an extended version of the model checking modulo theories framework for verifying parameterized systems under the TSO weak memory model. Our extension relies on three main ingredients: (1) an axiomatic theory of the TSO memory model based on relations over (read, write) events, (2) a TSO-specific backward reachability algorithm and (3) an SMT solver for reasoning about TSO formulas. One of the main originality of our work is a partial order reduction technique that exploits specificities of the TSO memory model. We have implemented this framework in a new version of the Cubicle model checker called Cubicle-W . Our experiments show that Cubicle-W is expressive and efficient enough to automatically prove safety of concurrent algorithms, for an arbitrary number of processes, ranging from mutual exclusion to synchronization barriers translated from actual x86-TSO implementations. Keywords Parameterized model checking · MCMT · SMT · Weak memory · Partial order reduction
1 Introduction Concurrent algorithms are usually designed under the sequential consistency (SC) memory model [24] which enforces a global-time linear ordering of (read or write) accesses to shared memories. However, modern multiprocessor architectures do not follow this SC semantics.
Work supported by the French ANR Project PARDI (ANR-16-CE25-0006).
B
David Declerck [email protected] Sylvain Conchon [email protected] Fatiha Zaïdi [email protected]
1
LRI (CNRS & Univ. Paris-Sud), Université Paris-Saclay, 91405 Orsay, France
2
Inria, Université Paris-Saclay, 91120 Palaiseau, France
3
OCamlPro, 91190 Gif-sur-Yvette, France
123
S. Conchon et al.
Instead, they implement several optimizations which lead to relaxed consistency models on shared memory where read and write operations may be reordered. For instance, in x86-TSO [25,26] writes can be delayed after reads due to a store buffering mechanism. Other relaxed models (PowerPC [6], ARM) allow even more types of reorderings. The new behaviors induced by these models may make out-of-the-shelf algorithms incorrect for subtle reasons mixing interleaving and reordering of events. In this context, finding bugs or proving the correctness of concurrent algorithms is very challenging. The challenge is even more difficult if we consider that most algorithms are parameterized, that is designed to be run on architectures containing an arbitrary (large) number of processors and manipulating an arbitrary number of variables. One of the most efficient technique for verifying concurrent systems is model checking. While this technique has been used to verify parameterized algorithms [1,3,4,10,13,19] and systems under some relaxed memory assumptions [1,2,7,11,12], hardly any state-of-the-art model checker supports both parameterized verification and weak memory models (the only exception we c
Data Loading...
