Pushing the Limit: Verified Performance-Optimal Causally-Consistent Database Transactions
OPEN ACCESS
Loading...
Author / Producer
Date
2025-05-01
Publication Type
Conference Paper
ETH Bibliography
yes
Citations
Scopus:
Altmetric
OPEN ACCESS
Data
Rights / License
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.
Permanent link
Publication status
published
External links
Book title
Tools and Algorithms for the Construction and Analysis of Systems
Journal / series
Volume
15698
Pages / Article No.
43 - 62
Publisher
Springer
Event
31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2025)
Edition / version
Methods
Software
Geographic location
Date collected
Date created
Subject
Organisational unit
03634 - Basin, David / Basin, David
Notes
Funding
231862 - 10003120 - Formal Verification of Isolation Guarantees in Database Systems (SNF)