A framework for deadlock detection in core ABS

TL;DR

This paper introduces a modular framework for static deadlock detection in a concurrent object-oriented language with asynchronous calls, recursion, and dynamic resources, aiming to improve precision and scalability.

Contribution

It proposes a flexible framework combining various analysis techniques, including contract inference and back-end analysis, to enhance deadlock detection accuracy in complex language features.

Findings

Framework effectively combines multiple techniques for deadlock detection.

Contracts retain resource dependency info for analysis.

Proof-of-concept demonstrates improved deadlock detection methods.

Abstract

We present a framework for statically detecting deadlocks in a concurrent object-oriented language with asynchronous method calls and cooperative scheduling of method activations. Since this language features recursion and dynamic resource creation, deadlock detection is extremely complex and state-of-the-art solutions either give imprecise answers or do not scale. In order to augment precision and scalability we propose a modular framework that allows several techniques to be combined. The basic component of the framework is a front-end inference algorithm that extracts abstract behavioural descriptions of methods, called contracts, which retain resource dependency information. This component is integrated with a number of possible different back-ends that analyse contracts and derive deadlock information. As a proof-of-concept, we discuss two such back-ends: (i) an evaluator that computes a fixpoint semantics and (ii) an evaluator using abstract model checking.