POPL 2024
Sun 14 - Sat 20 January 2024 London, United Kingdom
Sun 14 Jan 2024 14:00 - 14:45 at Lovelace Room - Session 3 Chair(s): Hugo Paquet

The CertiKOS project aims to develop a new ecosystem for specifying, programming, compiling, and composing large-scale certified heterogeneous systems. Since its inception, CertiKOS has applied ideas from game semantics and algebraic effects to support layered composition of deep specifications and certified abstraction layers. However, existing theory and tools for CertiKOS have only provided limited support for composing concurrent components. This talk will survey the challenges we encountered and then present a new general semantics for supporting horizontal and vertical composition of linearizable concurrent objects. We start by showcasing a common issue, which is independent of linearizability, in the construction of compositional models of concurrent computation: interaction with the neutral element for composition can lead to emergent behaviors, a hindrance to compositionality. Category theory provides a solution for the issue in the form of the Karoubi envelope. Surprisingly, this abstract construction is deeply related to linearizability and leads to a novel formulation of it. Notably, this new formulation neither relies on atomicity nor directly upon happens-before ordering and is only possible because of compositionality, revealing that linearizability and compositionality are intrinsically related to each other. We use this new, and compositional, understanding of linearizability to revisit much of the theory and practice of building certified concurrent abstraction layers.

Sun 14 Jan

Displayed time zone: London change

14:00 - 15:30
Session 3GALOP at Lovelace Room
Chair(s): Hugo Paquet LIPN, Université Sorbonne Paris Nord
Compositional Development of Certified System Software
Zhong Shao Yale University
SSA is Freyd Categories
Jad Elkhaleq Ghalayini University of Cambridge
A Denotational Approach to Release/Acquire Concurrency
Yotam Dvir Tel Aviv University, Ohad Kammar University of Edinburgh, Ori Lahav Tel Aviv University