[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to main content
Springer Nature Link
Log in

ST4MP: A Blueprint of Multiparty Session Typing for Multilingual Programming

  • Conference paper
  • First Online:
Leveraging Applications of Formal Methods, Verification and Validation. Verification Principles (ISoLA 2022)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 13701))

Included in the following conference series:

Abstract

Multiparty session types (MPST) constitute a method to simplify construction and analysis of distributed systems. The idea is that well-typedness of processes at compile-time (statically) entails deadlock freedom and protocol compliance of their sessions of communications at execution-time (dynamically).

In practice, the premier approach to apply the MPST method in combination with mainstream programming languages has been based on API generation. However, existing MPST tools support only unilingual programming (homogeneity), while many real-world distributed systems are engineered using multilingual programming (heterogeneity).

In this paper, we present a blueprint of ST4MP: a tool to apply the MPST method in multilingual programming, based on API generation.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
£29.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
GBP 19.95
Price includes VAT (United Kingdom)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
GBP 59.99
Price includes VAT (United Kingdom)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
GBP 74.99
Price includes VAT (United Kingdom)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

Notes

  1. 1.

    Thus, typically, the application of the MPST method using API generation is not absolutely zero-cost in terms of overhead: while the vast majority of the work is done statically, a bit of work is done dynamically. Previous experiments indicate that this overhead is negligible in practice, though (e.g., [7]).

  2. 2.

    https://www.tiobe.com/tiobe-index/.

