Oven: Safe and Live Communication Protocols in Scala, using Synthetic Behavioural Type Analysis
Pages 1511 - 1514
Abstract
We present Oven: a toolset to assure safety and liveness of communication protocols among threads in concurrent programs in Scala.
Oven is the first practical toolset that is built on top of new theoretical foundations of synthetic behavioural type analysis, recently developed by us to improve the expressiveness of existing work. We explain Oven's usage, summarise its design and implementation (main challenge: how to encode the new synthetic behavioural typing rules in Scala's existing type system), and discuss a preliminary evaluation of expressiveness (the results provide first evidence that Oven is an improvement over two state-of-the-art tools).
References
[1]
Luca Aceto, Anna Ingólfsdóttir, and Jirí Srba. 2012. The algorithmics of bisimilarity. In Advanced Topics in Bisimulation and Coinduction (Cambridge tracts in theoretical computer science, Vol. 52).
[2]
Davide Ancona et al. 2016. Behavioral Types in Programming Languages. Foundations and Trends in Programming Languages, 3, 2-3 (2016).
[3]
Ilaria Castellani, Mariangiola Dezani-Ciancaglini, and Paola Giannini. 2019. Reversible sessions with flexible choices. Acta Informatica, 56, 7-8 (2019).
[4]
Ilaria Castellani, Mariangiola Dezani-Ciancaglini, and Paola Giannini. 2022. Asynchronous Sessions with Input Races. CoRR, abs/2203.12876 (2022).
[5]
Ilaria Castellani, Mariangiola Dezani-Ciancaglini, Paola Giannini, and Ross Horne. 2020. Global types with internal delegation. Theor. Comput. Sci., 807 (2020).
[6]
David Castro, Raymond Hu, Sung-Shik Jongmans, Nicholas Ng, and Nobuko Yoshida. 2019. Distributed programming using role-parametric session types in go: statically-typed endpoint APIs for dynamically-instantiated communication structures. PACMPL, 3, POPL (2019).
[7]
Guillermina Cledou, Luc Edixhoven, Sung-Shik Jongmans, and José Proença. 2022. API Generation for Multiparty Session Types, Revisited and Revised Using Scala 3. In ECOOP (LIPIcs, Vol. 222).
[8]
Kohei Honda, Aybek Mukhamedov, Gary Brown, Tzu-Chun Chen, and Nobuko Yoshida. 2011. Scribbling Interactions with a Formal Foundation. In ICDCIT (LNCS, Vol. 6536).
[9]
Kohei Honda, Nobuko Yoshida, and Marco Carbone. 2008. Multiparty asynchronous session types. In POPL.
[10]
Raymond Hu and Nobuko Yoshida. 2016. Hybrid Session Verification Through Endpoint API Generation. In FASE (LNCS, Vol. 9633).
[11]
Raymond Hu and Nobuko Yoshida. 2017. Explicit Connection Actions in Multiparty Session Types. In FASE (LNCS, Vol. 10202).
[12]
Hans Hüttel, Ivan Lanese, Vasco T. Vasconcelos, Luís Caires, Marco Carbone, Pierre-Malo Deniélou, Dimitris Mostrous, Luca Padovani, António Ravara, Emilio Tuosto, Hugo Torres Vieira, and Gianluigi Zavattaro. 2016. Foundations of Session Types and Behavioural Contracts. ACM Comput. Surv., 49, 1 (2016).
[13]
Keigo Imai, Rumyana Neykova, Nobuko Yoshida, and Shoji Yuen. 2020. Multiparty Session Programming With Global Protocol Combinators. In ECOOP (LIPIcs, Vol. 166).
[14]
Sung-Shik Jongmans and Francisco Ferreira. 2023. Synthetic Behavioural Typing: Sound, Regular Multiparty Sessions via Implicit Local Types. In ECOOP (LIPIcs, Vol. 263). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 9:1–9:29.
[15]
Sung-Shik Jongmans and Francisco Ferreira. 2023. Synthetic Behavioural Typing: Sound, Regular Multiparty Sessions via Implicit Local Types (Artifact). Dagstuhl Artifacts Ser., 9, 2 (2023).
[16]
Sung-Shik Jongmans and N. Yoshida. 2020. Exploring Type-Level Bisimilarity towards More Expressive Multiparty Session Types. In ESOP (LNCS, Vol. 12075).
[17]
Nicolas Lagaillardie, Rumyana Neykova, and Nobuko Yoshida. 2020. Implementing Multiparty Session Types in Rust. In COORDINATION (LNCS, Vol. 12134).
[18]
Nicolas Lagaillardie, Rumyana Neykova, and Nobuko Yoshida. 2022. Stay Safe Under Panic: Affine Rust Programming with Multiparty Session Types. In ECOOP (LIPIcs, Vol. 222).
[19]
Rupak Majumdar, Madhavan Mukund, Felix Stutz, and Damien Zufferey. 2021. Generalising Projection in Asynchronous Multiparty Session Types. In CONCUR (LIPIcs, Vol. 203).
[20]
Anson Miu, Francisco Ferreira, Nobuko Yoshida, and Fangyi Zhou. 2021. Communication-safe web programming in TypeScript with routed multiparty session types. In CC.
[21]
Rumyana Neykova, Raymond Hu, Nobuko Yoshida, and Fahd Abdeljallal. 2018. A session type provider: compile-time API generation of distributed protocols with refinements in F#. In CC.
[22]
Alceste Scalas, Ornela Dardha, Raymond Hu, and Nobuko Yoshida. 2017. A Linear Decomposition of Multiparty Sessions for Safe Distributed Programming. In ECOOP (LIPIcs, Vol. 74).
[23]
Alceste Scalas and Nobuko Yoshida. 2019. Less is more: multiparty session types revisited. Proc. ACM Program. Lang., 3, POPL (2019).
[24]
Tengfei Tu, Xiaoyu Liu, Linhai Song, and Yiying Zhang. 2019. Understanding Real-World Concurrency Bugs in Go. In ASPLOS.
[25]
Rob van Glabbeek, Peter Höfner, and Ross Horne. 2021. Assuming Just Enough Fairness to make Session Types Complete for Lock-freedom. In LICS.
[26]
Fangyi Zhou, Francisco Ferreira, Raymond Hu, Rumyana Neykova, and Nobuko Yoshida. 2020. Statically verified refinements for multiparty protocols. Proc. ACM Program. Lang., 4, OOPSLA (2020).
Index Terms
- Oven: Safe and Live Communication Protocols in Scala, using Synthetic Behavioural Type Analysis
Recommendations
Foundations of Session Types and Behavioural Contracts
Behavioural type systems, usually associated to concurrent or distributed computations, encompass concepts such as interfaces, communication protocols, and contracts, in addition to the traditional input/output operations. The behavioural type of a ...
Verifying message-passing programs with dependent behavioural types
PLDI 2019: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and ImplementationConcurrent and distributed programming is notoriously hard. Modern languages and toolkits ease this difficulty by offering message-passing abstractions, such as actors (e.g., Erlang, Akka, Orleans) or processes (e.g., Go): they allow for simpler ...
A decentralized analysis of multiparty protocols
AbstractProtocols provide the unifying glue in concurrent and distributed software today; verifying that message-passing programs conform to such governing protocols is important but difficult. Static approaches based on multiparty session ...
Highlights- A new analysis of multiparty protocols expressed as Multiparty Session Types (MPST).
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
July 2023
1554 pages
Copyright © 2023 ACM.
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].
Sponsors
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 13 July 2023
Check for updates
Author Tags
Qualifiers
- Research-article
Funding Sources
- Netherlands Organisation of Scientific Research - NWO
Conference
ISSTA '23
Sponsor:
ISSTA '23: 32nd ACM SIGSOFT International Symposium on Software Testing and Analysis
July 17 - 21, 2023
WA, Seattle, USA
Acceptance Rates
Overall Acceptance Rate 58 of 213 submissions, 27%
Upcoming Conference
ISSTA '25
- Sponsor:
- sigsoft
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 56Total Downloads
- Downloads (Last 12 months)37
- Downloads (Last 6 weeks)2
Reflects downloads up to 28 Sep 2024
Other Metrics
Citations
Cited By
View allView Options
Get Access
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in