We present a type-based deadlock-freedom verification for concurrent programs with non-block-structured lock primitives and mutable references. Though those two features are frequently used, they are not dealt with in a sufficient manner by previous verification methods. Our type system uses a novel combination of lock levels, obligations and ownerships. Lock levels are used to guarantee that locks are acquired in a specific order. Obligations and ownerships guarantee that an acquired lock is released exactly once. © 2008 Springer Berlin Heidelberg.
CITATION STYLE
Suenaga, K. (2008). Type-based deadlock-freedom verification for non-block-structured lock primitives and mutable references. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5356 LNCS, pp. 155–170). Springer Verlag. https://doi.org/10.1007/978-3-540-89330-1_12
Mendeley helps you to discover research relevant for your work.