“CXL Automatically Solves Coherency”

"CXL handles coherency, so we do not have to think about it" is the most expensive belief in this module, because the others produce a wrong plan and this one produces a wrong system that passes its own tests.

The question this chapter turns on:

How many parts of the problem does the protocol supply — and how many are still yours?

"Automatically solves" is a claim about a division of labour. A coherence protocol supplies primitives: a way to acquire ownership, a way to be asked to give it up, a way to be told a copy is no longer valid. It does not supply the program that uses them correctly, the ordering a piece of software needs between two different addresses, the recovery path when a message is lost, or the decision about whether the cost is worth paying.

1. A Mechanism Is Not A Discipline

The other misconceptions in this module are about what something is. This one is about who is responsible, and that makes it different in kind.

Every row in the left column is real. The belief's error is not that the left column is empty — it is that the right column is, and the right column is where correctness lives.

A protocol is a mechanism. Correctness is a property of a system. A mechanism makes a property achievable; it does not make it true.

2. How To Use This Chapter

Each of the nine dimensions below is a working test of the claim, and every one answers the same seven questions:

The "what it costs" row is different in this chapter. For the other misconceptions the cost is a bad plan, discovered in a meeting. Here it is a data-integrity failure, discovered in production, which is why this chapter's DebugLabs are the most concrete in the module.

3. The One-Sentence Model

A coherence protocol guarantees that all agents agree about the value of ONE location, for the agents that participate, when no message is lost, at a cost on every access — and correctness needs an ordering across locations, every agent inside the domain, a recovery path, and a decision that the cost was worth it.

4. What This Chapter Owns

The boundary with 30.4 is worth stating. That chapter reviews a design that is trying to be coherent and checks whether its invariants hold. This one asks the prior question: which invariants is the protocol responsible for at all — and the answer is fewer than the claim assumes.

5. Teaching-Model Boundary And Source Discipline

Every model in this chapter is a teaching model, and each computes a property of a CLAIM rather than of a protocol. This chapter is subject to the strictest source discipline in the module, because coherence is the subject where an invented detail would be most plausible and most damaging.

Nothing in this chapter states a normative detail of any specification. No opcode, coherence state, state name, transition, snoop type, response encoding, message, channel, packet layout, bit position, field width, register definition, timeout constant, retry rule, timing guarantee or specification revision appears anywhere — checked by a scan over the finished page as well as by writing the models that way.

No memory model, barrier instruction or ordering rule from any architecture appears either. The ordering model uses an explicit reordered input standing for a machine that is free to reorder two stores, and the abstraction is declared in the model header.

6. Test 1 — Count The Parts On Each Side

The claim under test. That the problem is solved for you.

What "automatic" would require. That nothing were left.

