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
CountryItaly
CityPisa
Period4/4/164/8/16

Fingerprint

Model checking
Servers
Semantics

Keywords

  • Formal analysis
  • Multi-partition transactions
  • Rewriting logic

ASJC Scopus subject areas

  • Software

Cite this

Liu, S., Ganhotra, J., Ölveczky, P. C., Gupta, I., Rahman, M. R., & Meseguer, J. (2016). Formal modeling and analysis of RAMP transaction systems. In 2016 Symposium on Applied Computing, SAC 2016 (pp. 1700-1707). (Proceedings of the ACM Symposium on Applied Computing; Vol. 04-08-April-2016). Association for Computing Machinery. https://doi.org/10.1145/2851613.2851838

Formal modeling and analysis of RAMP transaction systems. / Liu, Si; Ganhotra, Jatin; Ölveczky, Peter Csaba; Gupta, Indranil; Rahman, Muntasir Raihan; Meseguer, José.

2016 Symposium on Applied Computing, SAC 2016. Association for Computing Machinery, 2016. p. 1700-1707 (Proceedings of the ACM Symposium on Applied Computing; Vol. 04-08-April-2016).

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

Liu, S, Ganhotra, J, Ölveczky, PC, Gupta, I, Rahman, MR & Meseguer, J 2016, Formal modeling and analysis of RAMP transaction systems. in 2016 Symposium on Applied Computing, SAC 2016. Proceedings of the ACM Symposium on Applied Computing, vol. 04-08-April-2016, Association for Computing Machinery, pp. 1700-1707, 31st Annual ACM Symposium on Applied Computing, SAC 2016, Pisa, Italy, 4/4/16. https://doi.org/10.1145/2851613.2851838
Liu S, Ganhotra J, Ölveczky PC, Gupta I, Rahman MR, Meseguer J. Formal modeling and analysis of RAMP transaction systems. In 2016 Symposium on Applied Computing, SAC 2016. Association for Computing Machinery. 2016. p. 1700-1707. (Proceedings of the ACM Symposium on Applied Computing). https://doi.org/10.1145/2851613.2851838
Liu, Si ; Ganhotra, Jatin ; Ölveczky, Peter Csaba ; Gupta, Indranil ; Rahman, Muntasir Raihan ; Meseguer, José. / Formal modeling and analysis of RAMP transaction systems. 2016 Symposium on Applied Computing, SAC 2016. Association for Computing Machinery, 2016. pp. 1700-1707 (Proceedings of the ACM Symposium on Applied Computing).
@inproceedings{35a2febe05ed4b928ecdc2eb8bc2dd12,
title = "Formal modeling and analysis of RAMP transaction systems",
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.",
keywords = "Formal analysis, Multi-partition transactions, Rewriting logic",
author = "Si Liu and Jatin Ganhotra and {\"O}lveczky, {Peter Csaba} and Indranil Gupta and Rahman, {Muntasir Raihan} and Jos{\'e} Meseguer",
year = "2016",
month = "4",
day = "4",
doi = "10.1145/2851613.2851838",
language = "English (US)",
series = "Proceedings of the ACM Symposium on Applied Computing",
publisher = "Association for Computing Machinery",
pages = "1700--1707",
booktitle = "2016 Symposium on Applied Computing, SAC 2016",

}

TY - GEN

T1 - Formal modeling and analysis of RAMP transaction systems

AU - Liu, Si

AU - Ganhotra, Jatin

AU - Ölveczky, Peter Csaba

AU - Gupta, Indranil

AU - Rahman, Muntasir Raihan

AU - Meseguer, José

PY - 2016/4/4

Y1 - 2016/4/4

N2 - 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.

AB - 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.

KW - Formal analysis

KW - Multi-partition transactions

KW - Rewriting logic

UR - http://www.scopus.com/inward/record.url?scp=84975886020&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84975886020&partnerID=8YFLogxK

U2 - 10.1145/2851613.2851838

DO - 10.1145/2851613.2851838

M3 - Conference contribution

AN - SCOPUS:84975886020

T3 - Proceedings of the ACM Symposium on Applied Computing

SP - 1700

EP - 1707

BT - 2016 Symposium on Applied Computing, SAC 2016

PB - Association for Computing Machinery

ER -