MobilityReadingGroup

A Session Type Provider: Compile-time API Generation for Distributed Protocols with Interaction Refinements in F#

Rumyana NEYKOVA, Raymond HU, Nobuko YOSHIDA, Fahd ABDELJALLAL

We present a library for the specification and implementation of distributed protocols in native F# (and other .NET languages) based on multiparty session types (MPST). There are two main contributions. Our library is the first practical development of MPST to support what we refer to as interaction refinements: a collection of features related to the refinement of protocols, such as message-type refinements (value constraints) and value dependent control flow. A well-typed endpoint program using our library is guaranteed to perform only compliant session I/O actions w.r.t. to the refined protocol, up to premature termination.

Second, our library is developed as a session type provider, that performs on-demand compile-time protocol validation and generation of protocol-specific .NET types for users writing the distributed endpoint programs. It is implemented by extending and integrating Scribble (a toolchain for MPST) with an SMT solver into the type providers framework. The safety guarantees are achieved by a combination of static type checking of the generated types for messages and I/O operations, correctness by construction from code generation, and automated inlining of assertions.

We evaluate our library based on several well-known protocols and algorithms. Our experience shows that our type-driven approach considerably simplifies the development of protocols, with negligible increase in compilation times.

@inproceedings{NHYA2018,
  author = {Rumyana Neykova and Raymond Hu and Nobuko Yoshida and Fahd Abdeljallal},
  title = {{A Session Type Provider: Compile-time API Generation for Distributed Protocols with Interaction Refinements in F#}},
  booktitle = {27th International Conference on Compiler Construction},
  pages = {128--138},
  publisher = {ACM},
  year = 2018
}

@inproceedings{NHYA2018,
  author = {Rumyana Neykova and Raymond Hu and Nobuko Yoshida and Fahd Abdeljallal},
  title = {{A Session Type Provider: Compile-time API Generation for Distributed Protocols with Interaction Refinements in F#}},
  booktitle = {27th International Conference on Compiler Construction},
  pages = {128--138},
  publisher = {ACM},
  doi = "10.1145/3178372.3179495",
  year = 2018
}