Stateless Model Checking for TSO and PSO
| Autor: | Mohamed Faouzi Atig, Konstantinos Sagonas, Stavros Aronis, Carl Leonardsson, Parosh Aziz Abdulla, Bengt Jonsson |
|---|---|
| Jazyk: | angličtina |
| Rok vydání: | 2015 |
| Předmět: |
Model checking
FOS: Computer and information sciences Computer Science - Logic in Computer Science Theoretical computer science Relation (database) Computer Networks and Communications Computer science D.1.3 D.2.4 F.3.1 02 engineering and technology Parallel computing 0202 electrical engineering electronic engineering information engineering Representation (mathematics) Standard model (cryptography) POSIX Threads Sequential consistency Computer Sciences 020207 software engineering Logic in Computer Science (cs.LO) Partial order reduction Datavetenskap (datalogi) Theory of computation 020201 artificial intelligence & image processing Software Information Systems |
| Popis: | We present a technique for efficient stateless model checking of programs that execute under the relaxed memory models TSO and PSO. The basis for our technique is a novel representation of executions under TSO and PSO, called chronological traces. Chronological traces induce a partial order relation on relaxed memory executions, capturing dependencies that are needed to represent the interaction via shared variables. They are optimal in the sense that they only distinguish computations that are inequivalent under the widely-used representation by Shasha and Snir. This allows an optimal dynamic partial order reduction algorithm to explore a minimal number of executions while still guaranteeing full coverage. We apply our techniques to check, under the TSO and PSO memory models, LLVM assembly produced for C/pthreads programs. Our experiments show that our technique reduces the verification effort for relaxed memory models to be almost that for the standard model of sequential consistency. This article is an extended version of Abdulla et al. (Tools and algorithms for the construction and analysis of systems, Springer, New York, pp 353–367, 2015), appearing in TACAS 2015. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|