A lightweight deadlock analysis for programs with threads and reentrant locks

Cosimo Laneve 1, 2
2 FOCUS - Foundations of Component-based Ubiquitous Systems
CRISAM - Inria Sophia Antipolis - Méditerranée , DISI - Dipartimento di Informatica - Scienza e Ingegneria [Bologna]
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 synchroniza-tions 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). The technique is intended to be an effective tool for the deadlock analysis of programming languages by defining ad-hoc extraction processes.
Document type :
Conference papers
Complete list of metadatas

Cited literature [20 references]  Display  Hide  Download

https://hal.inria.fr/hal-01926509
Contributor : Laneve Cosimo <>
Submitted on : Monday, November 19, 2018 - 12:02:09 PM
Last modification on : Friday, January 4, 2019 - 1:12:57 AM
Long-term archiving on : Wednesday, February 20, 2019 - 2:29:36 PM

File

FM2018-Laneve.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01926509, version 1

Collections

Citation

Cosimo Laneve. A lightweight deadlock analysis for programs with threads and reentrant locks. 22nd International Symposium on Formal Methods, Jul 2018, Oxford, United Kingdom. ⟨hal-01926509⟩

Share

Metrics

Record views

43

Files downloads

45