Authors: Elvira Albert, Miguel Gomez-Zamalloa, Miguel Isabel and Albert Rubio
Paper Information
Title: | Constrained Dynamic Partial Order Reduction |
Authors: | Elvira Albert, Miguel Gomez-Zamalloa, Miguel Isabel and Albert Rubio |
Proceedings: | CAV All Papers |
Editors: | Georg Weissenbacher, Hana Chockler and Igor Konnov |
Keywords: | Dynamic Partial Order Reduction, Conditional Independence, SMT, Static Analysis, Model Checking |
Abstract: | ABSTRACT. The cornerstone of dynamic partial order reduction (DPOR) is the notion of independence that is used to decide whether each pair of concurrent events p and t are in a race and thus both p.t and t.p must be explored. We present constrained dynamic partial order reduction (CDPOR), an extension of the DPOR framework which is able to avoid redundant explorations based on the notion of conditional independence --the execution of p and t commutes only when certain independence constraints (ICs) are satisfied. ICs can be declared by the programmer, but importantly, we present a novel SMT-based approach to automatically synthesize ICs in a static pre-analysis. A unique feature of our approach is that we have succeeded to exploit ICs within the state-of-the-art DPOR algorithm, achieving exponential reductions over existing implementations. |
Pages: | 17 |
Talk: | Jul 17 15:00 (Session 121A: Concurrency) |
Paper: |