POPL 2026
Sun 11 - Sat 17 January 2026 Rennes, France
Wed 14 Jan 2026 14:00 - 14:25 at Réfectoire - Concurrency: Models Chair(s): Noam Zilberstein

The fundamental tension between availability and consistency shapes the design of distributed storage systems. Classical results capture extreme points of this trade-off: the CAP theorem shows that strong models like linearizability preclude availability under partitions, while weak models like causal consistency remain implementable without coordination. These theorems apply to simple read-write interfaces, leaving open a precise explanation of the combinations of object semantics and consistency models that admit available implementations.

This paper develops a general semantic framework in which storage specifications combine operation semantics and consistency models. The framework encompasses a broad range of objects (key-value stores, counters, sets, CRDTs, and SQL databases) and consistency models (from causal consistency and sequential consistency to snapshot isolation and bounded staleness).

Within this framework, we prove the Arbitration-Free Consistency (AFC) theorem, showing that an object specification within a consistency model admits an available implementation if and only if it is arbitration-free, that is, it does not require a total arbitration order to resolve visibility or read dependencies.

The AFC theorem unifies and generalizes previous results, revealing arbitration-freedom as the fundamental property that delineates coordination-free consistency from inherently synchronized behavior.

Wed 14 Jan

Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

14:00 - 15:40
Concurrency: ModelsPOPL at Réfectoire
Chair(s): Noam Zilberstein Cornell University
14:00
25m
Talk
Arbitration-Free Consistency Is Available (and Vice Versa)
POPL
Hagit Attiya Technion - Israel Institute of Technology, Constantin Enea LIX, CNRS, Ecole Polytechnique, Enrique Román-Calvo University of Freiburg
DOI
14:25
25m
Talk
ArchSem: Reusable Rigorous Semantics of Relaxed Architectures
POPL
Thibaut Pérami University of Cambridge, Thomas Bauereiss University of Cambridge, Brian Campbell University of Edinburgh, Zongyuan Liu Aarhus University, Nils Lauermann University of Cambridge, Alasdair Armstrong University of Cambridge, Peter Sewell University of Cambridge
DOI
14:50
25m
Talk
Consistent Updates for Scalable Microservices
POPL
Devora Chait-Roth New York University, Kedar Namjoshi Nokia Bell Labs, Thomas Wies New York University
DOI
15:15
25m
Talk
Recurrence Sets for Proving Fair Non-termination under Axiomatic Memory Consistency Models
POPL
Thomas Haas TU Braunschweig, Roland Meyer TU Braunschweig, Hernán Ponce de León Huawei Dresden Research Center, Andrés Lomelí Garduño Huawei Dresden Research Center
DOI