DeadLock Analysis of Concurrent Objects ― Theory and Practice - Archive ouverte HAL Access content directly
Conference Papers Year : 2013

DeadLock Analysis of Concurrent Objects ― Theory and Practice

(1, 2) , (1, 2) , (1, 2) , (1, 3) , (4)


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.

Dates and versions

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



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 View
0 Download



Gmail Facebook Twitter LinkedIn More