Hostname: page-component-8448b6f56d-c4f8m Total loading time: 0 Render date: 2024-04-23T06:35:47.319Z Has data issue: false hasContentIssue false
  • English
  • Français

Global escape in multiparty sessions†

Published online by Cambridge University Press:  10 November 2014

SARA CAPECCHI ,
ELENA GIACHINO  and
NOBUKO YOSHIDA
SARA CAPECCHI
Affiliation:
Dipartimento di Informatica, Università di Torino, Corso Svizzera 185, 10149 Torino, Italy Email: sara.capecchi@unito.it
ELENA GIACHINO
Affiliation:
Dipartimento di Informatica, Università di Bologna/INRIA, Via Zamboni 33, 40126 Bologna, Italy Email: giachino@cs.unibo.it
NOBUKO YOSHIDA
Affiliation:
Department of Computing, Imperial College, South Kensington Campus, London SW7 2AZ, United Kingdom Email: n.yoshida@imperial.ac.uk
Get access Rights & Permissions [Opens in a new window]

Abstract

This article proposes a global escape mechanism which can handle unexpected or unwanted conditions changing the default execution of distributed communicational flows, preserving compatibility of the multiparty conversations. Our escape is realized by a collection of asynchronous local exceptions which can be thrown at any stage of the communication and to any subsets of participants in a multiparty session. This flexibility enables to model complex exceptions such as criss-crossing global interactions and error handling for distributed cooperating threads. Guided by multiparty session types, our semantics is proven to provide a termination algorithm for global escapes. Our type system guarantees further safety and liveness properties, such as progress within the session and atomicity of escapes with respect to the subset of involved participants.

Type
Paper
Information
Mathematical Structures in Computer Science , Volume 26 , Special Issue 2: Special Issue: Behavioural Types Part 1 , February 2016 , pp. 156 - 205
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.)

Footnotes

†

This work has been partially supported by ICT COST Action IC1201 BETTY EPSRC EP/G015635/01, EP/K011715/01, EP/K034413, EP/L00058X/1 EU project FP7-231620 ‘HATS’, EU project FP7-612985 UpScale, EU project ASCENS 257414, EU project FP7-610582 ENVISAGE MIUR Project ‘CINA’, Ateneo/CSP Project ‘SALT’ and by ANR 11 INSE 007 ‘REVER’.

References

