A framework for deadlock detection in core ABS - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Article Dans Une Revue Software and Systems Modeling Année : 2016

A framework for deadlock detection in core ABS

Résumé

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.
Fichier principal
Vignette du fichier
longDF4ABS.pdf (607.78 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-01229046 , version 1 (16-11-2015)

Identifiants

Citer

Elena Giachino, Cosimo Laneve, Michael Lienhardt. A framework for deadlock detection in core ABS. Software and Systems Modeling, 2016, ⟨10.1007/s10270-014-0444-y⟩. ⟨hal-01229046⟩
123 Consultations
129 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More