University of Illinois Urbana-Champaign

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

Liu, Si

Content Files
main.pdf

Permalink

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

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
Date of Ingest
2021-10-26T13:05:22Z
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
Genre of Resource
technical report
Language
en
Permalink
http://hdl.handle.net/2142/111771

Owning Collections

Research and Tech Reports - Computer Science PRIMARY