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

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

File

Forte_paper.pdf
Files produced by the author(s)

Licence


Distributed under a Creative Commons Attribution 4.0 International License

Identifiers

Citation

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⟩

Share

Metrics

Record views

121

Files downloads

177