memory consistency model

memory consistency model

memory models: the semantics of shared memory. WMM deals with ordering constraints, but is not just reordering.

Every hardware architecture has its own memory model. memory barrier (fence) can be used to enforce ordering constraints.

Sequential Consistency is the simpliest memory model.

Operational semantics

The operational semantics can be given in small steps semantics. The system is composed of a thread subsystem and a storage subsystem.

The thread subsystem interpret the sequential program in each thread. It might take internal steps, which does not use memory (such as operation on registers, so ), or take a step that requires memory access $P,S{\to }^{i:l}{P}^{\prime },S^{\prime }$. (The access or fences are represented as labels l)

The memory model defines how the storage subsystem works. It describes the effect of memory access and fences. It might take internal steps as well.

The whole system either takes internal step of either subsystem, or take steps with matching labels.

• SC operational semantics
• TSO operational semantics

Classification of memory consistency model

Classification of memory consistency model

Load Buffering (reordering of load and a subsequent store to different locations)

a = x // 1 | b = y // 1
y = 1      | x = 1

If load buffering is not allowed in a memory model, it is called porf-acyclic model, which includes:

• Sequential Consistency
• Total Store Order
• PSO
• RC11

Models that allow load buffering usually (?) disallow such reordering which leads to out-of-thin-air behaviours:

a = x // 1          | b = y // 1
if a = 1 then y = 1 | if b = 1 then x = 1

To rule out these behaviours, dependency-tracking models keep track of dependencies between instructions and restrict the reorderings. These models include:

• POWER
• ARMv7
• ARMv8
• RISC-V
• IMM (intermediate memory model)
• LKMM (Linux kernel memory model)

Other models, such as Promising and Weakestmo, consider multiple program executions to justify the outcomes of a single execution.

well-prefixedness

In an execution, apart from program order and read from order, there are also address, data, and control dependency order. A prefix of an event e is an event e’ in the same thread that: $(e^{\prime },e)\in (rf\cup addr\cup data\cup ctrl{)}^{+}$.

A model is well-prefixed if no consistent execution contains an event that is its own prefix. All porf-acyclic models (note that all dependency orders are subset of program order) and dependency-tracking models are well-prefixed

The original C11 model does not. It allows out-of-thin-air behaviour.

Related

• HMC

指向原始笔记的链接