Concerto Grosso for Sessions: Fair Termination of Sessions
Luca Ciccone

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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsDistributed systems and fault tolerance · Formal Methods in Verification · Logic, Reasoning, and Knowledge
