Formal modeling and analysis of RAMP transaction systems

Si Liu, Jatin Ganhotra, Peter Csaba Ölveczky, Indranil Gupta, Muntasir Raihan Rahman, José Meseguer

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

To cope with large data sets, distributed data stores partition their data across servers. However, real-world systems usually do not provide useful transactional semantics for operations accessing multiple partitions due to the delays involved in achieving multi-partition consistency. Read Atomic Multi-Partition (RAMP) transactions have recently been proposed as efficient light-weight multi-partition transactions that guarantee read atomicity: either all updates or no updates of a transaction are visible to other transactions. In this paper we formalize RAMP transactions in rewriting logic and perform model checking verification of key properties using the Maude tool. In particular, we develop detailed formal models- and formally analyze-a number of extensions and optimizations of RAMP that are only briefly mentioned by the RAMP developers.

Original languageEnglish (US)
Title of host publication2016 Symposium on Applied Computing, SAC 2016
PublisherAssociation for Computing Machinery
Pages1700-1707
Number of pages8
ISBN (Electronic)9781450337397
DOIs
StatePublished - Apr 4 2016
Event31st Annual ACM Symposium on Applied Computing, SAC 2016 - Pisa, Italy
Duration: Apr 4 2016Apr 8 2016

Publication series

NameProceedings of the ACM Symposium on Applied Computing
Volume04-08-April-2016

Other

Other31st Annual ACM Symposium on Applied Computing, SAC 2016
Country/TerritoryItaly
CityPisa
Period4/4/164/8/16

Keywords

  • Formal analysis
  • Multi-partition transactions
  • Rewriting logic

ASJC Scopus subject areas

  • Software

Fingerprint

Dive into the research topics of 'Formal modeling and analysis of RAMP transaction systems'. Together they form a unique fingerprint.

Cite this