A Hybrid Type System for Lock-Freedom of Mobile Processes

We propose a type system for lock-freedom in the -calculus, which guarantees that certain communications will eventually succeed. Distinguishing features of our type system are: it can verify lock-freedom of concurrent programs that have sophisticated recursive communication structures; it can be fully automated; it is hybrid, in that it combines a type system for lock-freedom with local reasoning about deadlockfreedom, termination, and confluence analyses. Moreover, the type system is parameterized by deadlock-freedom/termination/confluence analyses, so that any methods (e.g. type systems and model checking) can be used for those analyses. A lock-freedom analysis tool has been implemented based on the proposed type system, and tested for non-trivial programs.

• Type: Conference
• Year: 2008
• Where: CAV
• Authors: Naoki Kobayashi, Davide Sangiorgi
• Keywords: CAV 2008, Certain Communications, Confluence Analyses, Hardware, Type System