Unfolding-based Dynamic Partial Order Reduction of Asynchronous Distributed Programs

The Anh Pham 1 Thierry Jéron 2 Martin Quinson 3
1 MYRIADS - Design and Implementation of Autonomous Distributed Systems
Inria Rennes – Bretagne Atlantique , IRISA-D1 - SYSTÈMES LARGE ÉCHELLE
2 SUMO - SUpervision of large MOdular and distributed systems
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
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.
Complete list of metadatas

Cited literature [19 references]  Display  Hide  Download

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


Files produced by the author(s)


Distributed under a Creative Commons Attribution 4.0 International License



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⟩



Record views


Files downloads