Skip to Main content Skip to Navigation
Conference papers

Fair Refinement for Asynchronous Session Types

Mario Bravetti 1, 2 Julien Lange 3 Gianluigi Zavattaro 1, 2 
2 FOCUS - Foundations of Component-based Ubiquitous Systems
CRISAM - Inria Sophia Antipolis - Méditerranée , DISI - Dipartimento di Informatica - Scienza e Ingegneria [Bologna]
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.
Document type :
Conference papers
Complete list of metadata

https://hal.inria.fr/hal-03340696
Contributor : Zavattaro Gianluigi Connect in order to contact the contributor
Submitted on : Friday, September 10, 2021 - 12:12:48 PM
Last modification on : Friday, March 18, 2022 - 3:17:17 PM

File

Bravetti2021_Chapter_FairRefin...
Files produced by the author(s)

Identifiers

Collections

Citation

Mario Bravetti, Julien Lange, Gianluigi Zavattaro. Fair Refinement for Asynchronous Session Types. FOSSACS 2021 - 24th International Conference on Foundations of Software Science and Computation Structures, Mar 2021, Luxembourgh, Luxembourg. ⟨10.1007/978-3-030-71995-1⟩. ⟨hal-03340696⟩

Share

Metrics

Record views

10

Files downloads

66