Blocking-based simultaneous reachability analysis of asynchronous message-passing programs

Existing reachability analysis techniques for asynchronous message-passing programs assume causal communication, which means that messages sent to a destination are received in the order they are sent. In this paper we present a new reachability analysis approach, called blocking-based simultaneous reachability analysis (BSRA). BSRA can be applied to asynchronous message-passing programs based on any communication scheme. From a global state g, BSRA allows processes to proceed simultaneously until each of them terminates or is ready to execute a receive operation. Global states reached by such executions from g are called next blocking points of g. For each next blocking point of g, waiting messages and receive operations are matched to produce immediate BSRA-based successor states of g. Intermediate global states from g to each of g's immediate BSRA-based successors are not saved. We describe an algorithm for generating BSRA-based reachability graphs and show that this algorithm guarantees the detection of deadlocks. Our empirical results indicate that BSRA significantly reduces the number of states in reachability graphs. Extensions of BSRA for partial order reduction and model checking are discussed.