DeadLock Analysis of Concurrent Objects ― Theory and Practice

Abstract : We present a framework for statically detecting deadlocks in a concurrent object language with asynchronous invocations and operations for getting values and releasing the control. Our approach is based on the integration of two static analysis techniques: (i) an inference algorithm to extract abstract descriptions of methods in the form of behavioral types, called contracts, and (ii) an evaluator that computes a fixpoint semantics returning a finite state model of contracts. A potential deadlock is detected when a circular dependency is found in some state of the model. We discuss the theory and the prototype implementation of our framework. Our tool is validated on an industrial case study based on the Fredhopper Access Server (FAS) developed by SDL Fredhoppper. In particular we verify one of the core concurrent components of FAS to be deadlock-free.
Type de document :
Communication dans un congrès
Einar Broch Johnsen and Luigia Petr. IFM - 10th International Conference on integrated Formal Methods - 2013, 2013, Turku, Finland. Springer, 7940, pp.394-411, 2013, Lecture Notes in Computer Science. 〈10.1007/978-3-642-38613-8_27〉
Liste complète des métadonnées

https://hal.inria.fr/hal-00909311
Contributeur : Davide Sangiogi <>
Soumis le : mardi 26 novembre 2013 - 10:46:16
Dernière modification le : samedi 27 janvier 2018 - 01:30:51

Lien texte intégral

Identifiants

Collections

INRIA | PPS | USPC

Citation

Elena Giachino, Carlo A. Grazia, Cosimo Laneve, Michael Lienhardt, Peter Wong. DeadLock Analysis of Concurrent Objects ― Theory and Practice. Einar Broch Johnsen and Luigia Petr. IFM - 10th International Conference on integrated Formal Methods - 2013, 2013, Turku, Finland. Springer, 7940, pp.394-411, 2013, Lecture Notes in Computer Science. 〈10.1007/978-3-642-38613-8_27〉. 〈hal-00909311〉

Partager

Métriques

Consultations de la notice

123