Quasi-optimal partial order reduction
- PDF / 762,665 Bytes
- 31 Pages / 439.37 x 666.142 pts Page_size
- 56 Downloads / 198 Views
Quasi-optimal partial order reduction Camille Coti1 · Laure Petrucci1
· César Rodríguez1,3 · Marcelo Sousa2
Received: 26 June 2019 / Accepted: 22 September 2020 © Springer Science+Business Media, LLC, part of Springer Nature 2020
Abstract A dynamic partial order reduction (DPOR) algorithm is optimal when it always explores at most one representative per Mazurkiewicz trace. Existing literature suggests that the reduction obtained by the non-optimal, state-of-the-art Source-DPOR (SDPOR) algorithm is comparable to optimal DPOR. We show the first program with O(n) Mazurkiewicz traces where SDPOR explores O(2n ) redundant schedules. We furthermore identify the cause of this blowup as an NP-hard problem. Our main contribution is a new approach, called Quasi-Optimal POR, that can arbitrarily approximate an optimal exploration using a provided constant k. We present an implementation of our method in a new tool called Dpu using specialised data structures. Experiments with Dpu, including Debian packages, show that optimality is achieved with low values of k, outperforming state-of-the-art tools. Keywords Program analysis · Dynamic analysis · Partial-order reduction · Non-interleaving semantics
1 Introduction Dynamic partial-order reduction (DPOR) [1,17,31] is a mature approach to mitigate the state explosion problem in model checking of multithreaded programs. DPORs are based on Mazurkiewicz trace theory [22], a true-concurrency semantics where the set of executions of the program is partitioned into equivalence classes known as Mazurkiewicz traces (M-traces).
An independently and concurrently discovered example program with the same characteristics is presented in [4].
B
Laure Petrucci [email protected] Camille Coti [email protected] Marcelo Sousa [email protected]
1
LIPN, CNRS UMR 7030, Université Sorbonne Paris Nord, Villetaneuse, France
2
University of Oxford, Oxford, UK
3
Diffblue Ltd, Oxford, UK
123
Formal Methods in System Design w0 x0 = 7
w1 x1 = 8
w2 x2 = 9
count c=1 c=2
(a) w0
w1
w3 i = 0
w1
w2 i = 0
w0
w1
master i=c xi = 0 w2 c = 1
x0 = 0 c=1
c=1
i=1
w0
w2 c = 1
w0
x1 = 0 i = 1
w1
w2 c = 1
w1 c = 1 i=2
c=2
c=2
x0 = 0
(b)
w0
c=2
w0
c=2
x1 = 0
c=2
w1
c=2
x2 = 0
i=2
x2 = 0
w2
Fig. 1 a Programs, b partially-ordered executions
In a DPOR, this partitioning is defined by an independence relation over concurrent actions. Two actions are independent if executing one of them does neither enable nor disable the other one, and their execution order does not change the overall result. The independence relation is computed dynamically and DPOR explores executions which are representatives of M-traces. The exploration is sound when it explores all M-traces, and it is considered optimal [1] when it explores each M-trace only once. Since two independent actions might have to be explored from the same state in order to explore all M-traces, a DPOR algorithm uses independence to compute a provably-sufficient subset of the enabled transi
Data Loading...
