Document Type





da tasking, concurrent programs, deadlock detection, Petri net applications, race conditions, software testing, software tools, static analysis




Computer Sciences


A static analysis tool for detecting deadlocks and potential race conditions on shared variables in concurrent programs is presented. It is based on Petri Net modeling and reachability analysis, where a concurrent program is modeled as an augmented Petri net and a reachability graph is then derived and analyzed for desired information. Place-Transition subnets representing programming language constructs are described. Transitions in these subnets are augmented with sets of shared variables that occur in sections of the program, called concurrency zones, related to the transitions. The tool consists of four modules. The modeling module employs the augmented subnets as building blocks in translating only the synchronization-related statements of a concurrent program and connects the subnets to yield the total model. The second module produces an augmented reachability graph for the augmented Petri net. The analyzer module searches the augmented reachability graph for deadlocks, race conditions and other useful analysis information requested by the user about the underlying program. The user interface is provided by an X-window based module. Ada is used as a representative of concurrent languages that adopt the rendezvous model of interprocess communication and synchronization. The validation of the tool, its applicability and limitations are also discussed.

Additional Information

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





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.