Deadlock analysis of concurrent programs that contain coordination primitives (wait, notify and notifyAll) is notoriously challenging. Not only these primitives affect the scheduling of processes, but also notifications unmatched by a corresponding wait are silently lost. We design a behavioral type system for a core calculus featuring shared objects and Java-like coordination primitives. The type system is based on a simple language of object protocols -- called usages -- to determine whether objects are used reliably, so as to guarantee deadlock freedom.

Deadlock Analysis of Wait-Notify Coordination

Luca Padovani
2019-01-01

Abstract

Deadlock analysis of concurrent programs that contain coordination primitives (wait, notify and notifyAll) is notoriously challenging. Not only these primitives affect the scheduling of processes, but also notifications unmatched by a corresponding wait are silently lost. We design a behavioral type system for a core calculus featuring shared objects and Java-like coordination primitives. The type system is based on a simple language of object protocols -- called usages -- to determine whether objects are used reliably, so as to guarantee deadlock freedom.
2019
The Art of Modelling Computational Systems: A Journey from Logic and Concurrency to Security and Privacy: Essays Dedicated to Catuscia Palamidessi on the Occasion of Her 60th Birthday
Springer
11760
50
67
https://hal.inria.fr/hal-02166082
Cosimo Laneve, Luca Padovani
File in questo prodotto:
File Dimensione Formato  
main.pdf

Open Access dal 08/05/2019

Tipo di file: POSTPRINT (VERSIONE FINALE DELL’AUTORE)
Dimensione 706.38 kB
Formato Adobe PDF
706.38 kB Adobe PDF Visualizza/Apri

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/2318/1715156
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 2
  • ???jsp.display-item.citation.isi??? ND
social impact