All in One: Design, Verification, and Implementation of SNOW-Optimal Read Atomic Transactions

Liu, Si

Permalink

https://hdl.handle.net/2142/111771 Copy

Description

Title

All in One: Design, Verification, and Implementation of SNOW-Optimal Read Atomic Transactions

Author(s)

Liu, Si

Issue Date

2021

Keyword(s)

• distributed database transactions
• model checking
• statistical verification
• data consistency
• the SNOW theorem
• database performance evaluation

Abstract

Distributed read atomic transactions are important building blocks of modern cloud databases which magnificently bridge the gap between data availability and strong data consistency. The performance of their transactional reads is particularly critical to the overall system performance as many real-world database workloads are dominated by reads. Following the SNOW design principle for optimal reads, we develop LORA, a novel SNOW-optimal algorithm for distributed read atomic transactions. LORA completes its reads in exactly one round trip, even in the presence of conflicting writes, without imposing additional overhead to the communication and outperforms the state-of-the-art read atomic algorithms. To guide LORA's development we present a rewriting-logic-based framework and toolkit for design, verification, implementation, and evaluation of distributed databases. Within the framework, we formalize LORA and mathematically prove its data consistency guarantees. We also apply automatic model checking and statistical verification to validate our proofs and to estimate LORA's performance. We additionally generate from the formal model a correct-by-construction distributed implementation for testing and performance evaluation under realistic deployments. Our design-level and implementation-based experimental results are consistent, which together demonstrate LORA's promising data consistency and performance achievement.

Type of Resource

text

Language

en

Permalink

http://hdl.handle.net/2142/111771

Owning Collections