Document Open Access Logo

Dynamically Updatable Multiparty Session Protocols: Generating Concurrent Go Code from Unbounded Protocols

Authors David Castro-Perez , Nobuko Yoshida

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2023.6.pdf
  • Filesize: 1.34 MB
  • 30 pages

Document Identifiers

Author Details

David Castro-Perez
  • University of Kent, UK
Nobuko Yoshida
  • University of Oxford, UK

Funding

This work is supported by EPSRC EP/T006544/2, EP/K011715/1, EP/K034413/1, EP/L00058X/1, EP/N027833/2, EP/N028201/1, EP/T014709/2, EP/V000462/1, EP/X015955/1, NCSS/EPSRC VeTSS, EP/T014512/1, and Horizon EU TaRDIS 101093006.

Acknowledgements

We deeply thank Benito Echarren Serrano for his initial collaboration on a preliminary version of this work.

Cite AsGet BibTex

David Castro-Perez and Nobuko Yoshida. Dynamically Updatable Multiparty Session Protocols: Generating Concurrent Go Code from Unbounded Protocols. In 37th European Conference on Object-Oriented Programming (ECOOP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 263, pp. 6:1-6:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.ECOOP.2023.6

Abstract

Multiparty Session Types (MPST) are a typing disciplines that guarantee the absence of deadlocks and communication errors in concurrent and distributed systems. However, existing MPST frameworks do not support protocols with dynamic unbounded participants, and cannot express many common programming patterns that require the introduction of new participants into a protocol. This poses a barrier for the adoption of MPST in languages that favour the creation of new participants (processes, lightweight threads, etc) that communicate via message passing, such as Go or Erlang. This paper proposes Dynamically Updatable Multiparty Session Protocols, a new MPST theory (DMst) that supports protocols with an unbounded number of fresh participants, whose communication topologies are dynamically updatable. We prove that DMst guarantees deadlock-freedom and liveness. We implement a toolchain, GoScr (Go-Scribble), which generates Go implementations from DMst, ensuring by construction, that the different participants will only perform I/O actions that comply with a given protocol specification. We evaluate our toolchain by (1) implementing representative parallel and concurrent algorithms from existing benchmarks, textbooks and literature; (2) showing that GoScr does not introduce significant overheads compared to a naive implementation, for computationally expensive benchmarks; and (3) building three realistic protocols (dynamic task delegation, recursive Domain Name System, and a parallel Min-Max strategy) in GoScr that could not be represented with previous theories of session types.

Subject Classification

ACM Subject Classification
  • Theory of computation → Program specifications
  • Computing methodologies → Concurrent programming languages
Keywords
  • Multiparty Session Types
  • Correctness-by-construction
  • Concurrency
  • Golang

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. 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. Behavioral types in programming languages. Foundations and Trends in Programming Languages, 3(2-3):95-230, 2016. URL: https://doi.org/10.1561/2500000031.
  2. Lorenzo Bettini, Mario Coppo, Loris D'Antoni, Marco De Luca, Mariangiola Dezani-Ciancaglini, and Nobuko Yoshida. Global progress in dynamically interleaved multiparty sessions. In CONCUR 2008 - Concurrency Theory, pages 418-433. Springer, 2008. Google Scholar
  3. David Castro-Perez, Raymond Hu, Sung-Shik Jongmans, Nicholas Ng, and Nobuko Yoshida. Distributed programming using role-parametric session types in go. In POPL'19. ACM, 2019. URL: https://doi.org/10.1145/3290342.
  4. Mario Coppo, Mariangiola Dezani-Ciancaglini, Luca Padovani, and Nobuko Yoshida. Inference of Global Progress Properties for Dynamically Interleaved Multiparty Sessions. In 15th International Conference on Coordination Models and Languages, volume 7890 of LNCS, pages 45-59. Springer, 2013. Google Scholar
  5. Mario Coppo, Mariangiola Dezani-Ciancaglini, Nobuko Yoshida, and Luca Padovani. Global Progress for Dynamically Interleaved Multiparty Sessions. MSCS, 26:238-302, 2015. Google Scholar
  6. Zak Cutner, Nobuko Yoshida, and Martin Vassor. Deadlock-Free Asynchronous Message Reordering in Rust with Multiparty Session Types. In 27th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, volume abs/2112.12693. ACM, 2022. Google Scholar
  7. Romain Demangeon and Kohei Honda. Nested protocols in session types. In CONCUR 2012 - Concurrency Theory, pages 272-286. Springer, 2012. Google Scholar
  8. Romain Demangeon, Kohei Honda, Raymond Hu, Rumyana Neykova, and Nobuko Yoshida. Practical interruptible conversations: distributed dynamic verification with multiparty session types and python. Formal Methods in System Design, 46(3):197-225, 2015. URL: https://doi.org/10.1007/s10703-014-0218-8.
  9. Pierre-Malo Deniélou and Nobuko Yoshida. Dynamic multirole session types. In POPL'11, pages 435-446. ACM, 2011. Google Scholar
  10. Pierre-Malo Deniélou and Nobuko Yoshida. Multiparty compatibility in communicating automata: Characterisation and synthesis of global session types. In ICALP 2013, volume 7966 of LNCS, pages 174-186. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-39212-2_18.
  11. Pierre-Malo Deniélou, Nobuko Yoshida, Andi Bejleri, and Raymond Hu. Parameterised multiparty session types. Logical Methods in Computer Science, 8(4), 2012. URL: https://doi.org/10.2168/LMCS-8(4:6)2012.
  12. Mariangiola Dezani-Ciancaglini, Ugo de'Liguoro, and Nobuko Yoshida. On progress for structured communications. In TGC 2007, volume 4912 of LNCS, pages 257-275. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-78663-4_18.
  13. Docker: Empowering app development for developers. https://www.docker.com/, November 2020.
  14. Julia Gabet and Nobuko Yoshida. Static Race Detection and Mutex Safety and Liveness for Go Programs. In ECOOP'20, LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. Google Scholar
  15. Simon Gay and Antonio Ravara, editors. Behavioural Types: from Theory to Tools. River Publishers series in automation, control and robotics. River Publishers, June 2017. Google Scholar
  16. Githut 2.0: A small place to discover languages in github. https://madnight.github.io/githut/#/pull_requests/2020/3, 2020.
  17. Issac Gouy. Computer language benchmark game. http://benchmarksgame.alioth.debian.org, 2017.
  18. gRPC - a high-performance, open source universal rpc framework. https://grpc.io/, November 2020.
  19. Paul Harvey, Simon Fowler, Ornela Dardha, and Simon J. Gay. Multiparty Session Types for Safe Runtime Adaptation in an Actor Language. In ECOOP 2021, volume 194 of LIPIcs, pages 10:1-10:30. Schloss Dagstuhl, 2021. URL: https://doi.org/10.4230/LIPIcs.ECOOP.2021.10.
  20. C. A. R. Hoare. Communicating Sequential Processes. Prentice-Hall, Inc., 1985. Google Scholar
  21. Kohei Honda, Nobuko Yoshida, and Marco Carbone. Multiparty asynchronous session types. In Proc. of 35th Symp. on Princ. of Prog. Lang., POPL '08, pages 273-284. ACM, 2008. URL: https://doi.org/10.1145/1328438.1328472.
  22. Kohei Honda, Nobuko Yoshida, and Marco Carbone. Multiparty asynchronous session types. J. ACM, 63(1):9:1-9:67, 2016. URL: https://doi.org/10.1145/2827695.
  23. Raymond Hu. Distributed programming using Java APIs generated from Session Types. Behavioural Types: from Theory to Tools, pages 287-308, 2017. Google Scholar
  24. Raymond Hu, Dimitrios Kouzapas, Olivier Pernet, Nobuko Yoshida, and Kohei Honda. Type-Safe Eventful Sessions in Java. In ECOOP 2010, volume 6183 of LNCS, pages 329-353. Springer, 2010. Google Scholar
  25. Raymond Hu and Nobuko Yoshida. Hybrid session verification through endpoint API generation. In FASE 2016, volume 9633 of LNCS, pages 401-418. Springer, 2016. URL: https://doi.org/10.1007/978-3-662-49665-7_24.
  26. Raymond Hu and Nobuko Yoshida. Explicit connection actions in multiparty session types. In FASE 2017, volume 10202 of LNCS, pages 116-133. Springer, 2017. URL: https://doi.org/10.1007/978-3-662-54494-5_7.
  27. 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. Foundations of session types and behavioural contracts. ACM Comput. Surv., 49(1):3:1-3:36, 2016. URL: https://doi.org/10.1145/2873052.
  28. Keigo Imai, Rumyana Neykova, Nobuko Yoshida, and Shoji Yuen. Multiparty session programming with global protocol combinators. In ECOOP 2020, volume 166 of LIPIcs, pages 9:1-9:30. Schloss Dagstuhl, 2020. URL: https://doi.org/10.4230/LIPIcs.ECOOP.2020.9.
  29. Jules Jacobs, Stephanie Balzer, and Robbert Krebbers. Connectivity graphs: a method for proving deadlock freedom based on separation logic. Proc. ACM Program. Lang., 6(POPL):1-33, 2022. URL: https://doi.org/10.1145/3498662.
  30. Jules Jacobs, Stephanie Balzer, and Robbert Krebbers. Multiparty GV: Functional Multiparty Session Types with Certified Deadlock Freedom. Proc. ACM Program. Lang., 6(ICFP), August 2022. URL: https://doi.org/10.1145/3547638.
  31. Sung-Shik Jongmans and Petra van den Bos. A Predicate Transformer for Choreographies - Computing Preconditions in Choreographic Programming. In ESOP 2022, volume 13240 of LNCS, pages 520-547. Springer, 2022. URL: https://doi.org/10.1007/978-3-030-99336-8_19.
  32. Kubernetes: Production-grade container orchestration. https://kubernetes.io/, June 2017.
  33. Dimitrios Kouzapas, Ornela Dardha, Roly Perera, and Simon J. Gay. Typechecking protocols with Mungo and StMungo. In PPDP, pages 146-159, 2016. URL: https://doi.org/10.1145/2967973.2968595.
  34. Dimitrios Kouzapas, Nobuko Yoshida, Raymond Hu, and Kohei Honda. On Asynchronous Eventful Session Semantics. MSCS, 29:1-62, 2015. Google Scholar
  35. Nicolas Lagaillardie, Rumyana Neykova, and Nobuko Yoshida. Implementing Multiparty Session Types in Rust. In Coordination Models and Languages, volume 12134, pages 127-136. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-50029-08.
  36. Julien Lange, Nicholas Ng, Bernardo Toninho, and Nobuko Yoshida. Fencing off Go: Liveness and safety for channel-based programming. In Giuseppe Castagna and Andrew D. Gordon, editors, POPL 2017, pages 748-761. ACM, 2017. Google Scholar
  37. Julien Lange, Nicholas Ng, Bernardo Toninho, and Nobuko Yoshida. A Static Verification Framework for Message Passing in Go using Behavioural Types. In 40th International Conference on Software Engineering, pages 1137-1148. ACM, 2018. Google Scholar
  38. Julien Lange, Emilio Tuosto, and Nobuko Yoshida. From communicating machines to graphical choreographies. In POPL 2015, pages 221-232. ACM, 2015. URL: https://doi.org/10.1145/2676726.2676964.
  39. Ziheng Liu, Shuofei Zhu, Boqin Qin, Hao Chen, and Linhai Song. Automatically detecting and fixing concurrency bugs in Go software systems. In ASPLOS '21, April 2021. Google Scholar
  40. Robin Milner, Joachim Parrow, and David Walker. A calculus of mobile processes, i. Information and Computation, 100(1):1-40, 1992. URL: https://doi.org/10.1016/0890-5401(92)90008-4.
  41. Robin Milner, Joachim Parrow, and David Walker. A calculus of mobile processes, ii. Information and Computation, 100(1):41-77, 1992. URL: https://doi.org/10.1016/0890-5401(92)90009-5.
  42. Anson Miu, Francisco Ferreira, Nobuko Yoshida, and Fangyi Zhou. Communication-safe web programming in TypeScript with Routed Multiparty Session Types. In CC 2021, 2021. Google Scholar
  43. Rumyana Neykova, Raymond Hu, Nobuko Yoshida, and Fahd Abdeljallal. A session type provider: Compile-time API generation of distributed protocols with refinements in F#. In CC 2018, pages 128-138. ACM, 2018. URL: https://doi.org/10.1145/3178372.3179495.
  44. Rumyana Neykova and Nobuko Yoshida. Featherweight Scribble. Models, Languages, and Tools for Concurrent and Distributed Programming, 11665:236-259, 2019. URL: https://doi.org/10.1007/978-3-030-21485-2_14.
  45. Nicholas Ng, José Gabriel de Figueiredo Coutinho, and Nobuko Yoshida. Protocols by default - safe MPI code generation based on session types. In CC 2015, volume 9031 of LNCS, pages 212-232. Springer, 2015. URL: https://doi.org/10.1007/978-3-662-46663-6_11.
  46. Nicholas Ng and Nobuko Yoshida. Pabble: parameterised scribble. Service Oriented Computing and Applications, 9(3-4):269-284, 2015. URL: https://doi.org/10.1007/s11761-014-0172-8.
  47. Nicholas Ng and Nobuko Yoshida. Static deadlock detection for concurrent Go by global session graph synthesis. In CC 2016, pages 174-184. ACM, 2016. URL: https://doi.org/10.1145/2892208.2892232.
  48. The nuScr authors. nuscr homepage. https://nuscr.github.io/nuscr/, 2019.
  49. Stuart Russell and Peter Norvig. Artificial Intelligence: A Modern Approach. Prentice Hall series in artificial intelligence. Pearson Education, 2016. Google Scholar
  50. Alceste Scalas, Ornela Dardha, Raymond Hu, and Nobuko Yoshida. A linear decomposition of multiparty sessions for safe distributed programming. In ECOOP 2017, volume 74 of LIPIcs, pages 24:1-24:31. Schloss Dagstuhl, 2017. URL: https://doi.org/10.4230/LIPIcs.ECOOP.2017.24.
  51. Scribble Authors. Scribble: Describing multiparty protocols. http://www.scribble.org/, 2015. Accessed in Nov. 2020.
  52. Stack overflow developer survey 2020. https://insights.stackoverflow.com/survey/2020, 2020.
  53. Kai Stadtmüller, Martin Sulzmann, and Peter Thiemann. Static trace-based deadlock analysis for synchronous mini-go. In APLAS 2016, volume 10017 of LNCS, pages 116-136, 2016. URL: https://doi.org/10.1007/978-3-319-47958-3_7.
  54. I. Stoica, R. Morris, D. Liben-Nowell, D.R. Karger, M.F. Kaashoek, F. Dabek, and H. Balakrishnan. Chord: a Scalable Peer-to-peer Lookup Protocol for Internet Applications. IEEE/ACM Transactions on Networking, 11(1):17-32, 2003. URL: https://doi.org/10.1109/TNET.2002.808407.
  55. Martin Sulzmann and Peter Thiemann. Forkable regular expressions. In LATA 2016, volume 9618 of LNCS, pages 194-206. Springer, 2016. URL: https://doi.org/10.1007/978-3-319-30000-9_15.
  56. Tengfei Tu, Xiaoyu Liu, Linhai Song, and Yiying Zhang. Understanding real-world concurrency bugs in go. In ASPLOS 2019, pages 865-878. ACM, 2019. URL: https://doi.org/10.1145/3297858.3304069.
  57. Malte Viering, Raymond Hu, Patrick Eugster, and Lukasz Ziarek. A multiparty session typing discipline for fault-tolerant event-driven distributed programming. PACMPL, 5(OOPSLA):1-30, 2021. URL: https://doi.org/10.1145/3485501.
  58. Philip Wadler. Propositions as Sessions. In ICFP'12, pages 273-286. ACM, 2012. Google Scholar
  59. Felix A. Wolf, Linard Arquint, Martin Clochard, Wytse Oortwijn, João C. Pereira, and Peter Müller. Gobra: Modular specification and verification of Go programs. In CAV, pages 367-379. Springer, 2021. Google Scholar
  60. Nobuko Yoshida and Lorenzo Gheri. A very gentle introduction to Multiparty Session Types. In 16th International Conference on Distributed Computing and Internet Technology, volume 11969 of LNCS, pages 73-93. Springer, 2020. Google Scholar
  61. T. Yuan, G. Li, J. Lu, C. Liu, L. Li, and J. Xue. GoBench: A benchmark suite of real-world Go concurrency bugs. In CGO 2021. ACM/IEEE, 2021. Google Scholar
  62. Fangyi Zhou, Francisco Ferreira, Raymond Hu, Rumyana Neykova, and Nobuko Yoshida. Statically Verified Refinements for Multiparty Protocols. PACMPL, 4(OOPSLA), 2020. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact