Formal Modeling and Analysis of the Walter Transactional Data Store

Liu, Si; Olveczky, Peter C.; Wang, Qi; Meseguer, José

Permalink

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

Description

Title

Formal Modeling and Analysis of the Walter Transactional Data Store

Author(s)

• Liu, Si
• Olveczky, Peter C.
• Wang, Qi
• Meseguer, José

Issue Date

2018

Keyword(s)

• Maude
• Model Checking
• Statistical Model Checking
• Parallel Snapshot Isolation
• Transactional Data Store
• Performance

Abstract

Walter is a distributed partially replicated data store providing Parallel Snapshot Isolation (PSI), an important consistency property that offers attractive performance while ensuring adequate guarantees for certain kinds of applications. In this work we formally model Walter's design in Maude and formally specify and verify PSI by model checking. To also analyze Walter's performance we extend the Maude specification of Walter to a probabilistic rewrite theory and perform statistical model checking analysis to evaluate Walter's throughput for a wide range of workloads. Our performance results are consistent with a previous experimental evaluation and throw new light on Walter's performance for different workloads not evaluated before.

Type of Resource

other

Language

en

Permalink

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

Owning Collections