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


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
Number of pages8
ISBN (Electronic)9781450337397
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


Other31st Annual ACM Symposium on Applied Computing, SAC 2016


  • Formal analysis
  • Multi-partition transactions
  • Rewriting logic

ASJC Scopus subject areas

  • Software


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

Cite this