Files in this item



application/pdfsac2016_tech.pdf (444kB)
(no description provided)PDF


Title:Formal Modeling and Analysis of RAMP Transaction Systems in Maude
Author(s):Liu, Si; Olveczky, Peter C.; Rahman, Muntasir Raihan; Ganhotra, Jatin; Gupta, Indranil; Meseguer, José
Subject(s):Distributed Transactional Systems
Model Checking
Abstract:To cope with ever-increasing 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.
Issue Date:2016
Genre:Technical Report
Sponsor:AFOSR/AFRL FA8750-11-2-0084
NSF CCF 0964471
NSF CNS 1319527
NSF CNS 1409416
Date Available in IDEALS:2017-05-13

This item appears in the following Collection(s)

Item Statistics