Formal modeling and analysis of the walter transactional data store

Si Liu, Peter Csaba Ölveczky, Qi Wang, José Meseguer

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.

Original languageEnglish (US)
Title of host publicationRewriting Logic and Its Applications - 12th International Workshop, WRLA 2018, Held as a Satellite Event of ETAPS, 2018, Proceedings
EditorsVlad Rusu
PublisherSpringer-Verlag Berlin Heidelberg
Pages136-152
Number of pages17
ISBN (Print)9783319998398
DOIs
StatePublished - Jan 1 2018
Event12th International Workshop on Rewriting Logic and its Applications, WRLA 2018 - Thessaloniki, Greece
Duration: Jun 14 2018Jun 15 2018

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume11152 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other12th International Workshop on Rewriting Logic and its Applications, WRLA 2018
CountryGreece
CityThessaloniki
Period6/14/186/15/18

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Formal modeling and analysis of the walter transactional data store'. Together they form a unique fingerprint.

  • Cite this

    Liu, S., Ölveczky, P. C., Wang, Q., & Meseguer, J. (2018). Formal modeling and analysis of the walter transactional data store. In V. Rusu (Ed.), Rewriting Logic and Its Applications - 12th International Workshop, WRLA 2018, Held as a Satellite Event of ETAPS, 2018, Proceedings (pp. 136-152). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11152 LNCS). Springer-Verlag Berlin Heidelberg. https://doi.org/10.1007/978-3-319-99840-4_8