Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Pushing the Limit: Verified Performance-Optimal Causally-Consistent Database Transactions

Shabnam Ghasemirad, Christoph Sprenger, Si Liu, Luca Multazzu, David Basin

TL;DR

The paper tackles enabling high-performance, causally consistent transactions in geo-distributed databases by introducing Eiger-PORT+, a protocol that achievesTransactional Causal Consistency with convergence ($TCCv$). It provides a deductive, machine-checked verification in Isabelle/HOL and a refinement-based proof strategy to handle inverted commits, refuting the prior conjecture that $TCC$ is the strongest PORT isolation under transactional writes. The authors also demonstrate superiority in performance over state-of-the-art protocols, reporting up to 1.8x throughput improvement over Eiger-PORT and 2.5x over Eiger, while maintaining convergence and low latency. This work establishes the feasibility of performance-optimal, convergent causal consistency in distributed transactions and offers a rigorous blueprint for verifying complex concurrency control protocols.

Abstract

Modern web services crucially rely on high-performance distributed databases, where concurrent transactions are isolated from each other using concurrency control protocols. Relaxed isolation levels, which permit more complex concurrent behaviors than strong levels like serializability, are used in practice for higher performance and availability. In this paper, we present Eiger-PORT+, a concurrency control protocol that achieves a strong form of causal consistency, called TCCv (Transactional Causal Consistency with convergence). We show that Eiger-PORT+ also provides performance-optimal read transactions in the presence of transactional writes, thus refuting an open conjecture that this is impossible for TCCv. We also deductively verify that Eiger-PORT+ satisfies this isolation level by refining an abstract model of transactions. This yields the first deductive verification of a complex concurrency control protocol. Furthermore, we conduct a performance evaluation showing Eiger-PORT+'s superior performance over the state-of-the-art.

Pushing the Limit: Verified Performance-Optimal Causally-Consistent Database Transactions

TL;DR

The paper tackles enabling high-performance, causally consistent transactions in geo-distributed databases by introducing Eiger-PORT+, a protocol that achievesTransactional Causal Consistency with convergence (). It provides a deductive, machine-checked verification in Isabelle/HOL and a refinement-based proof strategy to handle inverted commits, refuting the prior conjecture that is the strongest PORT isolation under transactional writes. The authors also demonstrate superiority in performance over state-of-the-art protocols, reporting up to 1.8x throughput improvement over Eiger-PORT and 2.5x over Eiger, while maintaining convergence and low latency. This work establishes the feasibility of performance-optimal, convergent causal consistency in distributed transactions and offers a rigorous blueprint for verifying complex concurrency control protocols.

Abstract

Modern web services crucially rely on high-performance distributed databases, where concurrent transactions are isolated from each other using concurrency control protocols. Relaxed isolation levels, which permit more complex concurrent behaviors than strong levels like serializability, are used in practice for higher performance and availability. In this paper, we present Eiger-PORT+, a concurrency control protocol that achieves a strong form of causal consistency, called TCCv (Transactional Causal Consistency with convergence). We show that Eiger-PORT+ also provides performance-optimal read transactions in the presence of transactional writes, thus refuting an open conjecture that this is impossible for TCCv. We also deductively verify that Eiger-PORT+ satisfies this isolation level by refining an abstract model of transactions. This yields the first deductive verification of a complex concurrency control protocol. Furthermore, we conduct a performance evaluation showing Eiger-PORT+'s superior performance over the state-of-the-art.

Paper Structure

This paper contains 8 sections, 2 equations, 2 figures.

Table of Contents

  1. Introduction
  2. Background
  3. Distributed Database Transactions
  4. Transition Systems and Refinement
  5. An Abstract Transaction Model
  6. Eiger-PORT+: An Overview
  7. Timestamps
  8. Read and Write Transactions

Figures (2)

  • Figure 1: A spectrum of isolation levels. $A \to B$ means $A$ is weaker than $B$. RC: read committed si; RA: read atomicity ramp; TCC: transactional causal consistency NOC:OSDI2020, provided by Eiger-PORT NOC:OSDI2020; TCCv: TCC with convergence Cure:ICDCS2016Eiger:NSDI2013, offered by Eiger and our Eiger-PORT+; SI: snapshot isolation si; (S)SER: (strict) serializability serializability. Protocols supporting PORTs are highlighted in foogray!20 gray.
  • Figure 2: Alice and Bob reading (shown by arrows) from servers storing X and Y, illustrating convergence in Eiger-PORT+ and lack thereof in Eiger-PORT. Each square represents a version, and its color determines the version's writer, where orange, blue, and gray correspond to Alice, Bob, and other clients respectively.