Dynamic Resource Allocation

12.2 decided which host should get what.

15.3 established what is out there to give.

This chapter is the mechanism in between: taking a decision that has already been made and applying it to a running host, safely, reversibly, and without handing the last tenant's data to the next one.

1. The Engineering Problem — A Bind Is Not A Table Write

Six things make binding a device to a host harder than recording the decision.

The steps have an order and it is load-bearing. Reserve, program the routing, present, activate. A device presented before its routing exists is a device the host can address and the fabric cannot deliver to. Section 5 builds the ordering.

Unbinding is not the bind backwards. The host is using the device right now. Revoke the routing first and transactions in flight have nowhere to land. Section 6 builds notify, drain, revoke.

Exactly one host at a time. Two hosts bound to one device is not sharing — they have no protocol between them, and each believes it owns it. Section 8 builds the exclusion.

The host is already running. It does not re-enumerate because a device appeared; it has to be told, and told once. Section 9 measures the interval during which capacity is installed, bound, and unusable.

A bind can fail part-way, and the undo is different at each stage. A rollback that undoes the wrong amount either leaks a reservation or leaves routing programmed for a bind that never happened. Section 10 builds both failures.

And the memory still contains the last host's data. Rebinding without scrubbing hands one tenant's data to the next, and nothing in the binding protocol notices. Section 11 is the one to read twice.

This chapter against 12.2, stated precisely. That chapter owns the policy — fit, fairness, which host deserves the capacity. This one owns the transaction that carries a decision out. If a section here could be moved into Module 12 without loss, it is in the wrong chapter.

2. The One-Sentence Model

Binding is an ordered, reversible transaction against a live host, ending in a device that is exclusively owned, visible, routed, and clean — and every failure below is one of ordered, reversible, live, exclusive or clean missing.

3. What This Chapter Owns

Deferred:

4. Teaching-Model Boundary

Four devices, four hosts, a 64-unit device, an eight-word dirty counter. A real bind takes milliseconds and a real scrub takes far longer relative to everything else — which makes section 13's cost argument stronger, not weaker.

What is faithful: the four-stage bind ordering, the notify-drain-revoke unbind, the exclusion rule, the notification that a running host needs, the stage-dependent undo, the scrub-before-rebind requirement, slice arithmetic, and the compare-and-swap on the bind table.

What is not: every width, every duration, and the assumption that a scrub is one cycle per dirty word.

Every model is parameterised so the correct behaviour and a specific plausible failure are the same source under a different parameter.

5. RTL 1 — The Order Of A Bind

