A framework for deadlock detection in core ABS

Elena Giachino 1, 2 Cosimo Laneve 1, 2 Michael Lienhardt 2, 1
2 FOCUS - Foundations of Component-based Ubiquitous Systems
CRISAM - Inria Sophia Antipolis - Méditerranée , DISI - Dipartimento di Informatica - Scienza e Ingegneria [Bologna]
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.
Type de document :
Article dans une revue
Software and Systems Modeling, Springer Verlag, 2016, 〈10.1007/s10270-014-0444-y〉
Liste complète des métadonnées

Littérature citée [38 références]  Voir  Masquer  Télécharger

Contributeur : Elena Giachino <>
Soumis le : lundi 16 novembre 2015 - 12:05:50
Dernière modification le : jeudi 11 janvier 2018 - 17:07:00
Document(s) archivé(s) le : vendredi 28 avril 2017 - 15:19:30


Fichiers produits par l'(les) auteur(s)




Elena Giachino, Cosimo Laneve, Michael Lienhardt. A framework for deadlock detection in core ABS. Software and Systems Modeling, Springer Verlag, 2016, 〈10.1007/s10270-014-0444-y〉. 〈hal-01229046〉



Consultations de la notice


Téléchargements de fichiers