An Epistemic Perspective on Consistency of Concurrent Computations

TL;DR

This paper introduces a logical formalization of consistency properties in concurrent computations, offering a unified, declarative perspective based on a logic of knowledge to better understand various consistency models.

Contribution

It presents a novel formalization using a logic of knowledge, unifying different consistency properties in concurrent algorithms.

Findings

Provides a logical framework for consistency properties

Offers insights into the nature of consistency requirements

Unifies various consistency models under a single formal perspective

Abstract

Consistency properties of concurrent computations, e.g., sequential consistency, linearizability, or eventual consistency, are essential for devising correct concurrent algorithms. In this paper, we present a logical formalization of such consistency properties that is based on a standard logic of knowledge. Our formalization provides a declarative perspective on what is imposed by consistency requirements and provides some interesting unifying insight on differently looking properties.