FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
Quasi-Optimal Partial Order Reduction

Authors: Huyen T.T. Nguyen, Cesar Rodriguez, Marcelo Sousa, Camille Coti and Laure Petrucci

Paper Information

Title:Quasi-Optimal Partial Order Reduction
Authors:Huyen T.T. Nguyen, Cesar Rodriguez, Marcelo Sousa, Camille Coti and Laure Petrucci
Proceedings:CAV All Papers
Editors: Georg Weissenbacher, Hana Chockler and Igor Konnov
Keywords:Program analysis, Dynamic analysis, Partial-order reduction, Non-interleaving semantics
Abstract:

ABSTRACT. A dynamic partial order reduction (DPOR) algorithm is optimal when it always explores at most one representative per Mazurkiewicz trace. Existing literature suggests 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(2^n) redundant schedules and identify the cause of the blow-up 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 specialized data structures. Experiments with DPU, including Debian packages, show that optimality is achieved with low values of k, outperforming state-of-the-art tools.

Pages:18
Talk:Jul 17 14:30 (Session 121A: Concurrency)
Paper: