Type-Based Analysis of Deadlock for a Concurrent Calculus with Interrupts Export

@incollection{citeulike:2796689, abstract = {The goal of our research project is to establish a type-based method for verification of certain critical properties (such as deadlock- and race-freedom) of operating system kernels. As operating system kernels make heavy use of threads and interrupts, it is important that the method can properly deal with both of the two features. As a first step towards the goal, we formalize a concurrent calculus equipped with primitives for threads and interrupts handling. We also propose a type system that guarantees deadlock-freedom in the presence of interrupts. To our knowledge, ours is the first type system for deadlock-freedom that can deal with both thread and interrupt primitives.}, author = {Suenaga, Kohei and Kobayashi, Naoki}, citeulike-article-id = {2796689}, citeulike-linkout-0 = {http://dx.doi.org/10.1007/978-3-540-71316-6_33}, doi = {10.1007/978-3-540-71316-6_33}, journal = {Programming Languages and Systems}, keywords = {2007, concurrent, deadlock, pi, type}, pages = {490--504}, posted-at = {2008-05-14 06:54:18}, priority = {2}, title = {Type-Based Analysis of Deadlock for a Concurrent Calculus with Interrupts}, url = {http://dx.doi.org/10.1007/978-3-540-71316-6_33}, year = {2007} }

TY - CHAP ID - citeulike:2796689 L3 - citeulike-article-id:2796689 N2 - The goal of our research project is to establish a type-based method for verification of certain critical properties (such as deadlock- and race-freedom) of operating system kernels. As operating system kernels make heavy use of threads and interrupts, it is important that the method can properly deal with both of the two features. As a first step towards the goal, we formalize a concurrent calculus equipped with primitives for threads and interrupts handling. We also propose a type system that guarantees deadlock-freedom in the presence of interrupts. To our knowledge, ours is the first type system for deadlock-freedom that can deal with both thread and interrupt primitives. JF - Programming Languages and Systems EP - 504 TI - Type-Based Analysis of Deadlock for a Concurrent Calculus with Interrupts SP - 490 KW - 2007 KW - concurrent KW - deadlock KW - pi KW - type AU - Suenaga, Kohei AU - Kobayashi, Naoki PY - 2007/// UR - http://dx.doi.org/10.1007/978-3-540-71316-6_33 ER -