DPOR-DS: Dynamic Partial Order Reduction in Distributed Systems
In this paper, we present DPOR-DS, an algorithm for dynamic partial order reduction in model checking of distributed systems. This work is inspired by the techniques introduced in the seminal work of DPOR which is designed for multi-threaded systems. Different characteristics between distributed systems and multi-threaded systems raises new challenges for implementing the idea in distributed system domain. By developing techniques to address those challenges, we prove the soundness and completeness of DPOR-DS. The performance of DPOR-DS is then compared to exhaustive search and state-of-the-art heuristics. The experimental results show that even though dynamic partial order reduction can alleviate the exponential explosion problem of state space exploration algorithms, the exponential growth still shows up after some certain steps.