Deadlock analysis of multi-threaded programs with reentrant locks is complex because these programs may have infinitely many states. We define a simple calculus featuring recursion, threads and synchronizations that guarantee exclusive access to objects. We detect deadlocks by associating an abstract model to programs – the extended lam model – and we define an algorithm for verifying that a problematic object dependency (e.g. a circularity) between threads will not be manifested. The analysis is lightweight because the deadlock detection problem is fully reduced to the corresponding one in lams (without using other models). In fact, the technique is intended to be an effective tool for the deadlock analysis of programming languages by defining ad-hoc extraction processes. We demonstrate this effectivity by applying our analysis to a core calculus featuring shared objects, threads and Java-like synchronization primitives. We also discuss a prototype verifier, called JaDA, that covers several features of Java and deliver initial assessments of the tool.

Laneve C. (2019). A lightweight deadlock analysis for programs with threads and reentrant locks. SCIENCE OF COMPUTER PROGRAMMING, 181, 64-81 [10.1016/j.scico.2019.06.002].

A lightweight deadlock analysis for programs with threads and reentrant locks

Laneve C.
2019

Abstract

Deadlock analysis of multi-threaded programs with reentrant locks is complex because these programs may have infinitely many states. We define a simple calculus featuring recursion, threads and synchronizations that guarantee exclusive access to objects. We detect deadlocks by associating an abstract model to programs – the extended lam model – and we define an algorithm for verifying that a problematic object dependency (e.g. a circularity) between threads will not be manifested. The analysis is lightweight because the deadlock detection problem is fully reduced to the corresponding one in lams (without using other models). In fact, the technique is intended to be an effective tool for the deadlock analysis of programming languages by defining ad-hoc extraction processes. We demonstrate this effectivity by applying our analysis to a core calculus featuring shared objects, threads and Java-like synchronization primitives. We also discuss a prototype verifier, called JaDA, that covers several features of Java and deliver initial assessments of the tool.
2019
Laneve C. (2019). A lightweight deadlock analysis for programs with threads and reentrant locks. SCIENCE OF COMPUTER PROGRAMMING, 181, 64-81 [10.1016/j.scico.2019.06.002].
Laneve C.
File in questo prodotto:
Eventuali allegati, non sono esposti

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11585/725701
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 3
  • ???jsp.display-item.citation.isi??? 3
social impact