We are happy to present Sarah Larroze-Jardiné’s talk titled “Partial-Order Reduction is Hard”.
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.
In the last decade, optimality has been a guiding principle for developing stateless partial-order reduction algorithms, and without doubt contributed to a big progress in the field. In this paper we ask if we can get a similar principle for the stateful approach. We show that in stateful exploration, a polynomially close to optimal partial-order algorithm cannot exist unless P=NP. The result holds even for acyclic programs with just await instructions. This lower bound result justifies systematic study of heuristics for stateful partial-order reduction. We propose a notion of IFS oracle as a useful abstraction. The oracle can be used to get a very simple optimal stateless algorithm, which can then be adapted to a non-optimal stateful algorithm. While in general the oracle problem is NP-hard, we show a simple case where it can be solved in linear time.
Sarah Larroze-Jardiné is a PhD Student at LaBRI, Bordeaux. She is supervised by Igor Walukiewicz and Frédéric Herbreteau and will defend her thesis in December. The subject of her PhD is “Stateful partial-order reduction methods for concurrent systems with blocking instructions”