×

Mixed choice in session types. (English) Zbl 07852926

Summary: Session types provide a flexible programming style for structuring interaction, and are used to guarantee a safe and consistent composition of distributed processes. Traditional session types include only one-directional input (external) and output (internal) guarded choices. This prevents the session-processes to explore the full expressive power of the \(\pi\)-calculus where mixed choice was proved more expressive. Recently Casal, Mordido, and Vasconcelos proposed binary session types with mixed choices \((\mathsf{CMV}^+)\). Surprisingly, in spite of an inclusion of unrestricted channels with mixed choice, \(\mathsf{CMV}^+\)’s mixed choice is rather separate and not mixed. We prove this negative result using two methodologies (using either the leader election problem or a synchronisation pattern as distinguishing feature), showing that there exists no good encoding from the \(\pi\)-calculus into \(\mathsf{CMV}^+\), preserving distribution. We then close their open problem on the encoding from \(\mathsf{CMV}^+\) into \(\mathsf{CMV}\) (without mixed choice), proving its soundness.

MSC:

68Qxx Theory of computing
Full Text: DOI

References:

[1] Ancona, D.; Bono, V.; Bravetti, M.; Campos, J.; Castagna, G.; Deniélou, P.; Gay, S. J.; Gesbert, N.; Giachino, E.; Hu, R.; Johnsen, E. B.; Martins, F.; Mascardi, V.; Montesi, F.; Neykova, R.; Ng, N.; Padovani, L.; Vasconcelos, V. T.; Yoshida, N., Behavioral Types in Programming Languages, Foundations and Trends in Programming Languages, vol. 3, 95-230, 2016
[2] Bisping, B.; Nestmann, U.; Peters, K., Coupled similarity: the first 32 years, Acta Inform., 57, 439-463, 2019 · Zbl 1476.68166
[3] Boer, F. S.; Palamidessi, C., Embedding as a tool for language comparison: on the CSP hierarchy, (Proc. of CONCUR, 1991, Springer), 127-141
[4] Boudol, G., Asynchrony and the π-calculus (Note), 1992, Rapport de Recherche 1702
[5] Cacciagrano, D.; Corradini, F.; Palamidessi, C., Explicit fairness in testing semantics, Log. Methods Comput. Sci., 5, 1-27, 2009 · Zbl 1163.68031
[6] Cardelli, L.; Gordon, A. D., Mobile ambients, Theor. Comput. Sci., 240, 177-213, 2000 · Zbl 0954.68108
[7] Casal, F.; Mordido, A.; Vasconcelos, V. T., Mixed sessions, Theor. Comput. Sci., 897, 23-48, 2022 · Zbl 1498.68181
[8] Fournet, C.; Gonthier, G., The reflexive chemical abstract machine and the join-calculus, (Steele, J. G., Proc. of POPL, 1996, ACM), 372-385
[9] Fu, Y., Theory of interaction, Theor. Comput. Sci., 611, 1-49, 2016 · Zbl 1353.68082
[10] Fu, Y.; Lu, H., On the expressiveness of interaction, Theor. Comput. Sci., 411, 1387-1451, 2010 · Zbl 1191.68436
[11] van Glabbeek, R.; Goltz, U.; Schicke, J. W., On synchronous and asynchronous interaction in distributed systems, (Proc. of MFCS, 2008), 16-35 · Zbl 1173.68585
[12] van Glabbeek, R. J., Musings on encodings and expressiveness, (Proc. of EXPRESS/SOS, 2012), 81-98 · Zbl 1459.68149
[13] van Glabbeek, R. J., A theory of encodings and expressiveness (extended abstract), (Proc. of FoSSaCS, 2018), 183-202 · Zbl 1504.68125
[14] van Glabbeek, R. J., Comparing the expressiveness of the π-calculus and CCS, (Sergey, I., Proc. of ETAPS, 2022, Springer), 548-574 · Zbl 1528.68258
[15] Gorla, D., Comparing communication primitives via their relative expressive power, Inf. Comput., 206, 931-952, 2008 · Zbl 1169.68009
[16] Gorla, D., A taxonomy of process calculi for distribution and mobility, Distrib. Comput., 23, 273-299, 2010 · Zbl 1231.68169
[17] Gorla, D., Towards a unified approach to encodability and separation results for process calculi, Inf. Comput., 208, 1031-1053, 2010 · Zbl 1209.68336
[18] Honda, K., Types for dyadic interaction, (Best, E., Proc. of CONCUR, 1993, Springer), 509-523
[19] Honda, K.; Tokoro, M., An object calculus for asynchronous communication, (Tokoro, M.; Nierstrasz, O.; Wegner, P., Proc. of ECOOP, 1992, Springer), 133-147
[20] Honda, K.; Vasconcelos, V. T.; Kubo, M., Language primitives and type discipline for structured communication-based programming, (Proc. of ESOP, 1998, Springer), 122-138
[21] Honda, K.; Yoshida, N.; Carbone, M., Multiparty asynchronous session types, J. ACM, 63, 1-67, 2016 · Zbl 1426.68047
[22] Hüttel, H.; Lanese, I.; Vasconcelos, V. T.; Caires, L.; Carbone, M.; Deniélou, P.; Mostrous, D.; Padovani, L.; Ravara, A.; Tuosto, E.; Vieira, H. T.; Zavattaro, G., Foundations of session types and behavioural contracts, ACM Comput. Surv., 49, 3:1-3:36, 2016
[23] Jongmans, S. S.; Yoshida, N., Exploring type-level bisimilarity towards more expressive multiparty session types, (Proc. of ESOP, 2020, Springer), 251-279 · Zbl 1508.68244
[24] Majumdar, R.; Mukund, M.; Stutz, F.; Zufferey, D., Generalising projection in asynchronous multiparty session types, (Haddad, S.; Varacca, D., Proc. of CONCUR, 2021), 35:1-35:24 · Zbl 07730637
[25] Milner, R.; Parrow, J.; Walker, D., A calculus of mobile processes, Part I and II, Inf. Comput., 100, 1-77, 1992 · Zbl 0752.68037
[26] Milner, R.; Sangiorgi, D., Barbed bisimulation, (Proc. of ICALP, 1992), 685-695 · Zbl 1425.68298
[27] Nestmann, U., What is a “good” encoding of guarded choice?, Inf. Comput., 156, 287-319, 2000 · Zbl 1046.68625
[28] Palamidessi, C., Comparing the expressive power of the synchronous and the asynchronous π-calculus, (Proc. of POPL, 1997), 256-265
[29] Palamidessi, C., Comparing the expressive power of the synchronous and the asynchronous π-calculus, Math. Struct. Comput. Sci., 13, 685-719, 2003
[30] Parrow, J., Expressiveness of process algebras, Electron. Notes Theor. Comput. Sci., 209, 173-186, 2008 · Zbl 1279.68264
[31] Parrow, J., General conditions for full abstraction, Math. Struct. Comput. Sci., 26, 655-657, 2014 · Zbl 1361.68085
[32] Parrow, J.; Sjödin, P., Multiway synchronization verified with coupled simulation, (Cleaveland, W., Proc. of CONCUR, 1992, Springer Berlin Heidelberg), 518-533
[33] Peters, K., Translational Expressiveness, 2012, TU Berlin, Ph.D. thesis
[34] Peters, K., Comparing process calculi using encodings, (Proc. of EXPRESS/SOS, 2019), 19-38 · Zbl 07449992
[35] Peters, K.; van Glabbeek, R., Analysing and comparing encodability criteria, (Crafa, S.; Gebler, D., Proc. of EXPRESS/SOS, 2015), 46-60 · Zbl 1476.68181
[36] Peters, K.; Nestmann, U., Is it a “good” encoding of mixed choice?, (Proc. of FoSSaCS, 2012), 210-224 · Zbl 1352.68190
[37] Peters, K.; Nestmann, U., Breaking Symmetries, Mathematical Structures in Computer Science, vol. 26, 1054-1106, 2016 · Zbl 1362.68219
[38] Peters, K.; Nestmann, U., Distributability of mobile ambients, Inf. Comput., 275, Article 104608 pp., 2020 · Zbl 1496.68243
[39] Peters, K.; Nestmann, U.; Goltz, U., On distributability in process calculi, (Proc. of ESOP, 2013), 310-329 · Zbl 1381.68215
[40] Peters, K.; Schicke-Uffmann, J. W.; Goltz, U.; Nestmann, U., Synchrony versus causality in distributed systems, Math. Struct. Comput. Sci., 26, 1459-1498, 2016 · Zbl 1362.68220
[41] Peters, K.; Yoshida, N., On the expressiveness of mixed choice sessions, (Proc. of EXPRESS/SOS, 2022), 113-130 · Zbl 1532.68055
[42] Plotkin, G. D., The origins of structural operational semantics, J. Log. Algebraic Program., 60, 17-140, 2004, An earlier version of this paper was published as technical report at Aarhus University in 1981
[43] (Simon Gay, A. R., Behavioural Types: from Theory to Tools, 2017, River Publisher)
[44] Takeuchi, K.; Honda, K.; Kubo, M., An interaction-based language and its typing system, (Proc. of PARLE, 1994), 398-413
[45] Yoshida, N.; Vasconcelos, V. T., Language primitives and type discipline for structured communication-based programming revisited: two systems for higher-order session communication, (Proc. of SecReT, 2006), 73-93
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.