Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Revisiting Stateful Partial-Order Reduction

Frédéric Herbreteau, Sarah Larroze-Jardiné, Gérald Point, Igor Walukiewicz

TL;DR

A significant negative result is presented showing that in stateful exploration with blocking, a polynomially close to optimal partial-order algorithm cannot exist unless P=NP, which justifies looking for heuristics for the simple algorithm with an oracle.

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.

Revisiting Stateful Partial-Order Reduction

TL;DR

A significant negative result is presented showing that in stateful exploration with blocking, a polynomially close to optimal partial-order algorithm cannot exist unless P=NP, which justifies looking for heuristics for the simple algorithm with an oracle.

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.

Paper Structure

This paper contains 18 sections, 16 theorems, 5 equations, 11 figures, 1 table.

Table of Contents

  1. Introduction
  2. Overview of the paper
  3. Related work
  4. Client/Server systems
  5. Partial-order reduction
  6. Source sets vs. persistent sets
  7. Lex-first exploration and $\mathit{IFS}$ oracle
  8. $\mathit{IFS}(s,B)$ test is NP-hard
  9. Partial-order reduction is $\NP$-hard
  10. Proof of Theorem \ref{['thm:por-impossible']}
  11. Approximating $\mathit{IFS}$ test
  12. Approximating $\mathit{IFS}$ with $\mathit{PIFS}$
  13. A new partial-order reduction algorithm
  14. A $\mathit{rPIFS}$ based $\text{closure}$ operation
  15. Choose an action from a closure
  16. ...and 3 more sections

Key Result

proposition 1

Let $\mathrm{TS}$ be a finite acyclic transition system with a transition relation $\act{}$. Suppose $\stackrel{}{\Longrightarrow}$ is the restricted transition relation derived from a "covering source set" assignment. For every state $s$ of $\mathrm{TS}$, and every "maximal run" $s\act{u}$ there is

Figures (11)

  • Figure 1: An example of a client/server system (left) with clients $P_b$ and $P_{ce}$, and servers $S_{ab}$, $S_e$ and $S_c$. Processes synchronize on common actions. Its semantics is defined by the transition system to the right.
  • Figure 2: A counterexample to Proposition \ref{['prop:source-covering']} in presence of infinite runs
  • Figure 3: A covering source set may not be a persistent set.
  • Figure 4: Sleep sets are needed for optimality
  • Figure 5: A client/server system with two optimal "transition systems", one of linear size and one of exponential size
  • ...and 6 more figures

Theorems & Definitions (54)

  • definition 1
  • definition 2: Client/Server system
  • definition 3
  • remark 1
  • definition 4
  • definition 5
  • proposition 1
  • proof
  • remark 2
  • remark 3
  • ...and 44 more