MobilityReadingGroup

Dynamic multirole session types

Pierre-Malo DENIÉLOU, Nobuko YOSHIDA

Multiparty session types enforce structured safe communications between several participants, as long as their number is fixed when the session starts. In order to handle common distributed interaction patterns such as cloud algorithms or peer-to-peer protocols, we propose a new role-based multiparty session type theory where roles are defined as classes of local behaviours that an arbitrary number of participants can dynamically join and leave. We offer programmers a polling operation that gives access to the current set of a role’s participants in order to fork processes. Our type system with universal types for polling can handle this dynamism and retain type safety. A multiparty locking mechanism is introduced to provide communication safety, but also to ensure a stronger progress property for joining participants that has never been guaranteed in previous systems. Finally, we present some implementation mechanisms used in our prototype extension of ML.

@inproceedings{DY2011,
  author = {Pierre-Malo Deniélou and Nobuko Yoshida},
  title = {{Dynamic multirole session types}},
  booktitle = {38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
  pages = {435--446},
  publisher = {ACM},
  year = 2011
}

@inproceedings{DY2011,
  author = {Pierre-Malo Deniélou and Nobuko Yoshida},
  title = {{Dynamic multirole session types}},
  booktitle = {38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
  pages = {435--446},
  publisher = {ACM},
  doi = "10.1145/1926385.1926435",
  year = 2011
}