Skip to Main content Skip to Navigation
Conference papers

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.
Document type :
Conference papers
Complete list of metadata
Contributor : Davide Sangiogi Connect in order to contact the contributor
Submitted on : Tuesday, November 26, 2013 - 10:46:16 AM
Last modification on : Friday, October 30, 2020 - 12:04:02 PM

Links full text




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⟩



Record views