Explicit Connection Actions in Multiparty Session Types

  • Raymond HuEmail author
  • Nobuko Yoshida
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10202)


This work extends asynchronous multiparty session types (MPST) with explicit connection actions to support protocols with optional and dynamic participants. The actions by which endpoints are connected and disconnected are a key element of real-world protocols that is not treated in existing MPST works. In addition, the use cases motivating explicit connections often require a more relaxed form of multiparty choice: these extensions do not satisfy the conservative restrictions used to ensure safety in standard syntactic MPST. Instead, we develop a modelling-based approach to validate MPST safety and progress for these enriched protocols. We present a toolchain implementation, for distributed programming based on our extended MPST in Java, and a core formalism, demonstrating the soundness of our approach. We discuss key implementation issues related to the proposed extensions: a practical treatment of choice subtyping for MPST progress, and multiparty correlation of dynamic binary connections.


Local Type Session Type Connection Action Shared Channel Global Type 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.



We thank Gary Brown and Steve Ross-Talbot for collaborations, and Rumyana Neykova for comments. This work is partially supported by EPSRC projects EP/K034413/1, EP/K011715/1, EP/L00058X/1, EP/N027833/1, and EP/N028201/1; and by EU FP7 612985 (UPSCALE).


  1. 1.
    Ancona, D., et al.: Behavioral types in programming languages. Found. Trends Program. Lang. 3(2–3), 95–230 (2016)CrossRefGoogle Scholar
  2. 2.
    Basu, S., Bultan, T.: Automatic verification of interactions in asynchronous systems with unbounded buffers. In: ASE 2014, pp. 743–754. ACM (2014)Google Scholar
  3. 3.
    Basu, S., Bultan, T.: Automated choreography repair. In: Stevens, P., Wąsowski, A. (eds.) FASE 2016. LNCS, vol. 9633, pp. 13–30. Springer, Heidelberg (2016). doi: 10.1007/978-3-662-49665-7_2 CrossRefGoogle Scholar
  4. 4.
    Basu, S., Bultan, T., Ouederni, M.: Deciding choreography realizability. In: POPL 2012, pp. 191–202. ACM (2012)Google Scholar
  5. 5.
    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). doi: 10.1007/978-3-642-15375-4_12 CrossRefGoogle Scholar
  6. 6.
    Bocchi, L., Lange, J., Yoshida, N.: Meeting deadlines together. In: CONCUR 2015. LIPIcs, vol. 42, pp. 283–296. Schloss Dagstuhl (2015)Google Scholar
  7. 7.
    Bollig, B., Cyriac, A., Hélouët, L., Kara, A., Schwentick, T.: Dynamic communicating automata and branching high-level MSCs. In: Dediu, A.-H., Martín-Vide, C., Truthe, B. (eds.) LATA 2013. LNCS, vol. 7810, pp. 177–189. Springer, Heidelberg (2013). doi: 10.1007/978-3-642-37064-9_17 CrossRefGoogle Scholar
  8. 8.
    Bollig, B., Hélouët, L.: Realizability of dynamic MSC languages. In: Ablayev, F., Mayr, E.W. (eds.) CSR 2010. LNCS, vol. 6072, pp. 48–59. Springer, Heidelberg (2010). doi: 10.1007/978-3-642-13182-0_5 CrossRefGoogle Scholar
  9. 9.
    Brand, D., Zafiropulo, P.: On communicating finite-state machines. J. ACM 30, 323–342 (1983)MathSciNetCrossRefzbMATHGoogle Scholar
  10. 10.
    Caires, L., Vieira, H.T.: Conversation types. Theor. Comput. Sci. 411(51–52), 4399–4440 (2010)MathSciNetCrossRefzbMATHGoogle Scholar
  11. 11.
    Cécé, G., Finkel, A.: Verification of programs with half-duplex communication. Inf. Comput. 202(2), 166–190 (2005)MathSciNetCrossRefzbMATHGoogle Scholar
  12. 12.
    Coppo, M., Dezani-Ciancaglini, M., Yoshida, N., Padovani, L.: Global progress for dynamically interleaved multiparty sessions. Math. Struct. Comput. Sci. 760, 1–65 (2015)CrossRefzbMATHGoogle Scholar
  13. 13.
    Demangeon, R., Honda, K.: Full abstraction in a subtyped pi-calculus with linear types. In: Katoen, J.-P., König, B. (eds.) CONCUR 2011. LNCS, vol. 6901, pp. 280–296. Springer, Heidelberg (2011). doi: 10.1007/978-3-642-23217-6_19 CrossRefGoogle Scholar
  14. 14.
    Demangeon, R., Honda, K.: Nested protocols in session types. In: Koutny, M., Ulidowski, I. (eds.) CONCUR 2012. LNCS, vol. 7454, pp. 272–286. Springer, Heidelberg (2012). doi: 10.1007/978-3-642-32940-1_20 CrossRefGoogle Scholar
  15. 15.
    Demangeon, R., Honda, K., Hu, R., Neykova, R., Yoshida, N.: Practical interruptible conversations: distributed dynamic verification with multiparty session types and python. In: Formal Methods in System Design, pp. 1–29 (2015)Google Scholar
  16. 16.
    Deniélou, P.-M., Yoshida, N.: Dynamic multirole session types. In: POPL 2011, pp. 435–446. ACM (2011)Google Scholar
  17. 17.
    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). doi: 10.1007/978-3-642-28869-2_10 CrossRefGoogle Scholar
  18. 18.
    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). doi: 10.1007/978-3-642-39212-2_18 Google Scholar
  19. 19.
    Fowler, S.: An erlang implementation of multiparty session actors. In: ICE 2016. EPTCS, vol. 223, pp. 36–50 (2016)Google Scholar
  20. 20.
    Gay, S., Hole, M.: Subtyping for session types in the pi-calculus. Acta Informatica 42(2/3), 191–225 (2005)MathSciNetCrossRefzbMATHGoogle Scholar
  21. 21.
    Honda, K., Yoshida, N., Carbone, M.: Multiparty asynchronous session types. In: POPL 2008, pp. 273–284. ACM (2008)Google Scholar
  22. 22.
    Honda, K., Yoshida, N., Carbone, M.: Multiparty asynchronous session types. J. ACM 63(1), 9 (2016)MathSciNetCrossRefzbMATHGoogle Scholar
  23. 23.
    Hu, R., Yoshida, N.: Explicit Connection Actions in Multiparty Session Types (Long Version).
  24. 24.
    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). doi: 10.1007/978-3-662-49665-7_24 CrossRefGoogle Scholar
  25. 25.
    Hu, R., Yoshida, N., Honda, K.: Session-based distributed programming in java. In: Vitek, J. (ed.) ECOOP 2008. LNCS, vol. 5142, pp. 516–541. Springer, Heidelberg (2008). doi: 10.1007/978-3-540-70592-5_22 CrossRefGoogle Scholar
  26. 26.
    Imai, K., Yuen, S., Agusa, K.: Session type inference in haskell. In: PLACES. EPTCS, vol. 69, pp. 74–91 (2010)Google Scholar
  27. 27.
    Jespersen, T.B.L., Munksgaard, P., Larsen, K.F.: Session types for rust. In: WGP 2015, pp. 13–22. ACM (2015)Google Scholar
  28. 28.
    Klensin, J.: IETF RFC 5321 Simple Mail Transfer Protocol.
  29. 29.
    Kouzapas, D., Yoshida, N., Hu, R., Honda, K.: On asynchronous eventful session semantics. Math. Struct. Comput. Sci. 26(2), 303–364 (2016)MathSciNetCrossRefzbMATHGoogle Scholar
  30. 30.
    Lange, J., Tuosto, E., Yoshida, N.: From communicating machines to graphical choreographies. In: POPL 2015, pp. 221–232. ACM (2015)Google Scholar
  31. 31.
    Leucker, M., Madhusudan, P., Mukhopadhyay, S.: Dynamic message sequence charts. In: Agrawal, M., Seth, A. (eds.) FSTTCS 2002. LNCS, vol. 2556, pp. 253–264. Springer, Heidelberg (2002). doi: 10.1007/3-540-36206-1_23 CrossRefGoogle Scholar
  32. 32.
    Lindley, S., Morris, J.G.: Lightweight Functional Session Types.
  33. 33.
    Neykova, R., Bocchi, L., Yoshida, N.: Timed runtime monitoring for multiparty conversations. In: BEAT 2014. EPTCS, vol. 162, pp. 19–26 (2014)Google Scholar
  34. 34.
    Neykova, R., Yoshida, N., Hu, R.: SPY: local verification of global protocols. In: Legay, A., Bensalem, S. (eds.) RV 2013. LNCS, vol. 8174, pp. 358–363. Springer, Heidelberg (2013). doi: 10.1007/978-3-642-40787-1_25 CrossRefGoogle Scholar
  35. 35.
    Ng, N., Figueiredo Coutinho, J.G., Yoshida, N.: Protocols by default. In: Franke, B. (ed.) CC 2015. LNCS, vol. 9031, pp. 212–232. Springer, Heidelberg (2015). doi: 10.1007/978-3-662-46663-6_11 CrossRefGoogle Scholar
  36. 36.
  37. 37.
    Padovani, L.: Fair subtyping for multi-party session types. Math. Struct. Comput. Sci. 26(3), 424–464 (2016)MathSciNetCrossRefzbMATHGoogle Scholar
  38. 38.
    Perera, R., Lange, J., Gay, S.J.: Multiparty compatibility for concurrent objects. In: PLACES 2016. EPTCS, vol. 211, pp. 73–82 (2016)Google Scholar
  39. 39.
    Postel, J., Reynolds, J.: IETF RFC 959 File Transfer Protocol.
  40. 40.
    Pucella, R., Tov, J.A.: Haskell session types with (almost) no class. In: Haskell 2008, pp. 25–36. ACM (2008)Google Scholar
  41. 41.
    Salaün, G., Bultan, T., Roohi, N.: Realizability of choreographies using process algebra encodings. IEEE Trans. Serv. Comput. 5(3), 290–304 (2012)CrossRefGoogle Scholar
  42. 42.
    Scalas, A., Yoshida, N.: Lightweight session programming in scala. In: ECOOP 2016. LIPIcs, vol. 56, pp. 21:1–21:28. Schloss Dagstuhl (2016)Google Scholar
  43. 43.
    Scribble.: GitHub repository.
  44. 44.
    Scribble homepage.
  45. 45.
    Sivaramakrishnan, K.C., Qudeisat, M., Ziarek, L., Nagaraj, K., Eugster, P.: Efficient sessions. Sci. Comput. Program. 78(2), 147–167 (2013)CrossRefzbMATHGoogle Scholar
  46. 46.
    Yoshida, N., Deniélou, P.-M., Bejleri, A., Hu, R.: Parameterised multiparty session types. In: Ong, L. (ed.) FoSSaCS 2010. LNCS, vol. 6014, pp. 128–145. Springer, Heidelberg (2010). doi: 10.1007/978-3-642-12032-9_10 CrossRefGoogle Scholar
  47. 47.
    Yoshida, N., Hu, R., Neykova, R., Ng, N.: The scribble protocol language. In: Abadi, M., Lluch Lafuente, A. (eds.) TGC 2013. LNCS, vol. 8358, pp. 22–41. Springer, Cham (2014). doi: 10.1007/978-3-319-05119-2_3 CrossRefGoogle Scholar

Copyright information

© Springer-Verlag GmbH Germany 2017

Authors and Affiliations

  1. 1.Imperial College LondonLondonUK

Personalised recommendations