Consistency Models

Module 12 · Chapter 12.7 · Ordering and Consistency

Project thread — 12.1–12.6 built coherence, ordering, barriers, and the rules. This capstone places CHI in the consistency-model landscape and closes the module. Module 13 turns to data transfers.

1. Learning Outcomes

By the end of this chapter you should be able to:

• Order the consistency spectrum — sequential consistency, TSO, weakly-ordered.
• Describe what each model reorders — SC (nothing), TSO (store→load), weak (nearly all).
• State that CHI provides the primitives for a weakly-ordered model.
• Explain why software must program to the weak model, using barriers.
• Diagnose the failure of assuming a stronger model than the architecture provides.
• Implement a representative consistency check in SystemVerilog, Verilog-2001, and VHDL.

2. Why Should I Learn This?

This is the chapter that turns coherence and ordering into the thing software actually reasons about: the consistency model. A memory consistency model is the contract that tells a programmer which reorderings the hardware may perform — and therefore which orderings the program must enforce itself. The whole of Module 12 has been building toward it: coherence gives per-line order, barriers give cross-line order on request, and the consistency model is the sum of what that means for software.

The stakes are correctness across the whole ecosystem. Systems built on CHI present a weakly-ordered model — the ARM model — which reorders aggressively for speed and orders only where told. Software written for a stronger model, like x86's TSO or the intuitive sequential consistency, assumes orderings CHI does not provide, and breaks in subtle, load-dependent ways. Knowing where CHI sits on the spectrum — and that "weak" means "you must add the barriers" — is what separates concurrent code that is portable and correct from code that happens to work on one machine.

3. Key Terms

4. Previous Chapter Connection

Module 12 built the pieces: per-address coherence (12.1), the home's serialization (12.2), barriers (12.3–12.5), and the ordering rules (12.6). Each was a mechanism. This chapter assembles them into the consistency model software sees, and names where CHI sits.

The rules of 12.6 — same-address ordered, cross-address free unless barriered — are a weakly-ordered model. This chapter gives that model its name, places it against the stronger models (SC, TSO) programmers may be used to, and draws the practical conclusion: CHI's primitives support a weakly-ordered consistency model, so software must be written for it. The barriers of 12.3–12.5 are the tools the weak model requires; this chapter is why they are not optional but fundamental to programming CHI-based systems correctly.

5. Core Concept — CHI supports a weakly-ordered model

Consistency models span strong to weak, and CHI provides the primitives for a weakly-ordered one.

• Sequential consistency (SC). The strongest: all accesses appear in one global order, and no reordering is allowed. Easiest to reason about, but it forbids the buffering and reordering that make hardware fast.
• Total store order (TSO). The x86 model: relaxes only store→load — a store may be reordered after a later load to a different address (store buffering) — everything else stays ordered.
• Weakly-ordered. The ARM model: nearly all cross-address reordering is allowed; order is imposed only where the programmer inserts a barrier. Fastest, but the most work for software.
• CHI provides weak-model primitives. CHI gives per-address coherence for free and cross-address order on request via barriers (Chapters 12.1–12.6) — exactly a weakly-ordered model. Software on CHI must program to weak.

The synthesis:

Consistency models range from sequential consistency (no reordering, strongest) through TSO (only store→load reordered, x86) to weakly-ordered (nearly all cross-address reordering allowed, ARM). CHI provides the coherence and ordering primitives for a weakly-ordered model — per-address coherence free, cross-address order via barriers. So software must be written to the weak model, adding barriers where order matters, and must not assume a stronger one — which relies on orderings CHI does not provide.

6. Engineering Mental Model — house rules, from strict to relaxed

Three shared kitchens, with rules from strict to relaxed.

• The strict kitchen (SC): every task must be done in the exact order written, no exceptions. Predictable, but slow — no one can get ahead on an independent task.
• The x86 kitchen (TSO): almost everything is in order, but you may start prepping a later independent dish while an earlier one finishes (a store buffered behind a load). One relaxation, well understood.
• The ARM kitchen (weakly-ordered): do tasks in whatever order is fastest, except where a sign explicitly says "finish this before starting that" (a barrier). Fastest, but you must post the signs yourself.

