Static deadlock detection in polynomial time

Static deadlock detection in polynomial time

[igor.rutgers.edu!cadenza.rutgers.edu!masticol]

Hi, all,

My thesis, "Static Detection of Deadlocks in Polynomial Time," is now
available by anonymous FTP:

	Host:		cs.rutgers.edu
	Directory:	/pub/technical-reports
	Files:		lcsr-tr-208.abstract, lcsr-tr-208.ps.Z

The abstract follows. Thanks for your interest!

- Steve Masticola (masticol@cs.rutgers.edu)

-=-=-
	   Static Detection of Deadlocks in Polynomial Time

			 Stephen P. Masticola
			       May 1993

Parallel and distributed programming languages often include explicit
synchronization primitives, such as rendezvous and semaphores. Such
programs are subject to synchronization anomalies; the program behaves
incorrectly because it has a faulty synchronization structure. A
deadlock is an anomaly in which some subset of the active tasks of the
program mutually wait on each other to advance; thus, the program
cannot complete execution.

In static anomaly detection, the source code of a program is
automatically analyzed to determine if the program can ever exhibit a
specific anomaly. Static anomaly detection has the unique advantage
that it can certify programs to be free of the tested anomaly; dynamic
testing cannot generally do this. Though exact static detection of
deadlocks is NP-hard [Taylor, 1983], many researchers have tried to
detect deadlock by exhaustive enumeration of synchronization states,
using Petri nets or other program representations.  In practice,
programs often have large enough state spaces to render this approach
impractical.

Our approach, rather, is to make an approximate analysis of the
program in time polynomial in the size of the source code. Our
approximation is safe: if we certify a program free of deadlock, it
will never deadlock. We do this using iterative flow analysis
techniques to detect (but not enumerate) "deadlock cycles" in the
program's control and synchronization structure. We identify four
constraints on deadlock cycles which we use to prune invalid cycles,
thus avoiding false alarms. One pruning method uses a "can't happen
together" relation between statements; we show how such information
can be found, and how it may be of value in other analyses.

We have implemented our analysis for the rendezvous synchronization of
the Ada language, and have tested it on over 100 programs obtained
from government and industrial sources. We demonstrate that our
technique is quite accurate compared to exhaustive state generation;
few false alarms are seen in practice. Our technique is also well
behaved in execution time, running faster than the exhaustive
technique for all programs except those with the simplest state
spaces.

To demonstrate the generality of our methods, we show preliminary
algorithms for detecting deadlock in two very different
synchronization paradigms: binary semaphores, and the dynamic,
pointer-based process control of Concurrent C.