loading...
Blocking-based Simultaneous Reachability Analysis of Asynchronous Message-passing Programs
Annapolis, Maryland November 12-November 15
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/ISSRE.2002.117327913th International Symposium on Softw ...
 This Article 
 
PDF
HTML
 
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Yu Lei, The University of Texas at Arlington
Kuo-Chung Tai, North Carolina State University
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
Usage of this product signifies your acceptance of the Terms of Use.