Baeten, J. C. M. and Wejland, W. (1990) Process Algebra, Cambridge University Press.CrossRefGoogle Scholar
Bettini, L., Coppo, M., D'Antoni, L., De Luca, M., Dezani-Ciancaglini, M. and Yoshida, N. (2008) Global progress in dynamically interleaved multiparty sessions. In: International Conference on Concurrency Theory . Springer Lecture Notes in Computer Science 5201 418–433.CrossRefGoogle Scholar
Bocchi, L., Laneve, C. and Zavattaro, G. (2003) A calculus for long-running transactions. In: Proceedinds of Formal Methods for Open Object-Based Distributed Systems. Springer Lecture Notes in Computer Science 2884 124–138.CrossRefGoogle Scholar
Boreale, M., Bruni, R., Nicola, R. and Loreti, M. (2008) Sessions and pipelines for structured service programming. In: Barthe, G. and Boer, F. (eds.) Proceedings of Formal Methods for Open Object-Based Distributed Systems, Lecture Notes in Computer Science, 5051 19–38.CrossRefGoogle Scholar
Bravetti, M. and Zavattaro, G. (2009) On the expressive power of process interruption and compensation. Mathematical Structures in Computer Science, 19 (3) 565–599.CrossRefGoogle Scholar
Capecchi, S., Giachino, E. and Yoshida, N. (2010) Global escape in multiparty sessions. In: Proceedings of Foundations of Software Technology and Theoretical Computer Science. Leibniz International Proceedings in Informatics 8 Schloss Dagstuhl–Leibniz-Zentrum für Informatik 338–351.Google Scholar
Carbone, M. (2009) Session-based choreography with exceptions. Electronic Notes in Theoretical Computer Science 241 35–55.CrossRefGoogle Scholar
Carbone, M., Honda, K. and Yoshida, N. (2008) Structured interactional exceptions for session types. In: 19th International Conference on Concurrency Theory. Springer Lecture Notes in Computer Science 5201 402–417.CrossRefGoogle Scholar
Carbone, M., Honda, K., Yoshida, N., Milner, R., Brown, G. and Ross-Talbot, S. (2006) A theoretical basis of communication-centred concurrent programming. WCD-Working Note.Google Scholar
Castor Filho, F., Romanovsky, A. and Rubira, C. M. F. (2009) Improving reliability of cooperative concurrent systems with exception flow analysis. Journal Systems and Software 82 874–890.CrossRefGoogle Scholar
Demangeon, R. and Honda, K. (2012) Nested protocols in session types. In: Koutny, M. and Ulidowski, I. (eds.)Proceedings of International Conference on Concurrency Theory . 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: Proceedings of International Conference on Concurrency Theory . Springer Lecture Notes in Computer Science 6269 343–357.CrossRefGoogle Scholar
Gay, S. and Hole, M. (2005) Subtyping for session types in the Pi-calculus. Acta Informatica 42 (2/3) 191–225.CrossRefGoogle Scholar
Honda, K., Hu, R., Neykova, R., Chen, T.-C., Demangeon, R., Deniélou, P.-M. and Yoshida, N. (2012) Structuring communication with session types. In: Proceedings of Concurrent Objects and Beyond. Springer Lecture Notes in Computer Science 8665 105–127.CrossRefGoogle Scholar
Honda, K., Mukhamedov, A., Brown, G., Chen, T.-C. and Yoshida, N. (2011) Scribbling interactions with a formal foundation. In: International Conference on Distributed Computing and Internet Technology. Springer Lecture Notes in Computer Science 6536 55–75.CrossRefGoogle Scholar
Honda, K., Vasconcelos, V. T. and Kubo, M. (1998) Language primitives and type disciplines for structured communication-based programming. In: Proceedings of European Symposium on Programming. Springer Lecture Notes in Computer Science 1381 22–138.Google Scholar
Honda, K., Yoshida, N. and Carbone, M. (2008) Multiparty asynchronous session types. In: Principles of Programming Languages. ACM 43 273–284.Google Scholar
Hu, R., Kouzapas, D., Pernet, O., Yoshida, N. and Honda, K. (2010) Type-safe eventful sessions in Java. In: Proceedings of European Conference on Object-Oriented Programming. Springer Lecture Notes in Computer Science 6183 329–353.CrossRefGoogle Scholar
Hu, R., Neykova, R., Yoshida, N. and Demangeon, R. (2013) Practical interruptible conversations: Distributed dynamic verification with session types and Python. In: 4th International Conference on Runtime Verification Springer Lecture Notes in Computer Science 8174 130–148.CrossRefGoogle Scholar
Hu, R., Yoshida, N. and Honda, K. (2008) Session-based distributed programming in java. In: Proceedings of European Conference on Object-Oriented Programming. Springer Lecture Notes in Computer Science 5142 516–541.CrossRefGoogle Scholar
Jakšić, S. and Padovani, L. (2012) Exception handling for copyless messaging. In: Proceedings of the 14th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming, ACM 84 151–162.Google Scholar
Lanese, I. and Montesi, F. (2010) Error handling: From theory to practice. In: Margaria, T. and Steffen, B. (eds.) Leveraging Applications of Formal Methods, Verification, and Validation. volume 6416 Springer Berlin/Heidelberg 66–81.CrossRefGoogle Scholar
Lanese, I., Vaz, C. and Ferreira, C. (2010) On the expressive power of primitives for compensation handling. In: Proceedings of European Symposium on Programming 366–386.CrossRefGoogle Scholar
Lapadula, A., Pugliese, R. and Tiezzi, F. (2007) A calculus for orchestration of web services. In: Proceedings of European Symposium on Programming. Springer Lecture Notes in Computer Science 4421 33–47.CrossRefGoogle Scholar
Lewerentz, C. and Lindner, T. (eds.) (1995) Formal Development of Reactive Systems - Case Study Production Cell, London, UK. Springer-Verlag.CrossRefGoogle Scholar
Neykova, R., Yoshida, N. and Hu, R. (2013). SPY: Local verification of global protocols. In: 4th International Conference on Runtime Verification Springer Lecture Notes in Computer Science 8174 358–363.CrossRefGoogle Scholar
Rubira, C. M. F., de Lemos, R., Ferreira, G. R. M. and Filho, F. C. (2005) Exception handling in the development of dependable component-based systems. Software Practice and Experience 35 (3) 195–236.CrossRefGoogle Scholar
Rubira, C. M. F. and Wu, Z. (1995). Fault tolerance in concurrent object-oriented software through coordinated error recovery. In: Proceedings of the Twenty-Fifth International Symposium on Fault-Tolerant Computing, Washington, DC, USA, IEEE Computer Society 499.Google Scholar
Takeuchi, K., Honda, K. and Kubo, M. (1994). An interaction-based language and its typing system. In: Proceedings of Parallel Architectures and Languages Europe. Springer Lecture Notes in Computer Science 817 398–413.CrossRefGoogle Scholar
Tartanoglu, F., Issarny, V., Romanovsky, A. and Levy, N. (2003) Coordinated forward error recovery for composite web services. IEEE Symposium on Reliable Distributed Systems, 167.Google Scholar
Vieira, H. T., Caires, L. and Seco, J. C. (2008) The conversation calculus: A model of service-oriented computation. In: Proceedings of European Symposium on Programming. Springer Lecture Notes in Computer Science 4960 269–283.CrossRefGoogle Scholar
Xu, J., Romanovsky, A. and Randell, B. (1998) Coordinated exception handling in distributed object systems: From model to system implementation. In: Proceedings of the The 18th International Conference on Distributed Computing Systems, Washington, DC, USA, IEEE Computer Society 12–21.Google Scholar