[go: up one dir, main page]
More Web Proxy on the site http://driver.im/ skip to main content
research-article
Open access

Distributed programming using role-parametric session types in go: statically-typed endpoint APIs for dynamically-instantiated communication structures

Published: 02 January 2019 Publication History

Abstract

This paper presents a framework for the static specification and safe programming of message passing protocols where the number and kinds of participants are dynamically instantiated.
We develop the first theory of distributed multiparty session types (MPST) to support parameterised protocols with indexed roles—our framework statically infers the different kinds of participants induced by a protocol definition as role variants, and produces decoupled endpoint projections of the protocol onto each variant. This enables safe MPST-based programming of the parameterised endpoints in distributed settings: each endpoint can be implemented separately by different programmers, using different techniques (or languages). We prove the decidability of role variant inference and well-formedness checking, and the correctness of projection.
We implement our theory as a toolchain for programming such role-parametric MPST protocols in Go. Our approach is to generate API families of lightweight, protocol- and variant-specific type wrappers for I/O. The APIs ensure a well-typed Go endpoint program (by native Go type checking) will perform only compliant I/O actions w.r.t. the source protocol. We leverage the abstractions of MPST to support the specification and implementation of Go applications involving multiple channels, possibly over mixed transports (e.g., Go channels, TCP), and channel passing via a unified programming interface. We evaluate the applicability and run-time performance of our generated APIs using microbenchmarks and real-world applications.

Supplementary Material

WEBM File (a29-jongmans.webm)

References

