Multiparty session actors
File(s)
Accepted version
OA Location
Author(s)
Neykova, R
Yoshida, N
Type
Journal Article
Abstract
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 introduc-
ing 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 guarantee-
ing 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 implement-
ing 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.
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 introduc-
ing 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 guarantee-
ing 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 implement-
ing 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.
Date Issued
2017-03-29
Date Acceptance
2016-12-13
Citation
Logical Methods in Computer Science, 2017, 13 (1)
ISSN
1860-5974
Publisher
IfCoLog (International Federation of Computational Logic)
Journal / Book Title
Logical Methods in Computer Science
Volume
13
Issue
1
Copyright Statement
Creative Commons Attribution Non-Commercial License
Sponsor
Engineering & Physical Science Research Council (E
Engineering & Physical Science Research Council (E
Engineering & Physical Science Research Council (EPSRC)
Commission of the European Communities
Grant Number
ERI 025567 (EP/K034413/1)
PO 1553380
EP/K011715/1
612985
Subjects
Science & Technology
Technology
Computer Science, Theory & Methods
Logic
Computer Science
Science & Technology - Other Topics
Session types
Protocol description language
Actors
Python
Messaging Middleware
SYSTEMS
PARALLELISM
MODEL
0101 Pure Mathematics
0803 Computer Software
0802 Computation Theory And Mathematics
Publication Status
Published
Article Number
3227