Formal Modeling and Analysis of RAMP Transaction Systems in Maude

Liu, Si; Olveczky, Peter C.; Rahman, Muntasir Raihan; Ganhotra, Jatin; Gupta, Indranil; Meseguer, José

Permalink

https://hdl.handle.net/2142/96040 Copy

Description

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é

Issue Date

2016

Keyword(s)

• Distributed Transactional Systems
• Maude
• RAMP
• 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.

Type of Resource

text

Language

en

Permalink

http://hdl.handle.net/2142/96040

Sponsor(s)/Grant Number(s)

• AFOSR/AFRL FA8750-11-2-0084
• NSF CCF 0964471
• NSF CNS 1319527
• NSF CNS 1409416

Owning Collections