2019/05/14 by Eduard Kamburjan, Kamburjan, Eduard · 2 citations
Computer Science · #Advanced Software Engineering Methodologies #Formal Methods in Verification #Logic, programming, and type systems
paper · doi:10.14279/tuj.eceasst.76.1070.1038
openalex publication_date 2019/05/14 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/01
We present a novel notion of deadlock for synchronization on arbitrary boolean conditions and a sound, fully automatic deadlock analysis. Contrary to other approaches, our analysis aims to detect deadlocks caused by faulty system design, rather than implementation bugs. We analyze synchronization on boolean conditions on the fields of an object instead of targeting specific synchronization primitives. As usual, a deadlock is a circular dependency between multiple tasks. A task depends on a second task if the execution of this second task has a side-effect that makes the blocking guard-condition of the first one evaluate to true. This requires an analysis of the computations in a method beyond syntactic properties and we integrate a logical validity calculus to do so.