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. © 2013 Springer-Verlag Berlin Heidelberg.

Deadlock analysis of concurrent objects: Theory and practice / Giachino, Elena; Grazia, CARLO AUGUSTO; Laneve, Cosimo; Lienhardt, Michael; Wong, Peter Y. H.. - 7940:(2013), pp. 394-411. [10.1007/978-3-642-38613-8_27]

Deadlock analysis of concurrent objects: Theory and practice

GRAZIA, CARLO AUGUSTO;
2013

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. © 2013 Springer-Verlag Berlin Heidelberg.
7940
394
411
Giachino, Elena; Grazia, CARLO AUGUSTO; Laneve, Cosimo; Lienhardt, Michael; Wong, Peter Y. H.
Deadlock analysis of concurrent objects: Theory and practice / Giachino, Elena; Grazia, CARLO AUGUSTO; Laneve, Cosimo; Lienhardt, Michael; Wong, Peter Y. H.. - 7940:(2013), pp. 394-411. [10.1007/978-3-642-38613-8_27]
File in questo prodotto:
File Dimensione Formato  
daco.pdf

non disponibili

Descrizione: Versione dell'autore
Tipologia: Post-print dell'autore (bozza post referaggio)
Dimensione 428.84 kB
Formato Adobe PDF
428.84 kB Adobe PDF   Visualizza/Apri   Richiedi una copia
Pubblicazioni consigliate

Caricamento pubblicazioni consigliate

Licenza Creative Commons
I metadati presenti in IRIS UNIMORE sono rilasciati con licenza Creative Commons CC0 1.0 Universal, mentre i file delle pubblicazioni sono rilasciati con licenza Attribuzione 4.0 Internazionale (CC BY 4.0), salvo diversa indicazione.
In caso di violazione di copyright, contattare Supporto Iris

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/11380/1138935
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 18
  • ???jsp.display-item.citation.isi??? ND
social impact