Behaviour Inference for Deadlock Checking

Abstract

This paper extends our behavioural type and effect system for detecting deadlocks by polymorphism and formalizing type inference (with respect to lock types). Our inference is defined for a simple concurrent, first-order language. From the inferred effects, after suitable abstractions to keep the state space finite, we either obtain the verdict that the program will not deadlock, or that it may deadlock. We show soundness and completeness of the type inference.

Publication
Proceedings of the 8th International Symposium on Theoretical Aspects of Software Engineering
Date
Links