Hostname: page-component-78c5997874-mlc7c Total loading time: 0 Render date: 2024-11-05T13:13:58.222Z Has data issue: false hasContentIssue false

Global progress for dynamically interleaved multiparty sessions

Published online by Cambridge University Press:  10 November 2014

MARIO COPPO
Affiliation:
Dipartimento di Informatica, Università di Torino, Corso Svizzera 185, Torino, Italy Emails: [email protected], [email protected], [email protected]
MARIANGIOLA DEZANI-CIANCAGLINI
Affiliation:
Dipartimento di Informatica, Università di Torino, Corso Svizzera 185, Torino, Italy Emails: [email protected], [email protected], [email protected]
NOBUKO YOSHIDA
Affiliation:
Department of Computing, Imperial College London, London, United Kingdom Email: [email protected]
LUCA PADOVANI
Affiliation:
Dipartimento di Informatica, Università di Torino, Corso Svizzera 185, Torino, Italy Emails: [email protected], [email protected], [email protected]

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
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 642658.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 418433.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 124140.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 5065.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 162176.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 240256.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 1938.Google Scholar
Brand, D. and Zafiropulo, P. (1983) On communicating finite-state machines. Journal of the ACM 30 323342.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 100115.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) 43994440.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 237252.Google Scholar
Capecchi, S., Giachino, E. and Yoshida, N. (2010b) Global escape in multiparty sessions. In: FSTTCS'10. Leibniz International Proceedings in Informatics 8 338351.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 1327.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 263274.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 211228.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 2545.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 209224.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 4559.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 131.Google Scholar
Dardha, O., Giachino, E. and Sangiorgi, D. (2012) Session types revisited. In: PPDP'12. ACM Press 139150.Google Scholar
Demangeon, R. and Honda, K. (2012) Nested protocols in session types. In: CONCUR'12. Springer Lecture Notes in Computer Science 7454 272286.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 343357.Google Scholar
Deniélou, P.-M. and Yoshida, N. (2011) Dynamic multirole session types. In: POPL'11. ACM Press 435446.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 194213.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 174186.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) 146.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 128.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 257275.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 328352.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 124141.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 105127.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 291293.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 5575.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 22138.Google Scholar
Honda, K., Yoshida, N. and Carbone, M. (2008) Multiparty asynchronous session types. In: POPL'08. ACM Press 273284.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 329353.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 130148.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 516541.Google Scholar
Kobayashi, N. (2002) A type system for lock-free processes. Information and Computation 177 122159.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 305314.Google Scholar
Lange, J. and Tuosto, E. (2012) Synthesising choreographies from local session types. In: CONCUR'12. Springer Lecture Notes in Computer Science 7454 225239.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 425439.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 316332.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 358363.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 202218.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) 2227.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 110126.Google Scholar
Nielsen, L., Yoshida, N. and Honda, K. (2010) Multiparty symmetric sum types. In: EXPRESS'10. Electronic Proceedings in Theoretical Computer Science 41 121135.Google Scholar
Padovani, L. (2013) From lock freedom to progress using session types. In: PLACES'13. Electronic Proceedings in Theoretical Computer Science. 137 319.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 152167.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 266278.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 269283.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 371386.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 7393.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 226246.Google Scholar