[1]
Manuel Adameit, Kirstin Peters, and Uwe Nestmann. 2017. Session Types for Link Failures. In Formal Techniques for Distributed Objects, Components, and Systems - 37th IFIP WG 6.1 International Conference, FORTE 2017, Held as Part of the 12th International Federated Conference on Distributed Computing Techniques, DisCoTec 2017, Neuchâtel, Switzerland, June 19-22, 2017, Proceedings (Lecture Notes in Computer Science), Vol. 10321. Springer, 1–16.
[2]
Foat Akhmadeev. 2016. Web Crawling With Akka. http://foat.me/articles/crawling- with- akka/ .
[3]
Davide Ancona, Viviana Bono, Mario Bravetti, Joana Campos, Giuseppe Castagna, Pierre-Malo Deniélou, Simon J. Gay, Nils Gesbert, Elena Giachino, Raymond Hu, Einar Broch Johnsen, Francisco Martins, Viviana Mascardi, Fabrizio Montesi, Rumyana Neykova, Nicholas Ng, Luca Padovani, Vasco T. Vasconcelos, and Nobuko Yoshida. 2016. Behavioral Types in Programming Languages. Foundations and Trends in Programming Languages 3, 2-3 (2016), 95–230.
[4]
Daniel Austin, Abbie Barbir, Ed Peters, and Steve Ross-Talbot. 2004. Web Services Choreography Requirements. https: //www.w3.org/TR/2004/WD- ws- chor- reqs- 20040311/#UC- 002 .
[5]
Andi Bejleri, Raymond Hu, and Nobuko Yoshida. 2009. Session-Based Programming for Parallel Algorithms: Expressiveness and Performance. In Proceedings Second International Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software, PLACES 2009, York, UK, 22nd March 2009. (EPTCS), Vol. 17. 17–29.
[6]
Daniel Brand and Pitro Zafiropulo. 1983. On Communicating Finite-State Machines. J. ACM 30, 2 (1983), 323–342.
[7]
Stefan Brunthaler. 2010. Inline Caching Meets Quickening. In ECOOP 2010 - Object-Oriented Programming, 24th European Conference, Maribor, Slovenia, June 21-25, 2010. Proceedings (Lecture Notes in Computer Science), Theo D’Hondt (Ed.), Vol. 6183. Springer, 429–451.
[8]
Minas Charalambides, Peter Dinges, and Gul A. Agha. 2016. Parameterized, concurrent session types for asynchronous multi-actor interactions. Sci. Comput. Program. 115-116 (2016), 100–126.
[9]
Ernie Cohen, Markus Dahlweid, Mark A. Hillebrand, Dirk Leinenbach, Michal Moskal, Thomas Santen, Wolfram Schulte, and Stephan Tobies. 2009. VCC: A Practical System for Verifying Concurrent C. In Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings (Lecture Notes in Computer Science), Stefan Berghofer, Tobias Nipkow, Christian Urban, and Makarius Wenzel (Eds.), Vol. 5674. Springer, 23–42.
[10]
Mario Coppo, Mariangiola Dezani-Ciancaglini, Luca Padovani, and Nobuko Yoshida. 2015. A Gentle Introduction to Multiparty Asynchronous Session Types. In 15th International School on Formal Methods for the Design of Computer, Communication and Software Systems: Multicore Programming (LNCS), Vol. 9104. Springer, 146–178.
[11]
Mario Coppo, Mariangiola Dezani-Ciancaglini, Nobuko Yoshida, and Luca Padovani. 2016. Global progress for dynamically interleaved multiparty sessions. Mathematical Structures in Computer Science 26, 2 (2016), 238–302.
[12]
Pierre-Malo Deniélou and Nobuko Yoshida. 2012. Multiparty Session Types Meet Communicating Automata. In Programming Languages and Systems - 21st European Symposium on Programming, ESOP 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24 - April 1, 2012. Proceedings (Lecture Notes in Computer Science), Helmut Seidl (Ed.), Vol. 7211. Springer, 194–213.
[13]
Pierre-Malo Deniélou and Nobuko Yoshida. 2013. Multiparty Compatibility in Communicating Automata: Characterisation and Synthesis of Global Session Types. In Automata, Languages, and Programming - 40th International Colloquium, ICALP 2013, Riga, Latvia, July 8-12, 2013, Proceedings, Part II (Lecture Notes in Computer Science), Fedor V. Fomin, Rusins Freivalds, Marta Z. Kwiatkowska, and David Peleg (Eds.), Vol. 7966. Springer, 174–186.
[14]
Pierre-Malo Deniélou, Nobuko Yoshida, Andi Bejleri, and Raymond Hu. 2012. Parameterised Multiparty Session Types. Logical Methods in Computer Science 8, 4 (2012).
[15]
Simon J. Gay, Vasco T. Vasconcelos, António Ravara, Nils Gesbert, and Alexandre Z. Caldeira. 2010. Modular Session Types for Distributed Object-oriented Programming. In Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’10). ACM, New York, NY, USA, 299–312.
[16]
Issac Gouy. 2017. Computer Language Benchmark Game. http://benchmarksgame.alioth.debian.org .
[17]
Kohei Honda, Nobuko Yoshida, and Marco Carbone. 2016. Multiparty Asynchronous Session Types. J. ACM 63, 1 (2016), 9:1–9:67.
[18]
Raymond Hu and Nobuko Yoshida. 2016. Hybrid Session Verification Through Endpoint API Generation. In Fundamental Approaches to Software Engineering - 19th International Conference, FASE 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings (Lecture Notes in Computer Science), Perdita Stevens and Andrzej Wasowski (Eds.), Vol. 9633. Springer, 401–418.
[19]
Raymond Hu and Nobuko Yoshida. 2017. Explicit Connection Actions in Multiparty Session Types. In Fundamental Approaches to Software Engineering - 20th International Conference, FASE 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings (Lecture Notes in Computer Science), Marieke Huisman and Julia Rubin (Eds.), Vol. 10202. Springer, 116–133.
[20]
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), 3:1–3:36.
[21]
Dimitrios Kouzapas, Ornela Dardha, Roly Perera, and Simon J. Gay. 2016. Typechecking protocols with Mungo and StMungo. In PPDP. 146–159.
[22]
Julien Lange, Nicholas Ng, Bernardo Toninho, and Nobuko Yoshida. 2017. Fencing off go: liveness and safety for channelbased programming. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017, Giuseppe Castagna and Andrew D. Gordon (Eds.). ACM, 748–761. http: //dl.acm.org/citation.cf m?id=3009847
[23]
Julien Lange, Nicholas Ng, Bernardo Toninho, and Nobuko Yoshida. 2018. A Static Verification Framework for Message Passing in Go using Behavioural Types. In 40th International Conference on Software Engineering. ACM. To appear.
[24]
Julien Lange, Emilio Tuosto, and Nobuko Yoshida. 2015. From Communicating Machines to Graphical Choreographies. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015, Sriram K. Rajamani and David Walker (Eds.). ACM, 221–232.
[25]
Hugo A. López, Eduardo R. B. Marques, Francisco Martins, Nicholas Ng, César Santos, Vasco Thudichum Vasconcelos, and Nobuko Yoshida. 2015. Protocol-based verification of message-passing parallel programs. In Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2015, part of SPLASH 2015, Pittsburgh, PA, USA, October 25-30, 2015, Jonathan Aldrich and Patrick Eugster (Eds.). ACM, 280–298.
[26]
Rumyana Neykova and Nobuko Yoshida. 2017. Let It Recover: Multiparty Protocol-Induced Recovery. In 26th International Conference on Compiler Construction. ACM, 98–108.
[27]
Nicholas Ng, José Gabriel de Figueiredo Coutinho, and Nobuko Yoshida. 2015. Protocols by Default - Safe MPI Code Generation Based on Session Types. In Compiler Construction - 24th International Conference, CC 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings (Lecture Notes in Computer Science), Björn Franke (Ed.), Vol. 9031. Springer, 212–232.
[28]
Nicholas Ng and Nobuko Yoshida. 2015. Pabble: parameterised Scribble. Service Oriented Computing and Applications 9, 3-4 (2015), 269–284.
[29]
Nicholas Ng and Nobuko Yoshida. 2016. Static deadlock detection for concurrent go by global session graph synthesis. In Proceedings of the 25th International Conference on Compiler Construction, CC 2016, Barcelona, Spain, March 12-18, 2016, Ayal Zaks and Manuel V. Hermenegildo (Eds.). ACM, 174–184.
[30]
Luca Padovani. 2017. A simple library implementation of binary sessions. J. Funct. Program. 27 (2017), e4.
[31]
Aseem Rastogi, Matthew A. Hammer, and Michael Hicks. 2014. Wysteria: A Programming Language for Generic, MixedMode Multiparty Computations. In Proceedings of the 2014 IEEE Symposium on Security and Privacy (SP ’14). IEEE Computer Society, Washington, DC, USA, 655–670.
[32]
Alceste Scalas, Ornela Dardha, Raymond Hu, and Nobuko Yoshida. 2017. A Linear Decomposition of Multiparty Sessions for Safe Distributed Programming. In 31st European Conference on Object-Oriented Programming, ECOOP 2017, June 19-23, 2017, Barcelona, Spain (LIPIcs), Peter Müller (Ed.), Vol. 74. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 24:1–24:31.
[33]
Jun Shirako, David M. Peixotto, Vivek Sarkar, and William N. Scherer III. 2009. Phaser accumulators: A new reduction construct for dynamic parallelism. In 23rd IEEE International Symposium on Parallel and Distributed Processing, IPDPS 2009, Rome, Italy, May 23-29, 2009. IEEE, 1–12.
[34]
Vincent St-Amour, Sam Tobin-Hochstadt, and Matthias Felleisen. 2012. Optimization coaching: optimizers learn to communicate with programmers. In Proceedings of the 27th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2012, part of SPLASH 2012, Tucson, AZ, USA, October 21-25, 2012, Gary T. Leavens and Matthew B. Dwyer (Eds.). ACM, 163–178.
[35]
Kai Stadtmüller, Martin Sulzmann, and Peter Thiemann. 2016. Static Trace-Based Deadlock Analysis for Synchronous Mini-Go. In Programming Languages and Systems - 14th Asian Symposium, APLAS 2016, Hanoi, Vietnam, November 21-23, 2016, Proceedings (Lecture Notes in Computer Science), Atsushi Igarashi (Ed.), Vol. 10017. 116–136.
[36]
R E Strom and S Yemini. 1986. Typestate: A Programming Language Concept for Enhancing Software Reliability. IEEE Trans. Softw. Eng. 12, 1 (Jan. 1986), 157–171.
[37]
Martin Sulzmann and Peter Thiemann. 2016. Forkable Regular Expressions. In Language and Automata Theory and Applications - 10th International Conference, LATA 2016, Prague, Czech Republic, March 14-18, 2016, Proceedings (Lecture Notes in Computer Science), Adrian-Horia Dediu, Jan Janousek, Carlos Martín-Vide, and Bianca Truthe (Eds.), Vol. 9618. Springer, 194–206.
[38]
Jesse A. Tov and Riccardo Pucella. 2011. Practical affine types. In Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, Austin, TX, USA, January 26-28, 2011. ACM, 447–458.
[39]
Malte Viering, Tzu-Chun Chen, Patrick Eugster, Raymond Hu, and Lukasz Ziarek. 2018. A Typing Discipline for Statically Verified Crash Failure Handling in Distributed Systems. In Programming Languages and Systems - 27th European Symposium on Programming, ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings (Lecture Notes in Computer Science), Vol. 10801. Springer, 799–826.
[40]
Tobias Wrigstad, Francesco Zappa Nardelli, Sylvain Lebresne, Johan Östlund, and Jan Vitek. 2010. Integrating typed and untyped code in a scripting language. In Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, Madrid, Spain, January 17-23, 2010, Manuel V. Hermenegildo and Jens Palsberg (Eds.). ACM, 377–388.
[41]
Nobuko Yoshida, Pierre-Malo Deniélou, Andi Bejleri, and Raymond Hu. 2010. Parameterised Multiparty Session Types. In Foundations of Software Science and Computational Structures, 13th International Conference, FOSSACS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings (Lecture Notes in Computer Science), Vol. 6014. Springer, 128–145.