References

  1. Blanvillain, O., Brachthäuser, J.I., Kjaer, M., Odersky, M.: Type-level programming with match types. Proc. ACM Program. Lang. 6(POPL), 1–24 (2022)

    Google Scholar 

  2. Bocchi, L., Chen, T., Demangeon, R., Honda, K., Yoshida, N.: Monitoring networks through multiparty session types. Theor. Comput. Sci. 669, 33–58 (2017)

    Article  MathSciNet  Google Scholar 

  3. Bocchi, L., Honda, K., Tuosto, E., Yoshida, N.: A theory of design-by-contract for distributed multiparty interactions. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol. 6269, pp. 162–176. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-15375-4_12

    Chapter  MATH  Google Scholar 

  4. Bocchi, L., Lange, J., Yoshida, N.: Meeting deadlines together. In: CONCUR. LIPIcs, vol. 42, pp. 283–296. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2015)

    Google Scholar 

  5. Brand, D., Zafiropulo, P.: On communicating finite-state machines. J. ACM 30(2), 323–342 (1983)

    Article  MathSciNet  Google Scholar 

  6. Bray, T.: The JavaScript Object Notation (JSON) Data Interchange Format. RFC 7159, March 2014. https://doi.org/10.17487/RFC7159, https://www.rfc-editor.org/info/rfc7159

  7. Castro-Perez, D., Hu, R., Jongmans, S., Ng, N., Yoshida, N.: Distributed programming using role-parametric session types in Go: statically-typed endpoint APIs for dynamically-instantiated communication structures. Proc. ACM Program. Lang. 3(POPL), 29:1–29:30 (2019)

    Google Scholar 

  8. Cledou, G., Edixhoven, L., Jongmans, S.S., Proença, J.: API generation for multiparty session types, revisited and revised using Scala 3. In: ECOOP. LIPIcs, vol. 222, pp. 27:1–27:28. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)

    Google Scholar 

  9. Demangeon, R., Honda, K., Hu, R., Neykova, R., Yoshida, N.: Practical interruptible conversations: distributed dynamic verification with multiparty session types and Python. Formal Methods Syst. Des. 46(3), 197–225 (2015)

    Article  Google Scholar 

  10. Deniélou, P., Yoshida, N.: Dynamic multirole session types. In: POPL, pp. 435–446. ACM (2011)

    Google Scholar 

  11. Deniélou, P.-M., Yoshida, N.: Multiparty session types meet communicating automata. In: Seidl, H. (ed.) ESOP 2012. LNCS, vol. 7211, pp. 194–213. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-28869-2_10

    Chapter  Google Scholar 

  12. Deniélou, P.-M., Yoshida, N.: Multiparty compatibility in communicating automata: characterisation and synthesis of global session types. In: Fomin, F.V., Freivalds, R., Kwiatkowska, M., Peleg, D. (eds.) ICALP 2013. LNCS, vol. 7966, pp. 174–186. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39212-2_18

    Chapter  MATH  Google Scholar 

  13. Guanciale, R., Tuosto, E.: Realisability of pomsets. J. Log. Algebraic Methods Program. 108, 69–89 (2019)

    Article  MathSciNet  Google Scholar 

  14. Guanciale, R., Tuosto, E.: Pomcho: a tool chain for choreographic design. Sci. Comput. Program. 202, 102535 (2021)

    Article  Google Scholar 

  15. Hamers, R., Jongmans, S.-S.: Discourje: runtime verification of communication protocols in clojure. In: Biere, A., Parker, D. (eds.) TACAS 2020. LNCS, vol. 12078, pp. 266–284. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-45190-5_15

    Chapter  Google Scholar 

  16. Harvey, P., Fowler, S., Dardha, O., Gay, S.J.: Multiparty session types for safe runtime adaptation in an actor language. In: ECOOP. LIPIcs, vol. 194, pp. 10:1–10:30. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021)

    Google Scholar 

  17. Honda, K., Yoshida, N., Carbone, M.: Multiparty asynchronous session types. In: POPL, pp. 273–284. ACM (2008)

    Google Scholar 

  18. Honda, K., Yoshida, N., Carbone, M.: Multiparty asynchronous session types. J. ACM 63(1), 9:1–9:67 (2016)

    Google Scholar 

  19. Hu, R., Yoshida, N.: Hybrid session verification through endpoint API generation. In: Stevens, P., Wąsowski, A. (eds.) FASE 2016. LNCS, vol. 9633, pp. 401–418. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-662-49665-7_24

    Chapter  Google Scholar 

  20. Hu, R., Yoshida, N.: Explicit connection actions in multiparty session types. In: Huisman, M., Rubin, J. (eds.) FASE 2017. LNCS, vol. 10202, pp. 116–133. Springer, Heidelberg (2017). https://doi.org/10.1007/978-3-662-54494-5_7

    Chapter  Google Scholar 

  21. Imai, K., Neykova, R., Yoshida, N., Yuen, S.: Multiparty session programming with global protocol combinators. In: ECOOP. LIPIcs, vol. 166, pp. 9:1–9:30. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2020)

    Google Scholar 

  22. Jongmans, S.-S., Yoshida, N.: Exploring type-level bisimilarity towards more expressive multiparty session types. In: Müller, P. (ed.) ESOP 2020. LNCS, vol. 12075, pp. 251–279. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-44914-8_10

    Chapter  Google Scholar 

  23. King, J., Ng, N., Yoshida, N.: Multiparty session type-safe web development with static linearity. In: PLACES@ETAPS. EPTCS, vol. 291, pp. 35–46 (2019)

    Google Scholar 

  24. Kouzapas, D., Dardha, O., Perera, R., Gay, S.J.: Typechecking protocols with Mungo and StMungo: a session type toolchain for Java. Sci. Comput. Program. 155, 52–75 (2018)

    Article  Google Scholar 

  25. Lagaillardie, N., Neykova, R., Yoshida, N.: Implementing multiparty session types in rust. In: Bliudze, S., Bocchi, L. (eds.) COORDINATION 2020. LNCS, vol. 12134, pp. 127–136. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-50029-0_8

    Chapter  Google Scholar 

  26. Lange, J., Tuosto, E., Yoshida, N.: From communicating machines to graphical choreographies. In: POPL, pp. 221–232. ACM (2015)

    Google Scholar 

  27. Lange, J., Yoshida, N.: Verifying asynchronous interactions via communicating session automata. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11561, pp. 97–117. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-25540-4_6

    Chapter  Google Scholar 

  28. Miu, A., Ferreira, F., Yoshida, N., Zhou, F.: Communication-safe web programming in typescript with routed multiparty session types. In: CC, pp. 94–106. ACM (2021)

    Google Scholar 

  29. Neykova, R., Bocchi, L., Yoshida, N.: Timed runtime monitoring for multiparty conversations. Formal Asp. Comput. 29(5), 877–910 (2017)

    Article  MathSciNet  Google Scholar 

  30. Neykova, R., Hu, R., Yoshida, N., Abdeljallal, F.: A session type provider: compile-time API generation of distributed protocols with refinements in F#. In: CC, pp. 128–138. ACM (2018)

    Google Scholar 

  31. Neykova, R., Yoshida, N.: Featherweight scribble. In: Boreale, M., Corradini, F., Loreti, M., Pugliese, R. (eds.) Models, Languages, and Tools for Concurrent and Distributed Programming. LNCS, vol. 11665, pp. 236–259. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-21485-2_14

    Chapter  Google Scholar 

  32. Scalas, A., Dardha, O., Hu, R., Yoshida, N.: A linear decomposition of multiparty sessions for safe distributed programming. In: ECOOP. LIPIcs, vol. 74, pp. 24:1–24:31. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2017)

    Google Scholar 

  33. Scalas, A., Yoshida, N.: Less is more: multiparty session types revisited. Proc. ACM Program. Lang. 3(POPL), 30:1–30:29 (2019)

    Google Scholar 

  34. Scalas, A., Yoshida, N., Benussi, E.: EFFPI: verified message-passing programs in dotty. In: SCALA@ECOOP, pp. 27–31. ACM (2019)

    Google Scholar 

  35. Scalas, A., Yoshida, N., Benussi, E.: Verifying message-passing programs with dependent behavioural types. In: PLDI, pp. 502–516. ACM (2019)

    Google Scholar 

  36. Tuosto, E., Guanciale, R.: Semantics of global view of choreographies. J. Log. Algebr. Methods Program. 95, 17–40 (2018)

    Article  MathSciNet  Google Scholar 

  37. Voinea, A.L., Dardha, O., Gay, S.J.: Typechecking Java protocols with [St]Mungo. In: Gotsman, A., Sokolova, A. (eds.) FORTE 2020. LNCS, vol. 12136, pp. 208–224. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-50086-3_12

    Chapter  Google Scholar 

  38. Yoshida, N., Zhou, F., Ferreira, F.: Communicating finite state machines and an extensible toolchain for multiparty session types. In: Bampis, E., Pagourtzis, A. (eds.) FCT 2021. LNCS, vol. 12867, pp. 18–35. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-86593-1_2

    Chapter  Google Scholar 

  39. Zhou, F., Ferreira, F., Hu, R., Neykova, R., Yoshida, N.: Statically verified refinements for multiparty protocols. Proc. ACM Program. Lang. 4(OOPSLA), 148:1–148:30 (2020)

    Google Scholar 

