Improved Dynamic Partial-Order Reduction for Asynchronous Message-Passing Programs

This paper presents two algorithmic refinements that improve systematic testing of asynchronous message-passing programs for a fixed input. Such programs can have a large number of possible execution paths due to the nondeterministic interleaving of messages. However, many paths are equivalent, and dynamic partial-order reduction (DPOR) techniques attempt to explore all distinct, feasible behaviors while minimizing the number of redundant paths that are explored. Our two refinements never explore more redundant paths than the existing DPOR techniques for asynchronous message-passing programs. We implemented the refinements in the Basset tool, and experimental results show that they can reduce the number of redundant paths explored over existing DPOR techniques by up to two orders of magnitude.