Camille Coti, Sami Evangelista, Laure Petrucci: One-Sided Communications and Distributed State Compression for Distributed Model-Checking

Abstract:
Communications are often the bottleneck in distributed state space exploration. To overcome this problem and benefit from the distributed model-scheme, we propose to use one-sided communications. We thus revisit the state of the art distributed algorithm and adapt it to RDMA clusters with an implementation over the OpenSHMEM library. Experiments conducted on the Grid'5000 cluster show that this asynchronous approach reduces the significant communication costs induced by process synchronisation in two-sided communications.
To further improve distributed model checking, we propose a distributed implementation of the collapse compression technique used by explicit state model checkers to reduce memory usage. This adapatation makes use of lock-free distributed hash tables based on one-sided communication primitives. The experiments reveal that, for some models, this distributed implementation can altogether preserve the memory reduction provided by collapse compression and reduce execution times by allowing the exchanges of compressed states between processes.