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.; Padovani L.. - STAMPA. - 11760:(2019), pp. 50-67. (Intervento presentato al convegno 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 tenutosi a Parigi nel 4-5 Novembre 2019) [10.1007/978-3-030-31175-9_4].
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.| 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.
