Verify me if you can: Supervisors, Actors and Session Types

Rumyana Neykova

Imperial College London


Actor coordination armoured with a suitable protocol description language has been a pressing problem in the actors community. We study the applicability of multiparty session type protocols for verification of actor programs. We incorporate sessions to actors by introducing minimum additions to the model such as the notion of actor roles and protocol mailboxes. The framework uses Scribble, which is a protocol description language based on multiparty session types. Our programming model supports actor-like syntax and runtime verification mechanism guaranteeing communication safety of the participating entities. The usage of multiple roles allows safe cooperative interconcurrency in a single actor. We present the design of our session actor library in Python, which is evaluate by implementing twelve use cases from an actor benchmark suit. Benchmarks demonstrate that the runtime checks induce negligible overhead. We also present a recent work incorporating the session actors model into Erlang, where session types are used for faster error recovery on top of Erlang supervision trees.

Wednesday, March 11 2015