Hostname: page-component-8448b6f56d-mp689 Total loading time: 0 Render date: 2024-04-18T17:10:30.815Z Has data issue: false hasContentIssue false
  • English
  • Français

Global progress for dynamically interleaved multiparty sessions

Published online by Cambridge University Press:  10 November 2014

MARIO COPPO ,
MARIANGIOLA DEZANI-CIANCAGLINI ,
NOBUKO YOSHIDA  and
LUCA PADOVANI
MARIO COPPO
Affiliation:
Dipartimento di Informatica, Università di Torino, Corso Svizzera 185, Torino, Italy Emails: coppo@di.unito.it, dezani@di.unito.it, padovani@di.unito.it
MARIANGIOLA DEZANI-CIANCAGLINI
Affiliation:
Dipartimento di Informatica, Università di Torino, Corso Svizzera 185, Torino, Italy Emails: coppo@di.unito.it, dezani@di.unito.it, padovani@di.unito.it
NOBUKO YOSHIDA
Affiliation:
Department of Computing, Imperial College London, London, United Kingdom Email: n.yoshida@imperial.ac.uk
LUCA PADOVANI
Affiliation:
Dipartimento di Informatica, Università di Torino, Corso Svizzera 185, Torino, Italy Emails: coppo@di.unito.it, dezani@di.unito.it, padovani@di.unito.it
Get access Rights & Permissions [Opens in a new window]

Abstract

A multiparty session forms a unit of structured communication among many participants which follow communication sequences specified as a global type. When a process is engaged in two or more sessions simultaneously, different sessions can be interleaved and can interfere at runtime. Previous work on multiparty session types has ignored session interleaving, providing a limited progress property ensured only within a single session, by assuming non-interference among different sessions and by forbidding delegation. This paper develops, besides a more traditional, compositional communication type system, a novel static interaction type system for global progress in dynamically interleaved and interfered multiparty sessions. The interaction type system infers causalities of channels making sure that processes do not get stuck at intermediate stages of sessions also in presence of delegation.

