An Investigation of Models of Concurrent Programs

Reynolds has proposed an interesting new approach to verifying concurrent programs, called static incremental deadlock detection, where deadlock potential is automatically detected during the interactive construction of a concurrent program, before the program is ever run. In order to perform efl"ective
static incremental deadlock detection. we will require accurate models that can be analyzed efficiently. Towards this end. we investigate three existing classes of models: algebraic models, geometric models, and Petri net models. We report new results related to the accuracy of algebraic and geometric models, and we report new results on the efficient analysis of Petri net models. Finally, we use our results to derive a technique for performing elfective static incremental deadlock detection on a subclass of concurrent programs.
Note: Abstract extracted from PDF file via OCR

OHallaron, David, and Paul Reynolds. "An Investigation of Models of Concurrent Programs." University of Virginia Dept. of Computer Science Tech Report (1986).