Revisiting Stateful Partial-Order Reduction

TL;DR

This paper revisits stateful partial-order reduction for concurrent systems with blocking operations, establishing theoretical limits and proposing a practical heuristic algorithm with experimental validation.

Contribution

It introduces a simple trace-optimal algorithm with an oracle, proves a complexity lower bound, and presents a practical heuristic algorithm with implementation and evaluation.

Findings

A trace-optimal algorithm with an NP-hard oracle is identified.

No polynomially close to optimal algorithm exists unless P=NP.

A practical heuristic algorithm surpassing standard approaches is developed and tested.

Abstract

The goal of partial-order methods is to accelerate the exploration of concurrent systems by examining only a representative subset of all possible runs. The stateful approach builds a transition system with representative runs, while the stateless method simply enumerates them. The stateless approach may be preferable if the transition system is tree-like; otherwise, the stateful method is more effective. We focus on a stateful method for systems with blocking operations, like locks. First, we show a simple algorithm with an oracle that is trace-optimal if used as a stateless algorithm. The algorithm is not practical, though, as the oracle uses an NP-hard test. Next, we present a significant negative result showing that in stateful exploration with blocking, a polynomially close to optimal partial-order algorithm cannot exist unless P=NP. This lower bound result justifies looking for heuristics for our simple algorithm with an oracle. As the third contribution, we present a practical algorithm going beyond the standard stubborn/persistent/ample set approach. We report on the implementation and evaluation of the algorithm.