Hostname: page-component-78c5997874-j824f Total loading time: 0 Render date: 2024-11-05T15:24:12.881Z Has data issue: false hasContentIssue false

Global escape in multiparty sessions

Published online by Cambridge University Press:  10 November 2014

SARA CAPECCHI
Affiliation:
Dipartimento di Informatica, Università di Torino, Corso Svizzera 185, 10149 Torino, Italy Email: [email protected]
ELENA GIACHINO
Affiliation:
Dipartimento di Informatica, Università di Bologna/INRIA, Via Zamboni 33, 40126 Bologna, Italy Email: [email protected]
NOBUKO YOSHIDA
Affiliation:
Department of Computing, Imperial College, South Kensington Campus, London SW7 2AZ, United Kingdom Email: [email protected]

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
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 418433.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 124138.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 1938.CrossRefGoogle Scholar
Bravetti, M. and Zavattaro, G. (2009) On the expressive power of process interruption and compensation. Mathematical Structures in Computer Science, 19 (3) 565599.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 338351.Google Scholar
Carbone, M. (2009) Session-based choreography with exceptions. Electronic Notes in Theoretical Computer Science 241 3555.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 402417.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 874890.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 272286.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 343357.CrossRefGoogle Scholar
Gay, S. and Hole, M. (2005) Subtyping for session types in the Pi-calculus. Acta Informatica 42 (2/3) 191225.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 105127.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 5575.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 22138.Google Scholar
Honda, K., Yoshida, N. and Carbone, M. (2008) Multiparty asynchronous session types. In: Principles of Programming Languages. ACM 43 273284.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 329353.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 130148.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 516541.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 151162.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 6681.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 3347.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 358363.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) 195236.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 398413.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 269283.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 1221.Google Scholar