Formal Definitions of Memory Consistency Models

TL;DR

This paper provides formal definitions and a concise notation for various shared memory consistency models, aiding understanding and comparison of their behaviors in concurrent systems.

Contribution

It summarizes and formalizes multiple memory consistency models, including synchronized ones, with a clear notation for easier reasoning and comparison.

Findings

Formal definitions of key consistency models

A unified notation for comparing models

Enhanced understanding of model behaviors

Abstract

Shared Memory is a mechanism that allows several processes to communicate with each other by accessing -- writing or reading -- a set of variables that they have in common. A Consistency Model defines how each process observes the state of the Memory, according to the accesses performed by it and by the rest of the processes in the system. Therefore, it determines what value a read returns when a given process issues it. This implies that there must be an agreement among all, or among processes in different subsets, on the order in which all or a subset of the accesses happened. It is clear that a higher quantity of accesses or proceses taking part in the agreement makes it possibly harder or slower to be achieved. This is the main reason for which a number of Consistency Models for Shared Memory have been introduced. This paper is a handy summary of [2] and [3] where consistency models (Sequential, Causal, PRAM, Cache, Processors, Slow), including synchronized ones (Weak, Release, Entry), were formally defined. This provides a better understanding of those models and a way to reason and compare them through a concise notation. There are many papers on this subject in the literature such as [11] with which this work shares some concepts.