×
Kouzapas, Dimitrios; Forsberg Gutkovas, Ramunas; Voinea, A. Laura; Gay, Simon J.

A session type system for asynchronous unreliable broadcast communication. (English) Zbl 07906375

Log. Methods Comput. Sci. 20, No. 3, Paper No. 13, 54 p. (2024).
Summary: Session types are formal specifications of communication protocols, allowing protocol implementations to be verified by typechecking. Up to now, session type disciplines have assumed that the communication medium is reliable, with no loss of messages. However, unreliable broadcast communication is common in a wide class of distributed systems such as ad-hoc and wireless sensor networks. Often such systems have structured communication patterns that should be amenable to analysis by means of session types, but the necessary theory has not previously been developed. We introduce the Unreliable Broadcast Session Calculus, a process calculus with unreliable broadcast communication, and equip it with a session type system that we show is sound. We capture two common operations, broadcast and gather, inhabiting dual session types. Message loss may lead to non-synchronised session endpoints. To further account for unreliability we provide with an autonomous recovery mechanism that does not require acknowledgements from session participants. Our type system ensures soundness, safety, and progress between the synchronised endpoints within a session. We demonstrate the expressiveness of our framework by implementing Paxos, the textbook protocol for reaching consensus in an unreliable, asynchronous network.

MSC:

03B70 Logic in computer science
68-XX Computer science

Keywords:

session types; type safety; broadcasting; unreliability; Paxos

Software:

Paxos
Cite Review PDF
Full Text: DOI arXiv
OA License

References:

[1] D. Kouzapas, R. F. Gutkovas, A. L. Voinea, and S. J. Gay Vol. 20:3 13:32 D. Kouzapas, R. F. Gutkovas, A. L. Voinea, and S. J. Gay Vol. 20:3 13:36 D. Kouzapas, R. F. Gutkovas, A. L. Voinea, and S. J. Gay Vol. 20:3
[2] References [ABB + 16] 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:95-230, 2016.
[3] Manuel Adameit, Kirstin Peters, and Uwe Nestmann. Session types for link failures. In Ahmed Bouajjani and Alexandra Silva, editors, Formal Techniques for Distributed Objects, Components, and Systems, pages 1-16, Cham, 2017. Springer International Publishing. · Zbl 1489.68396
[4] Matthew Alan Le Brun and Ornela Dardha. Magπ: Types for failure-prone communication. In Thomas Wies, editor, Programming Languages and Systems -32nd European Symposium on Programming, ESOP 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, April 22-27, 2023, Proceedings, volume 13990 of Lecture Notes in Computer Science, pages 363-391. Springer, 2023. doi:10.1007/978-3-031-30044-8_14. · Zbl 1541.68035 · doi:10.1007/978-3-031-30044-8_14
[5] Giovanni Bernardi, Ornela Dardha, Simon J. Gay, and Dimitrios Kouzapas. On duality relations for session types. In Matteo Maffei and Emilio Tuosto, editors, Trustworthy Global Computing, pages 51-66, Berlin, Heidelberg, 2014. Springer Berlin Heidelberg. · Zbl 1444.68111
[6] BHJ + 11] Johannes Borgström, Shuqin Huang, Magnus Johansson, Palle Raabjerg, Björn Victor, Jo-hannes Åman Pohjola, and Joachim Parrow. Broadcast psi-calculi with an application to wireless protocols. In SEFM 2011, pages 74-89, 2011. · Zbl 1350.68041
[7] Giuseppe Castagna, Mariangiola Dezani-Ciancaglini, and Luca Padovani. On global types and multi-party session. Logical Methods in Computer Science, 8(1), 2012.
[8] Mario Coppo, Mariangiola Dezani-Ciancaglini, Nobuko Yoshida, and Luca Padovani. Global progress for dynamically interleaved multiparty sessions. Mathematical Structures in Computer Science, 26(2):238-302, 2016. · Zbl 1361.68165
[9] Tushar D Chandra, Robert Griesemer, and Joshua Redstone. Paxos made live: an engineering perspective. In Proceedings of the twenty-sixth annual ACM symposium on Principles of distributed computing, pages 398-407. ACM, 2007.
[10] Sara Capecchi, Elena Giachino, and Nobuko Yoshida. Global escape in multiparty sessions. Mathematical Structures in Computer Science, 26, 2 2016. · Zbl 1361.68163
[11] Marco Carbone, Kohei Honda, and Nobuko Yoshida. Structured interactional exceptions in session types. In CONCUR, volume 5201 of LNCS, pages 402-417. Springer, 2008. · Zbl 1160.68459
[12] Adam Dunkels, Fredrik Österlind, and Zhitao He. An adaptive communication architecture for wireless sensor networks. In Proceedings of Embedded Networked Sensor Systems, SenSys ’07, pages 335-349. ACM, 2007.
[13] Pierre-Malo Deniélou, Nobuko Yoshida, Andi Bejleri, and Raymond Hu. Parameterised multiparty session types. Logical Methods in Computer Science, 8(4), 2012. · Zbl 1248.68089
[14] Simon J. Gay and António Ravara, editors. Behavioural Types: from Theory to Tools. River Publishers, 2017.
[15] Simon J. Gay and Vasco Thudichum Vasconcelos. Linear type theory for asynchronous session types. J. Funct. Program., 20(1):19-50, 2010. doi:10.1017/S0956796809990268. · Zbl 1185.68194 · doi:10.1017/S0956796809990268
[16] HKP + 10] Raymond Hu, Dimitrios Kouzapas, Olivier Pernet, Nobuko Yoshida, and Kohei Honda. Type-safe eventful sessions in java. In ECOOP, pages 329-353, 2010.
[17] Matthew Hennessy and James Riely. Resource access control in systems of mobile agents. Infor-mation and Computation, 173(1):82 -120, 2002. · Zbl 1009.68081
[18] Kohei Honda, Vasco Thudichum Vasconcelos, and Makoto Kubo. Language primitives and type discipline for structured communication-based programming. In ESOP, pages 122-138. Springer-Verlag, 1998.
[19] Kohei Honda, Nobuko Yoshida, and Marco Carbone. Multiparty asynchronous session types. In POPL, pages 273-284, 2008. · Zbl 1295.68150
[20] Dimitrios Kouzapas, Ramunas Gutkovas, and Simon J. Gay. Session types for broadcasting. In PLACES, pages 25-31, 2014.
[21] Dimitrios Kouzapas. A Study of Bisimulation Theory for Session Types. PhD thesis, Imperial College London, 2012.
[22] Dimitrios Kouzapas, Nobuko Yoshida, Raymond Hu, and Kohei Honda. On asynchronous eventful session semantics. Mathematical Structures in Computer Science, 26(2):303-364, 2016. doi:10.1017/S096012951400019X. · Zbl 1361.68170 · doi:10.1017/S096012951400019X
[23] L + 01] Leslie Lamport et al. Paxos made simple. ACM Sigact News, 32(4):18-25, 2001.
[24] Leslie Lamport. The part-time parliament. ACM Trans. Comput. Syst., 16(2):133-169, 1998.
[25] Nicholas Ng and Nobuko Yoshida. Pabble: parameterised scribble. Service Oriented Computing and Applications, 9(3-4):269-284, 2015. doi:10.1007/s11761-014-0172-8. · doi:10.1007/s11761-014-0172-8
[26] Kirstin Peters, Uwe Nestmann, and Wagner Christoph. Ftmpst: Fault-tolerant multiparty session types, 2023. https://arxiv.org/pdf/2204.07728.pdf.
[27] Nobuko Yoshida and Vasco T. Vasconcelos. Language primitives and type discipline for structured communication-based programming revisited: Two systems for higher-order session communica-tion. Electronic Notes in Theoretical Computer Science, 171(4):73 -93, 2007. 13:48 D. Kouzapas, R. F. Gutkovas, A. L. Voinea, and S. J. Gay Vol. 20:3
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.