module bind_fsm #(parameter int PRESENT_EARLY = 0) (
  input  logic clk, rst_n,
  input  logic       bind_req, reserved, programmed, presented, host_ack,
  output logic [2:0] stage,     // 0 idle 1 reserve 2 program 3 present 4 active
  output logic       routed, visible_to_host, bound,
  output logic       unrouted_visible_err,
  output logic [7:0] n_bound, bind_cycles, max_bind
);
  assign routed = (st_q == PRES) || (st_q == ACT);
  // PRESENT_EARLY makes the device visible from the reserve stage, before any
  // routing exists for it.
  assign visible_to_host = (PRESENT_EARLY != 0) ? (st_q != IDLE)
                                                : ((st_q == PRES) || (st_q == ACT));
  // A host can see and address a device the fabric cannot route to.
  assign unrouted_visible_err = visible_to_host && !routed;
  assign bound = (st_q == ACT);
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      st_q <= IDLE; bc_q <= 8'd0; n_bound <= 8'd0; max_bind <= 8'd0;
    end else begin
      if (st_q != IDLE && st_q != ACT) begin
        bc_q <= bc_q + 8'd1;
        if (bc_q + 8'd1 > max_bind) max_bind <= bc_q + 8'd1;
      end
      case (st_q)
        IDLE: if (bind_req)   begin st_q <= RESV; bc_q <= 8'd0; end
        RESV: if (reserved)   st_q <= PROG;
        PROG: if (programmed) st_q <= PRES;
        // Both: the fabric offered it, and the host took it.
        PRES: if (presented && host_ack) begin
                st_q <= ACT; n_bound <= n_bound + 8'd1;
              end
        ACT:  ;
        default: st_q <= IDLE;
      endcase
    end
  end
endmodule

  bind    : visible correct=0 early build=1 | binds=1 longest bind=13

The whole section is one inequality: visible_to_host must never be true where routed is false. Everything else is machinery to make that hold.

The stages are checked against an oracle listing which of them may show the device to a host, and each transition is held open by the testbench to prove its guard is load-bearing. The presentation stage needs both presented and host_ack, and each half is driven alone to prove the other is required — a device presented that the host never acknowledged is not bound, and an acknowledgement of nothing presented is not either.

routed is asserted in the active stage as well as the presenting one. That sounds obvious and it is one of the mutations: routed true only in PRES leaves an active, visible, unroutable device — which is a fabric that delivered exactly one bind correctly and then forgot how.

6. RTL 2 — Unbinding Something That Is In Use

module unbind_drain #(parameter int REVOKE_FIRST = 0) (
  input  logic clk, rst_n,
  input  logic       unbind_req, host_released, drained,
  input  logic [3:0] in_flight,
  output logic [2:0] stage,      // 0 bound 1 notify 2 drain 3 revoke 4 free
  output logic       route_valid, may_revoke,
  output logic       stranded_err,
  output logic [7:0] n_unbound, n_stranded, drain_cycles, max_drain
);
  logic [2:0] st_q;
  logic [7:0] dc_q;
  localparam logic [2:0] BOUND=3'd0, NOTIFY=3'd1, DRAIN=3'd2, REVOKE=3'd3, FREE=3'd4;
  assign may_revoke  = (REVOKE_FIRST != 0) ? (st_q != BOUND) : (st_q == REVOKE);
  assign route_valid = !may_revoke && (st_q != FREE);
  // Transactions in flight with no route left to carry them.
  assign stranded_err = may_revoke && (in_flight != 4'd0);
  ...
        BOUND:  if (unbind_req) begin st_q <= NOTIFY; dc_q <= 8'd0; end
        // The host is told first, and must say it has stopped using it.
        NOTIFY: if (host_released) st_q <= DRAIN;
        DRAIN:  begin
                  if (drained && (in_flight == 4'd0)) st_q <= REVOKE;
                  else begin
                    dc_q <= dc_q + 8'd1;
                    if (dc_q + 8'd1 > max_drain) max_drain <= dc_q + 8'd1;
                  end
                end
        REVOKE: begin st_q <= FREE; n_unbound <= n_unbound + 8'd1; end
        FREE:   ;
        default: st_q <= BOUND;
      endcase

  unbind  : stranded correct=0 revoke-first build=9 | drain latched=8

Nine stranded cycles against zero, one parameter apart, on the same three in-flight transactions.

The unbind is not the bind reversed. The bind's first move is towards the fabric; the unbind's first move is towards the host, because the host is the only party that can stop generating new traffic. Reversing the bind literally — revoke, then unpresent, then unreserve — is exactly REVOKE_FIRST.

The drain condition has two halves, both driven alone to prove both are needed: the drained signal without an empty device does not end it, and an empty device without the signal does not either. One says the host believes it is finished; the other says the fabric is actually empty. Either alone is a different bug.

7. Waveform — Ten Cycles Of A Rebind

Transcribed from the printed trace. Both builds see one stimulus stream. This is the chapter's most important figure.

Read ns_own against dirty. The moment those two rows disagree — a new owner with an old tenant's data still present — is the entire failure, and it happens at cycle 6 with nothing else in the trace looking wrong.

8. RTL 3 — One Host At A Time

module bind_exclusive #(parameter int ALLOW_MULTI = 0) (
  input  logic clk, rst_n,
  input  logic       bind_ev, unbind_ev,
  input  logic [1:0] host_id, dev_id,
  output logic       accept,
  output logic [3:0] dev_bound_mask,
  output logic [1:0] owner0, owner1, owner2, owner3,
  output logic       double_bind_err, foreign_unbind_err,
  output logic [7:0] n_bound, n_refused, n_unbound
);
  logic [3:0] mask_q;
  logic [1:0] own_q [0:3];
  assign accept = bind_ev && (!mask_q[dev_id] || (ALLOW_MULTI != 0));
  assign double_bind_err = accept && mask_q[dev_id];
  // Only the host that holds a device may release it.
  assign foreign_unbind_err = unbind_ev && mask_q[dev_id]
                              && (own_q[dev_id] != host_id);
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      mask_q <= 4'd0;
      own_q[0] <= 2'd0; own_q[1] <= 2'd0; own_q[2] <= 2'd0; own_q[3] <= 2'd0;
      n_bound <= 8'd0; n_refused <= 8'd0; n_unbound <= 8'd0;
    end else begin
      if (accept) begin
        mask_q[dev_id] <= 1'b1;
        own_q[dev_id]  <= host_id;
        n_bound <= n_bound + 8'd1;
      end else if (bind_ev) n_refused <= n_refused + 8'd1;
      // Only the recorded owner releases it.
      if (unbind_ev && mask_q[dev_id] && (own_q[dev_id] == host_id)) begin
        mask_q[dev_id] <= 1'b0;
        n_unbound <= n_unbound + 8'd1;
      end
    end
  end
endmodule

  exclusive: double bind correct=0 multi build=1 | foreign unbind=1 refused=1

Two rules, and the second is the one that gets forgotten. Binding is guarded everywhere; unbinding is often not, and a host that can release a device it does not hold can take a device away from another host with one message.

The transcript shows the consequence of ALLOW_MULTI precisely: the correct build's device 2 still belongs to host 1, and the other build's owner2 has become host 3 — underneath host 1, which was told nothing and continues using it.

The lifecycle is driven all the way round: bind to host 1, refuse host 3, refuse host 3's release, accept host 1's release, then accept host 3's bind. A device that cannot be rebound after a legitimate release is a different bug that a shorter test never reaches.

9. RTL 4 — Telling A Host That Is Already Running

module hot_present #(parameter int NO_NOTIFY = 0) (
  input  logic clk, rst_n,
  input  logic       device_arrives, host_scans, host_maps,
  output logic       notify_host,
  output logic       in_fabric, in_host_map,
  output logic       invisible_capacity_err,
  output logic [7:0] n_arrived, n_mapped, unmapped_cycles, max_unmapped
);
  logic fab_q, map_q, notif_q;
  logic [7:0] un_q;
  // The notification is what makes a running host look again.
  assign notify_host = notif_q && (NO_NOTIFY == 0);
  // Present in the fabric, absent from the host's map: capacity that is
  // installed, powered, bound, and unusable.
  assign invisible_capacity_err = fab_q && !map_q;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      fab_q <= 1'b0; map_q <= 1'b0; notif_q <= 1'b0; un_q <= 8'd0;
      n_arrived <= 8'd0; n_mapped <= 8'd0; max_unmapped <= 8'd0;
    end else begin
      if (device_arrives) begin
        fab_q <= 1'b1; notif_q <= 1'b1;
        n_arrived <= n_arrived + 8'd1;
      end
      // The host maps it only if it looked, and it looks only if told.
      if (host_scans && (notify_host || host_maps) && fab_q) begin
        map_q <= 1'b1; notif_q <= 1'b0;   // one-shot
        if (!map_q) n_mapped <= n_mapped + 8'd1;
      end
      if (invisible_capacity_err) begin
        un_q <= un_q + 8'd1;
        if (un_q + 8'd1 > max_unmapped) max_unmapped <= un_q + 8'd1;
      end else un_q <= 8'd0;
    end
  end
endmodule

  hot-add : invisible=1 unmapped latched=3 mapped=1 | un-notified build invisible=1 for 41 cycles

Three cycles against forty-one and still counting. The un-notified host's interval does not end, because nothing will ever tell it to look — and the testbench asserts exactly that asymmetry by running both on for ten more cycles and checking one interval has closed and the other has not.

Three properties, each a mutation:

• The notification is one-shot. It is cleared when the host acts on it. A notification that stays asserted forever is a host that re-scans forever.
• A host cannot map a device that is not in the fabric. The testbench drives a scan before anything arrives.
• A host maps only if it was told. That is the whole mechanism; without the condition, the model quietly assumes hosts poll.

invisible_capacity_err names something that has no other name. The device is installed, powered, bound, and counted in every capacity report — and no workload can use a byte of it.

10. RTL 5 — A Bind That Fails Part-Way

// PARTIAL_UNDO: 0 = full undo, 1 = releases nothing, 2 = releases the
// reservation but leaves the routing programmed.
module bind_rollback #(parameter int PARTIAL_UNDO = 0) (
  input  logic clk, rst_n,
  input  logic       start, fail_ev,
  input  logic [2:0] fail_stage,     // 1 reserve 2 program 3 present
  input  logic       advance,
  output logic [2:0] stage,
  output logic       reservation_held, routing_held,
  output logic       leaked_reservation_err, leaked_routing_err,
  output logic [7:0] n_starts, n_failures, n_leaks
);
  logic [2:0] st_q;
  logic       res_q, rt_q;
  // Back at IDLE, nothing may still be held.
  assign leaked_reservation_err = (st_q == IDLE) && res_q;
  assign leaked_routing_err     = (st_q == IDLE) && rt_q;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      st_q <= IDLE; res_q <= 1'b0; rt_q <= 1'b0;
      n_starts <= 8'd0; n_failures <= 8'd0; n_leaks <= 8'd0;
    end else begin
      if ((st_q == IDLE) && start) begin
        st_q <= RESV; res_q <= 1'b1;
        n_starts <= n_starts + 8'd1;
      end else if (fail_ev && (st_q != IDLE)) begin
        st_q <= IDLE;
        if (PARTIAL_UNDO == 0) begin
          res_q <= 1'b0;
          rt_q  <= 1'b0;
        end else if (PARTIAL_UNDO == 2) begin
          res_q <= 1'b0;      // and the routing is forgotten
        end
        n_failures <= n_failures + 8'd1;
      end else if (advance) begin
        case (st_q)
          RESV: begin st_q <= PROG; end
          PROG: begin st_q <= PRES; rt_q <= 1'b1; end
          PRES: begin st_q <= ACT; end
          default: ;
        endcase
      end
      if (leaked_reservation_err || leaked_routing_err)
        n_leaks <= n_leaks + 8'd1;
    end
  end
endmodule

  rollback: leaks=0 of 2 failures | releases-nothing build resv=1 routing=1, resv-only build routing=1

Three builds, because two failure modes are not the same failure:

The third build exists because of a mutation. Counting the two leak monitors together — if (leaked_reservation_err || leaked_routing_err) — cannot be distinguished from counting only the first while every leaking build leaks both. A build that leaks only the routing is what makes the disjunction observable, and it is also the more realistic of the two bugs: releasing what you obviously took and forgetting what a later stage programmed.

Both monitors are gated on being back at IDLE, and the testbench samples reservation_held while the bind is still open to prove the gate is doing work. Holding a reservation during a bind is the point of a reservation; holding it afterwards is a leak.

11. RTL 6 — What The Previous Host Left Behind

module rebind_scrub #(parameter int NO_SCRUB = 0) (
  input  logic clk, rst_n,
  input  logic       write_ev, unbind_ev, scrub_step, bind_ev,
  input  logic [1:0] host_id,
  output logic [7:0] dirty_words,
  output logic       clean, scrub_done,
  output logic [1:0] last_owner, cur_owner,
  output logic       leak_err,
  output logic [7:0] n_binds, n_leaks, scrub_cycles, max_scrub
);
  logic [7:0] dirty_q, sc_q;
  logic [1:0] last_q, cur_q;
  logic       bound_q;
  assign clean      = (dirty_q == 8'd0);
  assign scrub_done = clean || (NO_SCRUB != 0);
  // Bound to a host that is not the one whose data is still in it.
  assign leak_err = bound_q && !clean && (cur_q != last_q);
  ...
      // Scrubbing only happens between bindings, and only if it is done.
      if (scrub_step && !bound_q && (dirty_q != 8'd0)) begin ... end
      if (write_ev && bound_q) begin
        dirty_q <= dirty_q + 8'd1;
        last_q  <= cur_q;
      end
      if (unbind_ev) begin bound_q <= 1'b0; sc_q <= 8'd0; end
      if (bind_ev && !bound_q && scrub_done) begin
        bound_q <= 1'b1; cur_q <= host_id;
        n_binds <= n_binds + 8'd1;
      end
      if (leak_err) n_leaks <= n_leaks + 8'd1;

  scrub   : 5 dirty words, scrub=5 cycles, leaks=0 | no-scrub build leaked host 1's data=1

The leak condition has three terms and every one of them is load-bearing:

• bound_q — an unbound device is exposed to nobody. The testbench drives the no-scrub build to a state where it is unbound while holding host 1's data and recorded as host 2's, and asserts its leak flag is low. Dangerous is not the same as leaking.
• !clean — a scrubbed device carries nothing.
• cur_q != last_q — a host rebinding a device it dirtied itself gets its own data back. That is not a leak, and a monitor without this term alarms on every re-acquisition.

Two guards make the transitions safe. Scrubbing happens only while unbound — a scrub running under a live host is erasing data in use. And a bind requires scrub_done, which is what the correct build uses to refuse host 2 at cycle 5 of Figure 3.

12. RTL 7 — Binding Part Of A Device

module partial_bind #(parameter int NO_OVERLAP_CHECK = 0) (
  input  logic clk, rst_n,
  input  logic       req,
  input  logic [7:0] base, size,
  input  logic [1:0] host_id,
  output logic       accept,
  output logic [7:0] allocated, free_left,
  output logic       overlap_err, oversize_err,
  output logic [7:0] n_accepted, n_refused, peak_alloc
);
  logic [7:0] alloc_q;
  logic [8:0] top;          // nine bits: base + size must not wrap
  logic       fits, overlaps;
  assign allocated = alloc_q;
  assign free_left = CAPACITY - alloc_q;
  localparam logic [7:0] CAPACITY = 8'd64;
  assign top = {1'b0, base} + {1'b0, size};
  // A slice must start where the last one ended and must fit in the device.
  assign overlaps = (base < alloc_q);
  assign fits     = (top <= {1'b0, CAPACITY});
  assign accept = req && fits && (!overlaps || (NO_OVERLAP_CHECK != 0));
  assign overlap_err  = accept && overlaps;
  assign oversize_err = req && !fits;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      alloc_q <= 8'd0; n_accepted <= 8'd0; n_refused <= 8'd0; peak_alloc <= 8'd0;
    end else if (req) begin
      if (accept) begin
        alloc_q <= top[7:0];
        n_accepted <= n_accepted + 8'd1;
        if (top[7:0] > peak_alloc) peak_alloc <= top[7:0];
      end else n_refused <= n_refused + 8'd1;
    end
  end
endmodule

  slices  : 32 allocated of 64, 3 accepted 2 refused | no-check build overlapped=1

Two refusals for two different reasons, and keeping them apart is the point:

• Overlap — the slice starts inside what is already allocated. Two hosts writing one address, which is section 8's exclusivity failure at sub-device granularity.
• Oversize — the slice runs past the end of the device. The request is arithmetically impossible, and it is nobody's ownership problem.

Both boundaries are driven exactly: a slice starting precisely where the last ended is accepted (<, not <=), and a slice exactly filling the device is accepted (<=, not <). One off in either direction refuses a request that is exactly right, and the two errors look identical from outside.

The top intermediate is nine bits wide. base + size on eight-bit operands wraps, and a wrapped sum is smaller than the capacity — so an oversize request passes the fit test by overflowing it.

13. RTL 8 — What Binding Costs

module bind_cost (
  input  logic clk, rst_n,
  input  logic        bound_done, unbound_done, rebound,
  input  logic [7:0]  bind_cycles, unbind_cycles, scrub_cycles,
  input  logic        in_use_cycle,
  output logic [15:0] n_binds, n_unbinds, n_rebinds, total_transition, n_in_use,
  output logic [7:0]  mean_bind, transition_pct, rebind_pct
);
  logic [31:0] weighted_tr, weighted_rb;
  logic [15:0] bind_total;
  assign life = total_transition + n_in_use;
  assign weighted_tr = {16'd0, total_transition} * 32'd100;
  // The share of a device's life spent NOT serving anybody.
  assign transition_pct = (life == 16'd0) ? 8'd0
                        : (weighted_tr / {16'd0, life});
  assign rebind_pct = (n_binds == 16'd0) ? 8'd0
                    : (weighted_rb / {16'd0, n_binds});
  assign mean_bind = (n_binds == 16'd0) ? 8'd0 : (bind_total / n_binds);
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      n_binds <= 16'd0; n_unbinds <= 16'd0; n_rebinds <= 16'd0;
      total_transition <= 16'd0; n_in_use <= 16'd0; bind_total <= 16'd0;
    end else begin
      if (bound_done) begin
        n_binds    <= n_binds + 16'd1;
        bind_total <= bind_total + {8'd0, bind_cycles};
        total_transition <= total_transition + {8'd0, bind_cycles};
      end
      if (unbound_done) begin
        n_unbinds <= n_unbinds + 16'd1;
        // The scrub is part of the cost of moving a device between tenants.
        total_transition <= total_transition
                          + {8'd0, unbind_cycles} + {8'd0, scrub_cycles};
      end
      if (rebound)      n_rebinds <= n_rebinds + 16'd1;
      if (in_use_cycle) n_in_use  <= n_in_use + 16'd1;
    end
  end
endmodule

  cost    : mean bind=8, transition=20% of life, rebinds=50% of binds

20 percent of a device's life spent not serving anybody. That is the number composability actually costs, and it is invisible in any per-operation measurement — a bind averaging eight cycles sounds cheap until you count how much of the device's existence is binds.

The unbind cost deliberately includes the scrub. Section 11 is not free, and a cost model that charges the drain but not the scrub understates the price of moving a device between tenants by most of it. That is one of the mutations, and it is exactly the accounting mistake a real system makes.

rebind_pct at 50 percent says half the binds were of a device that had been bound before. High churn with a high transition share is a pool that is thrashing: the devices spend their time changing hands rather than working.

14. RTL 9 — The Bind Table, And A Decision Computed Against An Old View

module bind_table #(parameter int NO_CAS = 0) (
  input  logic clk, rst_n,
  input  logic       apply_req,
  input  logic [3:0] req_gen,        // the generation the requester read
  input  logic [1:0] dev_id, host_id,
  input  logic       external_change,
  output logic [3:0] generation,
  output logic       apply_ok,
  output logic       lost_update_err,
  output logic [7:0] n_applied, n_rejected, n_lost, max_gen_gap
);
  logic [3:0] gen_q;
  assign generation = gen_q;
  assign gap = gen_q - req_gen;
  // Compare-and-swap: a request computed against an older view of the table
  // is refused, not applied on top of whatever happened since.
  assign apply_ok = apply_req && ((req_gen == gen_q) || (NO_CAS != 0));
  assign lost_update_err = apply_ok && (req_gen != gen_q);
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      gen_q <= 4'd0;
      n_applied <= 8'd0; n_rejected <= 8'd0; n_lost <= 8'd0; max_gen_gap <= 8'd0;
    end else begin
      if (external_change) gen_q <= gen_q + 4'd1;
      else if (apply_ok)   gen_q <= gen_q + 4'd1;
      if (apply_req) begin
        if (apply_ok) n_applied  <= n_applied + 8'd1;
        else          n_rejected <= n_rejected + 8'd1;
        if (req_gen != gen_q) begin
          if ({4'd0, gap} > max_gen_gap) max_gen_gap <= {4'd0, gap};
        end
      end
      if (lost_update_err) n_lost <= n_lost + 8'd1;
    end
  end
endmodule

  table   : gen=5 applied=2 refused=2 worst gap=3 | no-CAS build lost an update=1

This is 15.3 section 14's generation with teeth. There, a stale read was reported. Here, a stale request is refused — because a binding decision computed against an old table and applied anyway silently overwrites whatever happened since.

The transcript's worst gap=3 is the same distinction as in 15.3: one generation behind is a race, three is a component that computed a plan and never re-checked it before acting.

The correct response to a refusal is to re-read and recompute, and the testbench does exactly that: the requester refreshes its generation and the retry applies. A compare-and-swap that only refuses, with no path forward, is a system that livelocks under churn.

15. RTL 10 — Allocation Assembled

module alloc_top #(parameter int SKIP_SCRUB = 0) (
  input  logic clk, rst_n,
  input  logic       request, bound_ok, presented_ok, release_req,
  input  logic       drained_ok, scrubbed_ok,
  output logic [2:0] phase,   // 0 free 1 binding 2 presenting 3 in use
                              // 4 draining 5 scrubbing
  output logic       usable, dirty,
  output logic       unsafe_reuse_err,
  output logic [7:0] n_cycles_served, n_allocations,
                     transition_cycles, max_transition
);
  assign usable = (ph_q == INUSE);
  // The invariant: a device returned to the pool still holding the last
  // tenant's data is a device the next allocation will hand it to.
  assign unsafe_reuse_err = (ph_q == FREE) && dirty_q;
  ...
      if ((ph_q != FREE) && (ph_q != INUSE)) begin
        tr_q <= tr_q + 8'd1;                    // transition, not service
        if (tr_q + 8'd1 > max_transition) max_transition <= tr_q + 8'd1;
      end
      if (ph_q == INUSE) begin
        n_cycles_served <= n_cycles_served + 8'd1;
        dirty_q <= 1'b1;
      end
      case (ph_q)
        FREE:       if (request) begin ph_q <= BINDING; tr_q <= 8'd0; end
        BINDING:    if (bound_ok)     ph_q <= PRESENTING;
        PRESENTING: if (presented_ok) begin
                      ph_q <= INUSE; n_allocations <= n_allocations + 8'd1;
                    end
        INUSE:      if (release_req)  ph_q <= DRAINING;
        DRAINING:   if (drained_ok) begin
                      // SKIP_SCRUB returns the device to the pool without it.
                      if (SKIP_SCRUB != 0) ph_q <= FREE;
                      else                 ph_q <= SCRUBBING;
                    end
        SCRUBBING:  if (scrubbed_ok) begin ph_q <= FREE; dirty_q <= 1'b0; end
        default:    ph_q <= FREE;
      endcase

  assembled: served=13 transition latched=12 | skip-scrub build returned it dirty=1

Thirteen cycles of service, twelve of transition. Nearly half of this device's round trip was overhead — and that is with a three-cycle scrub.

The invariant is stated where it can be checked: at FREE, the device must be clean. SKIP_SCRUB reaches FREE with dirty still set, and the transcript catches it in the cycle it happens. The correct build has not returned the device at all yet, which is the honest comparison — the fast build is fast because it skipped the step.

The transition counter excludes time in use, and the testbench asserts it does not advance during the twelve service cycles. A transition counter that runs while the device is working reports every device as pure overhead and the metric becomes meaningless.

16. Quantitative Reasoning

Three worth a sentence.

0 stranded against 9. Same three transactions, same unbind, one parameter. The difference is entirely the order of notify and revoke.

3 cycles against 41. The un-notified host's capacity is not slow to arrive; it never arrives. The counter is still climbing when the run ends.

13 served against 12 in transition. Roughly half of this device's round trip was overhead, and section 11's scrub is a third of that. Composability is not free and this is the number that says how expensive.

17. Assertions

Every property is an immediate check written as cond !== 1'b1, sampled after a settle.

18. Mutation Testing

120 mutations, one at a time, each required to make the baseline print RESULT: FAIL.

120 of 120 were killed.

The first run killed 103 and left 17 survivors:

The first row is the pattern of this chapter. Six mutations lived in conditions of the form A && B where the testbench only ever drove both together: presented && host_ack, drained && in_flight == 0, host_scans && notified && in_fabric. Each looked thoroughly tested and each had a half nothing had ever exercised alone.

The last row produced a genuine design change. Counting the two rollback leak monitors together is indistinguishable from counting only the reservation, as long as every faulty build leaks both. Making the disjunction observable required a third build that leaks only the routing — and that build is the more realistic bug of the two.

A representative sample:

19. Verification Strategy

Parameterised builds — and this chapter needed three of one. PRESENT_EARLY, REVOKE_FIRST, ALLOW_MULTI, NO_NOTIFY, PARTIAL_UNDO (three values), NO_SCRUB, NO_OVERLAP_CHECK, NO_CAS, SKIP_SCRUB. A boolean parameter expresses one failure; when a monitor is a disjunction, one failure is not enough.

Every half of every compound condition, driven alone. Six mutations lived here. presented without host_ack and the reverse; drained without an empty device and the reverse; a scan without a notification and a notification without a device.

Guarded monitors sampled where they must be quiet. leaked_reservation_err is sampled while the bind is still open — a held reservation mid-bind is the reservation working. leak_err is sampled on an unbound dirty device with mismatched owners — dangerous is not the same as exposed.

The full lifecycle, not the happy path. Bind, refuse a second host, refuse a foreign release, accept the owner's release, rebind elsewhere. A device that cannot be rebound after a legitimate release is a bug no shorter test reaches.

Boundaries driven exactly. A slice starting precisely where the last ended. A slice exactly filling the device. A generation exactly equal.

Width discipline. top is nine bits, because an eight-bit base + size wraps — and a wrapped sum passes a fit test by being smaller than the capacity.

Delta discipline. Every combinational sample follows a settle, and the interval counters are sampled a cycle after the condition clears, because they clear on the following edge.

20. Synthesis and Implementation Reality

The state machines are trivial and they are the part that is real. Four and five states, a handful of flops each. bind_fsm and unbind_drain are smaller than a FIFO pointer pair, and they encode the whole ordering argument of this chapter.

The exclusion table is a small memory. One owner id per device, one valid bit. In a real fabric it is hundreds of entries in the manager's memory, not in a switch.

The scrub is the only expensive thing here, and it is the one that must not be optional. One cycle per dirty word is the model's fiction; in silicon it is a memory-bandwidth-bound operation across the whole bound region, and it dominates section 13's transition share completely. That is precisely why it gets skipped, and precisely why unsafe_reuse_err has to be a checkable state rather than a procedure someone follows.

Where the scrub actually happens is a design decision this chapter does not make. It can be the device (a background erase), the manager (writes across the region), or a memory-controller feature. What section 11 fixes is the ordering constraint: unbound before scrubbing, scrubbed before rebinding. Where the cycles are spent is an implementation choice; that they are spent before the next bind is not.

The compare-and-swap is one comparator and it is the difference between a bind table that can be updated concurrently and one that requires a global lock.

The divisions are firmware. Every percentage here is computed by the manager reading raw counters.

The counter widths are the model's. Eight bits survives a testbench. n_cycles_served on a real device needs to survive months.

21. Silicon Observability

Three to alarm on, and one of them is not like the others.

unsafe_reuse_err non-zero at all is the one to page someone about. Every other counter here describes a fabric working badly; this one describes a fabric that has handed one tenant's memory contents to another. It should be zero for the life of the system.

n_stranded non-zero means routing was torn down under live traffic. The transactions are already lost by the time it fires, and the fix is ordering, not retry.

transition_pct rising with rebind_pct high is a pool thrashing: devices spending their lives changing hands. That is an allocation-policy signal produced by the binding mechanism — 12.2 is where it gets acted on.

22. Debug Lab

22.1 A host sees a device and cannot reach it

Symptom. A newly bound device appears in the host's map. Accesses to it fail or time out.

The reading. unrouted_visible_err and the bind stage at which the host was told.

The diagnosis. The device was presented before its routing was programmed. The host is doing exactly the right thing with an address the fabric has no path for.

Why it is worth a counter rather than an investigation. From the host's side this is indistinguishable from a broken device. From the fabric's side, nothing is wrong — there is no routing to fail. Only a check that spans both, which is what visible_to_host && !routed is, sees it at all.

22.2 Transactions vanish when a device is removed

Symptom. A device is unbound administratively. Some in-flight transactions never complete.

The reading. n_stranded and the unbind stage sequence.

The diagnosis. The routing was revoked before the drain finished. If n_stranded is non-zero, the count is how many cycles the fabric spent with traffic in flight and no route for it.

The sub-case that matters. If n_stranded is zero and transactions still vanished, the unbind ordering is correct and the problem is elsewhere — the host said it had released the device before it actually had, which is a host-side bug that the host_released handshake makes visible rather than causing.

22.3 Capacity was allocated and the workload cannot see it

Symptom. The manager reports a device bound to a host. The host's memory map does not include it. Capacity reports count it.

The reading. max_unmapped, and whether it is still climbing.

The diagnosis. The host was never told, or was told and did not act. A closed interval means the host eventually mapped it and the delay is a latency problem; an interval still climbing means it never will, and the capacity is permanently invisible.

The trap. Every fabric-side measurement says this is working. The device is present, bound, powered and healthy. Only a check that compares the fabric's view against the host's map — which is what in_fabric && !in_host_map is — disagrees.

22.4 A device cannot be bound and nothing holds it

Symptom. A device is reported as unavailable. No host has it. Unbinding it does nothing because it is not bound.

The reading. The rollback leak counters, and which of the two fired.

The second row is the subtle one, and it does not present as this symptom at all — the device binds fine. It presents later, as routing entries that accumulate and eventually exhaust a switch's table, with no failed bind anywhere near it in time.

23. Design Review

1. In which stage does the host first learn about the device, and is the routing programmed before that stage? If not, hosts get addresses the fabric cannot reach.

2. Does an unbind notify the host before revoking anything? Reversing the bind literally is the failure.

3. What ends the drain — the host saying it has stopped, or the fabric being empty? Both. Either alone is a distinct bug.

4. Can a host release a device it does not hold? Binding is always guarded; unbinding often is not.

5. How does a running host learn a device has appeared, and is the notification one-shot? Never told, and told forever, are both failures.

6. For a bind that fails at each stage, exactly what must be released? Enumerate it per stage. The answer differs, and the incomplete undo is silent.

7. Is a device scrubbed between tenants, and is the scrub required before the next bind or merely scheduled? Required, as a state the bind checks.

8. Where does the scrub happen and what does it cost? It is the dominant term in the transition share, which is why it is the step under pressure.

9. Can a partial binding overlap another, and are overlap and oversize reported separately? They are different failures with different fixes.

10. Is a binding decision re-validated against the bind table's generation at the moment it is applied? And when refused, is there a recompute path, or does the system livelock under churn?

24. How This Appears In Real Engineering

The bind order is settled early and is nearly free to get right. Reserve, program, present. Getting it wrong produces a failure that looks like broken hardware from the host's side, and teams spend a long time on the device.

Unbind is written second and gets less attention. It is "the bind backwards" until the first time a device is removed under load, and then the ordering argument in section 6 has to be made from an incident report instead of a design review.

The hot-add notification lives in a different team's code. The fabric side is complete; the host has to act on a hotplug event. Section 9's forty-one cycles are what happens when that integration is assumed rather than tested, and the capacity is invisible while every dashboard counts it.

The scrub is the step that gets deferred, then made asynchronous, then skipped. It is the single most expensive operation in the sequence, it delays every rebind, and skipping it is invisible in every test that does not deliberately look for one tenant's data in another's memory. Making it a state the bind checks rather than a step in a runbook is the difference.

Partial binding arrives late and breaks the exclusion model. Whole-device binding needs one owner field. Slices need arithmetic, and the arithmetic is where two hosts end up writing one address.

Compare-and-swap on the bind table is added after the first concurrent-manager incident, for the same reason 15.3's generation counter is.

25. Common Misconceptions

"Binding is a table write." It is a four-stage transaction against a live host with a stage-dependent undo. The table write is the last thing that happens, not the thing that happens.

"Unbinding is binding in reverse." The bind's first move is towards the fabric; the unbind's first move is towards the host, because only the host can stop generating traffic. Reversing it literally is REVOKE_FIRST, and it stranded nine cycles of traffic on three transactions.

"Two hosts on one device is a sharing configuration." They have no protocol between them. Each believes it owns the device, and in section 8's multi-bind build the owner changed underneath host 1, which was told nothing.

"The host will notice the new device." A running host does not re-enumerate spontaneously. Un-notified, section 9's host never mapped it at all, while every capacity report counted it.

"A failed bind cleans up after itself." Only if the undo matches the stage it failed at. One build released nothing; another released the reservation and left routing programmed for a bind that never happened — and the second does not present as a failure at all until a switch table fills up.

"Coherency protects tenants from each other." Not here. The device is unbound from host 1 and bound to host 2 with host 1's data still in it. No coherency rule is violated; there is no shared line and no concurrent access. It is a lifecycle problem, and only a lifecycle check catches it.

"The scrub can happen in the background." It can happen wherever you like, as long as the next bind cannot complete until it is done. scrub_done gating bind_ev is what makes it safe; scheduling it is what makes it skippable.

"A device that is dirty and unbound is leaking." It is dangerous, not leaking. leak_err requires bound_q, and a monitor without that term alarms on every device between tenants — which is all of them, briefly.

26. Interview Reasoning

Q1. Why does the bind have an order at all? Because each step makes something true that the next step depends on. Presenting before the routing is programmed gives the host an address the fabric has no path for.

Q2. Which step must be last, and why? Telling the host. Everything before it exists so that when the host hears about the device, everything needed to reach it is already true.

Q3. Why does presentation require both a presented signal and a host acknowledgement? They are different facts: the fabric offered the device, and the host took it. A bind completing on either alone produces a binding one side does not know about.

Q4. Is the unbind the bind reversed? No. The bind starts at the fabric; the unbind starts at the host, because the host is the only party that can stop producing new traffic. Reversing it literally revokes routing under live transactions.

Q5. What ends the drain? Two conditions: the host has released the device, and the fabric is empty. The first is a claim about intent; the second is a fact about state, and either alone is a distinct bug.

Q6. Nine stranded cycles on three transactions. What does the number mean? Cycles during which routing was gone and traffic was still in flight. It is not three lost transactions — it is a window in which any transaction would have been lost, which is the more useful thing to bound.

Q7. Why is a foreign unbind worth its own check? Because binding is always guarded and unbinding often is not. A host that can release a device it does not hold can take a device from another host with one message.

Q8. A running host does not see a newly bound device. Whose bug? Read max_unmapped. If it closed, the host eventually mapped it and the delay is a latency question. If it is still climbing, the host was never told, or never acted, and the capacity is permanently invisible while every report counts it.

Q9. Why must the hot-add notification be one-shot? A notification that stays asserted is a host that re-scans forever. Clearing it when the host acts is what makes it an event rather than a state.

Q10. A bind fails. What must be released? Whatever had been taken by the stage it reached. That differs per stage, and it is why one undo path for all failures is wrong in one direction or the other.

Q11. What are the two ways an undo goes wrong? Releasing nothing — the state machine resets and the device stays reserved with routing programmed. Or releasing only what is obvious, leaving the routing behind.

Q12. Which is worse? The second, because it does not present as a failure. The device binds fine next time. The routing entries accumulate and eventually exhaust a switch table, with no failed bind anywhere near it in time.

Q13. Why must the leak monitors be gated on being back at IDLE? A held reservation during a bind is the reservation doing its job. It is a leak only after the transaction has ended.

Q14. A device moves from host 1 to host 2. What has to happen in between? It has to be scrubbed, and the next bind must not be able to complete until it has been. Otherwise host 2 gets host 1's data.

Q15. Why is that not a coherency problem? There is no shared line and no concurrent access. Host 1 is gone. No coherency rule is violated by handing a clean-looking device to host 2 with the old contents intact — it is a lifecycle constraint that the coherency layer never sees.

Q16. What are the three terms in the leak condition, and why each? Bound — an unbound device is exposed to nobody. Not clean — a scrubbed device carries nothing. And the current owner differing from the last writer — a host getting its own data back is not a leak.

Q17. What breaks if you drop the third term? The monitor alarms on every re-acquisition by the same host, which is common, and it gets disabled.

Q18. Why must a scrub happen only while unbound? A scrub running under a live host is erasing data in use. The device has to be released first, which is why the scrub is inside the unbind-to-rebind gap rather than at either end of it.

Q19. The scrub is expensive. How do you make it not skippable? Make it a state the bind checks, not a step in a procedure. scrub_done gating the bind is structural; scheduling a scrub is a convention that erodes.

Q20. Two slices, one starting where the last ended. Overlap? No. < not <=. One off refuses a request that is exactly right, and it looks identical from outside to a genuine overlap.

Q21. Why report overlap and oversize separately? Overlap is two hosts writing one address — an ownership failure. Oversize is arithmetic that cannot be satisfied by anyone. Different causes, different fixes.

Q22. Why is the slice sum computed in nine bits? Because an eight-bit base + size wraps, and a wrapped sum is smaller than the capacity — so an oversize request passes the fit test by overflowing it.

Q23. What does a 20 percent transition share tell you? That a fifth of the device's life was spent not serving anybody. It is the cost of composability, and no per-operation measurement shows it.

Q24. Why must the unbind cost include the scrub? Because the device is unavailable throughout it. A cost model charging the drain but not the scrub understates the price of moving a device between tenants by most of it.

Q25. High rebind percentage and high transition share together — what does that say? The pool is thrashing. Devices are spending their lives changing hands rather than working, and that is an allocation-policy signal produced by the binding mechanism.

Q26. Why does the bind table need compare-and-swap and not just a generation? 15.3's generation reports a stale read. Here a stale request would be applied, silently overwriting whatever happened since. Reporting is not enough when the read leads to a write.

Q27. A request is refused for staleness. What should the requester do? Re-read and recompute. A compare-and-swap that only refuses, with no path forward, livelocks under churn — and the testbench drives the refresh-and-retry to prove there is one.

Q28. What is the assembled machine's invariant, and where is it checked? At FREE, the device must be clean. It is checked in the free state itself, because that is the state the next allocation draws from.

Q29. Why must the transition counter exclude time in use? Otherwise every device reports as pure overhead and the metric says nothing. The testbench asserts it does not advance across twelve service cycles.

Q30. Of everything in this chapter, which failure would you check for first in a live system? unsafe_reuse_err. Every other counter describes a fabric working badly. That one describes a fabric that has handed one tenant's memory to another, and it should be zero for the life of the system.

27. Exercises

1. Add a stage to bind_fsm for capability negotiation between programming and presenting. Decide what a failure there must release, and extend bind_rollback to match.

2. Give unbind_drain a drain timeout. Decide what happens when it expires — revoke anyway, or refuse the unbind — and measure what each leaves behind.

3. Extend bind_exclusive to allow a device to be bound to two hosts with a protocol between them. Show precisely which check you have to remove and what has to replace it.

4. Make hot_present handle a device that arrives and departs before the host scans. Show what the host must be told, and whether the notification can simply be cancelled.

5. Add a fourth PARTIAL_UNDO mode that releases the routing but not the reservation. Predict which leak monitors fire before you run it.

6. Change rebind_scrub so the scrub runs in the background and the bind waits on a completion flag. Show that the leak is still impossible, and identify the new race you have introduced.

7. Extend partial_bind to free a slice in the middle, creating a hole. Show that the single alloc_q pointer can no longer express the state, and say what has to replace it.

8. Take the 120-mutation suite and drive presented and host_ack only together. Confirm both mutations return, and find every other compound condition in the batch with the same weakness.

28. Summary

Binding is an ordered, reversible transaction against a live host, ending in a device that is exclusively owned, visible, routed, and clean.

• Ordered: the host is told last, and the present-early build produced a device a host could address and the fabric could not reach.
• Reversible: three undo behaviours, one correct — and the failure that leaks only the routing does not present as a failure at all until a switch table fills up.
• Live: notify, drain, revoke. Reversed, it stranded nine cycles of traffic on three transactions. And a host that is never told about a new device leaves capacity installed, bound, counted, and unusable — 41 cycles and still climbing.
• Exclusive: the multi-bind build changed a device's owner underneath the host that held it.
• Clean: five dirty words, a five-cycle scrub, and a build that skipped it handed host 1's data to host 2 for four consecutive cycles with nothing else in the trace looking wrong.

The cost, measured: 13 cycles of service against 12 of transition, and 20 percent of a device's life spent not serving anybody. That is what composability costs, and the scrub is the largest single part of it — which is exactly why it is the step under pressure, and exactly why it has to be a state the bind checks rather than a step in a runbook.

120 mutations, 120 killed. Six of the seventeen first-run survivors were halves of compound conditions that had never been driven alone, in guards that read as fully covered. A conjunction needs each half falsified; a disjunction needs each disjunct alone.

15.5 asks what a datacentre built on all of this actually requires of the hardware.