Revisiting Stateful Partial-Order Reduction
Fuente:
arXiv
Saved in:
| Main Authors: | , , , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866916495286599680 |
|---|---|
| author | Herbreteau, Frédéric Larroze-Jardiné, Sarah Point, Gérald Walukiewicz, Igor |
| author_facet | Herbreteau, Frédéric Larroze-Jardiné, Sarah Point, Gérald Walukiewicz, Igor |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2411_16921 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Revisiting Stateful Partial-Order Reduction Herbreteau, Frédéric Larroze-Jardiné, Sarah Point, Gérald Walukiewicz, Igor Logic in Computer Science 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. |
| title | Revisiting Stateful Partial-Order Reduction |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2411.16921 |