Type
Paper
Information
Mathematical Structures in Computer Science , Volume 26 , Special Issue 2: Special Issue: Behavioural Types Part 1 , February 2016 , pp. 238 - 302
Copyright
Copyright © Cambridge University Press 2014 

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Acciai, L. and Boreale, M. (2008) A type system for client progress in a service-oriented calculus. In: Concurrency, Graphs and Models. Springer Lecture Notes in Computer Science 5065 642–658.CrossRefGoogle Scholar
Bettini, L., Coppo, M., D'Antoni, L., Luca, M. D., Dezani-Ciancaglini, M. and Yoshida, N. (2008) Global progress in dynamically interleaved multiparty sessions. In: CONCUR'08. Springer Lecture Notes in Computer Science 5201 418–433.Google Scholar
Bhargavan, K., Corin, R., Deniélou, P.-M., Fournet, C. and Leifer, J. J. (2009) Cryptographic protocol synthesis and verification for multiparty sessions. In: CSF'09. IEEE Computer Society Press 124–140.Google Scholar
Bocchi, L., Chen, T.-C., Demangeon, R., Honda, K. and Yoshida, N. (2013) Monitoring networks through multiparty session types. In: FMOODS/FORTE'13. Springer Lecture Notes in Computer Science 7892 50–65.CrossRefGoogle Scholar
Bocchi, L., Honda, K., Tuosto, E. and Yoshida, N. (2010) A theory of design-by-contract for distributed multiparty interactions. In: CONCUR'10. Springer Lecture Notes in Computer Science 6269 162–176.CrossRefGoogle Scholar
Bonelli, E. and Compagnoni, A. (2008) Multipoint session types for a distributed calculus. In: TGC'07. Springer Lecture Notes in Computer Science 4912 240–256.CrossRefGoogle Scholar
Boreale, M., Bruni, R., De Nicola, R. and Loreti, M. (2008) Sessions and pipelines for structured service programming. In: FMOODS'08. Springer Lecture Notes in Computer Science 5051 19–38.Google Scholar
Brand, D. and Zafiropulo, P. (1983) On communicating finite-state machines. Journal of the ACM 30 323–342.CrossRefGoogle Scholar
Bruni, R. and Mezzina, L. G. (2008) Types and deadlock freedom in a calculus of services, sessions and pipelines. In: AMAST'08. Springer Lecture Notes in Computer Science 5140 100–115.Google Scholar
Buscemi, M. G., Coppo, M., Dezani-Ciancaglini, M. and Montanari, U. (2012) Constraints for service contracts. In: TGC'11. Springer Lecture Notes in Computer Science 104–120.Google Scholar
Caires, L. and Vieira, H. T. (2010) Conversation types. Theoretical Computer Science 411 (51–52) 4399–4440.Google Scholar
Capecchi, S., Castellani, I., Dezani-Ciancaglini, M. and Rezk, T. (2010a) Session types for access and information flow control. In: CONCUR'10. Springer Lecture Notes in Computer Science 6269 237–252.Google Scholar
Capecchi, S., Giachino, E. and Yoshida, N. (2010b) Global escape in multiparty sessions. In: FSTTCS'10. Leibniz International Proceedings in Informatics 8 338–351.Google Scholar
Carbone, M. and Debois, S. (2010) A graphical approach to progress for structured communication in web services. In: ICE'10. Electronic Proceedings in Theoretical Computer Science 38 13–27.Google Scholar
Carbone, M., Honda, K. and Yoshida, N. (2012) Structured communication-centered programming for web services. ACM Transactions on Programming Languages and Systems 34 (2) 8.CrossRefGoogle Scholar
Carbone, M. and Montesi, F. (2013) Deadlock-freedom-by-design: Multiparty asynchronous global programming. In: POPL'13. ACM 263–274.Google Scholar
Castagna, G., Dezani-Ciancaglini, M. and Padovani, L. (2012) On global types and multi-party session. Logical Methods in Computer Science 8 (1) 24.Google Scholar
Castagna, G. and Padovani, L. (2009) Contracts for mobile processes. In: CONCUR'09. Springer Lecture Notes in Computer Science 5710 211–228.Google Scholar
Chen, T.-C., Bocchi, L., Deniélou, P.-M., Honda, K. and Yoshida, N. (2012) Asynchronous distributed monitoring for multiparty session enforcement. In: TGC'11. Springer Lecture Notes in Computer Science 7173 25–45.CrossRefGoogle Scholar
Chen, T.-C. and Honda, K. (2012) Specifying stateful asynchronous properties for distributed programs. In: CONCUR'12. Springer Lecture Notes in Computer Science 7454 209–224.Google Scholar
Coppo, M., Dezani-Ciancaglini, M., Padovani, L. and Yoshida, N. (2013) Inference of global progress properties for dynamically interleaved multiparty sessions. In: COORDINATION'13. Springer Lecture Notes in Computer Science 7890 45–59.Google Scholar
Coppo, M., Dezani-Ciancaglini, M. and Yoshida, N. (2007) Asynchronous session types and progress for object-oriented languages. In: FMOODS'07. Springer Lecture Notes in Computer Science 4468 1–31.Google Scholar
Dardha, O., Giachino, E. and Sangiorgi, D. (2012) Session types revisited. In: PPDP'12. ACM Press 139–150.Google Scholar
Demangeon, R. and Honda, K. (2012) Nested protocols in session types. In: CONCUR'12. Springer Lecture Notes in Computer Science 7454 272–286.CrossRefGoogle Scholar
Deniélou, P.-M. and Yoshida, N. (2010) Buffered communication analysis in distributed multiparty sessions. In: CONCUR'10. Springer Lecture Notes in Computer Science 6269 343–357.Google Scholar
Deniélou, P.-M. and Yoshida, N. (2011) Dynamic multirole session types. In: POPL'11. ACM Press 435–446.Google Scholar
Deniélou, P.-M. and Yoshida, N. (2012) Multiparty session types meet communicating automata. In: ESOP'12. Springer Lecture Notes in Computer Science 7211 194–213.Google Scholar
Deniélou, P.-M. and Yoshida, N. (2013) Multiparty compatibility in communicating automata: Characterisation and synthesis of global session types. In: ICALP'13. Springer Lecture Notes in Computer Science 7966 174–186.Google Scholar
Deniélou, P.-M., Yoshida, N., Bejleri, A. and Hu, R. (2012) Parameterised multiparty session types. Logical Methods in Computer Science 8 (4:6) 1–46.Google Scholar
Dezani-Ciancaglini, M. and de' Liguoro, U. (2010) Sessions and session types: An overview. In: WSFM'09. Springer Lecture Notes in Computer Science 6194 1–28.Google Scholar
Dezani-Ciancaglini, M., de' Liguoro, U. and Yoshida, N. (2008) On progress for structured communications. In: TGC'07. Springer Lecture Notes in Computer Science 4912 257–275.Google Scholar
Dezani-Ciancaglini, M., Mostrous, D., Yoshida, N. and Drossopoulou, S. (2006) Session types for object-oriented languages. In: ECOOP'06. Springer Lecture Notes in Computer Science 4067 328–352.CrossRefGoogle Scholar
Henriksen, A., Nielsen, L., Hildebrandt, T., Yoshida, N. and Henglein, F. (2013) Trustworthy pervasive healthcare services via multiparty session type. In: FHIES'12. Springer Lecture Notes in Computer Science 7789 124–141.Google Scholar
Honda, K., Hu, R., Neykova, R., Chen, T.-C., Demangeon, R., Deniélou, P.-M. and Yoshida, N. (2013) Structuring communication with session types. In: COB'12. Springer Lecture Notes in Computer Science. 8665 105–127.Google Scholar
Honda, K., Marques, E. R. B., Martins, F., Ng, N., Vasconcelos, V. T. and Yoshida, N. (2012) Verification of MPI programs using session types. In: EuroMPI. Springer Lecture Notes in Computer Science 7490 291–293.Google Scholar
Honda, K., Mukhamedov, A., Brown, G., Chen, T.-C. and Yoshida, N. (2011) Scribbling interactions with a formal foundation. In: ICDCIT'11. Springer Lecture Notes in Computer Science 6536 55–75.Google Scholar
Honda, K., Vasconcelos, V. T. and Kubo, M. (1998) Language primitives and type disciplines for structured communication-based programming. In: ESOP'98. Springer Lecture Notes in Computer Science 1381 22–138.Google Scholar
Honda, K., Yoshida, N. and Carbone, M. (2008) Multiparty asynchronous session types. In: POPL'08. ACM Press 273–284.Google Scholar
Hu, R., Kouzapas, D., Pernet, O., Yoshida, N. and Honda, K. (2010) Type-safe eventful sessions in Java. In: ECOOP'10. Springer Lecture Notes in Computer Science 6183 329–353.Google Scholar
Hu, R., Neykova, R., Yoshida, N., Demangeon, R. and Honda, K. (2013) Practical interruptible conversations: Distributed dynamic verification with session types and python. In: ICRV'13. Springer Lecture Notes in Computer Science. 8174 130–148.Google Scholar
Hu, R., Yoshida, N. and Honda, K. (2008) Session-based distributed programming in java. In: ECOOP'08. Springer Lecture Notes in Computer Science 5142 516–541.Google Scholar
Kobayashi, N. (2002) A type system for lock-free processes. Information and Computation 177 122–159.Google Scholar
Kouzapas, D. and Yoshida, N. (2013) Governed session semantics. In: CONCUR'13. Springer Lecture Notes in Computer Science. To appear.Google Scholar
Lanese, I., Vasconcelos, V. T., Martins, F. and Ravara, A. (2007) Disciplining orchestration and conversation in service-oriented computing. In: SEFM'07, IEEE Computer Society Press 305–314.Google Scholar
Lange, J. and Tuosto, E. (2012) Synthesising choreographies from local session types. In: CONCUR'12. Springer Lecture Notes in Computer Science 7454 225–239.Google Scholar
Milner, R. (1999) Communicating and Mobile Systems: The π-Calculus, Cambridge University Press.Google Scholar
Montesi, F. and Yoshida, N. (2013) Compositional choreographies. In: CONCUR'13. Springer Lecture Notes in Computer Science. 8052 425–439.Google Scholar
Mostrous, D., Yoshida, N. and Honda, K. (2009) Global Principal Typing in Partially Commutative Asynchronous Sessions. In: ESOP'09. Springer Lecture Notes in Computer Science 5502 316–332.Google Scholar
Neykova, R., Yoshida, N. and Hu, R. (2013) SPY:Local Verification of Global Protocols. In: ICRV'13. Springer Lecture Notes in Computer Science. 8174 358–363.CrossRefGoogle Scholar
Ng, N., Yoshida, N. and Honda, K. (2012a) Multiparty Session C: Safe Parallel Programming with Message Optimisation. In: TOOLS'12. Springer Lecture Notes in Computer Science 7304 202–218.Google Scholar
Ng, N., Yoshida, N., Niu, X., Tsoi, K. H. and Luke, W. (2012b) Session types: Towards safe and fast reconfigurable programming. SIGARCH Computer Architecture News 40 (5) 22–27.Google Scholar
Ng, N., Yoshida, N., Pernet, O., Hu, R. and Kryftis, Y. (2011) Safe parallel programming with session Java. In: COORDINATION'11. Springer Lecture Notes in Computer Science 6721 110–126.Google Scholar
Nielsen, L., Yoshida, N. and Honda, K. (2010) Multiparty symmetric sum types. In: EXPRESS'10. Electronic Proceedings in Theoretical Computer Science 41 121–135.Google Scholar
OOI (2010) Ocean observatories initiative. Available at: http://www.oceanleadership.org/programs-and-partnerships/ocean-observing/ooi/.Google Scholar
Padovani, L. (2013) From lock freedom to progress using session types. In: PLACES'13. Electronic Proceedings in Theoretical Computer Science. 137 3–19.CrossRefGoogle Scholar
Pierce, B. C. (2002) Types and Programming Languages. MIT Press.Google Scholar
Savara (2010) SAVARA JBoss RedHat Project. Available at: http://www.jboss.org/savara.Google Scholar
Scribble (2008) Scribble JBoss RedHat Project. Available at: http://www.jboss.org/scribble.Google Scholar
Sivaramakrishnan, K. C., Nagaraj, K., Ziarek, L. and Eugster, P. (2010) Efficient Session Type Guided Distributed Interaction. In: COORDINATION'10. Springer Lecture Notes in Computer Science 6116 152–167.Google Scholar
Swamy, N., Chen, J., Fournet, C., Strub, P.-Y., Bhargavan, K. and Yang, J. (2011) Secure distributed programming with value-dependent types. In: ICFP'11. ACM Press 266–278.Google Scholar
UNIFI (2002) International Organization for Standardization ISO 20022 UNIversal Financial Industry message scheme. Available at: http://www.iso20022.org.Google Scholar
Vieira, H. T., Caires, L. and Seco, J. (2008) The conversation calculus: A model of service-oriented computation. In: ESOP'08. Springer Lecture Notes in Computer Science 4960 269–283.Google Scholar
Web Services Choreography Working Group (2002) Web Services Choreography description language. Available at: http://www.w3.org/2002/ws/chor/.Google Scholar
Yoshida, N. (1996) Graph types for monadic mobile processes. In: FSTTCS'96. Springer Lecture Notes in Computer Science 1180 371–386.CrossRefGoogle Scholar
Yoshida, N. and Vasconcelos, V. T. (2007) Language primitives and type disciplines for structured communication-based programming revisited. In: SecRet'06. Elsevier Electronic Proceedings in Theoretical Computer Science 171 73–93.Google Scholar
Yoshida, N., Vasconcelos, V. T., Paulino, H. and Honda, K. (2008) Session-based compilation framework for multicore programming. In: FMCO'08. Springer Lecture Notes in Computer Science 5751 226–246.Google Scholar