· A Behavioral Module System for the Pi-Calculus
Sriram K. Rajamani and
Jakob Rehof
Proceedings SAS 01, Static Analysis
Symposium,
Abstract:
Distributed
message-passing based asynchronous systems are becoming increasingly important.
Such systems are notoriously hard to design and test. A promising approach to
help programmers design such programs is to provide a behavioral type system
that checks for behavioral properties such as deadlock freedom using a
combination of type inference and model checking. The fundamental challenge in
making a behavioral type system work for realistic concurrent programs is state
explosion. This paper develops the theory to design a behavioral module system
that permits decomposing the type checking problem, saving exponential cost in
the analysis. Unlike module systems for sequential programming languages, a
behavioral specification for a module typically assumes that the module
operates in an appropriate concurrent context. We identify assume-guarantee
reasoning as a fundamental principle in designing such a module system.
Concretely, we propose a behavioral module system for Pi-calculus programs.
Types are CCS processes that correctly approximate the behavior of programs,
and by applying model checking techniques to process types one can check many
interesting program properties, including deadlock-freedom and communication
progress. We show that modularity can be achieved in our type system by
applying circular assume-guarantee reasoning principles whose soundness
requires an induction over time. We state and prove an assume-guarantee rule
for CCS. Our module system integrates this assume-guarantee rule into our behavioral
type system.
