Exploring Design Alternatives for Replicated RAMP Transactions Using Maude
METADATA ONLY
Loading...
Author / Producer
Date
2021
Publication Type
Conference Paper
ETH Bibliography
yes
Citations
Altmetric
METADATA ONLY
Data
Rights / License
Abstract
Developing correct, scalable, and fault-tolerant distributed databases is hard and labor-intensive. The increasing complexity of such systems under modern cloud infrastructures, e.g., geo-replicated multi-partitioned datacenters, further limits the number of design alternatives that can be explored in practice. There is therefore a need for the formal analysis of both their qualitative properties, e.g., data consistency, and their quantitative properties, e.g., latency, at an early design stage. In this paper we use formal modeling and both standard and statistical model checking techniques to explore the design space of replicated RAMP (Read Atomic Multi-Partition) transactions for geo-replicated databases. Specifically, we develop in Maude formal, executable specifications of three replicated RAMP designs, two by the RAMP developers and one by us, and analyze their data consistency properties. We further transform the Maude models into probabilistic rewrite theories for statistical model checking w.r.t. performance properties. Our results: (i) are consistent with the conjectures made by the RAMP developers; (ii) uncover our promising new design that not only provides all crucial data consistency guarantees but also outperforms the other design alternatives.
Permanent link
Publication status
published
External links
Editor
Book title
2021 International Symposium on Theoretical Aspects of Software Engineering (TASE)
Journal / series
Volume
Pages / Article No.
111 - 118
Publisher
IEEE
Event
15th International Symposium on Theoretical Aspects of Software Engineering (TASE 2021)
Edition / version
Methods
Software
Geographic location
Date collected
Date created
Subject
Organisational unit
03634 - Basin, David / Basin, David
02150 - Dep. Informatik / Dep. of Computer Science