ESOP'12, joint work with Nobuko Yoshida.
Communicating finite state machines (CFSMs) represent processes which communicate by asynchronous exchanges of messages via FIFO channels. Their major impact has been in characterising essential properties of communications such as freedom from deadlock and communication error, and buffer boundedness. CFSMs are known to be computationally hard: most of these properties are undecidable even in restricted cases. At the same time, multiparty session types are a recent typed framework whose main feature is its ability to efficiently enforce these properties for mobile processes and programming languages. This paper ties the links between the two frameworks to achieve a two-fold goal. On one hand, we present a generalised variant of multiparty session types that have a direct semantical correspondence to CFSMs. Our calculus can treat expressive forking, merging and joining protocols that are absent from existing session frameworks, and our typing system can ensure properties such as safety, boundedness and liveness on distributed processes by a polynomial time type checking. On the other hand, multiparty session types allow us to identify a new class of CFSMs that automatically enjoy the aforementioned properties, generalising Gouda et al's work [GMY84] (for two machines) to an arbitrary number of machines.
This short version is close to the paper that is publised at ESOP'2012 [pdf].
This long version adds the missing appendices and examples [pdf].
Here is the source code of a preliminary implementation of a programming language whose internals follow the semantics described in the paper [tar.gz]. It consists of the source code of the compiler (in /src), the runtime (in /lib), the monitor (in /monitor), and the examples from the paper (in /ex). It requires make, a recent Ocaml compiler and the graph visualisation program dot. It has been tested under Linux. In the example directories, 'make' produces an implementation and a continuation-based API that the user can use.