// RTL 1 - what the protocol supplies, and what is still yours to build.
//
// "Automatically solves" is a claim about a DIVISION OF LABOUR. A coherence
// protocol supplies primitives: a way to acquire ownership, a way to be asked
// to give it up, a way to be told a copy is no longer valid. It does not
// supply the program that uses them correctly, the recovery path when one of
// them fails, or the ordering a piece of software needs between two different
// addresses. Counting the parts on each side is the whole refutation.
//
//   BAD  : "the protocol handles coherency"
//   GOOD : count the parts the protocol supplies and the parts the design
//          still has to supply, and publish both numbers
//
// TEACHING MODEL. Illustrative part counts. It is not a model of CXL or of any
// coherence protocol, and it contains no opcode, coherence state, state name,
// transition, snoop type, response encoding, layout, field width, register
// definition, timing guarantee or specification revision from any published
// standard.
//
//   INITIALIZATION CONTRACT (combinational + two counters):
//     power-on/reset : counters zero; the arithmetic is a pure function
//     re-initialise  : not applicable
//     telemetry      : supplied_by_design is published, so "automatic" becomes
//                      a number a reviewer can disagree with
module mechanism_vs_discipline #(parameter int PROTOCOL_DOES_IT_ALL = 0) (
  input  logic clk, rst_n,
  input  logic        assess,
  input  logic [7:0]  parts_total, supplied_by_protocol,
  output logic [7:0]  supplied_by_design, n_assessments, n_overclaims,
  output logic [15:0] automatic_pct,
  output logic        nothing_left, claimed_automatic,
  output logic        mech_err
);
  logic [31:0] a_q;
  logic [7:0]  prot_c;

  // The protocol cannot supply more parts than the problem has.
  assign prot_c = (supplied_by_protocol > parts_total) ? parts_total
                                                       : supplied_by_protocol;
  assign supplied_by_design = parts_total - prot_c;

  // The truth: the problem is solved for you only when nothing is left.
  assign nothing_left = (supplied_by_design == 8'd0);

  // How much of the problem the protocol covers. A problem with no parts is
  // reported as fully covered rather than dividing.
  assign a_q = (parts_total == 8'd0) ? 32'd100
             : (({24'd0, prot_c} * 32'd100) / {24'd0, parts_total});
  assign automatic_pct = a_q[15:0];

  // The whole review point: what the reader concludes from the primitives
  // existing at all.
  assign claimed_automatic = (PROTOCOL_DOES_IT_ALL != 0) ? 1'b1 : nothing_left;

  // SAFETY-OF-CLAIM VIOLATION: the problem was declared solved while parts of
  // it remain the design's responsibility.
  assign mech_err = assess && claimed_automatic && !nothing_left;

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      n_assessments <= 8'd0; n_overclaims <= 8'd0;
    end else if (assess) begin
      n_assessments <= n_assessments + 8'd1;
      if (mech_err) n_overclaims <= n_overclaims + 8'd1;
    end
  end
endmodule

The measurement. A problem of five parts with two supplied by the protocol:

5 parts, protocol supplies 2 : yours=3 automatic=40% protocol_does_it_all_says=1

Three parts are still the design's, and the problem is 40 percent automatic. The protocol-does-it-all build reports it solved — and that build is not a strawman, it is the state a reader is in at the end of an introduction that lists what the protocol provides.

The run drives the one-part-short case too — four of five, at 80 percent — because 80 percent automatic is not automatic, and a stimulus that only drives none supplied and all supplied never tests the word.

Why the belief is reasonable. Everything the introduction says the protocol provides, it provides. There is no false claim to correct, which is what makes this belief durable: the reader's error is in what they inferred about the complement.

What it costs to hold. A design with no ordering plan, no participation audit and no recovery path, each of which is discovered by a different failure.

What to say instead. "Count the parts the protocol supplies and the parts still yours, and publish both numbers. Forty percent automatic is a number somebody can act on."

Figure 1 — the amber boxes are the right-hand column of section 1. Every one of them is a structure somebody has to build, and none of them is mentioned in the sentence "the protocol handles coherency".

7. Test 2 — One Address, Or Two?

The claim under test. That coherence gives you the ordering.

What "automatic" would require. That the two guarantees were one guarantee.

The failure. A coherence protocol guarantees that all agents agree about the value of ONE location. It says nothing about the order in which accesses to TWO different locations become visible. A program that writes a payload and then sets a flag depends entirely on the second property, and gets none of it from the first.

// RTL 2 - coherence is per address; consistency is across addresses.
//
// A coherence protocol guarantees that all agents agree about the value of ONE
// location. It says nothing about the order in which accesses to TWO different
// locations become visible. A program that writes a payload and then sets a
// flag depends entirely on the second property, and gets none of it from the
// first. This is 30.4 section 1's distinction, met here as the load-bearing
// half of the misconception.
//
//   BAD  : "coherent, so the ordering is handled"
//   GOOD : ask whether the property you need is about one address or two
//
// TEACHING MODEL. Two illustrative booleans; no memory model, barrier
// instruction or ordering rule from any specification or architecture appears.
//
//   INITIALIZATION CONTRACT (combinational + two counters):
//     power-on/reset : counters zero
//     re-initialise  : not applicable
//     telemetry      : the two guarantees are published SEPARATELY, which is
//                      what stops one being read as the other
module coherence_is_not_consistency #(parameter int COHERENT_MEANS_ORDERED = 0) (
  input  logic clk, rst_n,
  input  logic assess,
  input  logic needs_spans_lines, coherence_provided, ordering_provided,
  output logic [7:0] n_programs, n_broken,
  output logic       need_met, per_line_only, reported_met,
  output logic       cons_err
);
  // The truth: a program needing an ordering across addresses needs the
  // ordering guarantee; a program needing only per-address agreement needs
  // coherence. They are different guarantees and are supplied separately.
  assign need_met = needs_spans_lines ? ordering_provided : coherence_provided;

  // The state the two readings disagree about, published on its own.
  assign per_line_only = coherence_provided && !ordering_provided;

  // The whole review point: a reader for whom coherence implies ordering.
  assign reported_met = (COHERENT_MEANS_ORDERED != 0) ? coherence_provided
                                                      : need_met;

  // SAFETY VIOLATION: a program's ordering requirement was reported met by a
  // guarantee that does not provide it.
  assign cons_err = assess && reported_met && !need_met;

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      n_programs <= 8'd0; n_broken <= 8'd0;
    end else if (assess) begin
      n_programs <= n_programs + 8'd1;
      if (cons_err) n_broken <= n_broken + 8'd1;
    end
  end
endmodule

The measurement. A program that needs an ordering, on a system that provides coherence only:

needs an ordering, has coherence only : met=0 per_line_only=1 coherent_means_ordered_says=1

This is 30.4 section 1's distinction, met here as the load-bearing half of the misconception. Per-address agreement and cross-address ordering are separate guarantees and are supplied separately.

The run drives the program that needs only per-address agreement too — and that program is served by coherence, with the ordering guarantee absent. A weak build that is wrong everywhere teaches nothing; this one is wrong in exactly the state the claim is about.

Why the belief is reasonable. The word "coherent" sounds like a property of a whole system rather than of one location, and the distinction between coherence and consistency is a distinction most engineers meet once, in a lecture.

What it costs to hold. A publish-then-flag pattern that works on every machine it was developed on and tears on one that reorders.

What to say instead. "Is the property you need about one address or two? Coherence answers the first and says nothing about the second."

8. Test 3 — Who Is Actually In The Domain?

The claim under test. That everything on the link is coherent.

What "automatic" would require. That participation were automatic too.

The failure. A coherence invariant holds over the agents that participate in it. An engine that moves data without participating — because it was never connected to the domain, or because a path bypasses it — can write a location while another agent holds a copy, and no protocol message is exchanged because none is owed. The protocol is not violated. The invariant is.

// RTL 3 - the agent that is not in the domain.
//
// A coherence invariant holds over the agents that PARTICIPATE in it. An engine
// that moves data without participating - because it was never connected to the
// domain, or because a path bypasses it - can write a location while another
// agent holds a copy, and no protocol message is exchanged because none is
// owed. The protocol is not violated. The invariant is.
//
//   BAD  : "everything on the link is coherent"
//   GOOD : count the agents that can touch this memory, and count the ones
//          inside the domain. The difference is the exposure
//
// TEACHING MODEL. Illustrative agent counts.
//
//   INITIALIZATION CONTRACT (combinational + two counters):
//     power-on/reset : counters zero
//     re-initialise  : not applicable
//     telemetry      : outside_domain must read zero, and it is one
//                      subtraction from two numbers a platform already has
module non_participating_agent #(parameter int ON_THE_LINK_IS_IN_THE_DOMAIN = 0) (
  input  logic clk, rst_n,
  input  logic        assess, outsider_writes,
  input  logic [7:0]  agents_total, participating,
  output logic [7:0]  outside_domain, n_assessments, n_violations,
  output logic        invariant_holds, reported_holds,
  output logic        part_err
);
  logic [7:0] part_c;

  // More participants than agents is a bad measurement, not a bigger domain.
  assign part_c = (participating > agents_total) ? agents_total : participating;
  assign outside_domain = agents_total - part_c;

  // The truth: the invariant holds while no agent outside the domain writes.
  // An outsider that never writes is an exposure, not yet a violation.
  assign invariant_holds = !(outsider_writes && (outside_domain != 8'd0));

  // The whole review point: a reader for whom attachment is participation.
  assign reported_holds = (ON_THE_LINK_IS_IN_THE_DOMAIN != 0) ? 1'b1
                                                              : invariant_holds;

  assign part_err = assess && reported_holds && !invariant_holds;

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      n_assessments <= 8'd0; n_violations <= 8'd0;
    end else if (assess) begin
      n_assessments <= n_assessments + 8'd1;
      if (part_err) n_violations <= n_violations + 8'd1;
    end
  end
endmodule

The measurement. Six agents, five participating, and the outsider writes:

6 agents, 5 participate, an outsider writes : outside=1 holds=0 on_the_link_says=1

One agent outside the domain is enough. The on-the-link build reports everything coherent because for it attachment is participation.

The run distinguishes exposure from violation. An outsider that exists and does not write has broken nothing — the invariant holds, and the honest build says so. An exposure is not a failure, and conflating the two makes every audit finding look like an incident.

Why the belief is reasonable. In a system where every agent was designed into the coherent domain, attachment and participation really are the same thing, and the counter-example is a device somebody added later.

What it costs to hold. A data-integrity failure whose trigger is a DMA engine nobody considered part of the memory system, in a window that only appears under specific traffic.

What to say instead. "Count the agents that can touch this memory, and the ones inside the domain. The difference is the exposure."

9. Test 4 — The Flag Arrived First

The claim under test. That the ordering cannot go wrong.

What "automatic" would require. That a coherent system preserved program order.

The classic pattern. A payload is written, then a flag is set, then a reader tests the flag and consumes the payload. Coherence guarantees both locations are agreed on individually. It does not guarantee the flag becomes visible after the payload — and on a machine that may reorder them, the reader can see the flag and the old payload.

// RTL 4 - the ordering the program still has to ask for.
//
// The classic pattern is a payload written, then a flag set, then a reader that
// tests the flag and consumes the payload. Coherence guarantees both locations
// are agreed on individually. It does not guarantee the flag becomes visible
// after the payload, and on a machine that may reorder them the reader can see
// the flag and the old payload. The program asks for the ordering explicitly or
// it does not get it.
//
//   BAD  : "it is coherent, so the flag cannot arrive first"
//   GOOD : name the ordering you need, and the construct that provides it
//
// TEACHING MODEL. Sequential. `reordered` is an explicit input standing for a
// machine that is free to reorder the two stores; no memory model, barrier
// instruction or ordering rule from any architecture appears.
//   Safety : a reader never consumes a payload the writer had not published.
//
// The payload store is modelled in TWO parts - issued, then landed - because
// the torn state the chapter is about is the window between them. A first
// version set the payload and the reordered flag on the same edge, which made
// `flag visible, payload not` structurally unreachable and the whole experiment
// inexpressible. That was caught by the model-expressiveness review before any
// simulation ran.
//
//   INITIALIZATION CONTRACT:
//     power-on/reset : payload and flag both clear, nothing published
//     initialisation : `write_payload` then `set_flag` is the publishing order
//     re-initialise  : `fresh_round` clears both and is legal at any time - it
//                      is how a second publication is measured without the
//                      first one's state, and it DOMINATES a simultaneous
//                      write, because a round boundary a store could cross
//                      would mix two publications
//     telemetry      : torn_reads must read zero
module software_visible_ordering #(parameter int COHERENCE_ORDERS_IT = 0) (
  input  logic clk, rst_n,
  input  logic write_payload, payload_lands, set_flag, fresh_round,
  input  logic reordered, barrier_used,
  input  logic reader_checks, assess,
  output logic [7:0] n_reads, torn_reads,
  output logic       payload_issued,
  output logic       payload_visible, flag_visible, safe_to_consume,
  output logic       consume_allowed,
  output logic       order_err
);
  logic pay_q, flg_q, iss_q;

  assign payload_issued  = iss_q;
  assign payload_visible = pay_q;
  assign flag_visible    = flg_q;

  // The truth: consuming is safe when the flag is up AND the payload really is
  // there. A barrier removes the reordering; without one, a reordering machine
  // can raise the flag first.
  assign safe_to_consume = flg_q && pay_q;

  // The whole review point: a reader who treats the flag as sufficient.
  assign consume_allowed = (COHERENCE_ORDERS_IT != 0) ? flg_q : safe_to_consume;

  // SAFETY VIOLATION: a payload was consumed that had not been published.
  assign order_err = assess && reader_checks && consume_allowed && !safe_to_consume;

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      pay_q <= 1'b0; flg_q <= 1'b0; iss_q <= 1'b0;
      n_reads <= 8'd0; torn_reads <= 8'd0;
    end else begin
      // ONE assignment each, priority written down: a round boundary dominates
      // a store arriving in the same cycle.
      // The payload store is ISSUED here and becomes VISIBLE later. The gap
      // between the two is the window a reordered flag can overtake.
      if (fresh_round)                iss_q <= 1'b0;
      else if (write_payload)         iss_q <= 1'b1;
      else                            iss_q <= iss_q;

      if (fresh_round)                    pay_q <= 1'b0;
      else if (payload_lands && iss_q)    pay_q <= 1'b1;
      else                                pay_q <= pay_q;

      // The flag becomes visible on its own store - and on a reordering machine
      // with no barrier it can also become visible when only the payload store
      // has been issued, which is the reordering this model exists to show.
      if (fresh_round)                              flg_q <= 1'b0;
      else if (set_flag)                            flg_q <= 1'b1;
      // A reordering machine with no barrier lets the flag become visible
      // while the payload store is issued and not yet landed.
      else if (reordered && !barrier_used && iss_q)
                                                    flg_q <= 1'b1;
      else                                          flg_q <= flg_q;

      if (reader_checks) begin
        n_reads <= (n_reads == 8'hFF) ? n_reads : n_reads + 8'd1;
        if (order_err) torn_reads <= (torn_reads == 8'hFF) ? torn_reads
                                                           : torn_reads + 8'd1;
      end
    end
  end
endmodule

The measurement. A reordering machine with no barrier:

reordering machine, no barrier : issued=1 payload_visible=0 flag_visible=1

The flag is visible and the payload is not. The coherence-orders-it build consumes on the flag alone and reads a payload that was never published — a torn read, and not one protocol message was out of place.

The payload store is modelled in two parts — issued, then landed — and that was not the first design. Section 18 records that the first version made this state structurally unreachable, which would have left the chapter's central experiment inexpressible.

The run drives the barrier case, where the flag cannot overtake and even the weak build consumes nothing: the barrier removes the hazard for both builds, which is the practical answer and the reason the item exists.

Why the belief is reasonable. On a strongly-ordered machine this pattern works, and most people's intuition was formed on one. The reordering is a property of the machine, not of the protocol, and the protocol is what the claim is about.

What it costs to hold. A publish-then-consume pattern that is correct on the development machine and tears in production, intermittently, under load.

What to say instead. "Name the ordering you need, and the construct that provides it. Coherence is not that construct."

10. Test 5 — The Protocol Serialised The LINE

The claim under test. That ownership is a lock.

What "automatic" would require. That serialising a line serialised the work.

The failure. Coherence makes a handoff of ownership legal and orderly. It does not decide whose turn it is. Two agents that both acquire ownership — in sequence, each legally — can still produce an application-level race, because the protocol arbitrated the LINE and the application never arbitrated the WORK.

// RTL 5 - two agents that each did everything right.
//
// Coherence makes a handoff of ownership legal and orderly. It does not decide
// whose turn it is. Two agents that both acquire ownership - in sequence, each
// legally - can still produce an application-level race, because the protocol
// arbitrated the LINE and the application never arbitrated the WORK. Every
// message was correct and the result is wrong.
//
//   BAD  : "the protocol serialises them, so there is no race"
//   GOOD : ask what the protocol serialised. A line is not a critical section
//
// TEACHING MODEL. Sequential. Ownership is an abstract single-holder token; no
// coherence state, transition or message from any specification appears.
//   Safety : the model never reports two simultaneous owners, because the
//            protocol genuinely prevents that - which is the point.
//
//   INITIALIZATION CONTRACT:
//     power-on/reset : nobody owns the line, no application lock is held
//     initialisation : `a_acquires` / `b_acquires` take ownership
//     re-initialise  : `fresh_round` releases everything, legal at any time,
//                      idempotent, and DOMINATES a simultaneous acquire
//     telemetry      : app_races must read zero, and it is the counter the
//                      protocol's own telemetry will never show
module race_still_exists #(parameter int OWNERSHIP_IS_A_LOCK = 0) (
  input  logic clk, rst_n,
  input  logic a_acquires, b_acquires, fresh_round, app_lock_held,
  input  logic does_work, assess,
  output logic [7:0] owner_id, n_works, app_races, n_handoffs,
  output logic       work_is_safe, work_allowed,
  output logic       race_err
);
  logic [7:0] own_q;
  assign owner_id = own_q;

  // The protocol's own telemetry: how many times ownership changed hands. Every
  // one of them was legal, and this counter is what a protocol-level health
  // dashboard shows. It stays perfectly healthy while the application races,
  // which is exactly why it cannot be used as evidence of correctness.
  //
  // A first version published `handoff_legal = (own_q <= 2)`. `own_q` is only
  // ever 0, 1 or 2, so that expression is TRUE FOR EVERY INPUT - a tautology
  // dressed as a guarantee. It was found by the boolean review before any
  // simulation ran, and replaced by a number that can actually move.

  // The truth: work is safe when the application has arbitrated it. Owning the
  // line is necessary and is not sufficient.
  assign work_is_safe = (own_q != 8'd0) && app_lock_held;

  // The whole review point: a reader for whom ownership IS the lock.
  assign work_allowed = (OWNERSHIP_IS_A_LOCK != 0) ? (own_q != 8'd0)
                                                   : work_is_safe;

  // SAFETY VIOLATION: work proceeded on an un-arbitrated critical section.
  assign race_err = assess && does_work && work_allowed && !work_is_safe;

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      own_q <= 8'd0; n_works <= 8'd0; app_races <= 8'd0; n_handoffs <= 8'd0;
    end else begin
      // ONE assignment, priority written down. A round boundary dominates an
      // acquire; between the two agents, A is arbitrated ahead of B, which is
      // the protocol doing exactly what it promises.
      if (fresh_round)      own_q <= 8'd0;
      else if (a_acquires)  own_q <= 8'd1;
      else if (b_acquires)  own_q <= 8'd2;
      else                  own_q <= own_q;

      // A handoff is an acquire that changes the holder.
      if (!fresh_round && ((a_acquires && (own_q != 8'd1))
                        || (b_acquires && !a_acquires && (own_q != 8'd2))))
        n_handoffs <= (n_handoffs == 8'hFF) ? n_handoffs : n_handoffs + 8'd1;

      if (does_work) begin
        n_works <= (n_works == 8'hFF) ? n_works : n_works + 8'd1;
        if (race_err) app_races <= (app_races == 8'hFF) ? app_races
                                                        : app_races + 8'd1;
      end
    end
  end
endmodule

The measurement. Agent A owns the line and holds no application lock:

A owns the line, no application lock : owner=1 handoffs=1 safe=0 ownership_is_a_lock_says=1

Every message was correct and the result is wrong. The ownership-is-a-lock build permits the work because the line is owned.

The protocol's own telemetry stays perfect

The handoff counter is the sharpest thing in this chapter. It counts ownership changes — every one legal — and it is exactly what a protocol-level health dashboard shows. The run drives two legal handoffs while the application races, and the counter reads 2 with nothing wrong from the protocol's point of view.

A number that stays healthy during the failure cannot be used as evidence of correctness. The model publishes it precisely so the reader sees that.

The model published something else first, and section 18 records what: a tautology dressed as a guarantee.

Why the belief is reasonable. Ownership is exclusive, and exclusivity is what a lock provides. The inference is one step and the step is almost right.

What it costs to hold. A critical section with no lock, and a corruption that reproduces under load and disappears under a debugger.

What to say instead. "Ask what the protocol serialised. A line is not a critical section."

11. Test 6 — Who Wrote The Recovery Path?

The claim under test. That the protocol guarantees correctness.

What "automatic" would require. That the wire were perfect.

The failure. A coherence protocol defines what a correct exchange looks like. It does not make the wire perfect. A message can be corrupted, retried, or never arrive, and the design has to be correct across all of that — which means a recovery path, a timeout, and a decision about what a partially-completed ownership change means.

// RTL 6 - what the protocol does when the link misbehaves.
//
// A coherence protocol defines what a correct exchange looks like. It does not
// make the wire perfect. A message can be corrupted, retried, or never arrive,
// and the design has to be correct across all of that - which means a recovery
// path, a timeout, and a decision about what a partially-completed ownership
// change means. "Automatic" implies none of this exists.
//
//   BAD  : "the protocol guarantees correctness"
//   GOOD : ask what happens when a message is lost, and who wrote that path
//
// TEACHING MODEL. Abstract error and recovery flags; no error code, retry rule,
// timeout constant or recovery flow from any specification appears.
//
//   INITIALIZATION CONTRACT (combinational + two counters):
//     power-on/reset : counters zero
//     re-initialise  : not applicable
//     telemetry      : recovery_built is published, so its absence is a
//                      reviewable fact rather than a discovery at bring-up
module error_still_possible #(parameter int PROTOCOL_IS_PERFECT = 0) (
  input  logic clk, rst_n,
  input  logic assess,
  input  logic link_error, recovery_built, retried,
  output logic [7:0] n_runs, n_unrecovered,
  output logic       correct_under_error, reported_correct, exposed,
  output logic       fault_err
);
  // The truth: correctness under an error needs a recovery path that ran.
  assign correct_under_error = (!link_error) || (recovery_built && retried);

  // The state the two readings disagree about: an error happened and nothing
  // was built to handle it.
  assign exposed = link_error && !recovery_built;

  // The whole review point: a reader for whom the protocol's definition of a
  // correct exchange is a guarantee that exchanges are correct.
  assign reported_correct = (PROTOCOL_IS_PERFECT != 0) ? 1'b1
                                                       : correct_under_error;

  assign fault_err = assess && reported_correct && !correct_under_error;

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      n_runs <= 8'd0; n_unrecovered <= 8'd0;
    end else if (assess) begin
      n_runs <= n_runs + 8'd1;
      if (fault_err) n_unrecovered <= n_unrecovered + 8'd1;
    end
  end
endmodule

The measurement. A link error with no recovery built:

a link error, no recovery built : correct=0 exposed=1 protocol_is_perfect_says=1

The protocol-is-perfect build reads a definition of correctness as a guarantee that exchanges are correct, which is the confusion in one line.

The run distinguishes three states, and the middle one is the interesting one: a recovery path that exists and has not run has not recovered anything. Built-and-run is correct; built-and-idle is merely un-exposed; neither-built-nor-run is exposed.

Why the belief is reasonable. A specification that says what a correct exchange is sounds like a guarantee that exchanges will be correct, and for most of a system's life they are.

What it costs to hold. A hang or a corruption after a link event, with no path that was designed to handle it, discovered by whichever customer has the marginal link.

What to say instead. "Ask what happens when a message is lost, and who wrote that path."

12. Test 7 — Coverage Of THIS Region

The claim under test. That the platform is coherent.

What "automatic" would require. That a platform claim applied to a region.

The failure. Participation is not a property of a system; it is a property of a REGION and the agents that touch it. A platform can be entirely coherent for one range and entirely not for another, and the useful number is the coverage of the region a given piece of software is using.

// RTL 7 - a region where only some of the agents participate.
//
// Participation is not a property of a system; it is a property of a REGION and
// the agents that touch it. A platform can be entirely coherent for one range
// and entirely not for another, and the useful number is the coverage of the
// region a given piece of software is using. A claim about the platform tells
// you nothing about the region, and the region is where the program lives.
//
//   BAD  : "the platform is coherent"
//   GOOD : for THIS region, how many of the agents that touch it participate?
//
// TEACHING MODEL. Illustrative agent counts per region.
//
//   INITIALIZATION CONTRACT (combinational + two counters):
//     power-on/reset : counters zero
//     re-initialise  : not applicable
//     telemetry      : covered_pct per region, which is the granularity a
//                      platform claim does not have
module partial_participation #(parameter int PLATFORM_CLAIM_IS_ENOUGH = 0) (
  input  logic clk, rst_n,
  input  logic        assess,
  input  logic [7:0]  region_agents, region_participants,
  output logic [15:0] covered_pct,
  output logic [7:0]  uncovered_agents, n_regions, n_assumed,
  output logic        fully_covered, reported_covered,
  output logic        cov_err
);
  logic [31:0] c_q;
  logic [7:0]  part_c;

  assign part_c = (region_participants > region_agents) ? region_agents
                                                        : region_participants;
  assign uncovered_agents = region_agents - part_c;

  // The truth: a region is coherent for a program when EVERY agent touching it
  // participates. One that does not is enough to break the invariant.
  assign fully_covered = (uncovered_agents == 8'd0);

  // A region nothing touches is vacuously covered rather than divided by zero.
  assign c_q = (region_agents == 8'd0) ? 32'd100
             : (({24'd0, part_c} * 32'd100) / {24'd0, region_agents});
  assign covered_pct = c_q[15:0];

  // The whole review point: a platform-level claim applied to a region.
  assign reported_covered = (PLATFORM_CLAIM_IS_ENOUGH != 0) ? 1'b1
                                                            : fully_covered;

  assign cov_err = assess && reported_covered && !fully_covered;

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      n_regions <= 8'd0; n_assumed <= 8'd0;
    end else if (assess) begin
      n_regions <= n_regions + 8'd1;
      if (cov_err) n_assumed <= n_assumed + 8'd1;
    end
  end
endmodule

The measurement. Four agents touching a region, three participating:

4 agents touch it, 3 participate : covered=75% uncovered=1 platform_claim_says=1

Seventy-five percent covered is not covered. One agent outside is enough to break the invariant, and the platform-claim build reports the region safe because the platform is described as coherent.

A claim about the platform tells you nothing about the region, and the region is where the program lives.

The run drives a region nothing touches, which is vacuously covered — a decision the model makes explicitly rather than by dividing by zero, and one a mutation attacked.

Why the belief is reasonable. A platform-level statement is the only statement most people are given, and it is usually true at the level it is made.

What it costs to hold. A workload placed in a region whose agent set includes a non-participant, on a platform whose documentation says "coherent".

What to say instead. "For THIS region, how many of the agents that touch it participate? A platform claim has the wrong granularity."

13. Test 8 — What Does The Mechanism Cost?

The claim under test. That there is nothing to weigh.

What "automatic" would require. That the mechanism were free.

// RTL 8 - "automatic" would mean free, and it is not.
//
// The mechanism costs something on the access path: a lookup, a possible
// interrogation of other holders, and a wait for the answer. A workload that
// shares little pays that cost on every access and gets correctness it was
// never going to violate. The word "automatic" hides the trade, and the trade
// is the reason a simpler attach continues to exist - the same crossover 31.1
// section 12 derives, met here from the correctness side rather than the
// capability side.
//
//   BAD  : "coherency is handled, so there is nothing to weigh"
//   GOOD : state the per-access cost and the sharing rate, and find the
//          crossover
//
// TEACHING MODEL. All latencies are illustrative integers in arbitrary units.
// None is a CXL figure and none is attributed to any product.
//
//   INITIALIZATION CONTRACT (combinational + two counters):
//     power-on/reset : counters zero
//     re-initialise  : not applicable
//     telemetry      : mechanism_cost is published beside base_lat, so
//                      "automatic" becomes a number
module cost_of_the_mechanism #(parameter int AUTOMATIC_MEANS_FREE = 0) (
  input  logic clk, rst_n,
  input  logic        evaluate,
  input  logic [7:0]  base_lat, ownership_lat, sharing_pct,
  output logic [15:0] coherent_cost, hand_written_cost, mechanism_cost,
  output logic [7:0]  n_evals, n_wrong_picks,
  output logic        coherent_better, reported_better,
  output logic        cost_err
);
  logic [31:0] h_q;
  logic [7:0]  share_c;

  assign share_c = (sharing_pct > 8'd100) ? 8'd100 : sharing_pct;

  // The mechanism is paid on EVERY access.
  assign mechanism_cost = {8'd0, ownership_lat};
  assign coherent_cost  = {8'd0, base_lat} + mechanism_cost;

  // The alternative pays nothing on most accesses and a hand-written
  // synchronisation cost - three times the ownership latency, an illustrative
  // penalty - on the fraction that shares.
  //
  // WIDTH INVARIANT, written down rather than guarded. `share_c` is clamped to
  // 100 and every other operand is 8 bits, so the intermediate product reaches
  // 100 x 255 x 3 = 76,500 in a 32-bit context and the result after the
  // division by 100 reaches 255 + 765 = 1,020 - far inside a 16-bit
  // destination. A clamp here would have no reachable input that takes its
  // true branch, and a mutation campaign proved exactly that. Widening
  // `base_lat` or `ownership_lat` beyond 8 bits invalidates this and needs a
  // clamp added back with a driven case that reaches it.
  assign h_q = {24'd0, base_lat}
             + ((({24'd0, share_c} * {24'd0, ownership_lat}) * 32'd3) / 32'd100);
  assign hand_written_cost = h_q[15:0];

  // The truth: the mechanism wins when it costs less than writing it by hand.
  assign coherent_better = (coherent_cost < hand_written_cost);

  // The whole review point: a reader for whom the mechanism is free.
  assign reported_better = (AUTOMATIC_MEANS_FREE != 0) ? 1'b1 : coherent_better;

  assign cost_err = evaluate && reported_better && !coherent_better;

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      n_evals <= 8'd0; n_wrong_picks <= 8'd0;
    end else if (evaluate) begin
      n_evals <= n_evals + 8'd1;
      if (cost_err) n_wrong_picks <= n_wrong_picks + 8'd1;
    end
  end
endmodule

The measurement. A base access cost of 100, an ownership cost of 30, and a workload sharing 10 percent of its accesses:

base 100, ownership 30, 10% sharing : coherent=130 hand_written=109 automatic_is_free_says=1

The mechanism is paid on EVERY access — 100 + 30 = 130. The alternative pays nothing on most accesses and a hand-written synchronisation cost on the shared fraction, which at 10 percent comes to 109. The mechanism is not the cheaper choice here, and the automatic-is-free build prefers it anyway.

The crossover is derived in the run, one percentage point at a time. At 33 percent sharing the hand-written path costs 129 and is still cheaper; at 34 percent it is exactly 130 and equal is not better; at 40 percent it is 136 and the mechanism wins. That is the trade the word "automatic" hides, and it is the same crossover 31.1 section 12 derives from the capability side.

All latencies are illustrative integers in arbitrary units. None is a CXL figure and none is attributed to any product. The crossover's existence is the durable result, not the numbers that produce it.

Why the belief is reasonable. The mechanism removes a class of bugs that are genuinely awful to write around by hand, and for a sharing workload it is unambiguously the right answer — which is the case that motivates the technology and therefore the case everybody has read about.

What it costs to hold. Overhead on every access of a streaming workload, bought to solve a problem that workload does not have.

What to say instead. "State the per-access cost and the sharing rate, and find the crossover. Around a third sharing, in this model's terms."

14. Test 9 — Write Down What Would Have To Be True

The claim under test. All of them, at once.

What "automatic" would require. Four conditions, and all four.

// RTL 9 - what would have to be true for "automatically solves" to hold?
//
// Same discipline, fifth chapter running. Four conditions: the protocol
// supplies every part of the problem, every agent that touches the memory
// participates, no program needs an ordering across addresses, and the design
// needs no recovery path of its own.
//
// TEACHING MODEL. Four illustrative booleans.
//
//   INITIALIZATION CONTRACT (combinational + counters):
//     power-on/reset : counters zero
//     re-initialise  : not applicable
//     telemetry      : met_pct beside the conjunction
module automatic_conditions #(parameter int MOSTLY_AUTOMATIC = 0) (
  input  logic clk, rst_n,
  input  logic       assess,
  input  logic       protocol_supplies_all, every_agent_participates,
  input  logic       no_ordering_needed, no_recovery_needed,
  output logic [7:0] conditions_met, n_assessments, n_overclaims,
  output logic [15:0] met_pct,
  output logic       would_hold, claimed_holds,
  output logic       auto_err
);
  logic [31:0] m_q;
  assign conditions_met = {7'd0, protocol_supplies_all} + {7'd0, every_agent_participates}
                        + {7'd0, no_ordering_needed} + {7'd0, no_recovery_needed};
  // No clamp: four one-bit values over four cannot exceed a hundred.
  assign m_q = ({24'd0, conditions_met} * 32'd100) / 32'd4;
  assign met_pct = m_q[15:0];
  assign would_hold = (conditions_met == 8'd4);
  assign claimed_holds = (MOSTLY_AUTOMATIC != 0) ? (conditions_met >= 8'd3) : would_hold;
  assign auto_err = assess && claimed_holds && !would_hold;

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      n_assessments <= 8'd0; n_overclaims <= 8'd0;
    end else if (assess) begin
      n_assessments <= n_assessments + 8'd1;
      if (auto_err) n_overclaims <= n_overclaims + 8'd1;
    end
  end
endmodule

The measurement. Three of four met:

3 of 4 conditions : met=75% would_hold=0 mostly_automatic_says=1

Seventy-five percent, and a conjunction has no partial credit. The fourth condition is the one that is never true of any real link, which means the claim fails by construction rather than by circumstance.

What to say instead. "Here are the four things that would have to be true. The fourth one is never true of a physical link."

15. The Misconception Assembled

Nine tests, one summary.

// RTL 10 - the misconception examined. Nine tests, one summary.
// "The protocol defines coherence" is bit 0: a true statement about a
// specification, and one sixth of an argument about a system.
module auto_review_signoff #(parameter int PROTOCOL_EXISTS_IS_PROOF = 0) (
  input  logic clk, rst_n,
  input  logic        review,
  input  logic        protocol_defines_it, parts_counted, participation_checked,
  input  logic        ordering_named, recovery_built, conditions_checked,
  output logic [5:0]  fail_mask,
  output logic [15:0] conditions_met, sound_pct,
  output logic        sound,
  output logic [7:0]  n_reviews, n_sound, n_claimed,
  output logic        mis_err
);
  logic [31:0] s_q;
  logic        truly_sound, claimed;
  assign fail_mask[0] = ~protocol_defines_it;
  assign fail_mask[1] = ~parts_counted;
  assign fail_mask[2] = ~participation_checked;
  assign fail_mask[3] = ~ordering_named;
  assign fail_mask[4] = ~recovery_built;
  assign fail_mask[5] = ~conditions_checked;
  assign conditions_met = {15'd0, protocol_defines_it} + {15'd0, parts_counted}
                        + {15'd0, participation_checked} + {15'd0, ordering_named}
                        + {15'd0, recovery_built} + {15'd0, conditions_checked};
  assign s_q = ({16'd0, conditions_met} * 32'd100) / 32'd6;
  // No clamp: six one-bit values over six cannot exceed a hundred.
  assign sound_pct = s_q[15:0];
  assign truly_sound = (fail_mask == 6'd0);
  assign claimed = (PROTOCOL_EXISTS_IS_PROOF != 0) ? protocol_defines_it : truly_sound;
  assign sound = claimed;
  assign mis_err = review && !truly_sound && claimed;

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      n_reviews <= 8'd0; n_sound <= 8'd0; n_claimed <= 8'd0;
    end else if (review) begin
      n_reviews <= n_reviews + 8'd1;
      if (truly_sound) n_sound <= n_sound + 8'd1;
      if (claimed)     n_claimed <= n_claimed + 8'd1;
    end
  end
endmodule

The measurement. Two views of the same argument:

no recovery path was built : mask=010000 met=5 sound=83%
the protocol defines coherence : mask=111110 met=1 sound=16%

The first line is a serious design with one thing missing — bit 4, no recovery path — and it is the one that costs the most when the link has its first bad day. Five of six, and the missing sixth is the one nobody notices until an incident.

The second line is the misconception. Bit 0 is clear — the protocol does define coherence — and nothing else was done. Sixteen percent of an argument, from a true statement about a specification.

Figure 3 — bit 0 is a fact about a document, and the other five are facts about a system. A claim about a system cannot be established from a fact about its specification.

16. Quantitative Reasoning

Every figure here is a teaching parameter or a value derived from one and asserted by the testbench. None is a measurement of a real system, and none is a figure from any specification.

The division of labour, derived. Five parts with two supplied leaves 5 − 2 = 3 for the design, and 2 × 100 / 5 = 40 percent automatic. The general form is yours = total − supplied, and "automatic" requires that number to be zero. At three of five it is not close. The run also drives four of five — 80 percent — which is still not automatic, because the word is a conjunction and not a threshold.

Guarantees. Two independent guarantees, per-address agreement and cross-address ordering, give four states. The two readings disagree in exactly one — a program needing the ordering on a system providing only coherence. One cell of four, which is why the shortcut survives.

Participation, derived. Six agents with five participating leaves 1 outside. The invariant holds unless an outsider writes, so the model separates exposure (an outsider exists) from violation (an outsider writes). One agent outside is enough, which makes this the only quantity in the chapter where the threshold is one rather than a fraction.

The ordering window. The payload store is issued on one edge and lands on a later one, and the reordered flag can become visible in between. The torn window is therefore (land − issue) cycles wide, and a barrier closes it to zero. A window of width zero is the only safe width, which is why a barrier is a construct rather than an optimisation.

Handoffs, derived. Two legal ownership changes give a handoff count of 2, and the application races throughout. A counter that reads 2 with nothing wrong from the protocol's point of view is the chapter's central number: it is healthy during the failure, so it cannot be evidence of correctness.

Recovery. Three states: not exposed, exposed and unhandled, exposed and handled. Correct-under-error is (no error) OR (recovery built AND retried), and the middle state — built and not run — is the one the shortcut gets wrong, because a path that exists has not recovered anything.

Region coverage, derived. Four agents with three participating is 3 × 100 / 4 = 75 percent, and 75 percent covered is not covered. A region nothing touches is vacuously covered — a decision the model makes explicitly rather than by dividing by zero, and one a mutation attacked.

The cost, derived. A base of 100 with an ownership cost of 30 gives a coherent path of 130 on every access. The hand-written alternative is 100 + (share × 30 × 3)/100, where the factor of three is an illustrative penalty for writing synchronisation by hand:

The bolded figure is the cheaper one, and at 34 percent neither is: equal is not better, which is one comparison operator's worth of difference and the reason the crossover sits at 34 rather than at 33.

The crossover is at 34 percent, it is driven one point at a time, and its existence does not depend on the factor of three — only its location does.

Conditions, derived. Four conditions with three met is 3 × 100 / 4 = 75 percent, and the fourth — that no message is ever lost — is never true of a physical link, so the claim fails by construction.

The sign-off arithmetic. Six conditions; five met is 5 × 100 / 6 = 83 percent under integer division, and one met is 100 / 6 = 16 percent.

17. Verification Method

Order of work

names.txt → ten models, each compiled alone → model-expressiveness review → boolean-tautology review → width review → structural gates → testbench → legal baseline → PASS → mutation campaign → re-baseline after every change → MDX assembled from the verified sources

Two of the three pre-simulation reviews fired on this chapter, and both findings are in section 18. The structural gates then returned zero on every model on their first run — because the reviews had already removed what the gates would have found.

Independent oracles

chkv prints got against expected, which is what lets an oracle be wrong out loud. In this chapter it caught one, mine, recorded in section 18.

X and Z rejected explicitly

chk(c, …) tests c !== 1'b1, so an X-valued condition fails rather than passing. chkv(got, exp, …) reduces the result and reports an explicit X/Z failure before comparing. The scripted output-connectivity gate returns zero on all ten models.

Pulses are latched, never sampled

Every evidence output — mech_err, cons_err, part_err, order_err, race_err, fault_err, cov_err, cost_err, auto_err, mis_err — is caught by a continuous always @(posedge clk) monitor into a sticky bit, asserted outside any conditional, in a window containing a clock edge.

Stimulus never lands on the active edge, and reset is released after it

step_clk is @(posedge clk); #1;, and reset release lands one delta after the edge.

Initialisation contracts are stated, not implied

Two models carry real sequential state, and both headers answer the same questions explicitly.

The ordering model's round boundary dominates a store arriving in the same cycle, because a boundary a store could cross would mix two publications into one measurement. The race model's round boundary dominates an acquire, and A is arbitrated ahead of B — which is the protocol doing exactly what it promises, stated as a priority rather than left to source order. All three priorities are driven by the run.

Both builds are always instantiated

Every model has both its honest and its shortcut build wired to the same stimulus, and the testbench asserts the internal figures on both. In nine of the ten, the shortcut build computes the honest figure internally and reports a different conclusion from it.

Safety, liveness and performance kept apart

Safety — a reader never consumes a payload the writer had not published. Work never proceeds on an un-arbitrated critical section. An invariant is never reported holding while an agent outside the domain has written. None requires an assumption.

Liveness — nothing in this chapter is a liveness claim.

Performance — one model is explicitly a performance claim and is marked as one: the cost comparison has a crossover, and being on the wrong side of it is expensive rather than incorrect.

18. Baseline Defects Found Before Mutation

RTL defects — two, and BOTH were found before a single cycle was simulated

The two pre-simulation gates this batch introduced both fired on this chapter, on their first real use.

The model-expressiveness review found a structurally unreachable state

The ordering model is the chapter's central experiment. In the first version both the payload and the reordered flag were set on the same edge from the same input, so "flag visible, payload not" was structurally unreachable and the whole experiment was inexpressible.

The §8 question is what caught it — can this model represent at least two observably different outcomes for the property the experiment claims to distinguish? It could not, and no amount of stimulus would have made it.

The fix models the payload store in two parts: issued, then landed. The window between them is the thing the chapter is about, and the reordered flag now overtakes an issued-and-unlanded payload. This is the third instance of the class in two batches — after 30.7's correlation model and 31.4's rebind sequence — which is why the review is a gate rather than a habit.

The boolean review found a tautology dressed as a guarantee

The race model published handoff_legal = (own_q <= 8'd2). own_q is only ever 0, 1 or 2, so the expression is true for every input. It looked like the protocol's guarantee and was a constant.

domcheck does not model a universally-true term, which is the same blind spot 30.7 recorded. It was found by the §11 review, by asking what input makes it false.

Its replacement is a better teaching signal. n_handoffs counts ownership changes — a number a protocol-level health dashboard would show, which stays perfectly healthy while the application races. That is the chapter's point made as telemetry rather than as prose, and it is now the sharpest number in section 10.

Testbench defects — none. Wrong oracles — one, mine.

An expectation stated for one position in the sequence and used at another. The re-acquire case expected a handoff count of 2, derived before it was placed after a simultaneous-acquire case that had already taken the count to 3. The correct expectation is that the count does not move — which is the property under test and reads better than the number did.

Third instance of this class in this batch, after 31.3 and 31.4. The habit: an expectation that follows an inserted case must be re-derived at its actual position, not carried.

A third dead clamp, found by the campaign

The hand-written cost clamped a value whose maximum is 255 + (100 × 255 × 3)/100 = 1,020 against a 16-bit destination holding 65,535. Unreachable, deleted, and the bound written into the source — 30.5 section 20's rule, third application in this batch.

Two clamps in the same batch were checked and are live: 31.3's ratio reaches 650,250, and 31.4's effective latency is fed by a clamped share. A clamp is dead or live as a function of its own operand widths, and every one has to be computed rather than assumed.

Coverage gaps found by the structural gates

This is the first chapter in three batches where every structural gate returned zero on the first run. The reason is not that the models were better written — it is that the two model defects above were removed before the testbench existed, so the gates had nothing left to find.

Compiler-warning findings

Under -Wall the ten models produce no truncation, select-width, signedness, cast, multiplication-width, shift-width or loop-width warnings.

Five width results were reasoned rather than trusted.

• share_c × ownership_lat × 3 reaches 100 × 255 × 3 = 76,500 in a 32-bit context; the division by 100 brings the result to at most 765, and the total with the base cost to 1,020. Documented, and the clamp that guarded it was dead and was deleted.
• parts_total − prot_c, agents_total − part_c and region_agents − part_c are 8-bit subtractions that cannot underflow, because each subtrahend is clamped to its minuend first. All three clamps are load-bearing and the campaign kills the mutations that remove them.
• prot_c × 100 and part_c × 100 reach 25,500 in 32 bits before a division that caps the result at 100.
• n_reads + 1, torn_reads + 1, n_works + 1, app_races + 1 and n_handoffs + 1 all saturate at 8'hFF explicitly.
• conditions_met × 100 / 4 and / 6 cannot exceed 100: a sum of one-bit values over its own denominator.

Simulator constraints

Icarus Verilog 13.0 rejects ref task arguments, carried forward.

19. Mutation Testing

77 mutations attempted, 77 non-equivalent, 77 killed. Four survivors, every one classified before anything was changed. Zero unexplained survivors, zero equivalents withdrawn.

Four survivors across the campaign, every one classified before anything was changed. Three came from the first run of the original sixty-five mutations; the fourth came from six mutations added afterwards to bring the three thinnest models up to the depth of the rest, and it found something the first sixty-five had not.

One was dead code, and the response was to delete it

The hand-written-cost clamp could not be killed because it can never fire. Deleted, with the bound written down — not withdrawn, and not asserted around. The mutation attacking it was retargeted to the live clamp in the same model, where it dies.

Three were the conjunction family

All three are one term of a conjunction driven false while the others are true. The third is the plainest of them: (!link_error) || (recovery_built && retried), with retried true and recovery_built false. Somebody retried, the incident review records a retry, and there was never a path for the retry to take — and until that case was driven, a build that credited the retry alone passed every check in the chapter.

For every conjunction, drive each term false with the others true.

That rule has now produced findings in every chapter of batches 031 and 032, and three of them in this one chapter. It is the highest-yield stimulus rule the track has, and the third finding here arrived only because the model was mutated more than the first campaign thought necessary.

The second one is worth keeping for its own sake. A re-acquire by the agent that already owns the line is every message legal and no handoff, which is a distinction a protocol-level counter has to make correctly or its healthy-looking number becomes a wrong number as well as a useless one.

The classification rule

Never add an assertion for a survivor before classifying it.

20. Synthesis And Implementation Reality

These models are not meant to be synthesised. What follows is the honest reading of what the mechanisms they abstract cost, because "automatic" is a cost claim and it deserves a cost answer.

The ownership lookup is on the access path, and that is the whole cost story. Every access that participates pays a lookup, a possible interrogation of other holders, and a wait for the answer. It is not a background task and it cannot be pipelined away, because the access depends on its result.

The ordering construct is not free either. A barrier is a stall or a drain, depending on where it is implemented, and the window it closes is exactly the window section 9's waveform shows. A barrier that costs nothing is a barrier that does nothing.

A participation audit is a design-time structure, not a runtime one. Its cost is an enumeration of every agent that can reach a region, kept current, and the expensive part is keeping it current rather than building it once.

The recovery path is the largest omission the belief produces. A timeout, a retry, and a decision about what a partially-completed ownership change means. Each of those is state and a specification, and the specification is the expensive half.

The telemetry is nearly free and is the part most often missing. A handoff counter is one register. A per-region participation count is a design-time number published in a register. An agents-outside-the-domain count is one subtraction. Section 21 lists them, and the total is a handful of flops against a class of failure that otherwise presents as data corruption.

Every counter in this chapter saturates rather than wrapping, and the campaign kills every mutation that removes a saturation. A comparator and a mux against a counter that reads zero when it should read 256 is not a trade anybody should consider.

No area, frequency or power figures appear in this chapter, because none was measured.

21. Silicon Observability

The fifth and sixth together are the chapter in two registers. Handoffs stay healthy while application races accumulate, and publishing both makes the distinction visible to anybody reading a dashboard — which is the only place the distinction can be made in production.

Three counters must read permanently zero — outside-domain writes, torn reads, and application races. Each costs a comparator and a register, and each catches a failure that otherwise arrives as a corruption report with no protocol error anywhere near it.

The seventh is the one nobody has. Recovery paths absent is a design-time fact published at runtime, and it is the only way an operator can know that a link event will not be handled before the link event happens.

22. DebugLabs

These labs debug systems built on the misconception. The symptom is a data-integrity failure with no protocol error anywhere, and that combination is the signature of this belief in every one of them.

Lab 1 — Data corruption with a clean protocol log

Symptom. Intermittent data corruption in a coherent region. Every protocol counter is healthy. No error is reported anywhere.

Evidence. The corruption correlates with a DMA engine's activity, not with any protocol event.

Hypothesis. An agent outside the coherent domain is writing.

Investigation. Count the agents that can reach the region and the agents inside the domain. Six and five.

Root cause. The protocol is not violated. The invariant is. No message is owed for a write by a non-participant, so nothing is logged.

Fix. Bring the engine into the domain, or route its accesses through an agent that is in it.

Prevention. Count the agents that can touch this memory, and the ones inside the domain. The difference is the exposure, and it is one subtraction.

Observability. Outside-domain writes. Permanently zero, and one counter.

Lab 2 — A publish-then-consume pattern tears in production only

Symptom. A producer-consumer pattern works on every development machine and tears intermittently in production under load.

Evidence. The payload is stale and the flag is set. Both locations are individually coherent.

Hypothesis. The flag became visible before the payload.

Investigation. Instrument the two stores separately. On the production machine the flag overtakes an issued-and-unlanded payload.

Root cause. Coherence guarantees per-address agreement and not cross-address ordering, and the development machine happened not to reorder.

Fix. The ordering construct the program needs, between the two stores.

Prevention. Name the ordering you need and the construct that provides it. Coherence is not that construct.

Observability. A torn-read counter. It is the only place this failure is visible as a failure rather than as corruption.

Lab 3 — Corruption under load, clean under a debugger

Symptom. Two agents corrupt shared data under load. Attaching a debugger makes it stop.

Evidence. Every ownership handoff is legal. The handoff counter is healthy and rising.

Hypothesis. The protocol serialised the line and nobody serialised the work.

Investigation. Check for an application-level lock around the critical section. There is none: the code relies on ownership being exclusive.

Root cause. Ownership is exclusive and is not a lock. A line is not a critical section, and the protocol arbitrated the wrong thing.

Fix. An application-level lock around the work.

Prevention. Ask what the protocol serialised. Exclusivity of a line is necessary and is not sufficient.

Observability. An application-race counter beside the handoff counter. The first reads non-zero while the second looks perfect, which is the whole diagnosis in two registers.

Lab 4 — A hang after a link event, with no path designed for it

Symptom. A link error is followed by a hang. The system never recovers.

Evidence. The design has no recovery path for a partially-completed ownership change. The protocol specification describes what a correct exchange is.

Hypothesis. A definition of correctness was read as a guarantee of it.

Investigation. Trace the exchange. A message was lost mid-transfer and nothing was written to handle that.

Root cause. The protocol defines a correct exchange and does not make the wire perfect.

Fix. A timeout, a retry, and an explicit decision about what a half-completed ownership change means.

Prevention. Ask what happens when a message is lost, and who wrote that path. It is the largest omission this belief produces.

Observability. Recovery paths invoked, and recovery paths absent. The second is a design-time fact published at runtime, and it is the only way to know before the event.

Lab 5 — A workload placed in a region that is not covered

Symptom. A workload experiences integrity failures on a platform documented as coherent.

Evidence. The platform claim is true at the platform level. The region the workload uses has an agent outside the domain.

Hypothesis. A platform-level claim was applied to a region.

Investigation. Compute the coverage of the region in question. Three of four agents participate.

Root cause. Participation is a property of a region and its agents, not of a system. Seventy-five percent covered is not covered.

Fix. Place the workload in a fully covered region, or bring the fourth agent into the domain.

Prevention. Ask for the coverage of THIS region. A platform claim has the wrong granularity.

Observability. Per-region participation coverage. A platform claim becomes a per-region number.

Lab 6 — A streaming workload got slower after being made coherent

Symptom. A workload that shares almost nothing degrades after being moved to a coherent path.

Evidence. Every access now pays an ownership lookup. The shared-access fraction is under 10 percent.

Hypothesis. The mechanism's cost is being paid on every access to buy correctness this workload was never going to violate.

Investigation. Compute both costs at the measured sharing rate. 130 against 109.

Root cause. "Automatic" read as "free", and a cost on every access weighed against a benefit on a tenth of them.

Fix. Move it back, and record the sharing fraction as the selection criterion.

Prevention. State the per-access cost and the sharing rate, and find the crossover. Around a third, in this model's terms.

Observability. Ownership cost per access and the shared-access fraction. Two numbers, and their comparison is the decision.

Lab 7 — A recovery path exists and has never run

Symptom. A link event produces a failure despite a recovery path being in the design.

Evidence. The recovery path was implemented and has never been exercised — not in verification, not in production.

Hypothesis. Built is not the same as working.

Investigation. Inject the error deliberately. The path is entered and does not complete.

Root cause. A recovery path that exists and has not run has not recovered anything, which is the middle of three states and the one the shortcut reading collapses into "handled".

Fix. Exercise it in verification, with error injection, and count invocations in production.

Prevention. Correct-under-error is built AND run, not built. The middle state is the one that looks safe.

Observability. Recovery invocations. Zero on a system with a marginal link is a finding, not a reassurance.

Lab 8 — A design review accepted "the protocol handles it"

Symptom. A design ships with no ordering plan, no participation audit and no recovery path. Each is found by a different failure over the following year.

Evidence. The review minutes record the protocol's guarantees and nothing about the complement.

Hypothesis. A division of labour was assumed rather than written down.

Investigation. Write the parts of the problem and mark who supplies each. Two of five are the protocol's.

Root cause. A mechanism read as a discipline. The protocol's contribution is real and is 40 percent.

Fix. The two-column table, in the review, with an owner for every row in the right-hand column.

Prevention. Count the parts on each side and publish both numbers. "Forty percent automatic" is a number somebody can act on; "the protocol handles coherency" is not.

Observability. Parts supplied against parts remaining. A design-time number, and the one that turns a belief into a plan.

23. Coverage Reasoning

Coverage of a design built on this belief is the most misleading coverage in the module, because the protocol-level bins all fill and the failures are all outside them.

Four coverage models are worth keeping:

Guarantee-versus-need coverage. A cross of needs cross-address ordering against ordering provided, four cells. The cell that matters is needs-and-not-provided, and a test suite written on a strongly-ordered machine fills it never.

Participation coverage. Agents-outside-the-domain crossed with whether an outsider writes, four cells. The distinction between exposure and violation is two of those cells, and conflating them makes every audit finding look like an incident.

Ordering-window coverage. Issued crossed with landed, with the reordered flag in between. The torn cell is issued-and-not-landed with the flag visible — and this chapter's model could not reach it until the store was split in two. An unreachable cell is a finding about the model, not about the plan.

Cost-crossover coverage. Sharing rate binned below, at and above the crossover. The bin at exactly the crossover is where equal-is-not-better lives, and it is the one value a comparison operator can get wrong.

The bin the shortcut build cannot hit is the most valuable bin in any model. In section 8 it is "an outsider exists and has not written". In section 9 it is "the flag is visible and the payload is not". In section 11 it is "a recovery path built and never run". Each is unreachable in the shortcut build and trivial in the honest one.

24. How This Appears In Real Engineering

Introductions list what a protocol provides, because that is what a protocol document contains, and the complement is left to the reader to infer.

The ordering distinction is taught once, usually in a lecture about memory models, and a lecture is a weaker prior than years of working on strongly-ordered machines.

Non-participating agents arrive later. The coherent domain is designed, and then something is added — an engine, a path, an accelerator — and the audit that would have caught it was a design-time activity that has already happened.

Development machines do not reorder as aggressively as production ones, so the ordering failure is systematically discovered by customers.

Ownership is exclusive, and exclusivity is what a lock provides, so the inference is one step and the step is almost right.

Recovery paths are written last because nothing needs them until something fails, and the first failure is in production.

Platform-level claims are the only claims anybody is given, and they are usually true at the level they are made.

And the cost is invisible because it is uniform. An ownership lookup on every access does not show up as a spike; it shows up as a baseline, and a baseline is what everybody calibrates against.

25. Where The Misconception Comes From

The protocol's contribution is real. Everything the introduction says it provides, it provides — so there is no false premise to correct, and the belief cannot be fixed by fixing a fact.

"Solves" is the word doing the damage. A mechanism makes a property achievable and the word suggests it makes the property true. That is one word's worth of overreach and it is repeated in every summary.

The division of labour is never written down. A protocol document describes its own half, and no document describes the other half, so the other half looks empty.

The failures are separated from their cause. An ordering failure presents as application corruption; a participation failure presents as corruption correlated with an unrelated engine; a missing recovery path presents as a hang. None of them presents as a protocol error, so none of them points back at the belief.

And the belief is load-bearing for a schedule. "Coherency is handled" removes three structures from a plan, and a plan without them is shorter. The belief is not just held; it is useful, which is the hardest kind to dislodge.

26. Common Misconceptions

"CXL handles coherency, so we do not have to think about it." Count the parts. Two of five are the protocol's, and 40 percent automatic is a number, not a verdict.

"It is coherent, so the ordering is handled." Coherence is per address; ordering is across addresses. Two guarantees, supplied separately.

"Everything on the link is coherent." Attachment is not participation. One agent outside the domain is enough.

"The flag cannot arrive before the payload." On a machine that may reorder them, it can — and not one protocol message is out of place when it does.

"The protocol serialises them, so there is no race." It serialised the line. A line is not a critical section.

"The handoff counter is healthy, so coherency is fine." It stays healthy during the failure. A number that cannot move when things go wrong is not evidence.

"The protocol guarantees correctness." It defines a correct exchange. It does not make the wire perfect.

"We have a recovery path." Has it run? Built and never run has recovered nothing.

"The platform is coherent." For which region? Participation is a property of a region and its agents.

"Coherency is handled, so there is nothing to weigh." The mechanism is paid on every access. Find the crossover — around a third sharing in this model's terms.

"Mostly automatic." A conjunction has no partial credit, and the fourth condition — no message is ever lost — is never true of a physical link.

"The protocol defines coherence." That is bit 0, and it is worth one sixth of an argument about a system.

27. Interview And Design-Review Questions

Mechanism and discipline

1. What kind of claim is "the protocol handles coherency"? A claim about a division of labour. It is not false about the protocol's half; it is false about the complement.

2. Name two things the protocol supplies and three it does not. Supplies: a way to acquire ownership, a way to be interrogated. Does not: the ordering across addresses, the participation audit, the recovery path.

3. Five parts with two supplied. What is the honest headline? Three parts are yours and the problem is 40 percent automatic — a number somebody can act on.

4. Four of five supplied. Is that automatic? No. The word is a conjunction, not a threshold, and 80 percent automatic still leaves a structure somebody has to build.

5. Why is this belief harder to dislodge than the others in this module? Because it is useful. It removes three structures from a plan, and a plan without them is shorter.

6. Which single word does the damage? "Solves". A mechanism makes a property achievable; the word suggests it makes the property true.

Coherence, consistency and ordering

7. State what a coherence protocol guarantees. That all participating agents agree about the value of one location.

8. State what it does not guarantee. The order in which accesses to two different locations become visible.

9. Which of the two does a publish-then-flag pattern depend on? Entirely the second, and it gets none of it from the first.

10. Describe the torn read. The flag becomes visible while the payload store is issued and not yet landed, so a reader that tests the flag consumes a payload that was never published.

11. How wide is the window? The gap between issue and landing. A barrier closes it to zero, and a window of width zero is the only safe width.

12. Why is this failure systematically found by customers? Because development machines reorder less aggressively than production ones, so the pattern is correct everywhere it is written and tested.

13. What is the fix? The ordering construct the program needs, between the two stores. Coherence is not that construct.

Participation and domains

14. Over what does a coherence invariant hold? The agents that participate in it — not the agents attached to the link.

15. An engine writes a location while another agent holds a copy, and no message is exchanged. Who is wrong? Nobody, from the protocol's point of view. No message is owed for a write by a non-participant. The protocol is not violated; the invariant is.

16. Why does that failure produce a clean protocol log? Because there was nothing to log. That is the signature of this belief in a debug session.

17. Distinguish an exposure from a violation. An agent outside the domain is an exposure. An agent outside the domain writing is a violation. Conflating them makes every audit finding look like an incident.

18. Is participation a property of a system or of a region? Of a region and the agents that touch it. A platform can be coherent for one range and not for another.

19. Four agents touch a region and three participate. Is it covered? No. Seventy-five percent covered is not covered, and one agent outside is enough.

20. What is the granularity error in "the platform is coherent"? It is usually true at the level it is made and says nothing about the region the program is using.

Races, recovery and cost

21. Ownership is exclusive. Is it a lock? No. It serialises the line; it does not decide whose turn it is to do the work.

22. Two agents each acquire ownership legally and the data is corrupted. What happened? The protocol arbitrated the line and the application never arbitrated the critical section. Every message was correct and the result is wrong.

23. Why can the handoff counter not be used as evidence of correctness? Because it stays healthy during exactly this failure. A number that cannot move when things go wrong is not evidence.

24. What two counters together diagnose this in production? Ownership handoffs and application-level races. The second reads non-zero while the first looks perfect.

25. A re-acquire by the agent that already owns the line — is it a handoff? No. Every message is legal and the holder does not change, and a counter that counts it is wrong as well as useless.

26. What does a protocol specification guarantee about a lost message? Nothing. It defines what a correct exchange looks like and does not make the wire perfect.

27. Give the three recovery states. Not exposed; exposed and unhandled; exposed and handled. Built-and-never-run is the middle one wearing the third one's clothes.

28. Write the correctness condition under error. No error, or (recovery built and retried). Dropping the second conjunct is the shortcut, and it makes a path that exists look like a path that worked.

29. What does the mechanism cost, mechanically? A lookup on the access path, a possible interrogation of other holders, and a wait for the answer — on every participating access.

30. Base 100, ownership 30, 10 percent sharing. Which path is cheaper? The hand-written one, at 109 against 130 — because the mechanism's 30 is paid on every access while the hand-written penalty is paid on the tenth of accesses that share.

31. Where is the crossover? Around 34 percent sharing in this model's terms. Below it the hand-written path wins; above it the mechanism does.

32. At exactly the crossover, which wins? Neither — they are equal, and equal is not better, which is a comparison operator's worth of difference.

33. Why is the mechanism's cost invisible in practice? Because it is uniform. It does not show up as a spike; it shows up as a baseline, and a baseline is what everybody calibrates against.

Method

34. Give the four conditions "automatically solves" requires. The protocol supplies every part, every agent participates, no program needs an ordering across addresses, and no message is ever lost.

35. Which of the four is never true? The fourth. No physical link is lossless, so the claim fails by construction rather than by circumstance.

36. What makes a mutation campaign invalid? A failing baseline. Every mutation then fails for the reason the baseline does.

37. A mutation cannot be killed. Distinguish the two model-level causes. An equivalent mutant means the code is tighter than it looks — no input separates them. A model-expressiveness gap means the model is looser than the world — the input exists in reality and the model cannot represent it.

38. This chapter's central experiment was inexpressible at first. What was wrong? The payload and the reordered flag were set on the same edge, so "flag visible, payload not" was structurally unreachable. The store had to be split into issued and landed.

39. Why is that a gate rather than a habit? Because it is the third instance in two batches, and because no amount of stimulus fixes it — the question has to be asked before the testbench exists.

40. What did the boolean review find here? A published output of the form own_q <= 2 where own_q is only ever 0, 1 or 2 — true for every input, a tautology dressed as the protocol's guarantee.

41. Why did domcheck report zero on it? It models domination between a guard and an enclosing condition, not a term that is universally true.

42. What replaced it, and why is the replacement better? A handoff counter — a number that can actually move, and one that demonstrates the chapter's point by staying healthy during the failure.

43. A clamp's mutation survives. What do you compute first? The maximum the expression can reach against its destination width. Here it was 1,020 against 65,535, so the clamp was dead and was deleted.

44. Your expected value was 2 and the result was 3. What is the lesson? Re-derive every expectation that follows an inserted case. An expectation carried across an insertion describes the old ordering.

45. Every structural gate returned zero on this chapter's first run. What does that prove? That the pre-simulation reviews had already removed what the gates would have found — not that the models were better written.

46. State the single question this chapter turns on. How many parts of the problem does the protocol supply, and how many are still yours?

28. Exercises

1 — Design review · Intermediate. Builds: writing down a division of labour. Take a coherent design you know. Bounded scope: list the parts of the coherency problem, mark each as supplied by the protocol or by the design, compute the automatic percentage, and name an owner for every part in the second column. Hint: the second column is where the failures in section 22 live.

2 — Analysis · Intermediate. Builds: separating two guarantees that share a name. Take three patterns from a codebase you know that depend on memory behaviour. Bounded scope: for each, say whether the property it needs is about one address or two, name the guarantee that supplies it, and mark the ones that would break on a reordering machine. Hint: a publish-then-flag pattern is the canonical case and there are usually several.

3 — Architecture · Advanced. Builds: auditing participation per region. Take a memory map with three regions. Bounded scope: for each region, enumerate the agents that can reach it and the agents inside the coherent domain, compute the coverage, and distinguish the regions that are exposed from the regions that are violated. Hint: an outsider that never writes is an exposure, and the two findings deserve different priorities.

4 — Debug · Advanced. Builds: reading a clean protocol log as evidence. You are given data corruption in a coherent region with every protocol counter healthy. Bounded scope: give the two hypotheses this chapter supports, the one measurement that distinguishes them, and the counter you would add so the next occurrence is diagnosable in one read. Hint: both hypotheses produce a clean log, for different reasons.

5 — Design · Advanced. Builds: specifying the largest omission the belief produces. Specify the recovery path for a partially-completed ownership change. Bounded scope: name the timeout, the retry policy, the state the system is left in at each interruption point, and the telemetry that proves the path has ever run. Hint: "built" and "run" are different states and the first one looks safe.

6 — Quantitative · Advanced. Builds: finding the crossover instead of holding a preference. A base access costs 200 units and the ownership lookup adds 50. The hand-written alternative costs three times the ownership latency on the shared fraction. Bounded scope: compute both costs at 10, 25 and 50 percent sharing, find the crossover, and say what happens to it if the ownership cost halves. Hint: the second half of the question is the one that shows whether the crossover depends on the constant.

7 — Design · Advanced. Builds: telemetry that survives a healthy dashboard. Specify the observability for a coherent design so that a correctness failure cannot hide behind healthy protocol counters. Bounded scope: name every counter, say which must read permanently zero, and identify the pair whose disagreement is the diagnosis. Hint: one of the pair is the number the protocol already publishes.

8 — Verification · Expert. Builds: asking whether a model can express its own experiment. Take a verification model you have written for a temporal property. Bounded scope: name the manipulated variable, the held variable, the independent observation and the expected divergence; then check whether the model can reach both outcomes, and if it cannot, say whether the fix is more stimulus or a different model. Hint: this chapter's central model could not, and no stimulus would have helped.

29. Summary

A protocol is a mechanism. Correctness is a property of a system. A mechanism makes a property achievable; it does not make it true.

Count the parts. Two of five supplied is 40 percent automatic, and the other three are structures somebody has to build.

Coherence is per address; consistency is across addresses. A publish-then-flag pattern depends entirely on the second and gets none of it from the first.

The flag can arrive first, and not one protocol message is out of place when it does. A barrier closes the window to zero, and zero is the only safe width.

An agent outside the domain breaks the invariant with no message exchanged. The protocol is not violated; the invariant is — which is why the log is clean.

Attachment is not participation, and participation is a property of a region rather than of a platform. Seventy-five percent covered is not covered.

Ownership is exclusive and is not a lock. The protocol serialised the line; a line is not a critical section.

The handoff counter stays healthy during the failure, which is exactly why it cannot be evidence of correctness — and the application-race counter beside it is the diagnosis.

A specification defines a correct exchange and does not make the wire perfect. A recovery path that exists and has never run has recovered nothing.

The mechanism is paid on every access. Find the crossover — around a third sharing in this model's terms — and know which side of it you are on.

A conjunction has no partial credit, and the fourth condition here — that no message is ever lost — is never true of a physical link.

Six conditions, and "the protocol defines coherence" is one of them. A fact about a document, checked correctly, is 16 percent of an argument about a system.