Download references

Acknowledgements

Sung-Shik Jongmans: Netherlands Organisation of Scientific Research (NWO): 016.Veni.192.103.

José Proença: This work was partially supported by National Funds through FCT/MCTES (Portuguese Foundation for Science and Technology), within the CISTER Unit (UIDP/UIDB/04234/2020) and the IBEX project (PTDC/CCI-COM/4280/2021); also by national funds through FCT and European funds through EU ECSEL JU, within project VALU3S (ECSEL/0016/2019 - JU grant nr. 876852) – The JU receives support from the European Union’s Horizon 2020 research and innovation programme and Austria, Czech Republic, Germany, Ireland, Italy, Portugal, Spain, Sweden, Turkey. Disclaimer: This document reflects only the author’s view and the Commission is not responsible for any use that may be made of the information it contains.

Author information

Authors and Affiliations

  1. Open University of the Netherlands, Heerlen, Netherlands

    Sung-Shik Jongmans

  2. Centrum Wiskunde & Informatica (CWI), NWO-I, Amsterdam, Netherlands

    Sung-Shik Jongmans

  3. CISTER, ISEP, Polytechnic Institute of Porto, Porto, Portugal

    José Proença

Authors
  1. Sung-Shik Jongmans
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. José Proença
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to José Proença .

Editor information

Editors and Affiliations

  1. University of Limerick, CSIS and Lero, Limerick, Ireland

    Tiziana Margaria

  2. TU Dortmund, Dortmund, Germany

    Bernhard Steffen

Rights and permissions

Reprints and permissions

Copyright information

© 2022 The Author(s), under exclusive license to Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Jongmans, SS., Proença, J. (2022). ST4MP: A Blueprint of Multiparty Session Typing for Multilingual Programming. In: Margaria, T., Steffen, B. (eds) Leveraging Applications of Formal Methods, Verification and Validation. Verification Principles. ISoLA 2022. Lecture Notes in Computer Science, vol 13701. Springer, Cham. https://doi.org/10.1007/978-3-031-19849-6_26

Download citation

  • DOI: https://doi.org/10.1007/978-3-031-19849-6_26

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-031-19848-9

  • Online ISBN: 978-3-031-19849-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation