Anybody working on multiparty session types for Rust?


#1

There are a couple of prototypes for dyadic (two-party) session types (session_types and nemo) but they don’t seem to be under active development.

For implementations of multiparty session types there are several prototypes to look at in various other languages, so far I’ve found examples in Ocaml, Scala, C, Python, Erlang, and (recently) Go. Of those the C and Go implementations are probably closest to what I would expect to see in Rust, although both rely on external verifiers in other languages (Python Scribble for Session C and Haskell Gong for Go/MiGo).

What I would like is to be able to set up a pre-defined topology of threads and channels and statically verify some nice properties to have such as deadlock freedom, communication safety, etc.


#2

One of the session_types authors here (assuming you meant https://github.com/Munksgaard/session-types).

We looked into multiparty session types, but did not pursue it at the time - I don’t exactly remember why, maybe because the types would get even crazier? One of our goals was to keep the implementation only dependent on Rust and not invent external verification tools.

Do you have links for the Go and C implementations?


#3

Session C: http://www.doc.ic.ac.uk/~cn06/sessionc/

Go/MiGo/Gong: http://mrg.doc.ic.ac.uk/tools/gong/

actually the latter is not multiparty session types but some other kind of behavioural types (haven’t read the paper completely)

Session C is basically a top-down approach: you specify the global protocol in Scribble and then a clang plugin does the type checking on the projected local types and local program implementations.

The communicating FSM model is appealing to me; it’s very easy to specify FSMs with using Rust macros.
http://www.doc.ic.ac.uk/~jlange/gmc.html has a bit more on synthesizing global graphs from CFSMs.

Edit: Here’s a previous system by two of the authors of the MiGo/Gong paper that uses a static deadlock detection tool written in Go (dingo) and has some kind of global session graph synthesis based on the above: http://www.doc.ic.ac.uk/~cn06/pub/2016/dingo/