A cook trained in the strict kitchen who moves to the ARM kitchen and assumes tasks still happen in order — without posting the signs — will find dishes come out in the wrong sequence. CHI is the ARM kitchen: you get speed, but you must post the barriers where order matters.

7. Engineering Diagram — the weak model on CHI's primitives

Read top to bottom: the weakly-ordered software model is what programs must reason about; it is built from barrier-imposed ordering over free per-address coherence, all provided by the CHI protocol. The contract at the top is weak — order is opt-in — which is the whole point of the module.

8. The Consistency Spectrum

The three models, by what they reorder.

The rule to carry: models trade ease of reasoning for performance — SC is easiest and slowest, weak is hardest and fastest. CHI supports the weakly-ordered end, so on CHI almost any cross-address reordering is permitted unless a barrier forbids it. Software written for SC (assumes no reordering) or TSO (assumes only store→load) relies on orderings the weak model does not provide — the source of the porting bug.

9. Program to the Weak Model

The practical conclusion of the whole module deserves its own statement.

• CHI is weakly-ordered. Assume the hardware may reorder any cross-address accesses unless a rule or barrier orders them (Chapter 12.6).
• Add barriers where order matters. Every cross-address ordering the algorithm depends on must be backed by a DMB (ordering) or DSB (completion) — the barriers are required, not optional.
• Do not assume a stronger model. Code that relies on SC (no reordering) or TSO (only store→load) assumes orderings CHI does not give, and breaks — often only under load or on a different implementation.
• Weak is portable if barriered. Correctly barriered code for the weak model runs correctly on any stronger model too (the barriers are redundant there but harmless). The reverse fails.

The point to carry:

The direction of safety is asymmetric, and that asymmetry is the whole practical lesson. Writing for the weakest model your code will run on — inserting every barrier the weak model needs — is portable: it is correct on weak hardware and remains correct on stronger hardware, where the extra ordering is simply free. Writing for a stronger model is a trap: it relies on orderings the weaker hardware does not provide, so it breaks when it meets the weaker system — which, for CHI, is the system it will actually run on. So the rule for CHI is unambiguous: program to the weakly-ordered model, place the barriers, and never assume the hardware orders more than it promised.

10. Reading the Models — a ported spinlock

Trace a spinlock ported from x86 (TSO) to a CHI-based (weak) system.

1. On x86 (TSO). The lock release writes the lock variable; TSO keeps stores ordered, so the protected data's stores are observed before the unlock without an explicit barrier. The code works.
2. Ported to CHI (weak). The same code runs on a weakly-ordered CHI system.
3. The weak model reorders. CHI permits the data stores and the unlock store — to different addresses — to be observed in either order, because nothing barriers them (Chapter 12.1).
4. A racer sees the unlock early. Another core acquires the lock (sees the unlock) before the protected data's stores are observed — it reads stale data inside the critical section.
5. The fix. Insert a DMB before the unlock, as the weak model requires. Now the data is ordered before the release, and the spinlock is correct on CHI.

The code was correct on TSO because TSO ordered the stores for it; on CHI's weak model it is not, because the ordering was assumed, not requested. The DebugLab is exactly this ported-assumption failure.

11. RTL / Hardware View — a consistency check

CHI's weak model orders a cross-address pair only via coherence (same address) or a barrier. A safety check compares that against what the code assumed. Representative.

// Representative consistency-model check (educational).
// CHI is WEAKLY-ORDERED: it orders a pair only if they are the same address
// (coherence) or a barrier separates them. Code that ASSUMES a stronger model
// (SC/TSO) expects ordering CHI does not give without a barrier -> needs_fix.
module chi_consistency (
  input  logic same_address,   // same-address (coherence orders it)
  input  logic has_barrier,    // a barrier orders the pair
  input  logic assumes_strong, // the code assumes a stronger model (SC/TSO) here
  output logic chi_orders,     // CHI's weak model orders this pair
  output logic safe,           // the code's assumption holds under CHI
  output logic needs_fix        // assumed order CHI does not provide -> bug
);
  // Weak model: ordered only by coherence or a barrier.
  assign chi_orders = same_address || has_barrier;
  // Safe if CHI orders it, or the code did not rely on ordering here.
  assign safe       = chi_orders || !assumes_strong;
  // A bug when the code assumed order CHI does not give.
  assign needs_fix  = assumes_strong && !chi_orders;
