×

Composition and decomposition of multiparty sessions. (English) Zbl 1462.68120

The authors look at multiparty sessions as open systems by allowing one to compose multiparty sessions by transforming two of their participants into a pair of coupled gateways, forwarding messages between the two sessions. It is shown that the session resulting from the composition can be typed, and its type can be computed from the global types of the starting sessions. As a consequence, lock-freedom is preserved by composition. Direct composition is also defined, which allows one to connect two global types without using gateways. Finally, a decomposition operator is proposed to split a global type into two, which is the left inverse of direct composition.

MSC:

68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68M14 Distributed systems
PDFBibTeX XMLCite
Full Text: DOI Link

References:

[1] Barbanera, F.; de’Liguoro, U.; Hennicker, R., Global types for open systems, (ICE (2018), Open Publishing Association), 4-20
[2] Barbanera, F.; de’Liguoro, U.; Hennicker, R., Connecting open systems of communicating finite state machines, J. Log. Algebraic Methods Program., 109, 1-34 (2019) · Zbl 1435.68211
[3] Barbanera, F.; Dezani-Ciancaglini, M., Open multiparty sessions, (ICE (2019), Open Publishing Association), 77-96
[4] Barbanera, F.; Dezani-Ciancaglini, M.; de’Liguoro, U., Compliance for reversible client/server interactions, (BEAT (2014), Open Publishing Association), 35-42
[5] Barbanera, F.; Dezani-Ciancaglini, M.; de’Liguoro, U., Reversible client/server interactions, Form. Asp. Comput., 28, 697-722 (2016) · Zbl 1345.68016
[6] BEHAPI website, Behapi website (2019)
[7] Bocchi, L.; Melgratti, H. C.; Tuosto, E., Resolving non-determinism in choreographies, (ESOP (2014), Springer), 493-512 · Zbl 1405.68071
[8] Bocchi, L.; Melgratti, H. C.; Tuosto, E., On resolving non-determinism in choreographies, Log. Methods Comput. Sci., 16 (2020) · Zbl 07269246
[9] Brand, D.; Zafiropulo, P., On communicating finite-state machines, J. ACM, 30, 323-342 (1983) · Zbl 0512.68039
[10] Bravetti, M.; Carbone, M.; Zavattaro, G., Undecidability of asynchronous session subtyping, Inf. Comput., 256, 300-320 (2017) · Zbl 1376.68098
[11] Bruni, R.; Corradini, A.; Gadducci, F.; Melgratti, H. C.; Montanari, U.; Tuosto, E., Data-driven choreographies à la Klaim, (Models, Languages, and Tools for Concurrent and Distributed Programming - Essays Dedicated to Rocco De Nicola on the Occasion of His 65th Birthday (2019), Springer), 170-190
[12] Caires, L.; Pérez, J. A., Multiparty session types within a canonical binary theory, and beyond, (FORTE (2016), Springer), 74-95 · Zbl 1347.68026
[13] Carbone, M.; Lindley, S.; Montesi, F.; Schürmann, C.; Wadler, P., Coherence generalises duality: a logical explanation of multiparty session types, (CONCUR (2016), Schloss Dagstuhl), 33:1-33:15 · Zbl 1392.68286
[14] Carbone, M.; Montesi, F.; Vieira, H. T., Choreographies for reactive programming, (2018) 1-25, CoRR
[15] Cardone, F.; Coppo, M., Recursive types, (Barendregt, H.; Dekkers, W.; Statman, R., Lambda Calculus with Types. Lambda Calculus with Types, Perspectives in Logic (2013), Cambridge University Press), 377-576
[16] Castagna, G.; Gesbert, N.; Padovani, L., A theory of contracts for web services, ACM Trans. Program. Lang. Syst., 31, 19:1-19:61 (2009)
[17] Castellani, I.; Dezani-Ciancaglini, M.; Giannini, P., Reversible sessions with flexible choices, Acta Inform., 56, 553-583 (2019) · Zbl 1462.68121
[18] Coppo, M.; Dezani-Ciancaglini, M.; Padovani, L.; Yoshida, N., A gentle introduction to multiparty asynchronous session types, (Formal Methods for Multicore Programming (2015), Springer), 146-178 · Zbl 1346.68034
[19] Coppo, M.; Dezani-Ciancaglini, M.; Yoshida, N.; Padovani, L., Global progress for dynamically interleaved multiparty sessions, Math. Struct. Comput. Sci., 26, 238-302 (2016) · Zbl 1361.68165
[20] Courcelle, B., Fundamental properties of infinite trees, Theor. Comput. Sci., 25, 95-169 (1983) · Zbl 0521.68013
[21] Dalla Preda, M.; Gabbrielli, M.; Giallorenzo, S.; Lanese, I.; Mauro, J., Dynamic choreographies: theory and implementation, Log. Methods Comput. Sci., 13, 1-57 (2017) · Zbl 1398.68088
[22] Demangeon, R.; Honda, K., Full abstraction in a subtyped Pi-calculus with linear types, (CONCUR (2011), Springer), 280-296 · Zbl 1343.68165
[23] Dezani-Ciancaglini, M.; Ghilezan, S.; Jaksic, S.; Pantovic, J.; Yoshida, N., Precise subtyping for synchronous multiparty sessions, (PLACES (2015), Open Publishing Association), 29-43
[24] Ferrari, G.; Guanciale, R.; Strollo, D.; Tuosto, E., Coordination via types in an event-based framework, (FORTE (2007), Springer), 66-80 · Zbl 1215.68148
[25] Ferrari, G.; Strollo, D.; Guanciale, R., JSCL: a middleware for service coordination, (Formal Methods for Networked and Distributed Systems (2006), Springer), 46-60
[26] Gabbrielli, M.; Giallorenzo, S.; Lanese, I.; Mauro, J., Guess who’s coming: runtime inclusion of participants in choreographies, (The Art of Modelling Computational Systems: A Journey from Logic and Concurrency to Security and Privacy - Essays Dedicated to Catuscia Palamidessi on the Occasion of Her 60th Birthday (2019), Springer), 118-138
[27] Gay, S., Subtyping supports safe session substitution, (A List of Successes That Can Change the World - Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday (2016), Springer), 95-108 · Zbl 1343.68056
[28] Gay, S.; Hole, M., Subtyping for session types in the Pi calculus, Acta Inform., 42, 191-225 (2005) · Zbl 1079.68065
[29] Ghilezan, S.; Jaksic, S.; Pantovic, J.; Scalas, A.; Yoshida, N., Precise subtyping for synchronous multiparty sessions, J. Log. Algebraic Methods Program., 104, 127-173 (2019) · Zbl 1423.68306
[30] Honda, K.; Vasconcelos, V. T.; Kubo, M., Language primitives and type discipline for structured communication-based programming, (ESOP (1998), Springer), 122-138
[31] Honda, K.; Yoshida, N.; Carbone, M., Multiparty asynchronous session types, (POPL (2008), ACM Press), 273-284 · Zbl 1295.68150
[32] Honda, K.; Yoshida, N.; Carbone, M., Multiparty asynchronous session types, J. ACM, 63, 9:1-9:67 (2016) · Zbl 1426.68047
[33] Hu, R.; Yoshida, N., Explicit connection actions in multiparty session types, (FASE (2017), Springer), 116-133
[34] Kobayashi, N., A type system for lock-free processes, Inf. Comput., 177, 122-159 (2002) · Zbl 1093.68065
[35] Kozen, D.; Silva, A., Practical Coinduction, Math. Struct. Comput. Sci., vol. 27, 1132-1152 (2017) · Zbl 1376.68095
[36] Lange, J., On the synthesis of choreographies (2014), Department of Computer Science, University of Leicester, Ph.D. thesis
[37] Lange, J.; Tuosto, E., Synthesising choreographies from local session types, (CONCUR (2012), Springer), 225-239 · Zbl 1364.68291
[38] Lange, J.; Yoshida, N., On the undecidability of asynchronous session subtyping, (FOSSACS (2017), Springer), 441-457 · Zbl 1486.68114
[39] Mostrous, D.; Yoshida, N.; Honda, K., Global principal typing in partially commutative asynchronous sessions, (ESOP (2009), Springer), 316-332 · Zbl 1234.68304
[40] Padovani, L., Deadlock and lock freedom in the linear π-calculus, (LICS (2014), ACM Press), 72:1-72:10 · Zbl 1392.68311
[41] Pierce, B. C., Types and Programming Languages (2002), MIT Press
[42] Savanovic, Z.; Vieira, H.; Galletta, L., A type language for message passing component-based systems, (ICE (2020), Open Publishing Association), 3-24
[43] Severi, P.; Dezani-Ciancaglini, M., Observational equivalence for multiparty sessions, Fundam. Inform., 167, 267-305 (2019) · Zbl 1436.68214
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.