Effect-Polymorphic Behaviour Inference for Deadlock Checking


We present a constraint-based effect inference algorithm for deadlock checking. The static analysis is developed for a concurrent calculus with higherorder functions and dynamic lock creation. The analysis is context-sensitive and locks are summarised based on their creation-site. The resulting effects can be checked for deadlocks using state space exploration. We use a specific deadlocksensitive simulation relation to show that the effects soundly over-approximate the behaviour of a program, in particular that deadlocks in the program are preserved in the effects.

Proceedings of the 12th International Conference on Software Engineering and Formal Methods