Optimal dynamic partial order reduction with observers
| Autor: | Konstantinos Sagonas, Bengt Jonsson, Stavros Aronis, Magnus Lång |
|---|---|
| Jazyk: | angličtina |
| Rok vydání: | 2018 |
| Předmět: |
Soundness
Model checking Theoretical computer science Computer science Computer Sciences Concurrency Message passing 020207 software engineering 02 engineering and technology Partial order reduction Datavetenskap (datalogi) Shared memory 020204 information systems 0202 electrical engineering electronic engineering information engineering Observability Combinatorial explosion |
| Zdroj: | Tools and Algorithms for the Construction and Analysis of Systems ISBN: 9783319899626 TACAS (2) |
| Popis: | Dynamic partial order reduction (DPOR) algorithms are used in stateless model checking (SMC) to combat the combinatorial explosion in the number of schedulings that need to be explored to guarantee soundness. The most effective of them, the Optimal DPOR algorithm, is optimal in the sense that it explores only one scheduling per Mazurkiewicz trace. In this paper, we enhance DPOR with the notion of observability, which makes dependencies between operations conditional on the existence of future operations, called observers. Observers naturally lead to a lazy construction of dependencies. This requires significant changes in the core of POR algorithms (and Optimal DPOR in particular), but also makes the resulting algorithm, Optimal DPOR with Observers, super-optimal in the sense that it explores exponentially less schedulings than Mazurkiewicz traces in some cases. We argue that observers come naturally in many concurrency models, and demonstrate the performance benefits that Optimal DPOR with Observers achieves in both an SMC tool for shared memory concurrency and a tool for concurrency via message passing, using both synthetic and actual programs as benchmarks. UPMARC |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|