Orthogonally Replicated Data Types

Orthogonally Replicated Data Types: Formal Semantics and Implementation for Strong Consistency Under Weak Replication

Abstract:

A distributed application that maintains high availability traditionally does so through weakly consistent replication. Programmers of such applications face challenges from the complexity of reasoning about different evolving states on different replicas and how to achieve consistency in the face of ever-changing states. But this does not have to be the case; programmers want to program against high-level abstractions, which, when used carefully, can witness strong consistency even under asynchronous, weakly consistent replication. By recognizing and replicating shared abstractions themselves, we can have the best of both worlds: a consistent, familiar programming model and fast, scalable replication.

We present ORDT, a programming abstraction that achieves sequential consistency and decouples data replication from conflict resolution. Our formalization employs relational semantics that form complete lattices, enabling deterministic n-way merges with restriction-aware validation. We prove that our merge algorithm guarantees convergence, preservation, and commutativity. These verification challenges are intractable for manual implementation but well-suited for compiler automation—yet traditional compiler infrastructures lack the capabilities necessary for ORDT programming.

In this talk, I wish to present the programming abstraction ORDT, the mathematical foundations underpinning its definitions and needed compiler support where consistency guarantees are proven at compile time rather than hoped for at runtime—laying the foundation for compiler-assisted distributed programming.

Programmers can leverage our abstraction through built-in library functions or by defining custom merge strategies and business constraints, with guaranteed convergence across replicas. Our gossip-based runtime demonstrates that ORDTs preserve both sequential consistency and availability under network partitions