Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

HistMSO: A Logic for Reasoning about Consistency Models with MONA

Isabelle Coget, Étienne Lozes

Abstract

Reasoning about consistency models for replicated data systems is a challenging task that requires a deep understanding of both the consistency models themselves and a large part of human inputs in mechanized verification approaches. In this work, we introduce an approach to reasoning about consistency models for replicated data systems. We introduce HistMSO, a monadic second-order logic (MSO) for histories and abstract executions, the formal models of executions of replicated data systems introduced by Burckhardt. We show that HistMSO can express 39 out of 42 consistency models from Viotti and Vukolic hierarchy. Moreover, we develop a method for reducing HistMSO satisfiability and model-checking to the same problems for MSO over words. While doing this, we leverage the MONA tool for automated reasoning on consistency models.

HistMSO: A Logic for Reasoning about Consistency Models with MONA

Abstract

Reasoning about consistency models for replicated data systems is a challenging task that requires a deep understanding of both the consistency models themselves and a large part of human inputs in mechanized verification approaches. In this work, we introduce an approach to reasoning about consistency models for replicated data systems. We introduce HistMSO, a monadic second-order logic (MSO) for histories and abstract executions, the formal models of executions of replicated data systems introduced by Burckhardt. We show that HistMSO can express 39 out of 42 consistency models from Viotti and Vukolic hierarchy. Moreover, we develop a method for reducing HistMSO satisfiability and model-checking to the same problems for MSO over words. While doing this, we leverage the MONA tool for automated reasoning on consistency models.

Paper Structure

This paper contains 35 sections, 17 theorems, 21 equations, 3 figures, 1 algorithm.

Table of Contents

  1. Introduction
  2. Outline
  3. Related works
  4. Background
  5. Histories
  6. Abstract executions
  7. A Logical Formalism for Consistency Models
  8. Definition of HistMSO
  9. Expressing Consistency Models in HistMSO
  10. Return value consistency
  11. Real time
  12. Linearizability
  13. Quiescent Consistency
  14. Translation to MONA
  15. Background on MONA
  16. ...and 20 more sections

Key Result

theorem 1

For every closed formula $\varphi$ of HistMSO$\setminus\{\xrightarrow{ar},\xrightarrow{vis}\}$, for every finite history $H\in\mathcal{H}^*(\mathbb{P}, \mathbb{T}, \mathbb{O}, \mathbb{V})$ (respectively $\omega$-history $H\in\mathcal{H}^\omega(\mathbb{P}, \mathbb{T}, \mathbb{O}, \mathbb{V})$), it ho $\blacktriangleleft$$\blacktriangleleft$

Figures (3)

  • Figure 1: A history on two processes, with operations $a$, $b$, $c$, $d$, $e$ and $f$
  • Figure 2: An abstract execution over the history of Figure \ref{['fig:ex-history']}, with arbitration and visibility relations
  • Figure 3: A finite history $H$ and its timeline encoding $\mathsf{Enc}_{tl}(H)$

Theorems & Definitions (37)

  • definition 1: History
  • definition 2: Direct Successor
  • definition 3: Abstract execution ViottiVukolic
  • remark 1
  • remark 2
  • remark 3
  • definition 4: No look-ahead
  • remark 4
  • remark 5
  • remark 6
  • ...and 27 more