Cited By

View all
  • (2024)Discourje: Run-Time Verification of Communication Protocols in Clojure — Live at LastFormal Methods10.1007/978-3-031-71177-0_11(158-166)Online publication date: 13-Sep-2024
  • (2024)Programming Language Implementations with Multiparty Session TypesActive Object Languages: Current Research Trends10.1007/978-3-031-51060-1_6(147-165)Online publication date: 29-Jan-2024
  • (2023)Verifying Reliable Network Components in a Distributed Separation Logic with Dependent Separation ProtocolsProceedings of the ACM on Programming Languages10.1145/36078597:ICFP(847-877)Online publication date: 31-Aug-2023
  • Show More Cited By

Recommendations

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Proceedings of the ACM on Programming Languages
Proceedings of the ACM on Programming Languages  Volume 3, Issue POPL
January 2019
2275 pages
EISSN:2475-1421
DOI:10.1145/3302515
Issue’s Table of Contents
This work is licensed under a Creative Commons Attribution International 4.0 License.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 02 January 2019
Published in PACMPL Volume 3, Issue POPL

Permissions

Request permissions for this article.

Check for updates

Badges

Author Tags

  1. Go
  2. distributed programming
  3. indexed roles
  4. multiparty session types

Qualifiers

  • Research-article

Funding Sources

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)147
  • Downloads (Last 6 weeks)14
