Hybrid session veri cation through endpoint API generation

Abstract

This paper proposes a new hybrid session veri cation method- ology for applying session types directly to mainstream languages, based on generating protocol-speci c endpoint APIs from multiparty session types. The API generation promotes static type checking of the be- havioural aspect of the source protocol by mapping the state space of an endpoint in the protocol to a family of channel types in the tar- get language. This is supplemented by very light run-time checks in the generated API that enforce a linear usage discipline on instances of the channel types. The resulting hybrid veri cation guarantees the absence of protocol violation errors during the execution of the session. We have implemented our methodology for Java as an extension to the Scrib- ble framework, and used it to implement compliant clients and servers for real-world protocols such as HTTP and SMTP. The API genera- tion methodology additionally provides a platform for applying further features from session type theory: our implementation supports choice subtyping through branch interface generation, and safe permutation of I/O actions and a ne inputs through input future generation.