Deadlock analysis of client/server programs

Deadlocks are a common type of fault in distributed programs. To detect deadlocks in a distributed program P, one approach is to construct the reachability graph (RG) of P, which contains all possible states of P, and analyze the RG to detect deadlocks. Since the size of RG(P) is an exponential function of the number of processes in P, the use of RG for deadlock detection has limited success. In this paper, we show an efficient technique for deadlock analysis of client/server programs. We present a theory of deadlock analysis of client/server LTS systems, in which a server or client is represented as a labeled transition system (LTS). For a client/server LTS system, we define its client/server reachability graph (CSRG), which has its size being a polynomial function of the number of clients. We show that the use of CSRG not only significantly reduces the effort for deadlock analysis but also provides a basis for proving freedom from deadlock for any number of clients