Multiparty Session Actors
2017
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 (MPST) 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. An actor can implement multiple roles in a similar way as an object
can implement multiple interfaces. Multiple roles allow for cooperative
inter-concurrency in a single actor. We demonstrate our framework by designing
and implementing a session actor library in Python and its runtime verification
mechanism. Benchmark results demonstrate that the runtime checks induce
negligible overhead. We evaluate the applicability of our verification
framework to specify actor interactions by implementing twelve examples from an
actor benchmark suit.
Keywords:
- Correction
- Source
- Cite
- Save
- Machine Reading By IdeaReader
0
References
9
Citations
NaN
KQI