Revisiting Stateful Partial-Order Reduction

Abstract Partial-order methods accelerate the verification of concurrent programs. These methods are based on a concept of independence of actions, which induces an equivalence between different program runs. The equivalence allows for the construction of a reduced transition system that represents all runs up to this equivalence. Such a system can be orders of magnitude smaller than the full transition system representing all possible runs, while still containing all relevant information. We propose a new partial-order reduction method for concurrent acyclic programs that use variables and locks. Our algorithm is derived from first principles, suggesting it can be readily adapted to other settings. As our evaluation demonstrates, the algorithm offers substantial gains over existing partial-order methods.

Authors

• Frédéric Herbreteau
• Gérald Point
• Gautham Viswanathan
• Igor Walukiewicz

Keywords

No keywords are indexed for this paper.