HistMSO: A Logic for Reasoning about Consistency Models with MONA

TL;DR

HistMSO is a monadic second-order logic framework for reasoning about various consistency models in replicated data systems, enabling automated verification through reduction to MSO over words.

Contribution

The paper introduces HistMSO, a new logic for formalizing consistency models, and demonstrates how to leverage MONA for automated reasoning about these models.

Findings

HistMSO can express 39 out of 42 studied consistency models.

Satisfiability and model-checking in HistMSO reduce to MSO problems over words.

The approach enables automated reasoning about complex consistency models.

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.