Read Atomic Transactions with Prevention of Lost Updates: ROLA and its Formal Analysis

Liu, Si; Olveczky, Peter C.; Wang, Qi; Gupta, Indranil; Meseguer, José

Permalink

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

Description

Title

Read Atomic Transactions with Prevention of Lost Updates: ROLA and its Formal Analysis

Author(s)

• Liu, Si
• Olveczky, Peter C.
• Wang, Qi
• Gupta, Indranil
• Meseguer, José

Issue Date

2018-10

Keyword(s)

• Distributed Database Systems
• Transaction Protocols
• Consistency Models
• Performance Evaluation
• Statistical Model Checking
• Rewriting Logic
• Maude

Abstract

Designers of distributed database systems face the choice between stronger consistency guarantees and better performance. A number of applications only require read atomicity (RA) (either all or none of a transaction's updates are visible to other transactions) and prevention of lost updates (PLU). Existing distributed transaction systems that meet these requirements also provide additional stronger consistency guarantees (such as causal consistency), but this comes at the price of lower performance. In this paper we propose a new distributed transaction protocol, ROLA, that targets application scenarios where only RA and PLU are needed. We formally specify ROLA in Maude. We then perform model checking to analyze both the correctness and the performance of ROLA. For correctness, we use standard model checking to analyze ROLA's satisfaction of RA and PLU. To analyze performance we: (a) perform statistical model checking to analyze key performance properties; and (b) compare these performance results with those obtained by also modeling and analyzing in Maude the well-known protocols Walter and Jessy that also guarantee RA and PLU. Our statistical model checking results show that ROLA outperforms both Walter and Jessy.

Type of Resource

text

Language

en

Permalink

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

Owning Collections