Pushing the Limit: Verified Performance-Optimal Causally-Consistent Database Transactions
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2024
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866910795261018112 |
|---|---|
| author | Ghasemirad, Shabnam Sprenger, Christoph Liu, Si Multazzu, Luca Basin, David |
| author_facet | Ghasemirad, Shabnam Sprenger, Christoph Liu, Si Multazzu, Luca Basin, David |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2411_07049 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Pushing the Limit: Verified Performance-Optimal Causally-Consistent Database Transactions Ghasemirad, Shabnam Sprenger, Christoph Liu, Si Multazzu, Luca Basin, David Databases Distributed, Parallel, and Cluster Computing Formal Languages and Automata Theory Logic in Computer Science 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. |
| title | Pushing the Limit: Verified Performance-Optimal Causally-Consistent Database Transactions |
| topic | Databases Distributed, Parallel, and Cluster Computing Formal Languages and Automata Theory Logic in Computer Science |
| url | https://arxiv.org/abs/2411.07049 |