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). The technique is intended to be an effective tool for the deadlock analysis of programming languages by defining ad-hoc extraction processes.
A lightweight deadlock analysis for programs with threads and reentrant locks / Laneve, Cosimo*. - ELETTRONICO. - 10951:(2018), pp. 608-624. (Intervento presentato al convegno 22nd International Symposium on Formal Methods, FM 2018 Held as Part of the Federated Logic Conference, FloC 2018 tenutosi a gbr nel 2018) [10.1007/978-3-319-95582-7_36].
A lightweight deadlock analysis for programs with threads and reentrant locks
Laneve, Cosimo
Formal Analysis
2018
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). The technique is intended to be an effective tool for the deadlock analysis of programming languages by defining ad-hoc extraction processes.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.