From f81a53cbf6f80eb492b404f3186d59c313513b4b Mon Sep 17 00:00:00 2001 From: Robert Allan James Date: Tue, 4 Aug 2026 08:02:52 -0400 Subject: [PATCH] FABRIC.md: resolve item 1.1 -- containment, not a lock MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Punch list §25 item 1.1 complete. Adds the ninth wire `contains` to §3, resolves §8's open exclusivity question as containment with a gated reap rule, bounds chain depth at 5 (Kconfig-tunable), and notes the distinction from item 1.7's separate VM-tree-recursion question. Co-Authored-By: Claude Sonnet 5 --- FABRIC.md | 84 ++++++++++++++++++++++++++++++++++++++++++++++--------- 1 file changed, 71 insertions(+), 13 deletions(-) diff --git a/FABRIC.md b/FABRIC.md index afa8555..7fb999a 100644 --- a/FABRIC.md +++ b/FABRIC.md @@ -97,6 +97,7 @@ One structure. No variants, no type field, no subclassing. | code field | behaviour tag from a closed enumeration (§18.3) | | **mass** | **cells this patron occupies — its footprint (§19.2)** | | payload | carried in the patron's own cells; large patrons are simply heavy (§23.1) | +| **contains** | **index of the patron currently held inside this one, or none — containment, not a lock (§8, item 1.1)** | Fixed-size cells. Links are indices, so the Stadium stays an array — no fragmentation, and tractable for Isabelle later. @@ -130,6 +131,13 @@ never reaped and never dispatched — it is floor space, accounted for in its ow > payload rule ("inline if small, by reference if large") was dissolved rather than > answered: a large patron occupies more cells, which is what mass already measures. > By-reference is reserved for things outside the Stadium, which are not patrons. +> +> **Amended again by item 1.1 (§25.2).** `contains` is a ninth wire — an index to the +> patron currently held inside this one, or none. This does not reopen the two-valued cell +> union above: the contained patron keeps its own independent header and cells elsewhere in +> the Stadium, resolved and ranked exactly as any other patron. `contains` is a reference to +> that residency, not a physical embedding of one patron's cells inside another's. See §8 for +> what this wire is for and why it replaced a lock. **The code field is the entire type system.** A block's code field migrates. A message's delivers. A VM's ticks. The engine never asks what kind of thing it is holding; it @@ -261,15 +269,46 @@ field re-entering through a metaphor. They are one entry shape differing only in code field — a car's lifetime is the show, a person's is a visit; a car's code field is *be attended to*, a person's is *move and attend*. -> **OPEN — the one thing in this section the design has not addressed.** *"Occasionally one -> sits in a car, which is the only exclusive thing in the room, scoped to a single object, -> no global lock."* That sentence asserts an exclusivity primitive: per-patron, not global. -> Nothing in §16–24 defines it. §21 addresses ISR-versus-mainline concurrency, which is a -> different question. +> **RESOLVED by item 1.1 (§25.2), 2026-08-04.** *"Occasionally one sits in a car, which is +> the only exclusive thing in the room, scoped to a single object, no global lock."* The +> instinct that this needs an exclusivity primitive was right; the instinct that it needs a +> **lock** was not. Sitting in a car is not mutual exclusion — it is **containment**. The +> person-patron does not get barred from the car-patron; it goes **inside** it. > -> It matters because a patron reaped while someone is "sitting in" it is a use-after-free -> under another name, and §22.3 gave up physical fault containment, which raises the stakes -> rather than lowering them. Tracked as a punch-list item in §25. +> **The mechanism is the ninth wire, `contains`** (§3): an index to the patron currently held +> inside this one, or none. Getting in sets it; getting out clears it. The contained patron +> keeps its own independent header and residency — it is still ranked, still heats and cools +> like anything else — `contains` only records the relationship. +> +> **Reap is gated, not derived.** A patron with a non-none `contains` link cannot be reaped. +> This is checked ahead of density ranking, as an absolute rule, not inferred from mass or +> density — a light, cold container with something inside it must not read as evictable just +> because the numbers say so. This is what actually answers the use-after-free concern §9 +> raised: the engine cannot select an occupied patron for reaping in the first place. +> +> **Containment chains, and unwinding is forced, not chosen.** Because a patron can itself be +> contained, `contains` links can form a chain — a patron inside a patron inside a patron. +> If A contains B contains C, A cannot become reapable until B is empty, and B cannot become +> reapable until C departs. This ordering is **topological, not a policy** — there is no +> FIFO/LIFO choice to make here; the chain's own shape forces innermost-first. +> +> **Bounded, single occupant per level.** Each patron holds at most one `contains` link +> (single occupant, not a set). Chain depth is capped — **default 5** — enforced by the +> engine at containment-entry time (refuse to nest past the cap). The cap is a **Kconfig +> symbol**, not a hardcoded constant, consistent with this project's existing tunable-knob +> convention (`STARFORTH_ENABLE_VM`, `HOTWORDS_CACHE_SIZE`, etc.) — named at implementation +> time in item 3.1, default 5, scannable via `menuconfig`. +> +> **What this leaves genuinely open, deferred, not blocking:** if multiple independent +> containment chains are simultaneously blocked and waiting to unwind, whether the engine +> gives any of them priority over another is a scheduling question, not a header-design one. +> It does not affect the wire, the reap gate, or the depth cap, and is left for whenever it +> becomes a real concern. +> +> §22.3's earlier remark that separate-region layout gives "physical fault containment" that +> the single-cell-pool layout gave up is unaffected by this — `contains` is a logical +> reference within one VM's own Stadium, the same trust boundary that layout decision already +> accepted. --- @@ -1434,7 +1473,11 @@ decides where work goes; that remains capability-based routing. 4. **Does the nesting recurse further?** A VM's Stadium holds patrons; if one of those patrons were itself a VM, the structure is a tree rather than two levels. Nothing currently requires this, and §11 would call it speculative generality — but it should be - ruled out deliberately, since the boot order in §6 does not forbid it. + ruled out deliberately, since the boot order in §6 does not forbid it. Still open as + item 1.7. **Not the same question as §8's `contains` chains (item 1.1, resolved)** — those + are same-Stadium patron-holds-patron relationships, bounded to depth 5, and do not create + a second Stadium. This item is specifically about a patron *being* a VM with its own + nested Stadium underneath it. --- @@ -1762,9 +1805,12 @@ These are numbers to check against a real build, not derived truths. The four reserved bytes are deliberate rather than a rounding artefact. The fields above sum to 28; padding to 32 keeps the header a clean half-cell, leaves room for the -header/continuation discriminator §3 now requires, and gives the exclusivity primitive of -§8 somewhere to live if item 1.1 resolves to a holder index. Reserved space in a header that -is expected to grow is cheaper than repacking one later. +header/continuation discriminator §3 now requires, and gives the `contains` wire item 1.1 +resolved to somewhere to live. Whether 4 bytes actually covers `contains` at whatever width +gets chosen (it is an index, the same kind of quantity as `link`, currently sized at 4 bytes +itself) is exactly the kind of thing item 3.1's real byte count settles, not this section — +flagged here rather than assumed. Reserved space in a header that is expected to grow is +cheaper than repacking one later. 256 KB per VM is comfortable against QEMU's `-m 1024`, and the outer Stadium's capacity (§20.5 #1) then follows from how many VMs the machine is willing to host. @@ -2189,7 +2235,7 @@ on until there is a tick on all three architectures (§16.1, §16.5).* *These need answers, not code. Each one is settled by amending the relevant section of this document and committing that amendment as its own item.* -- [ ] **1.1 — Exclusive access ("sitting in a car").** §8 asserts a per-patron exclusivity +- [x] **1.1 — Exclusive access ("sitting in a car").** §8 asserts a per-patron exclusivity primitive that is not a global lock. Nothing defines it. Decide what it is, what it blocks, and what happens if a patron is selected for reaping while held. *Refs:* §8. **This is the largest unresolved design question.** @@ -2205,6 +2251,18 @@ document and committing that amendment as its own item.* > quietly reordered later by someone who does not know what it was holding up. §23.3 > reserves 4 header bytes partly against this outcome. + > **RESOLVED 2026-08-04 — containment, not a lock.** A ninth wire, `contains` (§3): an + > index to the patron currently held inside this one, or none. Reap is **gated**, not + > density-derived — a patron with a non-none `contains` link cannot be reaped, full stop. + > Chains up to a depth cap, **default 5, exposed as a Kconfig symbol** (named at + > implementation time in item 3.1) rather than hardcoded — this project's existing + > tunable-knob convention. Unwinding is innermost-first, forced by the chain's own + > topology, not a policy choice — no FIFO/LIFO decision exists to make. Single occupant per + > level. Full argument in §8. **Same-Stadium relationship** — distinct from item 1.7's + > VM-tree-recursion question (§20.5 #4), which this does not resolve and remains open. + > Item 3.1 is now unblocked on this item; the ninth wire and the reserved header bytes + > (§23.3) are the concrete carry-forward. + - [ ] **1.2 — The resting floor.** Whether a VM's quota has a floor, and whether it is the mass of its pinned patrons (derived) or a constant (tuned). *Refs:* §22.5 #1.