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.
翻译:会话类型被广泛用作非同步电文传递系统的抽取。 改进这种抽取至关重要, 因为它允许在不损及与系统其他部分兼容性的情况下改进给定部件。 在会议类型中,最普遍的改进概念是会话分型,它允许预测电文排放,但在某些条件下才允许。 特别是,会话分解规则排除在通信协议中自然出现的候选人子类型,在通信协议中,例如,两方在将对方从各自的缓冲中除去之前,同时发送数量有限但不确定的信息。 为了解决这一缺陷,我们研究对不同步会话类型和公平改进的公平合规性,作为保持这种差异的关系。这使我们能够提出一个会议分型的新变式,利用服务合同理论的可控性概念,这是公平改进的正确定性。 此外,我们表明,公平的改进和我们的新子型分型都无法确定。 我们还提出一种合理的算法, 其实施过程涉及可能没有限制的缓冲性特征的例子。