FABRIC.md: resolve item 1.1 -- containment, not a lock
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 <noreply@anthropic.com>
This commit is contained in:
co-authored by
Claude Sonnet 5
parent
daf8f82f3b
commit
f81a53cbf6
@@ -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.
|
||||
|
||||
|
||||
Reference in New Issue
Block a user