endmodule

The same behavior in Verilog-2001:

// Representative consistency-model check (Verilog-2001).
module chi_consistency (
  input  same_address, has_barrier, assumes_strong,
  output chi_orders, safe, needs_fix
);
  assign chi_orders = same_address || has_barrier;
  assign safe       = chi_orders || !assumes_strong;
  assign needs_fix  = assumes_strong && !chi_orders;
endmodule

And in VHDL:

-- Representative consistency-model check (VHDL).
library ieee;
use ieee.std_logic_1164.all;
 
entity chi_consistency is
  port (
    same_address   : in  std_logic;
    has_barrier    : in  std_logic;
    assumes_strong : in  std_logic;
    chi_orders     : out std_logic;
    safe           : out std_logic;
    needs_fix      : out std_logic
  );
end entity;
 
architecture rtl of chi_consistency is
  signal co : std_logic;
begin
  co <= same_address or has_barrier;
  chi_orders <= co;
  safe       <= co or (not assumes_strong);
  needs_fix  <= assumes_strong and (not co);
end architecture;

All three order a pair under CHI's weak model only via coherence or a barrier, and flag needs_fix when the code assumed an ordering CHI does not provide. The DebugLab is exactly needs_fix — a stronger-model assumption on weak hardware.

12. Verification View — weak model orders only via coherence or a barrier

The properties that pin CHI's position: it orders only per-address or by a barrier, and flags stronger-model assumptions.

// Bind to chi_consistency.
// 1. CHI's weak model orders a pair only via coherence (same address) or a barrier.
property p_weak_orders_only;
  @(*) chi_orders == (same_address || has_barrier);
endproperty
 
// 2. Assuming a stronger model where CHI does not order the pair is a bug.
property p_strong_assumption_needs_fix;
  @(*) (assumes_strong && !chi_orders) |-> needs_fix;
endproperty
 
// 3. Correctly barriered (or same-address) code is safe regardless of assumption.
property p_barriered_is_safe;
  @(*) (same_address || has_barrier) |-> safe;
endproperty

The system point, beyond the checks:

The consistency model is where the entire module's mechanism becomes a programming contract, and the contract CHI offers is deliberately weak — because weakness is speed. A weakly-ordered model lets the hardware reorder everything it is not told to keep, extracting maximum performance, and pushes the cost of ordering onto software, which pays it only where it matters. This is a good trade if software honours it — and the failure mode is entirely one of assumption: code that carries the ordering intuition of a stronger machine assumes a contract CHI never signed. So the capstone discipline of coherence and ordering is a single sentence: program to the weakest model you will run on, and make every needed ordering explicit — because the hardware will reorder everything you did not, and on CHI that is nearly everything.

• What it proves: CHI orders only via coherence or a barrier; stronger-model assumptions are flagged.
• What it does not prove: the specific architecture's full memory model — this is a representative slice.
• Bug signature: needs_fix — code assuming an ordering CHI's weak model does not provide.

13. Testbench — weak-model ordering and the porting bug

Drives the ordering and assumption combinations and checks safety.

