Document Type
Report
Date
9-1990
Keywords
colored Petri nets, deadlock detection, parallel programs, static analysis
Language
English
Disciplines
Computer Sciences
Description/Abstract
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.
Recommended Citation
Mansouri, N. and Goel, Amrit L., "A Colored Petri Net-Based Approach for Automated Deadlock Detection in Parallel Programs" (1990). Electrical Engineering and Computer Science - Technical Reports. 88.
https://surface.syr.edu/eecs_techreports/88
Source
local
Additional Information
School of Computer and Information Science, Syracuse University, SU-CIS-90-29