Distributed Locking as a Data Type

TL;DR

The paper addresses the challenge of applying mixed-consistency guarantees in distributed applications by proposing programmable coordination mechanisms based on Algebraic Replicated Data Types (ARDTs). ARDTs provide composable, lattice-based building blocks that enable protocol reuse across diverse network environments, reducing the need for fixed, baked-in coordination strategies. The authors instantiate two mutual-exclusion protocols as ARDTs—token-based and voting-based—and demonstrate how to encode these protocols as data types (e.g., Token, Ownership, DotSet, and Voting) with automatic lattice derivation and delta-based updates, facilitating causally consistent replication and fine-grained causality tracking. They also discuss application-level compositions (Excl[T]), minimal network assumptions, and a path toward libraries of components and automatic verification within the LoRe framework, aiming to systematize protocol selection and correctness. The work holds practical significance by enabling flexible, verifiable, and reusable coordination mechanisms that can adapt to topology, fault tolerance, and delay tolerance requirements in real-world distributed systems, including local-first and geo-distributed deployments.

Abstract

Mixed-consistency programming models assist programmers in designing applications that provide high availability while still ensuring application-specific safety invariants. However, existing models often make specific system assumptions, such as building on a particular database system or having baked-in coordination strategies. This makes it difficult to apply these strategies in diverse settings, ranging from client/server to ad-hoc peer-to-peer networks. This work proposes a new strategy for building programmable coordination mechanisms based on the algebraic replicated data types (ARDTs) approach. ARDTs allow for simple and composable implementations of various protocols, while making minimal assumptions about the network environment. As a case study, two different locking protocols are presented, both implemented as ARDTs. In addition, we elaborate on our ongoing efforts to integrate the approach into the LoRe mixed-consistency programming language.