Concerto Grosso for Sessions: Fair Termination of Sessions

TL;DR

This paper investigates fair termination in session-based message-passing systems, providing a formal mechanization in Agda to analyze properties like lock freedom and their implications for concurrent session termination.

Contribution

It introduces a formal framework for fair termination in session types, mechanized in Agda, and explores its relation to lock freedom and other properties in concurrent systems.

Findings

Fair termination ensures eventual successful session completion.

Lock freedom does not imply fair termination for all sessions.

Assuming other sessions are fairly terminating, a session is also fairly terminating.

Abstract

Sessions are a fundamental notion in message-passing systems. A session is an abstract notion of communication between parties where each one owns an endpoint. Session types are types that are assigned to the endpoints and that are used to statically and dynamically enforce some desired properties of the communications, such as the absence of deadlocks. Properties of concurrent systems are usually divided in safety and liveness ones and depending on the class it belongs to, a property is defined using different (dual) techniques. However, there exist some properties that require to mix both techniques and the challenges in defining them are exacerbated in proof assistants (e.g. Agda, Coq, . . . ), that is, tools that allow users to formally characterize and prove theorems. In particular, we mechanize the meta-theory of inference systems in Agda. Among the interesting properties that can be studied in the session-based context, we study fair termination which is the property of those sessions that can always eventually reach successful termination under a fairness assumption. Fair termination implies many desirable and well known properties, such as lock freedom. Moreover, a lock free session does not imply that other sessions are lock free as well. On the other hand, if we consider a session and we assume that all the other ones are fairly terminating, we can conclude that the one under analysis is fairly terminating as well.