Automatic Analysis of Consistency Properties of Distributed Transaction Systems in Maude

Liu, Si; Ölveczky, Peter; Zhang, Min; Wang, Qi; Meseguer, José

Permalink

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

Description

Title

Automatic Analysis of Consistency Properties of Distributed Transaction Systems in Maude

Author(s)

• Liu, Si
• Ölveczky, Peter
• Zhang, Min
• Wang, Qi
• Meseguer, José

Issue Date

2019

Keyword(s)

• Model Checking
• Distributed Transaction Systems
• Consistency Model
• Maude

Abstract

Many transaction systems distribute, partition, and replicate their data for scalability, availability, and fault tolerance. However, observing and maintaining strong consistency of distributed and partially replicated data leads to high transaction latencies. Since different applications require different consistency guarantees, there is a plethora of consistency properties---from weak ones such as read atomicity through various forms of snapshot isolation to stronger serializability properties---and distributed transaction systems (DTSs) guaranteeing such properties. This paper presents a general framework for formally specifying a DTS in Maude, and formalizes in Maude nine common consistency properties for DTSs so defined. Furthermore, we provide a fully automated method for analyzing whether the DTS satisfies the desired property for all initial states up to given bounds on system parameters. This is based on automatically recording relevant history during a Maude run and defining the consistency properties on such histories. To the best of our knowledge, this is the first time that model checking of all these properties in a unified, systematic manner is investigated. We have implemented a tool that automates our method, and use it to model check state-of-the-art DTSs such as P-Store, RAMP, Walter, Jessy, and ROLA.

Type of Resource

text

Language

en

Permalink

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

Owning Collections