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é
N1 - Funding Information:
This work was supported in part by NSF CNS 1409416, NSF CNS 1319527, NSF CCF 0964471, AFOSR/AFRL FA8750-11-2-0084, and gifts from Microsoft and Google.
Copyright:
Copyright 2019 Elsevier B.V., All rights reserved.
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
T2 - 31st Annual ACM Symposium on Applied Computing, SAC 2016
Y2 - 4 April 2016 through 8 April 2016
ER -