We propose a type system for lock-freedom in the pi-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 deadlock-freedom, 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.
A Hybrid Type System for Lock-Freedom of Mobile Processes / N. Kobayashi; D. Sangiorgi. - STAMPA. - 5123:(2008), pp. 80-93. (Intervento presentato al convegno 20th International Conference on Computer Aided Verification (CAV'08) tenutosi a Princeton, NJ, USA nel July 7-14).
A Hybrid Type System for Lock-Freedom of Mobile Processes
SANGIORGI, DAVIDE
2008
Abstract
We propose a type system for lock-freedom in the pi-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 deadlock-freedom, 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.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
