Quasi-Optimal Partial Order Reduction

TL;DR

This paper introduces Quasi-Optimal Partial Order Reduction, a method that approximates optimal exploration in model checking with low overhead, outperforming existing tools on complex software systems.

Contribution

The paper presents a novel Quasi-Optimal POR approach that approximates optimal exploration within a tunable parameter, improving over state-of-the-art algorithms.

Findings

SDPOR can explore exponentially more schedules than optimal DPOR on certain programs.

The NP-hardness of the problem explains the blow-up in redundant schedules.

Experiments show low k values suffice for near-optimal exploration, outperforming existing tools.

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 $\mathop{\mathcal{O}}(n)$ Mazurkiewicz traces where SDPOR explores $\mathop{\mathcal{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 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.