13th International Symposium on Software Reliability Engineering (ISSRE'02)
Blocking-based Simultaneous Reachability Analysis of Asynchronous Message-passing Programs
Annapolis, Maryland
November 12-November 15
ISBN: 0-7695-1763-3
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 receive operation. Global states reached by such executions from g are called next blocking points of g.Foreach 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 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.
Citation:
Yu Lei, Kuo-Chung Tai, "Blocking-based Simultaneous Reachability Analysis of Asynchronous Message-passing Programs," issre, pp.316, 13th International Symposium on Software Reliability Engineering (ISSRE'02), 2002