A binary session is a private communication channel that connects two processes, each adhering to a protocol description called session type. In this work, we study the first type system that ensures the fair termination of binary sessions. A session fairly terminates if all of the infinite executions admitted by its protocol are deemed “unrealistic” because they violate certain fairness assumptions. Fair termination entails the eventual completion of all pending input/output actions, including those that depend on the completion of an unbounded number of other actions in possibly different sessions. This form of lock freedom allows us to address a large family of natural communication patterns that falls outside the scope of existing type systems. Our type system is also the first to adopt fair subtyping, a termination-preserving refinement of the standard subtyping relation for session types that so far has only been studied theoretically. Fair subtyping is surprisingly subtle not only to characterize concisely but also to use appropriately, to the point that the type system must carefully account for all usages of fair subtyping to avoid compromising its termination-preserving properties.
Fri 21 JanDisplayed time zone: Eastern Time (US & Canada) change
10:20 - 12:00 | |||
10:20 25mResearch paper | Pirouette: Higher-Order Typed Functional ChoreographiesDistinguished PaperInPerson POPL DOI Media Attached | ||
10:45 25mResearch paper | Fair Termination of Binary SessionsRemote POPL DOI Media Attached | ||
11:10 25mResearch paper | Safe, Modular Packet Pipeline ProgrammingRemote POPL DOI Media Attached | ||
11:35 25mResearch paper | Dependently-Typed Data Plane ProgrammingRemote POPL Matthias Eichholz TU Darmstadt, Eric Campbell Cornell University, Matthias Krebs TU Darmstadt, Nate Foster Cornell University, Mira Mezini TU Darmstadt DOI Media Attached |