One-Sided Communications for More Efficient Parallel State Space Exploration over RDMA Clusters

Abstract

This paper investigates the use of one-sided communications in the context of state space exploration. This operation is often the core component of model checking tools that explores a system state space to look for behaviours deviating from its specification. It basically consists in the exploration of a (usually huge) directed graph whose nodes and edges represent respectively system states and system changes. We revisit the state of the art distributed algorithm and adapt it to RDMA clusters with an implementation over the OpenSHMEM library and report on preliminary experiments conducted on the Grid’5000 cluster. This asynchronous approach thus reduces the significant communication costs induced by process synchronisation in two-sided communications.