Read atomic transactions with prevention of lost updates: ROLA and its formal analysis

Si Liu, Peter Csaba Ölveczky, Qi Wang, Indranil Gupta, José Meseguer

Research output: Contribution to journalArticlepeer-review

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.

Original languageEnglish (US)
Pages (from-to)503-540
Number of pages38
JournalFormal Aspects of Computing
Volume31
Issue number5
DOIs
StatePublished - Nov 1 2019

Keywords

  • Consistency models
  • Distributed database systems
  • Maude
  • Performance evaluation
  • Rewriting logic
  • Statistical model checking
  • Transaction protocols

ASJC Scopus subject areas

  • Software
  • Theoretical Computer Science

Fingerprint Dive into the research topics of 'Read atomic transactions with prevention of lost updates: ROLA and its formal analysis'. Together they form a unique fingerprint.

Cite this