HistMSO: A Logic for Reasoning about Consistency Models with MONA
This work provides a formal logic framework for automated verification of consistency models in distributed systems, though it is incremental as it builds on existing models and tools.
The authors tackled the challenge of reasoning about consistency models for replicated data systems by introducing HistMSO, a monadic second-order logic for histories and abstract executions, which can express 39 out of 42 consistency models from a known hierarchy.
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.