Sciweavers

Share
ESOP
2007
Springer

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

11 years 5 months ago
Type-Based Analysis of Deadlock for a Concurrent Calculus with Interrupts
The goal of our research project is to establish a type-based method for verification of certain critical properties (such as deadlockand 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.
Kohei Suenaga, Naoki Kobayashi
Added 07 Jun 2010
Updated 07 Jun 2010
Type Conference
Year 2007
Where ESOP
Authors Kohei Suenaga, Naoki Kobayashi
Comments (0)
books