Deadlock analysis of concurrent programs that contain coordination primitives (wait, notify and ) 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

Laneve C.
;
2019

Abstract

Deadlock analysis of concurrent programs that contain coordination primitives (wait, notify and ) 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
50
67
Laneve C.; Padovani L.
File in questo prodotto:
File Dimensione Formato  
LNCS11760-2019.pdf

accesso aperto

Tipo: Postprint
Licenza: Licenza per accesso libero gratuito
Dimensione 564.2 kB
Formato Adobe PDF
564.2 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/11585/725706
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 2
  • ???jsp.display-item.citation.isi??? 1
social impact