module tb_chi_consistency;
  logic same_address, has_barrier, assumes_strong;
  logic chi_orders, safe, needs_fix;
  int errors = 0;
 
  chi_consistency dut (.*);
 
  task automatic check(input logic sa, hb, as,
                       input logic exp_orders, exp_fix, input string name);
    same_address = sa; has_barrier = hb; assumes_strong = as; #1;
    if (chi_orders !== exp_orders || needs_fix !== exp_fix) begin
      errors++; $display("FAIL %s: orders=%0b fix=%0b", name, chi_orders, needs_fix);
    end else $display("PASS %s: orders=%0b fix=%0b", name, chi_orders, needs_fix);
  endtask
 
  initial begin
    check(1'b1, 1'b0, 1'b1, 1'b1, 1'b0, "same address -> coherence orders it, safe");
    check(1'b0, 1'b1, 1'b1, 1'b1, 1'b0, "cross-address + barrier -> ordered, safe");
    check(1'b0, 1'b0, 1'b1, 1'b0, 1'b1, "cross-address, NO barrier, assumes strong -> NEEDS FIX");
    check(1'b0, 1'b0, 1'b0, 1'b0, 1'b0, "cross-address, no barrier, no assumption -> ok");
 
    if (errors == 0) $display("ALL TESTS PASSED");
    else             $display("%0d FAILURE(S)", errors);
    $finish;
  end
endmodule

Expected output:

PASS same address -> coherence orders it, safe: orders=1 fix=0
PASS cross-address + barrier -> ordered, safe: orders=1 fix=0
PASS cross-address, NO barrier, assumes strong -> NEEDS FIX: orders=0 fix=1
PASS cross-address, no barrier, no assumption -> ok: orders=0 fix=0
ALL TESTS PASSED

14. DebugLab — assuming a stronger consistency model

x86 (TSO): store data @A; store unlock @B  -> stores observed in order (no barrier)
ported to CHI (weakly-ordered), same code, no barrier:
  @A and @B are different addresses -> CHI may reorder them
  racer sees unlock @B before data @A -> reads stale data in critical section
the code ASSUMED TSO ordering CHI does not provide without a barrier

15. Common Mistakes

• Assuming SC or TSO on CHI. Assumption: stores stay ordered. Bug: weak reordering breaks it (the DebugLab). Prevention: program to the weak model with barriers.
• Porting without adding barriers. Assumption: x86-correct is CHI-correct. Bug: reordering. Prevention: add the barriers the weak model needs.
• Thinking coherence gives consistency. Assumption: per-line order implies cross-line order. Bug: cross-address reordering. Prevention: consistency is separate (Chapter 12.1).
• Barriering for a stronger model. Assumption: match the source model. Bug: over- or under-barriering. Prevention: barrier for CHI's weak model.
• Testing only on strong hardware. Assumption: it works in test. Bug: fails on weak. Prevention: reason to the weak model.
• Treating weak as broken. Assumption: weak is a defect. Bug: fighting the model. Prevention: weak is fast; barrier where needed.

16. Engineering Checklist

• Recognize CHI as providing a weakly-ordered consistency model.
• Program to the weak model — assume cross-address reordering unless ordered.
• Insert barriers (DMB/DSB) wherever a cross-address order is required.
• Do not assume SC or TSO ordering that CHI does not provide.
• Add the barriers when porting from a stronger-model system.
• Prefer weak-model-correct code — it is portable to stronger models too.

17. Key Takeaways

• Consistency models span SC (no reordering) → TSO (store→load only) → weakly-ordered (nearly all).
• CHI provides the primitives for a weakly-ordered model — the ARM model.
• Per-address coherence is free; cross-address order is on request via barriers.
• Software must program to the weak model, adding barriers where order matters.
• Assuming a stronger model (SC/TSO) relies on ordering CHI does not provide — and breaks.
• Program to the weakest model, barrier explicitly; the model here is representative.

18. Quick Revision

Consistency models. A memory consistency model is the contract for which reorderings the hardware may perform. The spectrum runs strong to weak: sequential consistency (SC) allows no reordering (one global order); total store order (TSO), the x86 model, relaxes only store→load (store buffering); weakly-ordered, the ARM model, allows nearly all cross-address reordering, imposing order only where the programmer inserts a barrier. CHI provides the coherence and ordering primitives for a weakly-ordered model — per-address coherence free (Modules 10–11), cross-address order on request via barriers (Chapters 12.3–12.5). The practical rule: program to the weak model — assume the hardware may reorder cross-address accesses unless a barrier orders them, and place the barriers every cross-address dependency needs. Code that assumes a stronger model (SC's no-reordering, TSO's ordered stores) relies on ordering CHI does not provide and breaks under load — the classic bug when porting from x86. Weak-model-correct code, being explicitly barriered, is also correct on stronger models, so it is the portable choice. Representative model; Module 13 turns to CHI data transfers.

Coming Next

Chapter 13.1 — Data Packets. Ordering and consistency are settled; Module 13 turns to how data actually moves. Chapter 13.1 opens the data-transfer module with the DAT-channel data packet in depth — how a cache line is carried across the DAT channel, the fields that frame it, and the beats that deliver it — moving from the ordering of transactions to the mechanics of the bytes they carry.