Deadlock Analysis of Wait-Notify Coordination

open2noDeadlock 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.openLaneve C.; Padovani L.Laneve C.; Padovani L