A Pragmatic Approach to Stateful Partial Order Reduction

TL;DR

This paper introduces new, more efficient algorithms for stateful partial order reduction in model checking, focusing on overall performance rather than theoretical optimality, and evaluates them within Java Pathfinder for concurrent data structures.

Contribution

It proposes practical algorithms based on source sets that improve overall performance of model checking by reducing computational overhead.

Findings

New algorithms outperform existing methods in efficiency.

Source set-based POR reduces overhead in verifying concurrent data structures.

Implementation in Java Pathfinder demonstrates practical benefits.

Abstract

Partial order reduction (POR) is a classic technique for dealing with the state explosion problem in model checking of concurrent programs. Theoretical optimality, i.e., avoiding enumerating equivalent interleavings, does not necessarily guarantee optimal overall performance of the model checking algorithm. The computational overhead required to guarantee optimality may by far cancel out any benefits that an algorithm may have from exploring a smaller state space of interleavings. With a focus on overall performance, we propose new algorithms for stateful POR based on the recently proposed source sets, which are less precise but more efficient than the state of the art in practice. We evaluate efficiency using an implementation that extends Java Pathfinder in the context of verifying concurrent data structures.