Files in this item

FilesDescriptionFormat

application/pdf

application/pdfmain.pdf (361kB)
(no description provided)PDF

Description

Title:Formal Modeling and Analysis of the Walter Transactional Data Store
Author(s):Liu, Si; Olveczky, Peter C.; Wang, Qi; Meseguer, Jose
Subject(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.
Issue Date:2018
Genre:Technical Report
Type:Other
Language:English
URI:http://hdl.handle.net/2142/98988
Date Available in IDEALS:2018-01-20


This item appears in the following Collection(s)

Item Statistics