Document Type





colored Petri nets, deadlock detection, parallel programs, static analysis




Computer Sciences


A static analysis approach is proposed for automated detection of deadlocks in a common class of parallel programs, referred to as Single Code Multiple Data (SCMD) programs. It is based on colored Petri net (CP-net) modeling and reachability analysis, where colors correspond to parallel processes. An SCMD program is first translated into a CP-net and a reachability tree is then derived and analyzed for deadlock information. CP-subnets representing basic programming language constructs are described. These subnets are employed as building blocks by an algorithm that translates synchronization-related statements of a process in an SCMD program and connects the resulting subnets. The connection technique makes use of the characteristics of SCMD programs to produce a unified and folded CP-net model. These characteristics are also used to introduce a notion, referred to as poset-covering, that leads to a reduced reachability tree for the Cp-net. The usual algorithm for generating and analyzing reachability trees of CP-nets is modified by including poset-covering and excluding notions that are irrelevant to our application. The compactness of the CP-net model and the reachability tree makes the proposed approach appealing for practical implementation.

Additional Information

School of Computer and Information Science, Syracuse University, SU-CIS-90-29





To view the content in your browser, please download Adobe Reader or, alternately,
you may Download the file to your hard drive.

NOTE: The latest versions of Adobe Reader do not support viewing PDF files within Firefox on Mac OS and if you are using a modern (Intel) Mac, there is no official plugin for viewing PDF files within the browser window.