On exploring even reachable global state space to verify deadlock freedom of protocols.

Abstract

During the fourth international conference on computer communications and networks (ICCCN), which was held in Las Vegas in September 1995, Peng introduced another relief strategy for reachability analysis, called even reachability analysis. In the proceedings of ICCCN'95, Peng also attempts to prove that deadlock freedom of any n-process protocol with arbitrary topology is verifiable by even reachability analysis with more than one-half reduction in generated global states. This thesis reviews the Peng strategy and proves that the selected set of transition pairs is not sufficient to reach all deadlock states in an n-process protocol with arbitrary topology. Hence, deadlock freedom of the protocol is not verifiable by the Peng strategy for even reachability analysis. This thesis then forms an extended set of transition pairs to explore the entire even reachable global state space in a finite sequentially reachable global state space. Finally, the ideas of even reachability analysis are visited again and compared with existing relief strategies. (Abstract shortened by UMI.)