Abstract : Unfolding-based Dynamic Partial Order Reduction (UDPOR) is a recent technique mixing Dynamic Partial Order Reduction (DPOR) with concepts of concurrency such as unfoldings to efficiently mitigate state space explosion in model-checking of concurrent programs. It is optimal in the sense that each Mazurkiewicz trace, i.e. a class of interleavings equivalent by commuting independent actions, is explored exactly once. This paper shows that UDPOR can be extended to verify asynchronous distributed applications, where processes both communicate by messages and synchronize on shared resources. To do so, a general model of asynchronous distributed programs is formalized in TLA+. This allows to define an independence relation, a main ingredient of the unfolding semantics. Then, the adaptation of UDPOR, involving the construction of an unfolding, is made efficient by a precise analysis of dependencies. A prototype implementation gives promising experimental results.
https://hal.inria.fr/hal-02109769
Contributor : The Anh Pham
<>
Submitted on : Thursday, April 25, 2019 - 10:02:54 AM
Last modification on : Saturday, October 12, 2019 - 1:28:07 AM
Long-term archiving on : Friday, July 26, 2019 - 12:34:29 PM
The Anh Pham, Thierry Jéron, Martin Quinson. Unfolding-based Dynamic Partial Order Reduction of Asynchronous Distributed Programs. 39th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE), Jun 2019, Copenhagen, Denmark. pp.224-241, ⟨10.1007/978-3-030-21759-4_13⟩. ⟨hal-02109769⟩
