amadan
Review one answered: authority gains Confine, Equal in Recheck and Child, slash as a pin, ErrLink for ELOOP too, OpenRoot's path rules, a Platform predicate over Facts, and tests for the tenant boundary, the retained-parent pop, chmod, a foreign-owned component and descriptor accounting; the model's protocol boundaries become separate actions with a send, the ancestry barrier stated from the chain, sticky terminals and closed-implies-no-latch, nine new tests; dispositions and the spike note corrected
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
10 files changed,
+807
−109
DISPOSITIONS-replicator-pinned-root.md+23 −0docs/superpowers/specs/2026-10-03-replicator-pinned-roots-spikes.md+5 −4internal/authority/authority.go+19 −8internal/authority/authority_linux_test.go+116 −0internal/authority/authority_other.go+8 −7internal/authority/authority_unix.go+29 −9internal/authority/authority_unix_test.go+135 −3internal/authority/doc.go+7 −0internal/ops/admissionmodel/model.go+213 −55internal/ops/admissionmodel/model_test.go+252 −23
CI passed — run details
diff --git a/DISPOSITIONS-replicator-pinned-root.md b/DISPOSITIONS-replicator-pinned-root.md| new file mode 100644 |
| index 000000000..1f7923bf3 |
| --- /dev/null |
| +++ b/DISPOSITIONS-replicator-pinned-root.md |
| @@ -0,0 +1,23 @@ |
| +# Dispositions: design-replicator-pinned-root code reviews |
| + |
| +The design is `docs/superpowers/specs/2026-10-03-replicator-pinned-roots-design.md` (revision 8, `8a877936`, accepted at its eighth design review). Code reviews of the branch's commits by Opus (the production and authority reviewer) and Astra (the second reader), each finding answered here in the next commit. |
| + |
| +## Review one (of `5bfcc7ba`: the admission model and `internal/authority`) |
| + |
| +Opus: accept with fixes, no P1, three P2. Astra: reject, five P2, two P3. Reports: `logs/opus-replroot-review1.md`, `logs/astra-replroot-review1.md` in the run directory. |
| + |
| +| Finding | Disposition | |
| +|---|---| |
| +| Astra 2, Opus P2-1: an acquired tenant directory cannot become a confinement boundary | `(*Dir).Confine()` marks an acquired Dir as a root while keeping its ancestry; `TestConfinedTenantRoot` (ascent refused from the root and from beneath it, the edge above still rechecked). The platform-link predicate anchors a relative target at the link's directory under the platform root, so systemd's `../private/...` still resolves; the pinned set must include that directory's root. | |
| +| Astra 3, Opus P3-2: `Recheck` and `Child(expect)` compared identity only | `Facts.Equal` (identity, owner, mode) in both; `TestRootPlatformWalk` chmods an ancestor and sees a changed edge and a failed platform rule, then the restore. `Same` stays for listing-to-acquisition identity. | |
| +| Astra 6: slash itself a pinned root | matched before any component; `TestSlashPinned`. | |
| +| Opus P3-1: intermediates above a pin kept in a result | closed when the pin is entered; the descriptor test counts one descriptor for a result beneath a deeper pin. | |
| +| Opus P3-4: ELOOP not mapped | `ENOTDIR` or `ELOOP` from the directory open is looked at once and named `ErrLink`. | |
| +| Opus P3-5: `OpenRoot` on `/` or with `..` | refused (`ErrBadName`); a root is beneath slash. | |
| +| Opus P3-3: a Dir under a concurrent Close | documented as single-owner; the design's shutdown ordering keeps it; a lock is not added now. | |
| +| Astra 5, Opus P2-2: the foreign-owned component never isolated; the pop not distinguished from kernel `..`; leaks unobserved | the platform predicate takes `Facts`, so a test refuses one inode below an accepted slash; `TestAscentIsTheRetainedParent` moves `b` under another parent and asks for `..`; `TestDescriptorsAreReleased` (linux) counts `/proc/self/fd` across every failing and succeeding walk, three failing roots, a refused `Child`, a `List` and a `Close`, with spellings that leave intermediates open on the way; the swap test closes its result. Sixteen authority mutants run in a tree copy, all killed, including removal of each flag, kernel `..` for the pop, the uid check, each close site, `Result.Close` as a no-op, `Dir.Close` without the syscall, a dup for `List`, no expect check, no `Confine`, and the pin's intermediates kept; the `List` identity check's close is equivalent (`openat(fd, ".")` cannot be another directory). | |
| +| Opus: `/..` refused where today folds it | stated in `doc.go` as intended. | |
| +| Astra 1, Opus P2-3: the model's barrier owner-only and its invariant tautological; multi-owner fleets | the barrier is the design's (a durable unsettled admission bars its fleet's owners and every successor's through the unacknowledged ancestry, issued or not); the invariant is stated from the chain, the publisher from reach; `TestSuccessorBarredByPredecessorAdmission` (day 3 before settlement, and through a closed unacknowledged intermediate); the driver builds one owner per fleet. | |
| +| Astra 4: boundaries collapsed; two tests that could not kill their subject | commit, answer, failure, ambiguous return, read-back, send, exit and drain are separate actions; `TestBudgetExpiryWithoutDiscovery`, `TestBetweenCommitAndAnswer` (a discovery and a crash between), `TestReadBackOnlyAfterTheHandleCloses`, `TestSendNeedsDurableIssuedAdmission`, a fresh eligible participant in the guard test; the three-midnight test now sends on the 3rd. | |
| +| Opus: `Close` without the replay; acknowledgement holds possibly redundant; the proof term never binding; `unackAncestry` over-reach | a closed-implies-no-latch check; acknowledgement copying own-only is not equivalent (a schedule found it); the proof term and the over-reach are equivalent under the model and the spike note says why. | |
| +| Astra 7, Opus P3-6: a leaked result in the swap test; the spike note's header and overstated claims | fixed; the note's header, the boundary and barrier claims, and the three-midnight comment corrected. | |
diff --git a/docs/superpowers/specs/2026-10-03-replicator-pinned-roots-spikes.md b/docs/superpowers/specs/2026-10-03-replicator-pinned-roots-spikes.md| index d6b9ce836..e8defb10a 100644 |
| --- a/docs/superpowers/specs/2026-10-03-replicator-pinned-roots-spikes.md |
| +++ b/docs/superpowers/specs/2026-10-03-replicator-pinned-roots-spikes.md |
| @@ -1,6 +1,6 @@ |
| # Spike notes for the replicator's authority design |
| -Read-only findings (no code written or run), 2026-10-03 06:45, revised 07:25 for revision 5 of `2026-10-03-replicator-pinned-roots-design.md`. Two conclusions of the first version are superseded and struck below: that the Unix VFS's file methods could be delegated (they open the SHM and check moved files by pathname; the VFS owns every method now) and that `fstat` shows ancestry (it shows identity; the spike traces system calls). |
| +Findings for `2026-10-03-replicator-pinned-roots-design.md`: the first two sections are read-only (2026-10-03 06:45, revised 07:25 for revision 5); the admission model section is code that was run, and the entry-point section is a reading of every call. Two conclusions of the first version are superseded and struck below: that the Unix VFS's file methods could be delegated (they open the SHM and check moved files by pathname; the VFS owns every method now) and that `fstat` shows ancestry (it shows identity; the spike traces system calls). |
| ## The descriptor-rooted VFS on `modernc.org/sqlite` v1.55.0 |
| @@ -19,10 +19,11 @@ Read-only findings (no code written or run), 2026-10-03 06:45, revised 07:25 for |
| Plan step 0's second spike is code, kept in tree at `internal/ops/admissionmodel` (not wired, imported by nothing): Part C's transition table (`registered`, `admitted`, `transport done`, `recorder done`, `settled`, `unissued`, `cancelled`, `recovered-unknown`), the barrier and the uncertainty, the pending set under the discovery mutex, the pending-discovery latch and its one-transaction replay, construction backfill, reach over the unacknowledged ancestry, root-first acknowledgement, helper death with the lifecycle guard, the producer fence and process recovery, as plain Go over an integer clock with no SQLite. The model keeps a *truth* apart from the ledger it simulates (when the authority really changed, when each transport really began and ended, which helpers outlived the agent) and the tests check the ledger's answers against it. |
| - **The named sequences are tests**, one each: an unchanged fleet holds nothing; the three-midnight interval in both completion orders (closes at the settlement plus the margin); Astra's commit-after-discovery (unissued, the uncertainty closed once by the empty settlement); review 7's budget expiry then commit; a definite failure cancels and an ambiguous commit is read back either way with the pending set empty after; zero-pending discovery closes at once and holds the margin's extra day across midnight; a failed discovery's latch bars and refuses until the replay, which with nothing pending closes at the replay instant plus the margin; review 6's replay with a counted settlement (the 2nd, 3rd and 4th held, closed at 00:04, a successor built after the replay backfilled); Astra's A, B, C construction and root-first acknowledgement (C refused before B acknowledged A; C inherits U); helper death before and after recorder registration, a `Start` refused after the guard closed; the fence outliving the agent (recovery refused until the helper is gone; recovered-unknown covers the transport that finished after the crash); a healthy chain contributing nothing; and the lower bound reaching a request completed before the change was noticed (the clean look minus the margin). |
| -- **Randomised schedules**: every action above in random interleavings over about four days, 120 steps a schedule; after each step the barrier invariant (an issued unsettled admission bars its owner from its day on) and the hazard invariant (once the ledger knows of a change, every day on which a transport overlapped the true change is incomplete for its owner; after a crash, every admission unsettled at the crash likewise); at quiescence every fleet's owners hold every interval of every uncertainty on its whole chain, no uncertainty is open, and a day with no uncertainty reaching an owner is complete. `ADMISSION_MODEL_SEEDS=30000` passes in under two seconds; the default is 400. |
| +- **The boundaries are separate actions** (after the first code review): the writer's commit, the gate's answer (the recheck), a definite failure, an ambiguous return and its read-back, the send (the helper beginning the transport, which needs a durable issued row and a live helper, and is recorded as a violation otherwise), the helper's proven exit (the guard closes) and the drain (transport-lost, unrecorded) are each their own step, so a schedule can put a discovery, a budget expiry or a crash between a commit and its answer, hold a token for a day before sending, or ask for a recorder's `Start` between the exit and the drain. The composites the named tests use (`WriterReturns`, `HelperDies`) are those steps in order. |
| +- **Randomised schedules**: every action above in random interleavings over about four days, 120 steps a schedule, one owner per fleet (owner scope; the box-wide default is a superset); after each step: the barrier, stated from the chain and not from the publisher (for every fleet and every owner of it, a durable unsettled admission of that fleet or of any fleet in its unacknowledged ancestry bars the owner from its day on, whether or not the token was ever handed out), the hazard invariant (once the ledger knows of a change, every day on which a transport overlapped the true change is incomplete for its owner; after a crash, every admission unsettled at the crash likewise), a terminal state never changing, and a closed fleet having no latch or pending registration; at quiescence every fleet's owners hold every interval of every uncertainty on its whole chain, no uncertainty is open, and a day with no uncertainty reaching an owner is complete. `ADMISSION_MODEL_SEEDS=30000` passes in about six seconds; the default is 400. Publication is revisable by construction: a day published complete can be re-marked by a later hold (the design's materialisation and watermark), and the hazard invariant is satisfied by that retraction; the barrier's purpose is to make retraction rare, not to make it unnecessary. |
| - **What the first runs found** was in the model's own bookkeeping, not the design: the driver admitted an owner the fleet did not have (the model now refuses that, as the design implies), and a helper the crash killed left its transport's true end unset so the hazard looked open forever. The design's rules held once the truth was kept correctly; no interleaving the design does not already name was found. |
| -- **Mutants, in a tree copy**, each killed by a named test or a schedule: no construction backfill (reach); the pending set not counted (the commit-after-discovery tests); no recheck after commit (the same test, and a hazard at seed 264); the replay dropping counted settlements (hazard); the replay closing at the discovery instant (liveness and the latch tests); a settlement writing no interval (hazard); recovery ignoring the fence (the fence test); helper death without transport-lost (an uncertainty open at quiescence); the lower bound ignoring the clean look (the lower-bound test; the 30000-schedule sweep alone did not find it, which is why that sequence is a named test); the lower bound ignoring the earliest unsettled admission (liveness, because the model's proof then reached too far); unrecorded synthesised for a registered worker (the guard test); recovery skipping unclosed fleets (an uncertainty open at quiescence); acknowledgement not root-first and reach ignoring successors (reach). An epoch check made redundant by the stale state is the one equivalent mutant, noted in the model. |
| -- **What the model does not cover**, by construction: the ledger's commit latency on a box's disk under the replicator's request rate (the spike's other half, which needs a box), Part C2's owner scope beyond the owner-scoped holds the model writes, and process kills inside a transaction (the model's transactions are atomic by fiat; the ledger's are SQLite's). |
| +- **Mutants, in a tree copy**, each killed by a named test or a schedule. After the first code review: the budget expiry a no-op (its own test, with no discovery); the barrier owner-only, or over issued rows only (the successor-barred test and the schedules); the pending set skipped at registration; the guard ignored, and the drain before the guard; the replay clearing the latch without the lower bound's holds (a named test: the schedules did not reach it in 3000 seeds); the send unchecked; a close without the replay (the closed-implies-no-latch check); acknowledgement copying the predecessor's own uncertainties only (not equivalent: a schedule found a fifth fleet's owner unheld for the first fleet's uncertainty, because the chain's copies are how a closed interval reaches a fleet built after its predecessor acknowledged); the answer ignoring the refusal; a read-back while the writer runs (the named test; the later commit would land on a cancelled registration, which the terminal check reports). Equivalent under this model: the unacknowledged-ancestry walk not stopping at an acknowledged step (over-reach writes the same holds), and the registry proof dropped from the lower bound (every change here is seen by the next look, so the proof is never the earlier term; a witness change the file look cannot see would need its own change kind, which the design does not have). First: no construction backfill (reach); the pending set not counted (the commit-after-discovery tests); no recheck after commit (the same test, and a hazard at seed 264); the replay dropping counted settlements (hazard); the replay closing at the discovery instant (liveness and the latch tests); a settlement writing no interval (hazard); recovery ignoring the fence (the fence test); helper death without transport-lost (an uncertainty open at quiescence); the lower bound ignoring the clean look (the lower-bound test; the 30000-schedule sweep alone did not find it, which is why that sequence is a named test); the lower bound ignoring the earliest unsettled admission (liveness, because the model's proof then reached too far); unrecorded synthesised for a registered worker (the guard test); recovery skipping unclosed fleets (an uncertainty open at quiescence); acknowledgement not root-first and reach ignoring successors (reach). An epoch check made redundant by the stale state is the one equivalent mutant, noted in the model. |
| +- **What the model does not cover**, by construction: the latch clearing after the commit as two instants (the replay is one step here; the rule stays with the ledger's tests), a snapshot between those instants, the recorder worker's lifetime and the socket drain as separate events, the fence as anything but helper liveness, retries of a failed terminal or replay write, the ledger's commit latency on a box's disk under the replicator's request rate (the spike's other half, which needs a box), Part C2's owner scope beyond the owner-scoped holds the model writes, and process kills inside a transaction (the model's transactions are atomic by fiat; the ledger's are SQLite's). |
| ## The fork's pathname entry points (read 2026-10-03 08:25, every call, not a sample) |
diff --git a/internal/authority/authority.go b/internal/authority/authority.go| index 9ecc9fa99..7a920e5de 100644 |
| --- a/internal/authority/authority.go |
| +++ b/internal/authority/authority.go |
| @@ -13,11 +13,19 @@ type Facts struct { |
| Mode uint32 // the file type and permission bits as the kernel has them |
| } |
| -// Same reports whether two facts name the same object of the same type. |
| +// Same reports whether two facts name the same object of the same type: |
| +// identity, which is what acquisition checks against a listing. |
| func (f Facts) Same(o Facts) bool { |
| return f.Dev == o.Dev && f.Ino == o.Ino && f.Mode&modeTypeMask == o.Mode&modeTypeMask |
| } |
| +// Equal reports whether two facts are the same in every respect the |
| +// package retains: identity, owner and mode. Recheck compares with Equal, |
| +// so a chown or a chmod of a retained directory is a changed edge. |
| +func (f Facts) Equal(o Facts) bool { |
| + return f.Same(o) && f.UID == o.UID && f.Mode == o.Mode |
| +} |
| + |
| // Kind is what one look at a name found. |
| type Kind int |
| @@ -75,19 +83,22 @@ func validName(name string) error { |
| return nil |
| } |
| -// platformOK is the platform walk's rule for one component: owned by a |
| -// platform uid and not writable by group or others. |
| -func platformOK(f Facts, platform func(uint32) bool) bool { |
| - return platform != nil && platform(f.UID) && f.Mode&0o022 == 0 |
| +// Platform decides whether an entry is the platform's by its facts |
| +// (ordinarily by uid: root's or this process's user's). The mode rule, not |
| +// writable by group or others, is the package's and is applied as well. |
| +type Platform func(Facts) bool |
| + |
| +// platformOK is the platform walk's rule for one component. |
| +func platformOK(f Facts, platform Platform) bool { |
| + return platform != nil && platform(f) && f.Mode&0o022 == 0 |
| } |
| // Pins are what an absolute spelling is walked against: the pinned "/" |
| -// and the platform roots a walk may enter. Platform decides which uids |
| -// are the platform's. |
| +// and the platform roots a walk may enter. |
| type Pins struct { |
| Slash *Dir |
| Roots []*Root |
| - Platform func(uid uint32) bool |
| + Platform Platform |
| } |
| func (p *Pins) match(f Facts) *Root { |
diff --git a/internal/authority/authority_linux_test.go b/internal/authority/authority_linux_test.go| new file mode 100644 |
| index 000000000..4144a8e62 |
| --- /dev/null |
| +++ b/internal/authority/authority_linux_test.go |
| @@ -0,0 +1,116 @@ |
| +//go:build linux |
| + |
| +package authority |
| + |
| +import ( |
| + "os" |
| + "path/filepath" |
| + "testing" |
| +) |
| + |
| +func openFDs(t *testing.T) int { |
| + t.Helper() |
| + ents, err := os.ReadDir("/proc/self/fd") |
| + if err != nil { |
| + t.Fatal(err) |
| + } |
| + return len(ents) |
| +} |
| + |
| +// Every descriptor the package opens is closed again: on a failing walk, |
| +// on a succeeding walk once its result is closed, on a failing root, on a |
| +// list, and by Close itself; borrowed descriptors stay open. |
| +func TestDescriptorsAreReleased(t *testing.T) { |
| + base := tempDir(t) |
| + slash := open(t, base) |
| + r := filepath.Join(base, "r") |
| + mkdir(t, filepath.Join(r, "d", "inner")) |
| + write(t, filepath.Join(r, "f"), "x") |
| + link(t, "f", filepath.Join(r, "l")) |
| + write(t, filepath.Join(r, "d", "inner", "zz"), "x") |
| + mkdir(t, filepath.Join(base, "other")) |
| + write(t, filepath.Join(base, "other", "f"), "x") |
| + mkdir(t, filepath.Join(base, "w", "x")) |
| + os.Chmod(filepath.Join(base, "w"), 0o775) |
| + root, err := OpenRoot(slash, "r", me) |
| + if err != nil { |
| + t.Fatal(err) |
| + } |
| + defer root.Close() |
| + pins := &Pins{Slash: slash, Roots: []*Root{root}, Platform: me} |
| + before := openFDs(t) |
| + // failing spellings that leave intermediate directories open on the |
| + // way: "/other/f" (a platform directory outside every pin), "d/inner/zz/x" |
| + // (a file where a directory is needed, two levels down), "d/inner/zz/" |
| + for _, sp := range []string{"d/inner", "d/inner/", "f", "l", "nothing", "d/nothing", "f/x", "f/", "l/x", "/r/d/inner", "/r/f", "/w/x", "/other", "/other/f", "d/inner/zz/x", "d/inner/zz/", "/", "../x", "d/../f"} { |
| + res, err := root.Walk(sp, pins) |
| + if res.Kind == Directory && err == nil && res.Dir != root.Dir { |
| + if openFDs(t) <= before { |
| + t.Errorf("Walk(%q): a directory result holds no descriptor", sp) |
| + } |
| + } |
| + res.Close() |
| + if n := openFDs(t); n != before { |
| + t.Fatalf("Walk(%q): %d descriptors open, %d before", sp, n, before) |
| + } |
| + } |
| + if _, err := root.List(); err != nil { |
| + t.Fatal(err) |
| + } |
| + if _, err := OpenRoot(slash, "w/x", me); err == nil { |
| + t.Fatal("a group-writable ancestry built") |
| + } |
| + if _, err := OpenRoot(slash, "missing/x", me); err == nil { |
| + t.Fatal("a missing ancestry built") |
| + } |
| + if _, err := OpenRoot(slash, "r/d/missing", me); err == nil { |
| + t.Fatal("a root with a missing last component built") |
| + } |
| + if n := openFDs(t); n != before { |
| + t.Fatalf("after List and three failed roots: %d descriptors open, %d before", n, before) |
| + } |
| + // a refused acquisition (the entry changed) leaves nothing open |
| + _, dFacts, _ := root.Lookat("d") |
| + wrong := dFacts |
| + wrong.Ino++ |
| + if _, err := root.Child("d", &wrong); err == nil { |
| + t.Fatal("a changed entry acquired") |
| + } |
| + if n := openFDs(t); n != before { |
| + t.Fatalf("after a refused Child: %d open, %d before", n, before) |
| + } |
| + // a long-lived directory result of an absolute walk holds only the |
| + // directories beneath the pin, not the platform directories above it |
| + mkdir(t, filepath.Join(base, "a", "b", "deep", "d")) |
| + deep, err := OpenRoot(slash, "a/b/deep", me) |
| + if err != nil { |
| + t.Fatal(err) |
| + } |
| + defer deep.Close() |
| + before = openFDs(t) |
| + res, err := root.Walk("/a/b/deep/d", &Pins{Slash: slash, Roots: []*Root{root, deep}, Platform: me}) |
| + if err != nil || res.Kind != Directory { |
| + t.Fatalf("walk into the deeper pin: %v %v", res.Kind, err) |
| + } |
| + if n := openFDs(t); n != before+1 { |
| + t.Fatalf("a directory result beneath a deep pin holds %d descriptors, want 1", n-before) |
| + } |
| + res.Close() |
| + if n := openFDs(t); n != before { |
| + t.Fatalf("after closing it: %d open, %d before", n, before) |
| + } |
| + c, err := root.Child("d", nil) |
| + if err != nil { |
| + t.Fatal(err) |
| + } |
| + if n := openFDs(t); n != before+1 { |
| + t.Fatalf("Child: %d open, want %d", n, before+1) |
| + } |
| + c.Close() |
| + if n := openFDs(t); n != before { |
| + t.Fatalf("Close released nothing: %d open, %d before", n, before) |
| + } |
| + if err := root.Recheck(); err != nil { |
| + t.Fatalf("a borrowed descriptor was closed: %v", err) |
| + } |
| +} |
diff --git a/internal/authority/authority_other.go b/internal/authority/authority_other.go| index 9721d022d..cfe6869e5 100644 |
| --- a/internal/authority/authority_other.go |
| +++ b/internal/authority/authority_other.go |
| @@ -7,7 +7,8 @@ import "os" |
| const modeTypeMask = 0o170000 |
| // Dir on a platform without openat: the replicator does not run here; |
| -// every operation is ErrUnsupported. |
| +// every filesystem operation is ErrUnsupported (accessors and Close are |
| +// inert). |
| type Dir struct { |
| facts Facts |
| name string |
| @@ -28,15 +29,15 @@ func (d *Dir) Readlink(string) (string, error) { return "", ErrUnsup |
| func (d *Dir) OpenRegular(string, Facts) (*os.File, error) { return nil, ErrUnsupported } |
| func (d *Dir) Recheck() error { return ErrUnsupported } |
| func (d *Dir) Walk(string, *Pins) (Result, error) { return Result{}, ErrUnsupported } |
| +func (d *Dir) Confine() { d.root = true } |
| // Root on a platform without openat. |
| type Root struct { |
| *Dir |
| - Path string |
| - facts Facts |
| + Path string |
| } |
| -func OpenRoot(*Dir, string, func(uint32) bool) (*Root, error) { return nil, ErrUnsupported } |
| -func (r *Root) Ancestry() []Facts { return nil } |
| -func (r *Root) AncestryChanged() (bool, error) { return true, ErrUnsupported } |
| -func (r *Root) Close() error { return nil } |
| +func OpenRoot(*Dir, string, Platform) (*Root, error) { return nil, ErrUnsupported } |
| +func (r *Root) Ancestry() []Facts { return nil } |
| +func (r *Root) AncestryChanged() (bool, error) { return true, ErrUnsupported } |
| +func (r *Root) Close() error { return nil } |
diff --git a/internal/authority/authority_unix.go b/internal/authority/authority_unix.go| index 69cb85e7a..dbc2ab66c 100644 |
| --- a/internal/authority/authority_unix.go |
| +++ b/internal/authority/authority_unix.go |
| @@ -5,7 +5,6 @@ package authority |
| import ( |
| "errors" |
| "os" |
| - "path/filepath" |
| "sort" |
| "strings" |
| @@ -16,7 +15,9 @@ const modeTypeMask = unix.S_IFMT |
| const dirFlags = unix.O_DIRECTORY | unix.O_NOFOLLOW | unix.O_RDONLY | unix.O_CLOEXEC | unix.O_NOCTTY |
| -// Dir is a retained directory descriptor. |
| +// Dir is a retained directory descriptor. It has one owner: Close must |
| +// not race another method on the same Dir (the design's shutdown ordering |
| +// keeps that; nothing here locks). |
| type Dir struct { |
| fd int |
| name string // the name it was acquired by from parent; "" for a start |
| @@ -107,7 +108,7 @@ func (d *Dir) Child(name string, expect *Facts) (*Dir, error) { |
| // Linux answers ENOTDIR, not ELOOP, for a link under O_DIRECTORY |
| // with O_NOFOLLOW; one look names it, so a link is never mistaken |
| // for a file. The link is not followed either way. |
| - if err == unix.ENOTDIR { |
| + if err == unix.ENOTDIR || err == unix.ELOOP { |
| if k, _, lerr := d.Lookat(name); lerr == nil && k == Link { |
| return nil, &EdgeError{Name: name, Err: ErrLink} |
| } |
| @@ -120,7 +121,7 @@ func (d *Dir) Child(name string, expect *Facts) (*Dir, error) { |
| return nil, &EdgeError{Name: name, Err: err} |
| } |
| f := factsOf(&st) |
| - if expect != nil && !expect.Same(f) { |
| + if expect != nil && !expect.Equal(f) { |
| unix.Close(fd) |
| return nil, &EdgeError{Name: name, Err: ErrChanged} |
| } |
| @@ -255,13 +256,20 @@ func (d *Dir) Recheck() error { |
| if err := unix.Fstatat(c.parent.fd, c.name, &st, unix.AT_SYMLINK_NOFOLLOW); err != nil { |
| return &EdgeError{Name: c.name, Err: err} |
| } |
| - if !factsOf(&st).Same(c.facts) { |
| + if !factsOf(&st).Equal(c.facts) { |
| return &EdgeError{Name: c.name, Err: ErrChanged} |
| } |
| } |
| return nil |
| } |
| +// Confine makes this Dir a confinement boundary: a relative Walk from it |
| +// or from anything acquired beneath it cannot pop past it. Its retained |
| +// ancestry stays, so Recheck still sees every edge above it. This is how |
| +// a tenant root acquired beneath a platform root becomes the tenant's |
| +// boundary. |
| +func (d *Dir) Confine() { d.root = true } |
| + |
| // Walk classifies a captured link target. A relative spelling is walked |
| // from this Dir; an absolute one from the pinned "/" under the platform |
| // walk's rules until it enters a pinned root, then beneath that root. A |
| @@ -310,6 +318,10 @@ func (d *Dir) Walk(spelling string, pins *Pins) (Result, error) { |
| } |
| cur = pins.Slash |
| entered = false |
| + if pin := pins.match(pins.Slash.facts); pin != nil { |
| + cur = pin.Dir // slash itself is pinned |
| + entered = true |
| + } |
| } |
| res := Result{} |
| fail := func(err error) (Result, error) { |
| @@ -341,6 +353,7 @@ func (d *Dir) Walk(spelling string, pins *Pins) (Result, error) { |
| } |
| if pin := pins.match(child.facts); pin != nil { |
| child.Close() |
| + res.Close() // the platform directories above the pin are not kept |
| cur = pin.Dir |
| entered = true |
| } else { |
| @@ -414,7 +427,7 @@ type Root struct { |
| slash *Dir |
| comps []string |
| ancestry []Facts |
| - platform func(uint32) bool |
| + platform Platform |
| } |
| // OpenRoot walks path's components from slash, requiring each to be a |
| @@ -422,7 +435,7 @@ type Root struct { |
| // writable by group or others. The intermediate Dirs are retained as the |
| // root's stack. Path is spelled from slash, so "/var/lib/carlos" against |
| // the real "/" is that directory, and against a test's "/" it is beneath it. |
| -func OpenRoot(slash *Dir, path string, platform func(uint32) bool) (*Root, error) { |
| +func OpenRoot(slash *Dir, path string, platform Platform) (*Root, error) { |
| if err := slash.live(); err != nil { |
| return nil, err |
| } |
| @@ -430,11 +443,18 @@ func OpenRoot(slash *Dir, path string, platform func(uint32) bool) (*Root, error |
| return nil, &EdgeError{Name: "/", Err: ErrNotPlatform} |
| } |
| var comps []string |
| - for _, c := range strings.Split(filepath.Clean("/"+path), "/") { |
| - if c != "" { |
| + for _, c := range strings.Split(path, "/") { |
| + switch c { |
| + case "", ".": |
| + case "..": |
| + return nil, ErrBadName |
| + default: |
| comps = append(comps, c) |
| } |
| } |
| + if len(comps) == 0 { |
| + return nil, ErrBadName // a root is beneath slash, never slash itself |
| + } |
| cur := slash |
| var ancestry []Facts |
| var opened []*Dir |
diff --git a/internal/authority/authority_unix_test.go b/internal/authority/authority_unix_test.go| index 8ac1d8ef3..60dc9206f 100644 |
| --- a/internal/authority/authority_unix_test.go |
| +++ b/internal/authority/authority_unix_test.go |
| @@ -12,7 +12,7 @@ import ( |
| "golang.org/x/sys/unix" |
| ) |
| -func me(uid uint32) bool { return uid == uint32(os.Geteuid()) } |
| +func me(f Facts) bool { return f.UID == uint32(os.Geteuid()) } |
| // tempDir is t.TempDir with the mode the platform rule wants, whatever the |
| // umask (0002 makes a plain temp directory group-writable). |
| @@ -98,8 +98,21 @@ func TestRootPlatformWalk(t *testing.T) { |
| base := tempDir(t) |
| slash := open(t, base) |
| mkdir(t, filepath.Join(base, "a", "b")) |
| - if _, err := OpenRoot(slash, "a/b", func(uint32) bool { return false }); !edgeIs(err, ErrNotPlatform) { |
| - t.Fatalf("non-platform owner: %v", err) |
| + // a foreign-owned component below an accepted slash: refused by inode, |
| + // since a test cannot chown; slash and "a" are accepted |
| + _, bFacts, _ := child(t, slash, "a").Lookat("b") |
| + notB := func(f Facts) bool { return me(f) && !f.Same(bFacts) } |
| + var ee *EdgeError |
| + if _, err := OpenRoot(slash, "a/b", notB); !errors.As(err, &ee) || ee.Name != "b" || !errors.Is(ee.Err, ErrNotPlatform) { |
| + t.Fatalf("non-platform component: %v", err) |
| + } |
| + if _, err := OpenRoot(slash, "a/b", func(Facts) bool { return false }); !edgeIs(err, ErrNotPlatform) { |
| + t.Fatalf("non-platform slash: %v", err) |
| + } |
| + for _, bad := range []string{"", "/", ".", "a/../b", "../a"} { |
| + if _, err := OpenRoot(slash, bad, me); !errors.Is(err, ErrBadName) { |
| + t.Fatalf("OpenRoot(%q): %v", bad, err) |
| + } |
| } |
| if err := os.Chmod(filepath.Join(base, "a"), 0o775); err != nil { |
| t.Fatal(err) |
| @@ -124,6 +137,21 @@ func TestRootPlatformWalk(t *testing.T) { |
| if changed, err := r.AncestryChanged(); changed || err != nil { |
| t.Fatalf("unchanged ancestry read as changed: %v %v", changed, err) |
| } |
| + // a mode change on a retained ancestor is a changed edge and a failed |
| + // platform rule, without any replacement |
| + if err := os.Chmod(filepath.Join(base, "a"), 0o775); err != nil { |
| + t.Fatal(err) |
| + } |
| + if err := r.Recheck(); !edgeIs(err, ErrChanged) { |
| + t.Fatalf("Recheck after chmod of an ancestor: %v", err) |
| + } |
| + if changed, err := r.AncestryChanged(); !changed || !edgeIs(err, ErrNotPlatform) { |
| + t.Fatalf("AncestryChanged after chmod: %v %v", changed, err) |
| + } |
| + os.Chmod(filepath.Join(base, "a"), 0o755) |
| + if err := r.Recheck(); err != nil { |
| + t.Fatalf("Recheck after the mode was restored: %v", err) |
| + } |
| if err := os.Rename(filepath.Join(base, "a", "b"), filepath.Join(base, "a", "c")); err != nil { |
| t.Fatal(err) |
| } |
| @@ -161,6 +189,7 @@ func TestSwapBetweenListAndWalk(t *testing.T) { |
| if err != nil || res.Kind != Regular { |
| t.Fatalf("walk from the retained directory: %v %v", res.Kind, err) |
| } |
| + res.Close() |
| fresh := open(t, filepath.Join(base, "A")) |
| res, err = fresh.Walk(target, nil) |
| if err != nil || res.Kind != Absent { |
| @@ -483,3 +512,106 @@ func TestClosed(t *testing.T) { |
| t.Fatalf("Walk after Close: %v", err) |
| } |
| } |
| + |
| +// The pop is the retained parent, not the kernel's "..": after the child |
| +// is moved under another parent, ".." from it is still the directory it |
| +// was acquired from. |
| +func TestAscentIsTheRetainedParent(t *testing.T) { |
| + base := tempDir(t) |
| + slash := open(t, base) |
| + mkdir(t, filepath.Join(base, "r", "a", "b")) |
| + mkdir(t, filepath.Join(base, "r", "d")) |
| + r, err := OpenRoot(slash, "r", me) |
| + if err != nil { |
| + t.Fatal(err) |
| + } |
| + defer r.Close() |
| + a := child(t, r.Dir, "a") |
| + b := child(t, a, "b") |
| + if err := os.Rename(filepath.Join(base, "r", "a", "b"), filepath.Join(base, "r", "d", "b")); err != nil { |
| + t.Fatal(err) |
| + } |
| + res, err := b.Walk("..", nil) |
| + if err != nil || res.Kind != Directory || !res.Facts.Same(a.Facts()) || res.Dir != a { |
| + t.Fatalf("\"..\" after a move: %v %v (want the retained parent a)", res, err) |
| + } |
| + _, dFacts, _ := r.Lookat("d") |
| + if res.Facts.Same(dFacts) { |
| + t.Fatal("\"..\" followed the kernel to the new parent") |
| + } |
| + res, err = b.Walk("../..", nil) |
| + if err != nil || res.Dir != r.Dir { |
| + t.Fatalf("\"../..\" after a move: %v %v", res, err) |
| + } |
| +} |
| + |
| +// A tenant root acquired beneath a platform root is a boundary once |
| +// confined: a relative walk cannot pop past it, so a link spelled out of |
| +// the tenant's tree is refused rather than resolved to a sibling; its |
| +// ancestry above the boundary is still rechecked. |
| +func TestConfinedTenantRoot(t *testing.T) { |
| + base := tempDir(t) |
| + slash := open(t, base) |
| + mkdir(t, filepath.Join(base, "plat", "tenant", "d")) |
| + mkdir(t, filepath.Join(base, "plat", "other")) |
| + write(t, filepath.Join(base, "plat", "other", "x.db"), "x") |
| + plat, err := OpenRoot(slash, "plat", me) |
| + if err != nil { |
| + t.Fatal(err) |
| + } |
| + defer plat.Close() |
| + tenant := child(t, plat.Dir, "tenant") |
| + // before confinement the platform root is the boundary |
| + res, err := tenant.Walk("../other/x.db", nil) |
| + if err != nil || res.Kind != Regular { |
| + t.Fatalf("unconfined: %v %v", res.Kind, err) |
| + } |
| + res.Close() |
| + tenant.Confine() |
| + if _, err := tenant.Walk("../other/x.db", nil); !errors.Is(err, ErrAscentPastRoot) { |
| + t.Fatalf("confined: %v", err) |
| + } |
| + d := child(t, tenant, "d") |
| + if _, err := d.Walk("../../other/x.db", nil); !errors.Is(err, ErrAscentPastRoot) { |
| + t.Fatalf("confined from beneath: %v", err) |
| + } |
| + res, err = d.Walk("..", nil) |
| + if err != nil || res.Dir != tenant { |
| + t.Fatalf("to the tenant root: %v %v", res, err) |
| + } |
| + if tenant.Depth() != 2 { |
| + t.Fatalf("confinement dropped the ancestry: depth %d", tenant.Depth()) |
| + } |
| + if err := os.Rename(filepath.Join(base, "plat", "tenant"), filepath.Join(base, "plat", "moved")); err != nil { |
| + t.Fatal(err) |
| + } |
| + if err := d.Recheck(); err == nil { |
| + t.Fatal("the edge above the confined root was not rechecked") |
| + } |
| +} |
| + |
| +// Slash itself may be a pinned root: absolute spellings then classify |
| +// beneath it directly. |
| +func TestSlashPinned(t *testing.T) { |
| + base := tempDir(t) |
| + slash := open(t, base) |
| + mkdir(t, filepath.Join(base, "pin", "d")) |
| + write(t, filepath.Join(base, "pin", "f"), "x") |
| + pin := open(t, filepath.Join(base, "pin")) |
| + root, err := OpenRoot(slash, "pin", me) |
| + if err != nil { |
| + t.Fatal(err) |
| + } |
| + defer root.Close() |
| + pins := &Pins{Slash: root.Dir, Roots: []*Root{root}, Platform: me} |
| + for spelling, kind := range map[string]Kind{"/": Directory, "/f": Regular, "/d": Directory, "/d/": Directory, "/nothing": Absent} { |
| + res, err := pin.Walk(spelling, pins) |
| + if err != nil || res.Kind != kind { |
| + t.Errorf("Walk(%q) with slash pinned: %v %v", spelling, res.Kind, err) |
| + } |
| + if spelling == "/" && res.Dir != root.Dir { |
| + t.Errorf("\"/\" is not the pinned Dir") |
| + } |
| + res.Close() |
| + } |
| +} |
diff --git a/internal/authority/doc.go b/internal/authority/doc.go| index ae3796d78..7179486e2 100644 |
| --- a/internal/authority/doc.go |
| +++ b/internal/authority/doc.go |
| @@ -13,6 +13,13 @@ |
| // leaves the root it started in. A Root is a Dir reached from a pinned "/" |
| // by a walk whose every component is the platform's. |
| // |
| +// Two choices differ from today's pathname code on purpose. An absolute |
| +// spelling with a leading ".." ("/../x") is refused, where filepath.Dir |
| +// folds it to "/" today: a captured target that spells an ascent above |
| +// the root is not something a walk should repair. And Recheck compares |
| +// every retained fact (owner and mode too), so a chmod or chown of a |
| +// retained directory is a changed edge, not only a replacement. |
| +// |
| // What this package does not claim: a bind mount or a device node already |
| // inside a tree is reachable within containment; a swap put back between |
| // two looks is not detected by polling. Those are the design's stated |
diff --git a/internal/ops/admissionmodel/model.go b/internal/ops/admissionmodel/model.go| index 129546f60..205ddea8b 100644 |
| --- a/internal/ops/admissionmodel/model.go |
| +++ b/internal/ops/admissionmodel/model.go |
| @@ -65,7 +65,10 @@ type Admission struct { |
| Refused bool // the gate's budget expired or the recheck refused |
| writerRunning bool |
| - epoch int // the fleet's discovery epoch at registration |
| + handleClosed bool // the writer's handle is closed (an ambiguous return) |
| + landed bool // truth: the ambiguous write did land |
| + answered bool // the gate has answered (issued or unissued) |
| + epoch int // the fleet's discovery epoch at registration |
| TransportDoneAt Time |
| RecorderStartedAt Time |
| @@ -132,6 +135,7 @@ type Fleet struct { |
| helperAlive bool |
| helperStopped bool |
| guardClosed bool |
| + drained bool |
| // truth |
| ChangedAt Time // the instant authority truly changed (unset if never) |
| @@ -152,11 +156,13 @@ type Model struct { |
| nextToken int |
| nextUnc int |
| Log []string |
| + Violations []string // rules the model refused to break but was asked to |
| + final map[int]State // a terminal state, once reached, never changes |
| } |
| // New returns an empty box with a live agent. |
| func New(seed int64) *Model { |
| - return &Model{rnd: rand.New(rand.NewSource(seed)), Holds: map[int64]map[Owner]bool{}, Alive: true, Recovered: true, CrashedAt: unset} |
| + return &Model{rnd: rand.New(rand.NewSource(seed)), Holds: map[int64]map[Owner]bool{}, Alive: true, Recovered: true, CrashedAt: unset, final: map[int]State{}} |
| } |
| func (m *Model) logf(f string, args ...any) { |
| @@ -319,44 +325,61 @@ func (m *Model) Register(f *Fleet, o Owner) *Admission { |
| return a |
| } |
| -// BudgetExpires: the gate refuses the request while the writer still runs. |
| +// BudgetExpires: the gate refuses the request before it has answered, |
| +// whether the writer still runs or the row is durable and unanswered. |
| func (m *Model) BudgetExpires(a *Admission) { |
| - if a.State == Registered && a.writerRunning { |
| + if (a.State == Registered && a.writerRunning) || (a.State == Admitted && !a.answered) { |
| a.Refused = true |
| } |
| } |
| -// WriterReturns resolves a registration: "commit", "fail", or "ambiguous" |
| -// (the writer cannot tell; the model decides whether the write landed and |
| -// the read-back, after the handle is closed, finds it). |
| +// WriterReturns is the composite the named tests use: the writer's |
| +// return ("commit", "fail" or "ambiguous"), then for a commit the gate's |
| +// answer at once, and for an ambiguous return the read-back at once. The |
| +// boundaries are separate actions below, so a schedule can put a |
| +// discovery, a budget expiry or a crash between them. |
| func (m *Model) WriterReturns(a *Admission, outcome string) { |
| - if !m.Alive || a.State != Registered || !a.writerRunning { |
| - return |
| + switch outcome { |
| + case "commit": |
| + m.WriterCommits(a) |
| + m.GateAnswers(a) |
| + case "fail": |
| + m.WriterFails(a) |
| + case "ambiguous": |
| + m.WriterAmbiguous(a) |
| + m.ReadBack(a) |
| } |
| - a.writerRunning = false |
| - f := a.Fleet |
| - landed := outcome == "commit" || (outcome == "ambiguous" && m.rnd.Intn(2) == 0) |
| - if outcome == "ambiguous" { |
| - a.Refused = true // the gate could not answer within its budget |
| - } |
| - if !landed { |
| - // conclusive cancellation: the writer has returned (or its handle is |
| - // closed and a fresh read found no row) |
| - a.State = Cancelled |
| - a.SettledAt = m.Now |
| - a.How = "cancelled" |
| - delete(f.pending, a.Token) |
| - m.logf("T%d cancelled", a.Token) |
| - m.emptySettlement(a) |
| - return |
| +} |
| + |
| +// WriterCommits: the row is durable; under the discovery mutex the |
| +// registration leaves the pending set and the row carries it. The gate |
| +// has not answered yet. |
| +func (m *Model) WriterCommits(a *Admission) { |
| + if !m.Alive || !a.writerRunning || (a.State != Registered && a.State != Cancelled) { |
| + return // a writer still running commits even if something called the registration cancelled |
| } |
| + if a.State == Cancelled { |
| + a.Fleet.pending[a.Token] = a // the row lands: the terminal was not final (Check reports it) |
| + } |
| + a.writerRunning = false |
| a.Durable = true |
| a.State = Admitted |
| - f.Admissions = append(f.Admissions, a) |
| - delete(f.pending, a.Token) // under the mutex: the row now carries it |
| - // the recheck under the mutex (the epoch test is redundant with the |
| - // stale state here, since every discovery stales the fleet; it is kept |
| - // because the design names it) |
| + a.Fleet.Admissions = append(a.Fleet.Admissions, a) |
| + delete(a.Fleet.pending, a.Token) |
| + m.logf("T%d committed", a.Token) |
| +} |
| + |
| +// GateAnswers is the recheck under the discovery mutex after the commit: |
| +// unissued if the request was refused meanwhile, the fleet went stale or |
| +// a discovery began since registration; else the token is issued. |
| +func (m *Model) GateAnswers(a *Admission) { |
| + if !m.Alive || a.State != Admitted || a.answered { |
| + return |
| + } |
| + a.answered = true |
| + f := a.Fleet |
| + // the epoch test is redundant with the stale state here, since every |
| + // discovery stales the fleet; it is kept because the design names it |
| if a.Refused || f.State != Open || f.inDiscovery || f.epoch != a.epoch || f.latch != nil { |
| m.terminal(a, Unissued, "unissued") |
| m.logf("T%d unissued", a.Token) |
| @@ -364,10 +387,79 @@ func (m *Model) WriterReturns(a *Admission, outcome string) { |
| return |
| } |
| a.Issued = true |
| - a.SentAt = m.Now |
| m.logf("T%d issued", a.Token) |
| } |
| +// WriterFails: a definite failure, no row; the cancellation is conclusive |
| +// because the writer has returned. |
| +func (m *Model) WriterFails(a *Admission) { |
| + if !m.Alive || a.State != Registered || !a.writerRunning { |
| + return |
| + } |
| + a.writerRunning = false |
| + m.cancel(a) |
| +} |
| + |
| +func (m *Model) cancel(a *Admission) { |
| + a.State = Cancelled |
| + a.SettledAt = m.Now |
| + a.How = "cancelled" |
| + delete(a.Fleet.pending, a.Token) |
| + m.logf("T%d cancelled", a.Token) |
| + m.emptySettlement(a) |
| +} |
| + |
| +// WriterAmbiguous: the writer cannot tell whether its commit landed; its |
| +// handle is closed, the gate refuses the request, and the registration |
| +// stays pending until a read-back decides. |
| +func (m *Model) WriterAmbiguous(a *Admission) { |
| + if !m.Alive || a.State != Registered || !a.writerRunning { |
| + return |
| + } |
| + a.writerRunning = false |
| + a.handleClosed = true |
| + a.Refused = true |
| + a.landed = m.rnd.Intn(2) == 0 |
| +} |
| + |
| +// ReadBack decides an ambiguous registration on a read opened after the |
| +// writer's handle closed: a row found takes admitted then unissued; none |
| +// found is a conclusive cancellation. A read while the writer could still |
| +// commit is not conclusive: the guard on writerRunning is that rule, and |
| +// a model without it lets a cancelled registration's row land later, |
| +// which Check reports as a terminal that did not hold. |
| +func (m *Model) ReadBack(a *Admission) bool { |
| + if !m.Alive || a.State != Registered || a.writerRunning || !a.handleClosed { |
| + return false |
| + } |
| + if a.landed { |
| + a.writerRunning = true // the commit is the writer's, seen by the read |
| + m.WriterCommits(a) |
| + m.GateAnswers(a) |
| + return true |
| + } |
| + m.cancel(a) |
| + return true |
| +} |
| + |
| +// Send is the helper beginning the transport. It requires a durable row, |
| +// an issued token and the fence (a live helper of a live agent, or a |
| +// helper that outlived its agent still holding the fence's description). |
| +func (m *Model) Send(a *Admission) { |
| + if a.SentAt != unset || a.State.Terminal() { |
| + return |
| + } |
| + if !a.Durable || !a.Issued { |
| + m.Violations = append(m.Violations, fmt.Sprintf("T%d sent without a durable issued admission", a.Token)) |
| + return |
| + } |
| + if !a.Fleet.helperAlive { |
| + return // a dead helper does nothing; the held token dies with it |
| + } |
| + a.SentAt = m.Now |
| + m.logf("T%d sent", a.Token) |
| +} |
| + |
| func (m *Model) terminal(a *Admission, s State, how string) { |
| a.State = s |
| a.How = how |
| @@ -496,7 +588,7 @@ func (m *Model) Replay(f *Fleet) { |
| // TransportDone is the SDK middleware's finalize step. |
| func (m *Model) TransportDone(a *Admission) { |
| - if !a.Issued || a.TransportDoneAt != unset { |
| + if !m.Alive || !a.Issued || a.SentAt == unset || a.TransportDoneAt != unset { |
| return |
| } |
| a.TransportDoneAt = m.Now |
| @@ -551,28 +643,47 @@ func (m *Model) settle(a *Admission) { |
| m.logf("T%d settled", a.Token) |
| } |
| -// HelperDies: the helper's death proven by waitpid. It is a change; the |
| -// guard closes, the socket drains, transports are lost and never-registered |
| -// recorders are unrecorded. Registered workers are kept. |
| +// HelperDies is the composite: the exit proven, then the drain. |
| func (m *Model) HelperDies(f *Fleet, discoveryFails bool) { |
| + m.HelperExits(f, discoveryFails) |
| + m.DrainHelper(f) |
| +} |
| + |
| +// HelperExits: the helper's death proven by waitpid. It is a change; the |
| +// lifecycle guard closes first, so no Start can register after this. |
| +func (m *Model) HelperExits(f *Fleet, discoveryFails bool) { |
| if !f.helperAlive { |
| return |
| } |
| f.helperAlive = false |
| f.DiedAt = m.Now |
| + for _, a := range f.Admissions { |
| + if a.Issued && a.SentAt != unset && a.SentEndAt == unset { |
| + a.SentEndAt = m.Now |
| + } |
| + } |
| if !m.Alive { |
| return // the agent is gone; recovery handles it |
| } |
| + f.guardClosed = true |
| m.Change(f) |
| m.Discover(f, discoveryFails) |
| - f.guardClosed = true |
| +} |
| + |
| +// DrainHelper: after the proven exit, what the socket held is drained, |
| +// then transports are lost and never-registered recorders are unrecorded. |
| +// Registered workers are kept. |
| +func (m *Model) DrainHelper(f *Fleet) { |
| + if !m.Alive || f.helperAlive || !f.guardClosed || f.drained { |
| + return |
| + } |
| + f.drained = true |
| for _, a := range f.Admissions { |
| if !a.Issued || a.State.Terminal() { |
| continue |
| } |
| if a.TransportDoneAt == unset { |
| - a.TransportDoneAt = m.Now |
| - a.SentEndAt = m.Now |
| + a.TransportDoneAt = m.Now // transport-lost |
| if a.State == Admitted { |
| a.State = TransportDone |
| } |
| @@ -593,7 +704,7 @@ func (m *Model) StopHelper(f *Fleet) bool { |
| return false |
| } |
| for _, a := range f.Admissions { |
| - if a.Issued && a.TransportDoneAt == unset { |
| + if a.Issued && a.SentAt != unset && a.TransportDoneAt == unset { |
| return false |
| } |
| } |
| @@ -601,11 +712,20 @@ func (m *Model) StopHelper(f *Fleet) bool { |
| f.helperAlive = false |
| f.helperStopped = true |
| f.guardClosed = true |
| - for _, a := range f.Admissions { // Start can no longer arrive |
| - if a.Issued && !a.State.Terminal() && a.RecorderDoneAt == unset && a.RecorderStartedAt == unset { |
| - a.RecorderDoneAt = m.Now |
| - a.How = "unrecorded" |
| - if a.TransportDoneAt != unset { |
| + f.drained = true |
| + for _, a := range f.Admissions { // Start can no longer arrive; a held token is never sent |
| + if a.Issued && !a.State.Terminal() { |
| + if a.TransportDoneAt == unset { |
| + a.TransportDoneAt = m.Now |
| + if a.State == Admitted { |
| + a.State = TransportDone |
| + } |
| + } |
| + if a.RecorderDoneAt == unset && a.RecorderStartedAt == unset { |
| + a.RecorderDoneAt = m.Now |
| + a.How = "unrecorded" |
| + } |
| + if a.TransportDoneAt != unset && a.RecorderDoneAt != unset { |
| m.settle(a) |
| } |
| } |
| @@ -669,8 +789,12 @@ func (m *Model) Crash(helperSurvives func(*Fleet) bool) { |
| m.CrashedAt = m.Now |
| for _, f := range m.Fleets { |
| for tok, a := range f.pending { |
| + landed := a.landed |
| + if a.writerRunning { |
| + landed = m.rnd.Intn(2) == 0 |
| + } |
| a.writerRunning = false |
| - if m.rnd.Intn(2) == 0 { // the commit landed before the crash |
| + if landed { // the commit landed before the crash: a durable unanswered row |
| a.Durable = true |
| a.State = Admitted |
| f.Admissions = append(f.Admissions, a) |
| @@ -688,7 +812,7 @@ func (m *Model) Crash(helperSurvives func(*Fleet) bool) { |
| f.helperAlive = false |
| f.DiedAt = m.Now |
| for _, a := range f.Admissions { |
| - if a.Issued && a.SentEndAt == unset { |
| + if a.Issued && a.SentAt != unset && a.SentEndAt == unset { |
| a.SentEndAt = m.Now |
| } |
| } |
| @@ -700,9 +824,12 @@ func (m *Model) Crash(helperSurvives func(*Fleet) bool) { |
| // SurvivingHelperTransport: a helper that outlived its agent still finishes |
| // a transport it had in hand. |
| func (m *Model) SurvivingHelperTransport(a *Admission) { |
| - if m.Alive || !a.Fleet.helperAlive || !a.Issued || a.TransportDoneAt != unset { |
| + if m.Alive || !a.Fleet.helperAlive || !a.Issued || a.TransportDoneAt != unset || a.SentEndAt != unset { |
| return |
| } |
| + if a.SentAt == unset { |
| + m.Send(a) // a held token, sent now under the fence the helper still holds |
| + } |
| a.SentEndAt = m.Now // the truth; the row is not written, the agent is dead |
| } |
| @@ -712,7 +839,7 @@ func (m *Model) SurvivingHelperDies(f *Fleet) { |
| f.helperAlive = false |
| f.DiedAt = m.Now |
| for _, a := range f.Admissions { |
| - if a.Issued && a.SentEndAt == unset { |
| + if a.Issued && a.SentAt != unset && a.SentEndAt == unset { |
| a.SentEndAt = m.Now |
| } |
| } |
| @@ -795,8 +922,12 @@ func (m *Model) Complete(o Owner, day int64) bool { |
| return false |
| } |
| for _, a := range m.Admissions { |
| - if a.Durable && a.Issued && a.unsettled() && a.Owner == o && dayOf(a.AdmittedAt) <= day { |
| - return false |
| + if a.Durable && a.unsettled() && dayOf(a.AdmittedAt) <= day { |
| + for _, r := range m.reach(a.Fleet) { // its fleet's owners and every successor's through the unacknowledged ancestry |
| + if r == o { |
| + return false |
| + } |
| + } |
| } |
| } |
| for _, f := range m.Fleets { |
| @@ -818,12 +949,39 @@ func (m *Model) Check() error { |
| return nil |
| } |
| today := dayOf(m.Now) |
| - // barrier: an issued, unsettled admission bars its owner from its day on |
| + if len(m.Violations) > 0 { |
| + return fmt.Errorf("violation: %s", m.Violations[0]) |
| + } |
| + // a terminal state is final |
| for _, a := range m.Admissions { |
| - if a.Durable && a.Issued && a.unsettled() { |
| - for d := dayOf(a.AdmittedAt); d <= today; d++ { |
| - if m.Complete(a.Owner, d) { |
| - return fmt.Errorf("barrier: T%d unsettled but %s day %d complete", a.Token, a.Owner, d) |
| + if was, ok := m.final[a.Token]; ok && was != a.State { |
| + return fmt.Errorf("T%d left terminal %s for %s", a.Token, was, a.State) |
| + } |
| + if a.State.Terminal() { |
| + m.final[a.Token] = a.State |
| + } |
| + } |
| + // a closed fleet has no uncommitted discovery and nothing pending |
| + for _, f := range m.Fleets { |
| + if f.State == Closed && (f.latch != nil || len(f.pending) > 0) { |
| + return fmt.Errorf("fleet %d closed with a latch or a pending registration", f.ID) |
| + } |
| + } |
| + // barrier, stated from the chain: for every fleet G and every owner of |
| + // G, a durable unsettled admission of G or of any fleet in G's |
| + // unacknowledged ancestry bars that owner from its day on |
| + for _, g := range m.Fleets { |
| + for _, p := range append([]*Fleet{g}, unackAncestry(g)...) { |
| + for _, a := range p.Admissions { |
| + if !a.Durable || !a.unsettled() { |
| + continue |
| + } |
| + for _, o := range g.Owners { |
| + for d := dayOf(a.AdmittedAt); d <= today; d++ { |
| + if m.Complete(o, d) { |
| + return fmt.Errorf("barrier: T%d (fleet %d) unsettled but fleet %d's owner %s day %d complete", a.Token, p.ID, g.ID, o, d) |
| + } |
| + } |
| } |
| } |
| } |
diff --git a/internal/ops/admissionmodel/model_test.go b/internal/ops/admissionmodel/model_test.go| index 179b82abe..679fffd60 100644 |
| --- a/internal/ops/admissionmodel/model_test.go |
| +++ b/internal/ops/admissionmodel/model_test.go |
| @@ -49,8 +49,17 @@ func complete(t *testing.T, m *Model, o Owner, days ...int) { |
| } |
| } |
| -// issue registers and commits an admission on a healthy fleet. |
| +// issue registers, commits and answers an admission on a healthy fleet, |
| +// and the helper sends at once. |
| func issue(t *testing.T, m *Model, f *Fleet, o Owner) *Admission { |
| + t.Helper() |
| + a := hold(t, m, f, o) |
| + m.Send(a) |
| + return a |
| +} |
| + |
| +// hold is issue without the send: the helper holds the token. |
| +func hold(t *testing.T, m *Model, f *Fleet, o Owner) *Admission { |
| t.Helper() |
| a := m.Register(f, o) |
| if a == nil { |
| @@ -88,17 +97,20 @@ func TestUnchangedFleetHoldsNothing(t *testing.T) { |
| } |
| // The multiple-midnights sequence in both completion orders: admitted on |
| -// the 2nd, the change at 23:58:10, sent on the 3rd, finished on the 4th; |
| -// the 2nd, 3rd and 4th are held whichever participant finished last. |
| +// the 2nd, the change at 23:58, sent on the 3rd (after the change, before |
| +// it is noticed), finished on the 4th; the 2nd, 3rd and 4th are held |
| +// whichever participant finished last. |
| func TestThreeMidnightsBothOrders(t *testing.T) { |
| for _, transportLast := range []bool{false, true} { |
| m := New(1) |
| m.Now = at(1, 9, 0) |
| f := m.Build(alice) |
| m.Now = at(2, 23, 57) |
| - a := issue(t, m, f, alice) |
| + a := hold(t, m, f, alice) // admitted on the 2nd, the token held |
| m.Now = at(2, 23, 58) |
| m.Change(f) |
| + m.Now = at(3, 0, 0) |
| + m.Send(a) // sent on the 3rd, after the change and before it is noticed |
| m.Now = at(3, 0, 1) |
| m.Look(f) // the discovery |
| must(t, m) |
| @@ -375,9 +387,23 @@ func TestHelperDeathAndRecorderGuard(t *testing.T) { |
| t.Fatalf("registered worker not kept: %s", live.State) |
| } |
| if m.RecorderStart(live) { |
| - t.Fatal("Start accepted after the guard closed") |
| + t.Fatal("Start accepted for an already registered recorder") |
| } |
| held(t, m, alice, 1) |
| + // a fresh, eligible, not yet registered participant: the guard is closed |
| + // before the drain, so between the two its Start is refused |
| + m2 := New(2) |
| + m2.Now = at(1, 10, 0) |
| + f2 := m2.Build(alice) |
| + fresh := issue(t, m2, f2, alice) |
| + m2.HelperExits(f2, false) |
| + if m2.RecorderStart(fresh) { |
| + t.Fatal("Start accepted after the guard closed and before the drain") |
| + } |
| + m2.DrainHelper(f2) |
| + if fresh.State != Settled || fresh.How != "unrecorded" { |
| + t.Fatalf("fresh after the drain: %s %q", fresh.State, fresh.How) |
| + } |
| u := f.Uncertainties[0] |
| if !u.open() { |
| t.Fatal("closed with the worker still running") |
| @@ -430,7 +456,7 @@ func TestHealthyChainContributesNothing(t *testing.T) { |
| m.StopHelper(A) |
| m.Close(A) |
| m.Advance(1) |
| - B := m.Build(alice, bob) |
| + B := m.Build(bob) |
| m.Acknowledge(B) |
| complete(t, m, alice, 1) |
| complete(t, m, bob, 1) |
| @@ -441,6 +467,171 @@ func TestHealthyChainContributesNothing(t *testing.T) { |
| } |
| } |
| +// Review 1: a budget expiry with no discovery at all still ends unissued, |
| +// whether the writer commits before or after the expiry. |
| +func TestBudgetExpiryWithoutDiscovery(t *testing.T) { |
| + for _, commitFirst := range []bool{false, true} { |
| + m := New(1) |
| + m.Now = at(1, 10, 0) |
| + f := m.Build(alice) |
| + a := m.Register(f, alice) |
| + if commitFirst { |
| + m.WriterCommits(a) |
| + m.BudgetExpires(a) |
| + } else { |
| + m.BudgetExpires(a) |
| + m.WriterCommits(a) |
| + } |
| + m.GateAnswers(a) |
| + if a.Issued || a.State != Unissued { |
| + t.Fatalf("commitFirst=%v: issued=%v state=%s", commitFirst, a.Issued, a.State) |
| + } |
| + complete(t, m, alice, 1) |
| + must(t, m) |
| + } |
| +} |
| + |
| +// A discovery, or a crash, between the durable commit and the gate's |
| +// answer: the row is counted and the answer is unissued; after a crash it |
| +// is recovered-unknown. |
| +func TestBetweenCommitAndAnswer(t *testing.T) { |
| + m := New(1) |
| + m.Now = at(1, 10, 0) |
| + f := m.Build(alice) |
| + a := m.Register(f, alice) |
| + m.WriterCommits(a) |
| + held(t, m, alice, 1) // a durable unanswered row bars |
| + m.Discover(f, false) |
| + u := f.Uncertainties[0] |
| + if u.Counted[a.Token] == nil || !u.open() { |
| + t.Fatal("the durable unanswered row was not counted") |
| + } |
| + m.GateAnswers(a) |
| + if a.Issued || a.State != Unissued || u.open() { |
| + t.Fatalf("issued=%v state=%s open=%v", a.Issued, a.State, u.open()) |
| + } |
| + must(t, m) |
| + |
| + m = New(1) |
| + m.Now = at(1, 10, 0) |
| + f = m.Build(alice) |
| + a = m.Register(f, alice) |
| + m.WriterCommits(a) |
| + m.Crash(func(*Fleet) bool { return false }) |
| + m.Now = at(1, 10, 5) |
| + m.Recover() |
| + if a.State != RecoveredUnknown { |
| + t.Fatalf("after a crash between commit and answer: %s", a.State) |
| + } |
| + held(t, m, alice, 1) |
| + must(t, m) |
| +} |
| + |
| +// A read-back before the writer's handle is closed is not conclusive and |
| +// the model refuses it; after the close it decides either way, once. |
| +func TestReadBackOnlyAfterTheHandleCloses(t *testing.T) { |
| + m := New(1) |
| + m.Now = at(1, 10, 0) |
| + f := m.Build(alice) |
| + a := m.Register(f, alice) |
| + if m.ReadBack(a) { |
| + t.Fatal("read back while the writer runs") |
| + } |
| + m.WriterAmbiguous(a) |
| + if !m.ReadBack(a) || (a.State != Unissued && a.State != Cancelled) { |
| + t.Fatalf("after the handle closed: %s", a.State) |
| + } |
| + must(t, m) |
| +} |
| + |
| +// A send needs a durable, issued admission and a live helper; the model |
| +// records the attempt otherwise. |
| +func TestSendNeedsDurableIssuedAdmission(t *testing.T) { |
| + m := New(1) |
| + m.Now = at(1, 10, 0) |
| + f := m.Build(alice) |
| + a := m.Register(f, alice) |
| + m.Send(a) |
| + if a.SentAt != unset || len(m.Violations) != 1 { |
| + t.Fatalf("sent without a row: %d %v", a.SentAt, m.Violations) |
| + } |
| + m.Violations = nil |
| + m.WriterCommits(a) |
| + m.Send(a) |
| + if a.SentAt != unset || len(m.Violations) != 1 { |
| + t.Fatalf("sent without the answer: %d %v", a.SentAt, m.Violations) |
| + } |
| + m.Violations = nil |
| + m.GateAnswers(a) |
| + m.Send(a) |
| + if a.SentAt == unset || len(m.Violations) != 0 { |
| + t.Fatalf("not sent when issued: %d %v", a.SentAt, m.Violations) |
| + } |
| +} |
| + |
| +// The design's named test: a successor is barred by the predecessor's |
| +// unsettled admission from its construction, before any settlement |
| +// materialises anything, and through a closed, unacknowledged |
| +// intermediate fleet. |
| +func TestSuccessorBarredByPredecessorAdmission(t *testing.T) { |
| + m := New(1) |
| + m.Now = at(1, 9, 0) |
| + A := m.Build(alice) |
| + a := issue(t, m, A, alice) |
| + m.Now = at(2, 9, 0) |
| + B := m.Build(bob) |
| + held(t, m, bob, 2) |
| + m.Now = at(3, 9, 0) |
| + held(t, m, bob, 2, 3) // the following day too, while A's admission is unsettled |
| + must(t, m) |
| + if !m.StopHelper(B) || !m.Close(B) { |
| + t.Fatal("B did not close unopened") |
| + } |
| + m.Now = at(4, 9, 0) |
| + m.Build(carol) |
| + held(t, m, carol, 4) |
| + must(t, m) |
| + m.Now = at(5, 9, 0) |
| + finish(m, a) // no uncertainty on A: the barrier lifts and nothing is held |
| + if len(A.Uncertainties) != 0 { |
| + t.Fatal("an uncertainty on an unchanged fleet") |
| + } |
| + complete(t, m, bob, 2, 3) |
| + complete(t, m, carol, 4) |
| + must(t, m) |
| +} |
| + |
| +// The replay holds the discovery's own interval from the lower bound while |
| +// the uncertainty stays open: a request that completed before the change |
| +// was noticed, on the day before the counted admission, is held from the |
| +// replay on, not only when the uncertainty closes. |
| +func TestReplayHoldsTheLowerBoundWhileOpen(t *testing.T) { |
| + m := New(1) |
| + m.Now = at(1, 9, 0) |
| + f := m.Build(alice) |
| + m.Now = at(1, 23, 0) |
| + m.Look(f) |
| + m.Now = at(1, 23, 40) |
| + t0 := issue(t, m, f, alice) |
| + m.Now = at(1, 23, 45) |
| + m.Change(f) |
| + m.Now = at(1, 23, 50) |
| + finish(m, t0) |
| + complete(t, m, alice, 1) |
| + m.Now = at(2, 0, 30) |
| + issue(t, m, f, alice) // t1, counted, left unsettled |
| + m.Now = at(2, 1, 0) |
| + m.Discover(f, true) // the write fails: the latch bars from the clean look |
| + held(t, m, alice, 1, 2) |
| + m.Now = at(2, 1, 5) |
| + m.Replay(f) |
| + if !f.Uncertainties[0].open() { |
| + t.Fatal("closed with t1 unsettled") |
| + } |
| + held(t, m, alice, 1, 2) // day 1 through the replay's holds, not the barrier |
| + must(t, m) |
| +} |
| + |
| // Randomised schedules: every action the design names, in random |
| // interleavings over several days, with the invariants checked after each |
| // step and the end state checked at quiescence. |
| @@ -475,14 +666,19 @@ func runSchedule(seed int64, steps int) (err error) { |
| } |
| for i := 0; i < steps; i++ { |
| m.Advance(Time(m.rnd.Intn(90))) |
| - var regs, issued, inflight, recorderless []*Admission |
| + var regs, ambiguous, unanswered, held, inflight, recorderless []*Admission |
| for _, a := range m.Admissions { |
| switch { |
| - case a.State == Registered: |
| + case a.State == Registered && a.writerRunning: |
| regs = append(regs, a) |
| + case a.State == Registered && a.handleClosed: |
| + ambiguous = append(ambiguous, a) |
| + case a.State == Admitted && !a.answered: |
| + unanswered = append(unanswered, a) |
| case a.Issued && !a.State.Terminal(): |
| - issued = append(issued, a) |
| - if a.TransportDoneAt == unset { |
| + if a.SentAt == unset { |
| + held = append(held, a) |
| + } else if a.TransportDoneAt == unset { |
| inflight = append(inflight, a) |
| } |
| if a.RecorderDoneAt == unset { |
| @@ -493,7 +689,7 @@ func runSchedule(seed int64, steps int) (err error) { |
| if !m.Alive { |
| switch m.rnd.Intn(4) { |
| case 0: |
| - if a := pick(inflight); a != nil { |
| + if a := pick(append(inflight, held...)); a != nil { |
| m.SurvivingHelperTransport(a) |
| } |
| case 1: |
| @@ -504,15 +700,34 @@ func runSchedule(seed int64, steps int) (err error) { |
| continue |
| } |
| f := tip() |
| - switch m.rnd.Intn(20) { |
| + switch m.rnd.Intn(24) { |
| case 0, 1, 2, 3: |
| m.Register(f, f.Owners[m.rnd.Intn(len(f.Owners))]) |
| case 4, 5: |
| if a := pick(regs); a != nil { |
| - m.WriterReturns(a, []string{"commit", "commit", "commit", "fail", "ambiguous"}[m.rnd.Intn(5)]) |
| + switch m.rnd.Intn(5) { |
| + case 0: |
| + m.WriterFails(a) |
| + case 1: |
| + m.WriterAmbiguous(a) |
| + default: |
| + m.WriterCommits(a) |
| + } |
| + } |
| + case 20: |
| + if a := pick(unanswered); a != nil { |
| + m.GateAnswers(a) |
| + } |
| + case 21: |
| + if a := pick(ambiguous); a != nil { |
| + m.ReadBack(a) |
| + } |
| + case 22, 23: |
| + if a := pick(held); a != nil { |
| + m.Send(a) |
| } |
| case 6: |
| - if a := pick(regs); a != nil { |
| + if a := pick(append(regs, unanswered...)); a != nil { |
| m.BudgetExpires(a) |
| } |
| case 7, 8: |
| @@ -548,7 +763,12 @@ func runSchedule(seed int64, steps int) (err error) { |
| } |
| } |
| case 14: |
| - m.HelperDies(m.Fleets[m.rnd.Intn(len(m.Fleets))], m.rnd.Intn(3) == 0) |
| + g := m.Fleets[m.rnd.Intn(len(m.Fleets))] |
| + if g.helperAlive { |
| + m.HelperExits(g, m.rnd.Intn(3) == 0) |
| + } else { |
| + m.DrainHelper(g) |
| + } |
| case 15: |
| g := m.Fleets[m.rnd.Intn(len(m.Fleets))] |
| m.StopHelper(g) |
| @@ -562,12 +782,7 @@ func runSchedule(seed int64, steps int) (err error) { |
| } |
| case 18: |
| if f.State != Open || m.rnd.Intn(3) == 0 { |
| - n := 1 + m.rnd.Intn(2) |
| - var os_ []Owner |
| - for k := 0; k < n; k++ { |
| - os_ = append(os_, owners[m.rnd.Intn(len(owners))]) |
| - } |
| - m.Build(os_...) |
| + m.Build(owners[m.rnd.Intn(len(owners))]) // one owner per fleet under owner scope |
| } |
| case 19: |
| if m.rnd.Intn(6) == 0 { |
| @@ -586,13 +801,27 @@ func runSchedule(seed int64, steps int) (err error) { |
| m.Recover() |
| } |
| for _, a := range m.Admissions { |
| - if a.State == Registered { |
| - m.WriterReturns(a, "commit") |
| + switch { |
| + case a.State == Registered && a.writerRunning: |
| + m.WriterCommits(a) |
| + case a.State == Registered && a.handleClosed: |
| + m.ReadBack(a) |
| + } |
| + if a.State == Admitted && !a.answered { |
| + m.GateAnswers(a) |
| } |
| } |
| m.Advance(1) |
| + for _, g := range m.Fleets { |
| + if !g.helperAlive { |
| + m.DrainHelper(g) |
| + } |
| + } |
| for _, a := range m.Admissions { |
| if a.Issued && !a.State.Terminal() { |
| + if a.SentAt == unset && a.Fleet.helperAlive { |
| + m.Send(a) |
| + } |
| m.TransportDone(a) |
| if a.RecorderDoneAt == unset { |
| if a.RecorderStartedAt == unset && !a.Fleet.guardClosed { |