Reflects downloads up to 24 Dec 2024

Other Metrics

Citations

Cited By

View all
  • (2024)Discourje: Run-Time Verification of Communication Protocols in Clojure — Live at LastFormal Methods10.1007/978-3-031-71177-0_11(158-166)Online publication date: 13-Sep-2024
  • (2024)Programming Language Implementations with Multiparty Session TypesActive Object Languages: Current Research Trends10.1007/978-3-031-51060-1_6(147-165)Online publication date: 29-Jan-2024
  • (2023)Verifying Reliable Network Components in a Distributed Separation Logic with Dependent Separation ProtocolsProceedings of the ACM on Programming Languages10.1145/36078597:ICFP(847-877)Online publication date: 31-Aug-2023
  • (2023)Oven: Safe and Live Communication Protocols in Scala, using Synthetic Behavioural Type AnalysisProceedings of the 32nd ACM SIGSOFT International Symposium on Software Testing and Analysis10.1145/3597926.3604926(1511-1514)Online publication date: 12-Jul-2023
  • (2023)Hybrid Multiparty Session Types: Compositionality for Protocol Specification through Endpoint ProjectionProceedings of the ACM on Programming Languages10.1145/35860317:OOPSLA1(112-142)Online publication date: 6-Apr-2023
  • (2023)Safe Asynchronous Mixed-Choice for Timed InteractionsCoordination Models and Languages10.1007/978-3-031-35361-1_12(214-231)Online publication date: 15-Jun-2023
  • (2023)Multiparty Session Typing in Java, DeductivelyTools and Algorithms for the Construction and Analysis of Systems10.1007/978-3-031-30820-8_3(19-27)Online publication date: 22-Apr-2023
  • (2023)VeyMont: Parallelising Verified Programs Instead of Verifying Parallel ProgramsFormal Methods10.1007/978-3-031-27481-7_19(321-339)Online publication date: 3-Mar-2023
  • (2022)A Type Discipline for Message Passing Parallel ProgramsACM Transactions on Programming Languages and Systems10.1145/355251944:4(1-55)Online publication date: 21-Dec-2022
  • (2022)Towards Gradual Multiparty Session TypingProceedings of the 37th IEEE/ACM International Conference on Automated Software Engineering10.1145/3551349.3561167(1-3)Online publication date: 10-Oct-2022
  • Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Login options

Full Access

Media

Figures

Other

Tables

Share

Share

Share this Publication link

Share on social media