Static deadlock detection in polynomial time

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.
--

Return to the comp.compilers page.
Search the comp.compilers archives again.