DeadLock Analysis of Concurrent Objects ― Theory and Practice - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2013

DeadLock Analysis of Concurrent Objects ― Theory and Practice

Résumé

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.

Domaines

Informatique

Dates et versions

hal-00909311 , version 1 (26-11-2013)

Identifiants

Citer

Elena Giachino, Carlo A. Grazia, Cosimo Laneve, Michael Lienhardt, Peter Wong. DeadLock Analysis of Concurrent Objects ― Theory and Practice. IFM - 10th International Conference on integrated Formal Methods - 2013, 2013, Turku, Finland. pp.394-411, ⟨10.1007/978-3-642-38613-8_27⟩. ⟨hal-00909311⟩
62 Consultations
0 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More