Two-Way Protocols for occam-pi

In the occam-pi programming language, the client-server communication pattern is generally implemented using a pair of unidirectional channels. While each channel's protocol can be specified individually, no mechanism is yet provided to indicate the relationship between the two protocols; it is therefore not possible to statically check the safety of client-server communications. This paper proposes two-way protocols for individual channels, which would both define the structure of messages and allow the patterns of communication between processes to be specified. We show how conformance to two-way protocols can be statically checked by the occam-pi compiler using Honda's session types. These mechanisms would considerably simplify the implementation of complex, dynamic client-server systems.