AbstractParallel 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.
RightsThis Item is protected by copyright and/or related rights.You are free to use this Item in any way that is permitted by the copyright and related rights legislation that applies to your use.For other uses you need to obtain permission from the rights-holder(s).