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 message emissions to be anticipated 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 which deals with examples that feature potentially unbounded buffering. Finally, we present an implementation of our algorithm and an empirical evaluation of it on synthetic benchmarks.

翻译：会话类型被广泛用作异步消息传递系统的抽象。此类抽象的细化至关重要，因为它允许在不破坏组件与系统其他部分兼容性的前提下改进特定组件。在会话类型背景下，最通用的细化概念是异步会话子类型，它允许消息发送被提前，但仅能在特定条件下进行。特别地，异步会话子类型排除了通信协议中自然出现的候选子类型，例如当两方在从各自缓冲区移除消息之前同时向对方发送有限但未指定数量的消息时。为解决此缺陷，我们研究了异步会话类型上的公平遵从性以及保持该遵从性的公平细化关系。由此，我们提出了一种新颖的会话子类型变体，该变体利用服务契约理论中的可控性概念，并成为公平细化的可靠刻画。此外，我们证明了公平细化以及我们提出的新型子类型均是不可判定的。我们还提出了一种可处理潜在无界缓冲示例的可靠算法。最后，我们给出了该算法的实现，并在合成基准测试上进行了实证评估。