Multiparty asynchronous session types

ABSTRACT

Communication is becoming one of the central elements in software development. As a potential typed foundation for structured communication-centred programming, session types have been studied over the last decade for a wide range of process calculi and programming languages, focussing on binary (two-party) sessions. This work extends the foregoing theories of binary session types to multiparty, asynchronous sessions, which often arise in practical communication-centred applications. Presented as a typed calculus for mobile processes, the theory introduces a new notion of types in which interactions involving multiple peers are directly abstracted as a global scenario. Global types retain a friendly type syntax of binary session types while capturing complex causal chains of multiparty asynchronous interactions. A global type plays the role of a shared agreement among communication peers, and is used as a basis of efficient type checking through its projection onto individual peers. The fundamental properties of the session type discipline such as communication safety, progress and session fidelity are established for generaln-party asynchronous interactions.

REFERENCES

• 1: Eduardo Bonelli and Adriana Compagnoni. Multipoint session types for a distributed calculus. In TGC07, LNCS. Springer, 2008. To appear.
• 2: Marco Carbone, Kohei Honda, Nobuko Yoshida, Robin Milner, Gary Brown, and Steve Ross-Talbot. A theoretical basis of communication--centred concurrent programming. To be published by W3C. Available at www.dcs.qmul.ac.uk/~carbonem/cdlpaper, 2006.
• 3: Marco Carbone, Kohei Honda, and Nobuko Yoshida. Structured Communication--Centred Programming for Web Services. In ESOP'07, volume 4421 of LNCS, pages 2--17. Springer, 2007.
• 4: Mario Coppo, Mariangiola Dezani-Ciancaglini, and Nobuko Yoshida. Asynchronous Session Types and Progress for Object--Oriented Languages. In FMOODS'07, volume 4468 of LNCS, pages 1--31, 2007.
• 5: Ricardo Corin , Pierre-Malo Denielou , Cedric Fournet , Karthikeyan Bhargavan , James Leifer, Secure Implementations for Typed Session Abstractions, Proceedings of the 20th IEEE Computer Security Foundations Symposium, p.170-186, July 06-08, 2007 [doi>10.1109/CSF.2007.29]
• 6: Mariangiola Dezani-Ciancaglini, Dimitris Mostrous, Nobuko Yoshida, and Sophia Drossopoulou. Session Types for Object-Oriented Languages. In ECOOP'06, volume 4067 of LNCS, pages 328--352. Springer, 2006.
• 7: Mariangiola Dezani-Ciancaglini, Ugo de' Liguoro, and Nobuko Yoshida. On Progress for Structured Communications. In TGC07, LNCS. Springer, 2008. To appear.
• 8: Manuel Fähndrich , Mark Aiken , Chris Hawblitzel , Orion Hodson , Galen Hunt , James R. Larus , Steven Levi, Language support for fast and reliable message-based communication in singularity OS, Proceedings of the 1st ACM SIGOPS/EuroSys European Conference on Computer Systems 2006, April 18-21, 2006, Leuven, Belgium
• 9: Pablo Garralda , Adriana Compagnoni , Mariangiola Dezani-Ciancaglini, BASS: boxed ambients with safe sessions, Proceedings of the 8th ACM SIGPLAN international conference on Principles and practice of declarative programming, July 10-12, 2006, Venice, Italy [doi>10.1145/1140335.1140344]
• 10: Simon Gay , Malcolm Hole, Subtyping for session types in the pi calculus, Acta Informatica, v.42 n.2, p.191-225, November 2005 [doi>10.1007/s00236-005-0177-z]
• 11: Simon Gay and Vasco T. Vasconcelos. Asynchronous functional session types. TR 2007-251, University of Glasgow, may 2007.
• 12: Jean-Yves Girard, Linear logic, Theoretical Computer Science, v.50 n.1, p.1-102, Jan. 30, 1987 [doi>10.1016/0304-3975(87)90045-4]
• 13: Matthew Hennessy, A Distributed Pi-Calculus, Cambridge University Press, New York, NY, 2007
• 14: Kohei Honda , Mario Tokoro, An Object Calculus for Asynchronous Communication, Proceedings of the European Conference on Object-Oriented Programming, p.133-147, July 15-19, 1991
• 15: Kohei Honda , Vasco Thudichum Vasconcelos , Makoto Kubo, Language Primitives and Type Discipline for Structured Communication-Based Programming, Proceedings of the 7th European Symposium on Programming: Programming Languages and Systems, p.122-138, March 28-April 04, 1998
• 16: Kohei Honda, Nobuko Yoshida, and Marco Carbone. Web Services, Mobile Processes and Types. The Bulletin of the European Association for Theoretical Computer Science, February(91):165--185, 2007.
• 17: Kohei Honda, Nobuko Yoshida, and Marco Carbone. Full version of this paper. Technical Report 5, Imperial College London, 2007.
• 18: Raymond Hu, Nobuko Yoshida, and Kohei Honda. Type-safe Communication in Java with Session Types. http://www.doc.ic.ac.uk/~rh105/sessiondj.html, March 2007.
• 19: Atsushi Igarashi , Naoki Kobayashi, A generic type system for the Pi-calculus, Theoretical Computer Science, v.311 n.1-3, p.121-163, 23 January 2004 [doi>10.1016/S0304-3975(03)00325-6]
• 20: Naoki Kobayashi. A new type system for deadlock-free processes. In CONCUR'06, volume 4137 of LNCS, pages 233--247, 2006.
• 21: Naoki Kobayashi , Shin Saito , Eijiro Sumii, An Implicitly-Typed Deadlock-Free Process Calculus, Proceedings of the 11th International Conference on Concurrency Theory, p.489-503, August 22-25, 2000
• 22: Leslie Lamport, Time, clocks, and the ordering of events in a distributed system, Communications of the ACM, v.21 n.7, p.558-565, July 1978 [doi>10.1145/359545.359563]
• 23: Dimitris Mostrous and Nobuko Yoshida. Two session typing systems for higher-order mobile processes. In TLCA'07, volume 4583 of LNCS, pages 321--335. Springer, 2007.
• 24: Matthias Neubauer and Peter Thiemann. Session Types for Asynchronous Communication. Universität Freiburg, 2004.
• 25: Matthias Neubauer and Peter Thiemann. An Implementation of Session Types. In PADL, volume 3057 of LNCS, pages 56--70. Springer, 2004.
• 26: Benjamin C. Pierce, Types and programming languages, MIT Press, Cambridge, MA, 2002
• 27: Bruce Schneier, Applied Cryptography: Protocols, Algorithms, and Source Code in C, John Wiley & Sons, Inc., New York, NY, 1993
• 28: Charlene O'Hanlon, A conversation with Steve Ross-Talbot, Queue, v.4 n.2, March 2006 [doi>10.1145/1122674.1122684]
• 29: Kaku Takeuchi , Kohei Honda , Makoto Kubo, An Interaction-based Language and its Typing System, Proceedings of the 6th International PARLE Conference on Parallel Architectures and Languages Europe, p.398-413, July 04-08, 1994
• 30: UNIFI. International Organization for Standardization ISO 20022 UNIversal Financial Industry message scheme. http://www.iso20022.org.
• 31: Vasco T. Vasconcelos , Simon J. Gay , António Ravara, Type checking a multithreaded functional language with session types, Theoretical Computer Science, v.368 n.1-2, p.64-87, December, 2006 [doi>10.1016/j.tcs.2006.06.028]
• 32: WS-CDL. Web Services Choreography Working Group. http://www.w3.org/2002/ws/chor/.
• 33: Nobuko Yoshida, Graph Types for Monadic Mobile Processes, Proceedings of the 16th Conference on Foundations of Software Technology and Theoretical Computer Science, p.371-386, December 18-20, 1996
• 34: Nobuko Yoshida , Vasco T. Vasconcelos, Language Primitives and Type Discipline for Structured Communication-Based Programming Revisited: Two Systems for Higher-Order Session Communication, Electronic Notes in Theoretical Computer Science (ENTCS), v.171 n.4, p.73-93, July, 2007 [doi>10.1016/j.entcs.2007.02.056]

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages
          Subjects: Process models

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory
      D.3.3 Language Constructs and Features

General Terms:
Design, Theory

Keywords:
causality, choreography, communications, mobile processes, multiparty, session types, structured programming