Multiparty Session Types for Safe Runtime Adaptation in an Actor Language
Sat 17 Jul 2021 09:50 - 10:10 at ECOOP 1 - Multiparty Programming and Session Types (time band 3) Chair(s): Lu Zhang
Human fallibility, unpredictable operational environments, and the heterogeneity of hardware devices are driving in the need for software to be able to adapt as seen in the Internet of Things or national telecommunication networks. Unfortunately, mainstream programming languages do not readily allow a software component to sense and respond to its operating environment, by discovering, replacing, and communicating with other software components that are not part of the original system design, while maintaining static correctness guarantees. In particular, if a new component is discovered at runtime, there is no guarantee that its communication behaviour is compatible with existing components.
We address this problem by using multiparty session types with explicit connection actions, a type formalism used to model distributed communication protocols. By associating session types with software components, the discovery process can check protocol compatibility and, when required, correctly replace components.
We present the design and implementation of EnsembleS, the first actor-based language with adaptive features and a static session type system. We apply it to a case study based on an adaptive DNS server. Finally, we formalise the type system of EnsembleS and prove the safety of well-typed programs, making essential use of recent advances in non-classical multiparty session types.
Thu 15 JulDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change
19:00 - 20:00 | Multiparty Programming and Session Types (time band 1)ECOOP Technical Papers at ECOOP 2 Chair(s): Mira Mezini TU Darmstadt, Germany | ||
19:00 20mTalk | Multiparty Languages: the Choreographic and Multitier CasesDistinguished PaperPearl ECOOP Technical Papers Saverio Giallorenzo Alma Mater Studiorum - Università di Bologna, Fabrizio Montesi University of Southern Denmark, Marco Peressotti University of Southern Denmark, David Richter Technical University of Darmstadt, Guido Salvaneschi University of St. Gallen, Pascal Weisenburger TU Darmstadt Link to publication DOI | ||
19:20 20mTalk | Multiparty Session Types for Safe Runtime Adaptation in an Actor Language ECOOP Technical Papers Paul Harvey Rakuten Mobile Innovation Studio, Simon Fowler University of Glasgow, Ornela Dardha University of Glasgow, Simon J. Gay University of Glasgow, UK DOI Pre-print Media Attached | ||
19:40 20mTalk | On the Monitorability of Session Types, in Theory and Practice ECOOP Technical Papers Christian Bartolo Burlò Gran Sasso Science Institute, Adrian Francalanza University of Malta, Alceste Scalas Technical University of Denmark DOI |
Sat 17 JulDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change
09:30 - 10:50 | Multiparty Programming and Session Types (time band 3)ECOOP Technical Papers at ECOOP 1 Chair(s): Lu Zhang Peking University | ||
09:30 20mTalk | On the Monitorability of Session Types, in Theory and Practice ECOOP Technical Papers Christian Bartolo Burlò Gran Sasso Science Institute, Adrian Francalanza University of Malta, Alceste Scalas Technical University of Denmark DOI | ||
09:50 20mTalk | Multiparty Session Types for Safe Runtime Adaptation in an Actor Language ECOOP Technical Papers Paul Harvey Rakuten Mobile Innovation Studio, Simon Fowler University of Glasgow, Ornela Dardha University of Glasgow, Simon J. Gay University of Glasgow, UK DOI Pre-print Media Attached | ||
10:10 20mTalk | Signal Classes: A Mechanism for Building Synchronous and Persistent Signal Networks ECOOP Technical Papers Tetsuo Kamina Oita University, Tomoyuki Aotani Mamezou Co.,Ltd., Hidehiko Masuhara Tokyo Institute of Technology DOI | ||
10:30 20mTalk | Multiparty Languages: the Choreographic and Multitier CasesDistinguished PaperPearl ECOOP Technical Papers Saverio Giallorenzo Alma Mater Studiorum - Università di Bologna, Fabrizio Montesi University of Southern Denmark, Marco Peressotti University of Southern Denmark, David Richter Technical University of Darmstadt, Guido Salvaneschi University of St. Gallen, Pascal Weisenburger TU Darmstadt Link to publication DOI |