Abstract
Session types are widely used as abstractions of asynchronous message passing systems. Refinement for such abstractions is crucial as it allows improvements of a given component without compromising its compatibility with the rest of the system. In the context of session types, the most general notion of refinement is the asynchronous session subtyping, which allows to anticipate message emissions but only under certain conditions. In particular, asynchronous session subtyping rules out candidates subtypes that occur naturally in communication protocols where, e.g., two parties simultaneously send each other a finite but unspecified amount of messages before removing them from their respective buffers. To address this shortcoming, we study fair compliance over asynchronous session types and fair refinement as the relation that preserves it. This allows us to propose a novel variant of session subtyping that leverages the notion of controllability from service contract theory and that is a sound characterisation of fair refinement. In addition, we show that both fair refinement and our novel subtyping are undecidable. We also present a sound algorithm, and its implementation, which deals with examples that feature potentially unbounded buffering.
Research partly supported by the H2020-MSCA-RISE project ID 778233 “Behavioural Application Program Interfaces (BEHAPI)”.
Chapter PDF
Similar content being viewed by others
References
Adam Wiggins. The Twelve Factor methodology. https://12factor.net, 2017.
F. Barbanera and U. de’Liguoro. Two notions of sub-behaviour for session-based client/server systems. In Proc. of the 12th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, PPDP’10, pages 155–164. ACM, 2010.
G. T. Bernardi and M. Hennessy. Modelling session types using contracts. Mathematical Structures in Computer Science, 26(3):510–560, 2016.
A. Bouajjani, C. Enea, K. Ji, and S. Qadeer. On the completeness of verifying message passing programs under bounded asynchrony. In CAV (2), volume 10982 of Lecture Notes in Computer Science, pages 372–391. Springer, 2018.
D. Brand and P. Zafiropulo. On communicating finite-state machines. J. ACM, 30(2):323–342, 1983.
M. Bravetti, M. Carbone, J. Lange, N. Yoshida, and G. Zavattaro. A sound algorithm for asynchronous session subtyping. In CONCUR, volume 140 of LIPIcs, pages 38:1–38:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019.
M. Bravetti, M. Carbone, and G. Zavattaro. Undecidability of asynchronous session subtyping. Inf. Comput., 256:300–320, 2017.
M. Bravetti, M. Carbone, and G. Zavattaro. On the boundary between decidability and undecidability of asynchronous session subtyping. Theor. Comput. Sci., 722:19–51, 2018.
M. Bravetti, J. Lange, and G. Zavattaro. Fair refinement for asynchronous session types (extended version). CoRR abs/2101.08181, 2021.
M. Bravetti and G. Zavattaro. Contract Compliance and Choreography Conformance in the Presence of Message Queues. In WS-FM’08, volume 5387 of Lecture Notes in Computer Science, pages 37–54. Springer, 2008.
M. Bravetti and G. Zavattaro. A foundational theory of contracts for multi-party service composition. Fundam. Inform., 89(4):451–478, 2008.
M. Bravetti and G. Zavattaro. A theory of contracts for strong service compliance. Math. Struct. Comput. Sci., 19(3):601–638, 2009.
M. Bravetti and G. Zavattaro. Relating session types and behavioural contracts: The asynchronous case. In SEFM, volume 11724 of Lecture Notes in Computer Science, pages 29–47. Springer, 2019.
T. Chen, M. Dezani-Ciancaglini, A. Scalas, and N. Yoshida. On the preciseness of subtyping in session types. Logical Methods in Computer Science, 13(2), 2017.
T.-C. Chen, M. Dezani-Ciancaglini, and N. Yoshida. On the preciseness of subtyping in session types. In PPDP 2014, pages 146–135. ACM Press, 2014.
P. Deniélou and N. Yoshida. Multiparty compatibility in communicating automata: Characterisation and synthesis of global session types. In ICALP 2013, pages 174–186, 2013.
S. J. Gay and M. Hole. Types and subtypes for client-server interactions. In ESOP 1999, pages 74–90, 1999.
S. J. Gay and M. Hole. Subtyping for session types in the pi calculus. Acta Inf., 42(2-3):191–225, 2005.
B. Genest, D. Kuske, and A. Muscholl. A Kleene theorem and model checking algorithms for existentially bounded communicating automata. Inf. Comput., 204(6):920–956, 2006.
B. Genest, D. Kuske, and A. Muscholl. On communicating automata with bounded channels. Fundam. Inform., 80(1-3):147–167, 2007.
K. Honda, N. Yoshida, and M. Carbone. Multiparty asynchronous session types. J. ACM, 63(1):9, 2016.
J. Lange and N. Yoshida. Characteristic formulae for session types. In TACAS, volume 9636 of Lecture Notes in Computer Science, pages 833–850. Springer, 2016.
J. Lange and N. Yoshida. On the undecidability of asynchronous session subtyping. In Proc. of 20th Int. Conference on Foundations of Software Science and Computation Structures, FOSSACS’17, volume 10203 of Lecture Notes in Computer Science, pages 441–457, 2017.
J. Lange and N. Yoshida. Verifying asynchronous interactions via communicating session automata. In CAV (1), volume 11561 of Lecture Notes in Computer Science, pages 97–117. Springer, 2019.
N. Lohmann. Why does my service have no partners? In WS-FM, volume 5387 of Lecture Notes in Computer Science, pages 191–206. Springer, 2008.
D. Mostrous, N. Yoshida, and K. Honda. Global principal typing in partially commutative asynchronous sessions. In ESOP, volume 5502 of Lecture Notes in Computer Science, pages 316–332. Springer, 2009.
R. D. Nicola and M. Hennessy. Testing Equivalences for Processes. Theoretical Computer Science, 34:83–133, 1984.
L. Padovani. Fair subtyping for open session types. In ICALP, volume 7966 of Lecture Notes in Computer Science, pages 373–384. Springer, 2013.
L. Padovani. Fair subtyping for multi-party session types. Math. Struct. Comput. Sci., 26(3):424–464, 2016.
A. Rensink and W. Vogler. Fair testing. Inf. Comput., 205(2):125–198, 2007.
M. Bravetti, J. Lange, and G. Zavattaro. Fair refinement for asynchronous session types. https://github.com/julien-lange/fair-asynchronous-subtyping, 2020.
R. van Glabbeek and P. Höfner. Progress, justness, and fairness. ACM Comput. Surv., 52(4):69:1–69:38, 2019.
D. Weinberg. Efficient controllability analysis of open nets. In WS-FM, volume 5387 of Lecture Notes in Computer Science, pages 224–239. Springer, 2008.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
Copyright information
© 2021 The Author(s)
About this paper
Cite this paper
Bravetti, M., Lange, J., Zavattaro, G. (2021). Fair Refinement for Asynchronous Session Types. In: Kiefer, S., Tasson, C. (eds) Foundations of Software Science and Computation Structures. FOSSACS 2021. Lecture Notes in Computer Science(), vol 12650. Springer, Cham. https://doi.org/10.1007/978-3-030-71995-1_8
Download citation
DOI: https://doi.org/10.1007/978-3-030-71995-1_8
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-71994-4
Online ISBN: 978-3-030-71995-1
eBook Packages: Computer ScienceComputer Science (R0)