diff --git a/docs/long-turn-memory.md b/benchmarks/long-turn-memory.md similarity index 100% rename from docs/long-turn-memory.md rename to benchmarks/long-turn-memory.md diff --git a/src/acp/server.zig b/src/acp/server.zig index fdc8e0cf6..294003e99 100644 --- a/src/acp/server.zig +++ b/src/acp/server.zig @@ -877,7 +877,7 @@ fn resolveSubagentAuthority( } /// Joins the child threads before the session they append to can close -/// (`tla/Wiring.tla` ParentOutlivesChildren). +/// (`src/core/session_manager/tla/Wiring.tla` ParentOutlivesChildren). pub fn disableSubagentHost(state: *ServerState) void { if (state.subagent_host) |host| { host.deinit(); diff --git a/src/core/app/app_session_runtime.zig b/src/core/app/app_session_runtime.zig index 04a0ccbed..36f130d82 100644 --- a/src/core/app/app_session_runtime.zig +++ b/src/core/app/app_session_runtime.zig @@ -3824,7 +3824,7 @@ pub fn Runtime(comptime App: type) type { } /// Stops the subagent host, joining its child threads, before the - /// session they append to can close (`tla/Wiring.tla` + /// session they append to can close (`src/core/session_manager/tla/Wiring.tla` /// ParentOutlivesChildren). pub fn disableSubagentHost(app: *App) void { if (app.session_persistence.subagent_host) |host| { diff --git a/src/core/indexer/git_index.zig b/src/core/indexer/git_index.zig index 122a2d127..692e36229 100644 --- a/src/core/indexer/git_index.zig +++ b/src/core/indexer/git_index.zig @@ -9,7 +9,7 @@ const io_mod = @import("../shared/io.zig"); const Allocator = std.mem.Allocator; -/// D7: the index is never read beyond this size. +/// The index is never read beyond this size. const max_index_bytes: usize = 128 * 1024 * 1024; const mode_type_mask: u32 = 0o170000; diff --git a/src/core/indexer/ignore.zig b/src/core/indexer/ignore.zig index d49ebc4e8..2de15dab8 100644 --- a/src/core/indexer/ignore.zig +++ b/src/core/indexer/ignore.zig @@ -8,7 +8,7 @@ const wildmatch = @import("wildmatch.zig"); const Allocator = std.mem.Allocator; -/// Largest pattern file read, per source (D7). +/// Largest pattern file read, per source. pub const max_pattern_file_bytes: usize = 1024 * 1024; const Pattern = struct { diff --git a/src/core/indexer/scan.zig b/src/core/indexer/scan.zig index a8b7569b1..363ab1b00 100644 --- a/src/core/indexer/scan.zig +++ b/src/core/indexer/scan.zig @@ -29,12 +29,12 @@ pub const Kind = tree_mod.Kind; pub const Entry = tree_mod.Entry; pub const Options = struct { - /// D7: at most this many files are returned. Folder rows do not count; + /// At most this many files are returned. Folder rows do not count; /// the collection limit (`collect_factor`) bounds them. candidate_cap: usize = 100_000, max_path_bytes: usize = 2048, /// Folder and file names skipped outside repositories and below an - /// ignored root (D4, U3). Never applied inside a repository. + /// ignored root. Never applied inside a repository. skipped_names: []const []const u8 = &default_skipped_names, max_workers: usize = 8, }; @@ -634,7 +634,7 @@ fn entryLessThan(_: void, a: Entry, b: Entry) bool { } /// Length of the sorted prefix that holds the first `cap` files, or null when -/// `entries` has no more than `cap` files. Folder rows do not count (D7). +/// `entries` has no more than `cap` files. Folder rows do not count. fn capCut(entries: []const Entry, cap: usize) ?usize { var files: usize = 0; for (entries, 0..) |entry, index| { diff --git a/src/core/indexer/tla/Refresh.tla b/src/core/indexer/tla/Refresh.tla new file mode 100644 index 000000000..bbb5b3dbf --- /dev/null +++ b/src/core/indexer/tla/Refresh.tla @@ -0,0 +1,74 @@ +-------------------------------- MODULE Refresh -------------------------------- +EXTENDS Naturals, Sequences +CONSTANTS MaxSteps, Guarded +Files == {"a.txt", "b.txt"} +VARIABLES fs, tick, stamp, ignoreB, ignoreEpoch, knownStamp, knownIgnore, + reusable, snapshot, phase, beforeStamp, beforeIgnore, beforeTick, + listed, published, history +vars == <> +Visible == IF ignoreB THEN fs \ {"b.txt"} ELSE fs +Init == /\ fs = {} /\ tick = 0 /\ stamp = 0 + /\ ignoreB = FALSE /\ ignoreEpoch = 0 + /\ knownStamp = 0 /\ knownIgnore = 0 /\ reusable = FALSE + /\ snapshot = {} /\ phase = "idle" /\ beforeStamp = 0 + /\ beforeIgnore = 0 /\ beforeTick = 0 /\ listed = {} + /\ published = FALSE /\ history = <<>> +Edit(p) == /\ fs' = IF p \in fs THEN fs \ {p} ELSE fs \cup {p} + /\ stamp' = tick /\ published' = FALSE + /\ history' = Append(history, "Edit:" \o p) + /\ UNCHANGED <> +Tick == /\ tick < 2 /\ tick' = tick + 1 /\ published' = FALSE + /\ history' = Append(history, "Tick") + /\ UNCHANGED <> +ChangeIgnore == /\ ignoreB' = ~ignoreB /\ ignoreEpoch' = ignoreEpoch + 1 + /\ published' = FALSE + /\ history' = Append(history, "ChangeIgnore") + /\ UNCHANGED <> +Reuse == /\ phase = "idle" /\ stamp = knownStamp + /\ (~Guarded \/ (reusable /\ stamp < tick /\ + ignoreEpoch = knownIgnore)) + /\ published' = TRUE /\ history' = Append(history, "Reuse") + /\ UNCHANGED <> +Begin == /\ phase = "idle" /\ phase' = "listing" + /\ beforeStamp' = stamp /\ beforeIgnore' = ignoreEpoch + /\ beforeTick' = tick /\ published' = FALSE + /\ history' = Append(history, "Begin") + /\ UNCHANGED <> +List == /\ phase = "listing" /\ phase' = "validate" /\ listed' = Visible + /\ published' = FALSE /\ history' = Append(history, "List") + /\ UNCHANGED <> +Commit == LET valid == ~Guarded \/ (stamp = beforeStamp /\ + ignoreEpoch = beforeIgnore /\ + stamp < beforeTick) + IN /\ phase = "validate" /\ phase' = "idle" + /\ snapshot' = IF valid THEN listed ELSE snapshot + /\ knownStamp' = IF valid THEN stamp ELSE knownStamp + /\ knownIgnore' = IF valid THEN ignoreEpoch ELSE knownIgnore + /\ reusable' = IF valid THEN TRUE ELSE reusable + /\ published' = valid /\ history' = Append(history, "Commit") + /\ UNCHANGED <> +Next == /\ Len(history) < MaxSteps + /\ ((\E p \in Files : Edit(p)) \/ Tick \/ ChangeIgnore \/ + Reuse \/ Begin \/ List \/ Commit) +Spec == Init /\ [][Next]_vars +TypeOK == /\ fs \subseteq Files /\ snapshot \subseteq Files + /\ listed \subseteq Files /\ tick \in 0..2 /\ stamp \in 0..2 + /\ ignoreB \in BOOLEAN /\ published \in BOOLEAN + /\ reusable \in BOOLEAN /\ phase \in {"idle", "listing", "validate"} + /\ ignoreEpoch \in 0..MaxSteps /\ Len(history) <= MaxSteps +NoStalePublication == published => snapshot = Visible +============================================================================= diff --git a/src/core/indexer/tla/RefreshWitness.tla b/src/core/indexer/tla/RefreshWitness.tla new file mode 100644 index 000000000..45db99729 --- /dev/null +++ b/src/core/indexer/tla/RefreshWitness.tla @@ -0,0 +1,21 @@ +---------------------------- MODULE RefreshWitness ---------------------------- +\* Each invariant claims a reuse path cannot happen. TLC's counterexample is +\* then the shortest trace that exercises it, which the real replay runs. +EXTENDS Refresh +Before(a, b) == \E i, j \in 1..Len(history) : i < j /\ history[i] \in a /\ history[j] = b +NoReuse == ~Before({"Begin"}, "Reuse") +NoReuseAfterEdit == ~Before({"Edit:a.txt", "Edit:b.txt"}, "Reuse") +\* Real files have only times, so an ignore change counts once a Tick passes; +\* b.txt exists first so the reused snapshot must reflect the new rule. +NoReuseAfterIgnore == ~\E i, k, m, j \in 1..Len(history) : + /\ i < k /\ k < m /\ m < j + /\ history[i] = "Edit:b.txt" /\ history[k] = "ChangeIgnore" + /\ history[m] = "Tick" /\ history[j] = "Reuse" +\* A change after a reuse: the real code must notice it at the next check. +NoEditAfterReuse == ~\E i, j \in 1..Len(history) : + i < j /\ history[i] = "Reuse" /\ history[j] \in {"Edit:a.txt", "Edit:b.txt"} +NoIgnoreChangeAfterReuse == ~\E i, k, j \in 1..Len(history) : + /\ i < k /\ k < j + /\ history[i] = "Edit:b.txt" /\ history[k] = "Reuse" + /\ history[j] = "ChangeIgnore" +============================================================================= diff --git a/src/core/indexer/tla/refresh-mutation.cfg b/src/core/indexer/tla/refresh-mutation.cfg new file mode 100644 index 000000000..7260a92ff --- /dev/null +++ b/src/core/indexer/tla/refresh-mutation.cfg @@ -0,0 +1,4 @@ +SPECIFICATION Spec +CONSTANTS MaxSteps = 6 + Guarded = FALSE +INVARIANTS TypeOK NoStalePublication diff --git a/src/core/indexer/tla/refresh-simulation.cfg b/src/core/indexer/tla/refresh-simulation.cfg new file mode 100644 index 000000000..1cffe66e4 --- /dev/null +++ b/src/core/indexer/tla/refresh-simulation.cfg @@ -0,0 +1,3 @@ +SPECIFICATION Spec +CONSTANTS MaxSteps = 10 Guarded = TRUE +INVARIANTS TypeOK NoStalePublication diff --git a/src/core/indexer/tla/refresh-witness-NoEditAfterReuse.cfg b/src/core/indexer/tla/refresh-witness-NoEditAfterReuse.cfg new file mode 100644 index 000000000..88bfca7ed --- /dev/null +++ b/src/core/indexer/tla/refresh-witness-NoEditAfterReuse.cfg @@ -0,0 +1,3 @@ +SPECIFICATION Spec +CONSTANTS MaxSteps = 10 Guarded = TRUE +INVARIANTS TypeOK NoStalePublication NoEditAfterReuse diff --git a/src/core/indexer/tla/refresh-witness-NoIgnoreChangeAfterReuse.cfg b/src/core/indexer/tla/refresh-witness-NoIgnoreChangeAfterReuse.cfg new file mode 100644 index 000000000..d41e69e7f --- /dev/null +++ b/src/core/indexer/tla/refresh-witness-NoIgnoreChangeAfterReuse.cfg @@ -0,0 +1,3 @@ +SPECIFICATION Spec +CONSTANTS MaxSteps = 10 Guarded = TRUE +INVARIANTS TypeOK NoStalePublication NoIgnoreChangeAfterReuse diff --git a/src/core/indexer/tla/refresh-witness-NoReuse.cfg b/src/core/indexer/tla/refresh-witness-NoReuse.cfg new file mode 100644 index 000000000..20c00173a --- /dev/null +++ b/src/core/indexer/tla/refresh-witness-NoReuse.cfg @@ -0,0 +1,3 @@ +SPECIFICATION Spec +CONSTANTS MaxSteps = 10 Guarded = TRUE +INVARIANTS TypeOK NoStalePublication NoReuse diff --git a/src/core/indexer/tla/refresh-witness-NoReuseAfterEdit.cfg b/src/core/indexer/tla/refresh-witness-NoReuseAfterEdit.cfg new file mode 100644 index 000000000..16dcb024b --- /dev/null +++ b/src/core/indexer/tla/refresh-witness-NoReuseAfterEdit.cfg @@ -0,0 +1,3 @@ +SPECIFICATION Spec +CONSTANTS MaxSteps = 10 Guarded = TRUE +INVARIANTS TypeOK NoStalePublication NoReuseAfterEdit diff --git a/src/core/indexer/tla/refresh-witness-NoReuseAfterIgnore.cfg b/src/core/indexer/tla/refresh-witness-NoReuseAfterIgnore.cfg new file mode 100644 index 000000000..ce1208225 --- /dev/null +++ b/src/core/indexer/tla/refresh-witness-NoReuseAfterIgnore.cfg @@ -0,0 +1,3 @@ +SPECIFICATION Spec +CONSTANTS MaxSteps = 10 Guarded = TRUE +INVARIANTS TypeOK NoStalePublication NoReuseAfterIgnore diff --git a/src/core/indexer/tla/refresh.cfg b/src/core/indexer/tla/refresh.cfg new file mode 100644 index 000000000..91f51f117 --- /dev/null +++ b/src/core/indexer/tla/refresh.cfg @@ -0,0 +1,4 @@ +SPECIFICATION Spec +CONSTANTS MaxSteps = 6 + Guarded = TRUE +INVARIANTS TypeOK NoStalePublication diff --git a/src/core/indexer/tree.zig b/src/core/indexer/tree.zig index 7c7966ea7..3d86ed2ce 100644 --- a/src/core/indexer/tree.zig +++ b/src/core/indexer/tree.zig @@ -4,7 +4,7 @@ //! its times are older than the scan's start by the granularity margin, so a //! change in the same clock tick as the scan, which a later stamp comparison //! could not see, always forces a new scan. This is the reuse certificate the -//! refresh model (Refresh.tla) requires. +//! refresh model (`tla/Refresh.tla`) requires. const std = @import("std"); const io_mod = @import("../shared/io.zig"); diff --git a/src/core/mcp_host/runtime.zig b/src/core/mcp_host/runtime.zig index d6d9e9bbc..75c9e3fb0 100644 --- a/src/core/mcp_host/runtime.zig +++ b/src/core/mcp_host/runtime.zig @@ -1160,7 +1160,7 @@ pub const Runtime = struct { } /// Permission is fx's tool admission, before the call reaches the - /// runtime, and only the runtime calls the engine (D6). + /// runtime, and only the runtime calls the engine. fn allow(_: *anyopaque, _: []const u8, _: []const u8, _: ?[]const u8) bool { return true; } diff --git a/src/core/session/session_adapter.zig b/src/core/session/session_adapter.zig index b25e558a2..4d783bdc7 100644 --- a/src/core/session/session_adapter.zig +++ b/src/core/session/session_adapter.zig @@ -18,7 +18,7 @@ //! ACP client's prompt and tool identities are settings (D46); hosted //! terminal state lives in `~/.fx/terminal/{id}/` (D45). An older session //! with a `~/.fx/session-files/{id}/` side folder moves on its first -//! writable open (D47, `tla/MoveSideFiles.tla`). +//! writable open (D47, `src/core/session_manager/tla/MoveSideFiles.tla`). const std = @import("std"); const testing_allocator = @import("../shared/testing_allocator.zig"); @@ -1123,7 +1123,7 @@ pub const Session = struct { } /// Closes the session and frees the adapter. Every child thread of this - /// session must have joined (`tla/Wiring.tla` ParentOutlivesChildren). + /// session must have joined (`src/core/session_manager/tla/Wiring.tla` ParentOutlivesChildren). /// A copy of its capability that a background reader still holds keeps /// reading, and stores nothing more (D44). pub fn close(self: *Session) void { @@ -1782,11 +1782,12 @@ pub const Session = struct { // -- the move off the side folder (D47) ----------------------------------- - /// Makes an older session one manager folder (D47, `tla/MoveSideFiles.tla`) - /// on its first writable open, then loads the map its old handles resolve - /// through. Every body in the side folder becomes a blob, the map from - /// each old name to its blob is one more blob, and one batch records the - /// map, every moved blob, and the client's settings from the old files. + /// Makes an older session one manager folder (D47, + /// `src/core/session_manager/tla/MoveSideFiles.tla`) on its first writable + /// open, then loads the map its old handles resolve through. Every body + /// in the side folder becomes a blob, the map from each old name to its + /// blob is one more blob, and one batch records the map, every moved + /// blob, and the client's settings from the old files. /// Then the terminal folder moves to `~/.fx/terminal/{id}` and the side /// folder goes. Each step can be repeated, so a crash at any point /// redoes the move on the next open. @@ -1813,7 +1814,7 @@ pub const Session = struct { } /// Every step of the move but the side folder's removal, in the order - /// `tla/MoveSideFiles.tla` checks; returns how many bodies moved. + /// `src/core/session_manager/tla/MoveSideFiles.tla` checks; returns how many bodies moved. fn moveOut(self: *Session, side: *io_mod.VerifiedDir) !usize { var scratch = std.heap.ArenaAllocator.init(self.alloc); defer scratch.deinit(); diff --git a/src/core/session_manager/api.zig b/src/core/session_manager/api.zig index c257cb216..13b6e9392 100644 --- a/src/core/session_manager/api.zig +++ b/src/core/session_manager/api.zig @@ -3,7 +3,7 @@ //! //! This file (L4) is the only public root; fx imports it and nothing else. //! A process creates one `Manager` with `init`, which does no disk I/O. -//! Thirteen operations cover every host (docs/session-manager/system-design.md +//! Thirteen operations cover every host (`system-design.md` //! "API"), plus `verify` and `rebuild` for doctor: //! //! openNew openResume openFork openImport -> Session diff --git a/src/core/session_manager/system-design.md b/src/core/session_manager/system-design.md new file mode 100644 index 000000000..f255c7fda --- /dev/null +++ b/src/core/session_manager/system-design.md @@ -0,0 +1,1353 @@ +# Session Manager (Sessions v2) Design And Contracts + +This document is canonical for the v2 format, API, contracts and decisions, +and `tla/` models each step. It was written before the code, so a name that +does not cite fx source was a proposal. Decisions D1 to D19 were settled on +2026-09-27 (Decisions section). + +## Intent + +**Outcome:** one self-contained Zig module, the session-manager, owns +everything about fx sessions: +- storage; +- the live-session lifecycle: create, append, resume, fork, close, delete; +- crash recovery and listing. + +Each session is one append-only JSONL log. The interactive app, `fx ask`, +ACP, subagents and the wasm SDK reach sessions only through its API. It is +built and proven standalone, then wired into fx next to v1, then replaces +v1. + +**Constraints and non-goals** that shape this design: +- Zig and the standard library only; +- no I/O until the first session call, because of the 2 ms startup budget; +- Linux and macOS; +- the host thread models; +- no daemon and no second writing process. + +## Repository Evidence + +All paths are relative to fx at `46408935b`. + +- `src/core/session/session_store.zig::Store` (line 526) is the front desk. Its + 47 public methods open, list, delete and migrate; none of them appends. +- `src/core/session/session_log.zig::LoadedWritableSession.appendEvent` + (line 3353) is the only writer. It routes six update kinds to four files. +- `src/core/session/session_log.zig::ConversationWriter.writePrepared` + (line 537) does a positional write plus a plain `fsync` on every append. +- `src/core/session/session_log.zig::ConversationWriter.init` (line 150) + cuts a torn frame and discards an unfinished turn on open. +- `src/core/session/session_event.zig::Envelope` (line 847) and + `src/core/session/session_event.zig::ConversationEvent` (line 174) are + today's line envelope and history event kinds. +- `src/core/agent/runtime/deps.zig::AgentRuntimeDeps` (line 189) holds the + persistence callbacks the agent loop uses. +- `src/core/agent/runtime/orchestrator.zig:3857` (`persistRecoveryCheckpoint`) + rebuilds the whole current turn at each of 13 step boundaries. +- The four host copies of the save logic: + `src/core/app/app_session_runtime.zig::Persistence` (line 1210), + `src/core/cli/cli_ask.zig:3102`, `src/acp/prompt.zig:2143`, + `src/core/subagent/execution.zig:509`. +- `src/core/app/app_session_runtime.zig:2604` and `:1754` make `-c` remember + only the interactive app's sessions; `session_store.zig:1168` resolves + `--resume last` as the newest session in the workspace from any host. +- `src/core/session/session_log.zig:4060` shows today's atomic publish. +- `src/core/hosts/runtime_profile.zig::native` and `::wasm` are the capability + profiles; wasm sets `js_host_sessions`. +- `sdk/fx-sdk.js:922` shows the embedder-supplied `sessionStore` with + `load`, `commit(id, bytes, expectedRevision)`, `list` and `remove`; it + backs `src/core/session/js_host_session_store.zig`. +- `src/acp/sessions.zig:45` (`handleNewLibfxSession`): the N-API host keeps + sessions in memory only. +- `build.zig.zon` has no dependencies. +- End-to-end coverage: `tests/e2e/session-recovery.test.ts`, + `tests/e2e/tui-resume-brutal.test.ts`, + `tests/e2e/tui-interrupt-recovery.test.ts`, `tests/e2e/acp.test.ts`, + `tests/e2e/cli.test.ts`, `sdk/tests/test-term-session-resume.mjs`. + +## Current System And Contracts + +**Current flow and owner:** the agent loop calls one of four host callbacks. +The host's own copy of the save logic calls `LoadedWritableSession`, which +writes five files. wasm writes whole snapshots through the embedder's +`sessionStore`. `Store` owns opening, listing and deleting; nothing owns the +live session as a whole. + +**Binding contracts v2 must keep:** +- **One writer.** One writing process per session. A contender waits up to 2 s, + then gets Busy. +- **Crash safety.** Committed turns survive an fx crash. An unfinished turn is + never silently continued after an unclean exit, and asking stays sticky + until the turn is resolved (`session_log.zig:38` comment). +- **Resume by id, by `--resume last` and through the picker.** `--resume last` + means the newest session of any host. +- **`-c` returns to the session the interactive app last opened.** `fx ask` + and ACP runs never change it. +- **Portability.** Sessions are global and portable, and each tracks + `workspace_root` (fx `AGENTS.md`, Configuration and State). +- **Children.** Child sessions stay out of discovery and cannot be resumed + directly. The parent collects a child's result by work id. +- **What survives resume.** Preferences, title, permissions, usage and the + conversation language. +- **wasm embedders' `sessionStore` API keeps working.** +- **Private files.** Session folders are created `0700`, files `0600` and + blobs `0400` (D49), and + paths are opened without following symlinks, as v1 does + (`session_log.zig:25`, `io_mod.VerifiedDir`). Sessions contain code and + secrets. +- **Startup stays within the per-command budget.** + +## Proposed Delta + +**Approach:** add one module that owns session storage and the live-session +lifecycle. +- A session is a folder with `log.jsonl`, `lock` and `blobs/`. +- State is the fold of the log. +- The manager assigns `seq`, enforces the turn rules and takes every lock. +- fx reaches it through one adapter file. +- v1 and v2 run side by side behind a backend switch until v1 is removed. + +**Preserved:** every binding contract above, the host entry points, the +`sessionStore` SDK API, and the agent loop's existing callbacks. + +**Changed:** +- **One log holds everything:** preferences, title, permissions, usage, + workspace, conversation language, fx recovery details and children. v1 spread these over five + files plus a child registry. +- **Streamed turns (D10).** Each completed piece of a turn is appended as it + happens, through one new agent-loop callback, `append_turn_piece` (D12). + The recovery checkpoint shrinks to fx's small recovery details. +- **No truncation (D1).** An unfinished turn gets `turn_interrupted` on + reopen instead of being cut. `recovery.json`, `recovery.asked` and + `owner.live` go away; flock is the only liveness signal. +- **Sync at durability points only (D3).** A plain `fsync` on every platform, + and no fsync per line. +- **Lazy creation (D2).** A session folder is created at the first turn. There + is no startup I/O and no delete-if-empty logic. Reads create nothing: with + no root, `open(.resume)`, `read`, `get_blob` and `verify` return NotFound + and `list` returns an empty page. +- **Checksums (D4).** Every line ends with a CRC32C field. +- **Snapshots (D7).** Snapshots after each compaction and every ~64 KB bound + resume cost. The transcript is paged on demand. +- **Blobs (D6).** Large bodies move from fx's four stores into per-session + blobs. +- **Index.** `index.jsonl`, derived and rebuildable, replaces + `.resume-catalog`. It records host and open time, which keeps `-c` distinct + (D11). +- **Children in the parent log.** They replace `children.json`, + `children.lock`, `owner.json`, `control.json` and `relationship-index.bin`. +- **Fork is new** and starts only at turn boundaries (D5). +- **v1 conversion (D8).** A one-time background conversion carries every v1 + session into v2. +- **wasm (D9).** wasm persists through a JS-host storage level (L0) over the + unchanged `sessionStore`. +- **Hosts hold no session locks.** The four host copies of the save logic + collapse into the adapter. +- **Terminal state leaves the session folder (D13).** Hosted terminal state + moves to an fx-owned `~/.fx/terminal/{session-id}/`, like Unix + `/var/lib/{service}`. The terminal store keeps its own recovery protocol; + only its base path changes. +- **Diagnostics through the caller (D14).** The manager reports every repair + or drop through one optional callback; the adapter forwards it to + `debug_trace`. +- **Session commands keep working (D15).** + - `fx session recover` forks at the last good turn. + - `fx session migrate` runs the conversion. + - `fx sessions`, `fx session last|{id}` and doctor map onto `list`, `read`, + `verify` and `rebuild`. + +### On-disk layout + +```text +~/.fx/sessions/v2/ inside v1's folder, which v1 skips (D19) + index.jsonl session list, one line per change, derived + index.lock flock held while appending to or rewriting the index + .tmp/ staging for new, forked and imported sessions + .trash/ sessions being deleted + {id}/ + log.jsonl the session; append-only; the only source of truth + lock empty file held with flock by the writing process + blobs/{sha256} large bodies, content-addressed, immutable +``` + +On wasm, the embedder's `sessionStore` holds each session's `log.jsonl` +bytes under its id, and the manager keeps the index in memory, rebuilt from +`list()`. Where blobs live on wasm is still open (inline in the log, or as +separate `sessionStore` entries), and the format gains nothing for it until +that is settled. + +### Line format (persisted contract) + +One event is one JSON object followed by `\n`. The last field is always +`crc`: + +```text +{"v":1,"seq":7,"ts":1727400000000,"kind":"turn_committed","turn":1,"crc":"1a2b3c4d"} +``` + +- **Envelope:** `v` (format version), `seq`, `ts` (ms), `kind` and `crc` + belong to the manager. Kind-specific fields sit between `kind` and `crc`. + `data` holds fx content, which the manager stores but never interprets. +- **`crc`:** CRC32C, as 8 lowercase hex digits, of the exact bytes of the line + before `,"crc":"`. The line stays valid JSON, so `jq`, `grep` and `tail` + keep working. +- **`seq`:** starts at 1 on `session_created` and goes up by exactly 1 per + line. Only the manager assigns it. +- **`ts`:** stamped by the manager. The one exception is a Session opened + with `.import`, which keeps each event's original `ts`. +- **Validity:** a line counts only when it ends with `\n`, parses, and its + `crc` matches. + - A final line that is incomplete or fails those checks is torn and gets + cut on open. That is the only shape a crash can leave. + - A failing line before the final one, or a `seq` gap anywhere, makes the + session readable only up to the last good line. A line with a good `crc` + is never cut. Nothing is ever skipped silently. +- **Compatibility:** unknown kinds are skipped by the fold. A `v` newer than + the manager supports opens read-only. +- **Size:** each line has a hard cap of 4 MiB, newline included. The + adapter moves bodies above a smaller threshold into blobs. + +| Kind | Fields | Written by | Rule | +|---|---|---|---| +| `session_created` | `workspace`, `role` (`root` or `child`), `host`, `parent` (child), `forked_from` (fork: `id`, `seq`) | manager | Always line 1; written with the first turn | +| `turn_started` | `turn` | host call; the manager assigns the number | Only when no turn is open | +| `item` | `turn`, `type`, `data`, `blobs` (optional hashes) | host, through `append_turn_piece` | Only inside an open turn; one line per completed piece, never per token; `type` is required, 1 to 32 of `a-z`, `0-9` and `_`, named by fx (D17); every blob named in `blobs` must already exist in the session | +| `compacted` | `turn` (inside a turn), `data` | host | Allowed at any time; a snapshot follows | +| `turn_committed` | `turn` | host | Ends the open turn | +| `turn_interrupted` | `turn`, `reason`: `cancel` or `failed` (host), `closed` or `crash` (manager) | host, or the manager on close or reopen | Ends the open turn (D21) | +| `set` | `key` (`prefs`, `title`, `permissions`, `usage`, `workspace`, `language`), `value` | host | Allowed at any time; the newest per key wins; before the first turn it is held in memory | +| `child_spawned` | `child`, `work_id`, `data` (optional, at most 4 KiB) | host (parent) | A new spawn, or a new work id for a persistent child; refused while that child has unfinished work (D22) | +| `child_finished` | `child`, `work_id`, `outcome` (`ok`, `failed`, `cancelled`, `interrupted`, `lost`), `data` (optional, at most 4 KiB) | host, or the manager on parent reopen (`interrupted`, `lost`) | That work item is the child's unfinished one; hosts never write `lost` (D22) | +| `snapshot` | `covers_seq`, `state`, `compaction_offset` | manager, after each `compacted` and whenever ~64 KB of log was written since the previous snapshot | Derived cache, never needed for correctness; skipped, with a diagnostic, when the state does not fit in one line | +| `closed` | none | manager on `close()` | Marks a clean exit | + +The values of `prefs`, `permissions` and `usage`, and every `data` payload, +are JSON whose shape fx owns. `title` and `workspace` are strings that the +manager also puts in the index. Token counters (input, output, cost) live +inside fx's `usage` value; the index and `fx sessions` do not list them +(D25). + +### Fold (how state is computed) + +| State field | Comes from | +|---|---| +| identity (`id`, `role`, `host`, `parent`, `forked_from`, initial `workspace`) | line 1 | +| `open_turn` | a `turn_started` with no end line yet | +| turn counts | end lines, split by committed or interrupted | +| `last_interrupted` | newest `turn_interrupted`, with `reason` | +| `prefs`, `title`, `permissions`, `usage`, current `workspace`, `language` | newest `set` per key | +| `children` | one record per child, in first-spawn order, counting only lines after `forked_from.seq`: the newest `work_id`, whether that work is unfinished, the newest finished work's `outcome`, the newest `child_spawned` and `child_finished` `data`, and the seq of the child's newest line, which fx uses as a generation (D22) | +| `last_compaction_seq`, `compaction_offset` | newest `compacted` and its byte offset; fx's `data` may keep a tail of earlier lines, which the adapter reads back to | +| `clean_exit` | the last line is `closed` | +| `last_seq` | last good line | +| `created_ms`, `updated_ms` | `ts` of line 1 and of the newest line; 0 before the first turn (D20) | + +A snapshot carries this state without the identity fields and the two +times: the session reads both from the log it opens and updates them on +every write, so they are not folded. Its +`compaction_offset` is a byte offset, and a fork's line 1 has a different +length, so a fork encodes each copied snapshot again from its own fold, with +the same `seq`. Folding from line 1 and folding from the newest snapshot must +give identical state (`tla/ResumeSnapshot.tla`). + +### API (the only boundary fx sees) + +The manager is created once per process with +`init{root, backend: posix or js_host, diagnostics}`. `diagnostics` is an +optional callback (D14). It receives a typed event, with a kind, a session id +and numbers such as the bytes cut or the seq, for every repair or drop: +- a torn or bad-checksum final line cut; +- a session opened read-only after a damaged middle line; +- held settings discarded at a close before the first turn; +- an index self-heal; +- a rebuild sweep; +- a snapshot skipped because the state does not fit in one line; +- a converter skip or failure. + +With no callback, the cost is one null check. + +Thirteen operations: + +```text +open(.new{workspace, role, parent, host, id}) -> Session no disk I/O until the first turn; `id` for a child only (D34) +open(.resume{target, workspace, parent, host, lock_wait_ms}) + -> Session Busy, NotFound, ChildSession, Corrupt, UnsupportedVersion + target: id | .last (newest updated, any host) | .last_opened{host} (newest opened by that host) + lock_wait_ms: this open's wait for the writer lock; unset uses the manager's (D38) +open(.fork{source, at_turn, workspace, host}) -> Session new id at a turn boundary; NotFound, InvalidForkPoint +open(.import{id, workspace, role, parent, created_ts}) + -> Session one-time v1 conversion only; Exists if the id is taken +append(session, events) -> last seq InvalidTransition, SessionClosed, TooLarge, Io +put_blob(session, bytes) -> hash returns once the blob is durable; InvalidTransition before the first turn, TooLarge, Io +state(session) -> State owned copy taken under the mutex, no I/O +read(id, from, direction, limit) -> lines lock-free; forward from a seq, or backward from the end +session.read(from, direction, limit) -> lines the open session's own log: no open; empty before the first turn; SessionClosed +get_blob(id, hash) -> bytes NotFound +peek(id) -> State lock-free: line 1, the newest snapshot and the tail, as the catalog reads it (D37) +list(workspace or all, cursor, limit) -> summaries reads the index only +close(session) closed line, fsync, index, unlock +delete(id) Busy if open anywhere; removes owned children +``` + +- **Threads:** a `Session` is safe to use from any thread, and each call is + atomic relative to the others on the same session. +- **Batches:** `append` writes a batch with one `write()`, and does an + `fsync` before returning if the batch holds a durable-class event. +- **Child sessions:** resuming a child requires its `parent`; otherwise the + result is ChildSession. +- **Host names:** `host` is one of `app`, `ask`, `acp`, `sdk` or `child`. + `-c` maps to `.last_opened{host: app}`. `--resume last` maps to `.last`. + +### fx mapping (the adapter's side) + +The pre-wiring API check (2026-09-27) traced every host's persistence +through the API above. These rules live in `session_adapter.zig`, not in the +manager: +- **Item types and data:** each completed piece is one `item`, and its + `data` comes from v1's piece codec (`encodeConversationFrame`, + `src/core/session/session_event.zig` lines 439 to 482). The types are + `user`, `assistant`, `tool_call`, `tool_result`, `steering`, `turn_end` + (files and turn summary), `interruption` (reason detail, partial text, + command refs, origin), `recovery` and `continues`. +- **Recovery:** the agent loop's checkpoint becomes a small `recovery` item + (cause, action, tool state, attempts, route, partial text). The pieces it + used to copy are already in the log (D10). +- **Continue (D23):** continuing an interrupted turn starts a new turn whose + first item is `continues{turn}`; the adapter joins both turns when it + rebuilds fx's history. +- **Turn endings:** an `interruption` item precedes `turn_interrupted`, whose + reason is `cancel` or `failed` (D21). +- **Settings:** `set` replaces the whole value, so the adapter writes fx's + merged preferences. `title` holds a JSON string; whether a title was + generated or typed stays in fx's `prefs`. +- **Compaction:** `compacted.data` names the seq of the first kept line when + fx keeps a tail; the adapter reads back to it from `compaction_offset`. +- **Order:** `turn_started` comes before `put_blob`, which refuses earlier. +- **Subagents (D22):** names, the agent, the request fingerprint and failure + text go in child `data`; a child's instructions go in the child's own + `prefs`. fx checks its own rules (unique names, at most 256 children) + under an in-process lock, which is enough because only the process holding + the parent's flock can append to it. Unfinished work's message and + root-user evidence stay in memory: v1 drops them on restart too + (`child_state.zig` `interruptActive`), and the child's own log holds the + message once its turn starts. A child's turn opens on disk when its work + starts, as `tla/Subagents.tla` `ChildStart` models, so the bodies its + tools keep are blobs of a session on disk (D44, user ruling 2026-10-01); + its pieces are written whole at its end, as v1's children are, while + roots stream theirs (D28). A crash before that start leaves no log + (`lost`); after it, the child's log keeps an open turn with no pieces, + the parent's repair records the work `interrupted`, and replay skips the + empty turn, so the child's history is its earlier turns. A child keeps no paused-response checkpoint (D31), so the + child runner, like a v2 root, offers the orchestrator none. `lost` + reaches the parent's model as `child_lost`, whose result says the + message never ran and may be sent again (D33). +- **Usage:** the profile's usage-recovery marker stays fx's. For v2 + sessions it lives in `~/.fx/usage-recovery-v2/{id}`, apart from v1's + folder. The adapter follows v1's rules around `set usage` (a durability + point whose value carries a checkpoint time that only grows): + - before a checkpoint that still owes the profile ledger, it writes the + marker, unless one already covers the session and keeps its first time; + - once a durable checkpoint owes nothing, it clears the marker. + + fx's usage recovery reads the v2 markers too. It takes the newest usage + from the log without the lock, and trusts it only when the checkpoint's + time is at least the marker's (D20, `tla/Wiring.tla`). +- **Checks the adapter keeps:** tool call and result pairing, and v1's + per-piece size rules, before anything reaches `append`. + +### Levels + +```text +L4 api the calls above, input validation, error mapping +L3 catalog index.jsonl, .last and .last_opened, list, rebuild, self-heal +L2 session fold, turn rules, open/resume/fork/import/close/delete, crash rules, + snapshots, per-session mutex +L1 log line framing and CRC32C, append, backward scan, read range, torn-tail cut, seq check +L0 storage posix: open, positional write at the end, fsync, flock, mkdir, rename, link, unlink + js-host: load, commit(expected revision), list, remove over the SDK sessionStore +``` + +Each level calls only the one below, and only L4 is public. + +### Reuse Decision + +Strategy: a new mechanism that replaces v1. The v1 patterns that fit are +reused as ideas; no v1 code is shared. + +- **Extending v1 was rejected.** Extending `Store` and `LoadedWritableSession` + (`src/core/session/session_log.zig:3207`) keeps the five-file state split + and the per-host copies of the save logic. +- **Composing inside fx was rejected.** Merging the callbacks inside + `src/core/app/app_session_runtime.zig` alone leaves `fx ask`, ACP and + subagents on their own copies. +- **Reused as patterns:** + - the event envelope from `session_event.zig::Envelope`; + - the staged publish from `Root.startConversationSession`; + - the bounded lock wait from `session_log.zig:27`; + - fx's kebab-case flags and `FX_*` environment variables (`FX_MODEL`, + `FX_PERMISSION_MODE`) for the switch (D26). +- **Reused unchanged:** the embedder `sessionStore` contract (`sdk/fx-sdk.js:922`). + +### New Mechanism Justification + +| Kind and name | Present requirement | Existing candidates inspected | Contract mismatch | Owner and lifecycle | Replaces/removes, or why coexistence is necessary | +|---|---|---|---|---|---| +| Module `session-manager` (L0 to L4) | One owner for session storage and the live-session lifecycle across all hosts | `session_store.zig::Store`, `session_log.zig::LoadedWritableSession`, `app_session_runtime.zig::Persistence` | State spans five files, the open turn is truncated on reopen, and nothing owns the live session | A host opens a Session per log; `close()` or process exit ends it | Coexists with v1 behind the switch, then replaces v1 | +| fx file `session_adapter.zig` | fx types become events; the persistence callbacks are implemented once | The four host copies in Repository Evidence | Each copy embeds host state and host-specific side effects | fx core; each host creates one adapter per open session | Replaces the four host copies | +| Callback `append_turn_piece` in `AgentRuntimeDeps` | Streaming each completed piece (D10) | `propagate_history_turn` (whole turn at the end), `recovery_checkpoint.set` (full rebuild at 13 boundaries) | The first arrives too late; the second is quadratic and misses pieces between checkpoints | Called by the agent loop; implemented by the adapter | Shrinks the recovery checkpoint to fx recovery details | +| Derived file `index.jsonl` | Listing and `.last` or `.last_opened` without opening every session | `session_catalog_cache.zig` (`.resume-catalog`), v1 `continue/` files | Keyed to stat fingerprints of v1 files; the remembered session lives in a separate file | Written by the manager on create, open, title, workspace or language change, close and delete; rebuilt by scanning logs | Replaces `.resume-catalog` and `continue/` | +| Folder `blobs/` per session | Large bodies kept out of the log and shared with forks through hard links | `result_store.zig`, `command_replay_store.zig`, the `images/` dir, `web_fetch_artifacts.zig` | Four stores with their own formats, and no fork rule | Written before the line that references it; removed with its session | Replaces those four stores (D6) | +| L0 `storage_js` | wasm persistence without changing the SDK (D9) | `js_host_session_store.zig` | It stores whole v1 state snapshots, not a log | Created by the wasm host profile; commits at durability points | Replaces `js_host_session_store.zig` | +| fx v1 converter | Carry v1 sessions into v2 under the same ids (D8) | `session_store.zig::migrateLegacyStorageOnly` | It migrates only between v1 formats | fx background task on the first v2 run; writes through `open(.import)` | Temporary; deleted with the v1 reader one release after v2 becomes the default | + +## Durable State And Schema + +- **Source of truth:** `{id}/log.jsonl`, or the log bytes held by + `sessionStore` on wasm. The index, snapshots and in-memory state are + derived and can be rebuilt. +- **Write points:** every `append` is one positional `write()` at the end + offset, which the writer knows because it holds the session flock. That + survives an fx crash, because the bytes are already in the kernel. On wasm, + lines not yet committed stay in memory. +- **Durability points** (a plain `fsync` on native; a `sessionStore` commit + on wasm): + - after a batch containing `turn_committed`, `turn_interrupted`, + `set permissions`, `set usage`, `child_spawned` or `child_finished` + (`set usage` since the wiring check: fx clears its usage-recovery + marker only after the usage is durable, `tla/Wiring.tla`); + - on `close()`; + - on the first publish; + - at the end of `open(.resume)` repair. + + A blob is durable before `put_blob` returns: its file, then its folder + entry. That is required because one log `fsync` makes every line already + written durable, including a line another thread wrote after its own blob, + so a blob cannot wait for the next durability point (`tla/Fork.tla` + `RefsExist`). Cost: two `fsync` calls per blob. +- **What a sync guarantees:** a synced line survives an fx crash and an OS + crash (kernel panic or freeze) on every platform, and a power cut on Linux. + - On macOS, a plain `fsync` can leave recent data in the drive's own cache, + so a power cut can lose the newest synced lines. + - In rare cases a power cut can also damage a line in the middle. Such + damage is recent, so it lies in what open reads, and the checksum makes + the session open read-only up to the last good line. Older damage (bit + rot) is found by `read` and `verify`. + - This is accepted by D3. +- **Acknowledged seq:** a `seq` is stable only after a durability point. After + a machine crash, a line that was never synced can vanish and its `seq` + number is handed out again (`tla/SessionLog.tla`). +- **Publish (D2):** the first batch that contains `turn_started`, together + with any held `set` lines, is written to `.tmp/{id}/log.jsonl` and synced. + Then it's renamed to `{id}` and the parent directory is synced. + - A visible session always has a durable first line (`tla/Lifecycle.tla`). + - A session that never starts a turn never touches the disk. +- **Restart:** + - `open(.resume)` cuts a torn or bad-checksum final line. + - It appends `turn_interrupted{reason: crash}` for an open turn, and + `child_finished{interrupted or lost}` for unfinished children. + - Then it syncs (`tla/TurnLifecycle.tla`, `tla/Subagents.tla`). +- **Versioning:** `v` is on every line, and only the manager writes it. + Readers accept every version up to their own, skip unknown kinds, and open + newer versions read-only. +- **Migration (D8, D16):** on every start with v2 as the default, during the + one-release window, an fx background task converts every v1 session with + at least one turn that isn't in v2 yet. It runs after startup and never on + the startup path. + - It uses `open(.import)` under the same id and keeps original timestamps + and children. + - It is crash-safe (staged in `.tmp`) and safe to rerun (Exists means + skip). + - v1 files are left untouched. + - wasm v1 snapshots are converted the same way through `sessionStore`. + - A session converted earlier and then continued in an old fx binary is + not re-imported, because its id already exists; the newer turns stay + only in the v1 copy. + - v1 terminal state is not converted (D13). + - It skips `~/.fx/sessions/v2` itself, the v2 root (D19). + - v1 event kinds map one to one: `user`, `assistant`, `tool_call`, + `tool_result` and `steering` become `item` lines with that `type`; + `turn_completed` becomes `turn_committed`, `interrupted` becomes + `turn_interrupted`, and `context_checkpoint` becomes `compacted`. +- **Cleanup:** + - `delete` renames `{id}` to `.trash/{id}`, appends an index tombstone, then + removes it. + - Rebuild removes stale `.tmp` and `.trash` entries. + - An unreferenced blob goes away with its session. + - When fx deletes a session, the adapter also removes + `~/.fx/terminal/{session-id}/`, for its children too. Doctor removes any + terminal folder whose session no longer exists (D13). + +## Concurrency And Ordering + +- **Between processes (native):** one exclusive `flock` on `{id}/lock`, held + from open to close. A contender retries for up to 2 s, then gets Busy; a + resume may set its own wait, and fx's session picker sets none (D38). The + kernel releases the lock on process death (`tla/WriterLock.tla`). +- **Between writers (wasm):** single-writer is optimistic. Every commit + carries the expected revision, and a conflict makes that Session fail with + Busy. This is not covered by `WriterLock.tla` (Design Risks). +- **Inside a process:** + - one mutex per `Session` serializes seq assignment, validation, the write + and the fold update; + - the sync may run after the mutex is released, and the requesting + call returns only after its own sync; + - hosts call from any thread and take no locks. +- **Ordering:** file order is seq order, which is the order in which calls + took the mutex. +- **Readers:** `read`, `get_blob`, `list` and `fork` take no session lock. + They read up to the last complete, valid line; written bytes never change. +- **Index:** appends and rewrites hold `index.lock`, and every `open` appends + an `opened` line (D11); a resume writes the whole entry instead, since its + repair may move the workspace or interrupt a turn (D42). A new session + counts as opened by the host that created it. The index is derived: when an index write fails after the + session change it records succeeded, the change stands and the failure is + reported once (`index_stale`); the next change or a rebuild fixes it. +- **Close:** `close()` takes the mutex, interrupts an open turn with + `reason: closed`, appends `closed` and syncs. Later calls return + SessionClosed. +- **Children:** each child is its own session. The child thread appends + `child_finished` through the parent's Session, ordered by the parent's + mutex. A child has at most one unfinished work item, so a spawn and a + finish can never race for the same child (D22). + +## Performance And Capacity + +The workload is one interactive session: a few to hundreds of pieces per turn, +and up to hundreds of thousands of turns over a session's life. + +The standalone module's ReleaseSafe benchmark measured every row through the +public API against a Zig replay of v1's I/O pattern on the same file system. +The figures are medians from 2026-09-27 on a Mac (APFS, SSD). +- The v1 replay follows v1's code: + - one `fsync` per log frame (`session_log.zig:254`); + - a temp-file rewrite with two syncs per side file (`io.zig:700`); + - resume takes `session.lock`, writes `owner.live`, reads four side files + and replays every event; + - list parses `.resume-catalog` and checks seven stat fingerprints per + session (`session_catalog_cache.zig`). +- Where v1 does more than the replay (authority and commit guards, the + history cache, catalog rewrites), the replay leaves it out, so no gate is + easier than v1 itself. +- A piece is a ~200-byte line; a turn is 32 pieces and 10 tool steps. + +| Operation | v2 | v1 replay | +|---|---|---| +| Startup | no session I/O | a session created at startup | +| Append one piece | one `write()`, 1.9 µs | positional write plus `fsync`, 23.6 µs | +| End of turn | 32 writes plus one `fsync`, 0.12 ms | a sync per frame plus side-file rewrites, 3.4 ms | +| Permission change | one write plus one `fsync`, 24 µs | a `permissions.json` rewrite, 167 µs | +| Resume at 10 turns | 130 µs | 186 µs | +| Resume at 1K, 10K, 100K turns | 376, 390, 393 µs | 5.6, 53, 529 ms | +| Scrollback of 100 lines at 10 turns, in the open session | 30 µs | 83 µs to load the history | +| Scrollback of 100 lines at 1K, 10K, 100K turns | 126, 125, 124 µs | 5.5, 55, 548 ms to load the history | +| Read of 100 lines by id at 10 turns, a session not open (no gate) | 57 to 94 µs | 74 to 83 µs to load the history | +| List of 1K sessions | 4.0 ms | 6.7 ms | +| First page (50) of 1K sessions | 2.9 ms | 6.7 ms | +| Fork of a 1K-turn session at turn 500 | 1.7 ms | none; a raw durable copy of the prefix takes 0.07 ms | + +- **Gate:** every row is at least as fast as v1, with no exceptions, and + permission change and resume take at most 5 ms. Every row passes. + - The thinnest gated margin is resume at 10 turns, where fixed costs + dominate: 1.4x to 2.4x across runs. v2 opens the session folder without + following symlinks, takes the flock, and records the open in the index. + - Scrollback reads the open session through its handle (`session.read`), + with no open per page: 2.6x to 2.9x at 10 turns, also under load. + - Reading a session that is not open (`read(id)`, a picker preview) + opens its folder and log without following symlinks for each page. At + 10 turns that is about v1's whole-history load (0.9x to 1.3x across + runs, slower under heavy load). It is not a scrollback row and has no + gate; from 1K turns on it is far faster than v1. + - Fork has no v1 row. It parses every copied line to encode the fork's + own snapshots, so it grows with the prefix; it is a rare user action. +- **Size independence:** from 1K to 100K turns, resume grows 5% and + scrollback stays flat (the gate allows 3x); v1 grows 100x. +- **Where the time goes:** list is mostly parsing index lines, then one + `stat` per listed session for self-heal. Resume is mostly checking and + folding the tail after the newest snapshot. +- **Memory:** a sync allocates nothing. It asks the kernel to write pages + already in the page cache, so it lowers kernel dirty memory. + - On native, the manager holds no unsynced lines of its own, because each + line goes to the kernel with one `write()`. + - On wasm, lines stay in memory until the next commit, so at most one + turn's worth. + - Resume keeps only the folded state and the model context since the last + compaction. The transcript is paged, never loaded whole as v1 does. +- **Tuning (D7):** resume at 100K turns by snapshot distance. + + | Distance | Resume | Snapshot lines | + |---|---|---| + | 16 KB | 0.27 ms | 1.0% | + | 32 KB | 0.27 ms | 0.5% | + | 64 KB | 0.42 ms | 0.3% | + | 128 KB | 0.71 ms | 0.1% | + | 256 KB | 1.20 ms | 0.07% | + + 64 KB is the default. It resumes about three times faster than 256 KB, + and it keeps snapshots a small share of the log even when the folded + state (settings, children) is large; smaller distances gain little. + +## Compatibility And Rollout + +- **Phases:** + - standalone first; + - then side by side behind the switch; + - then v2 by default, with the one-time conversion; + - then v1 removed one release later. +- **Mixed state:** v1 and v2 use separate roots, `~/.fx/sessions/{id}` and + `~/.fx/sessions/v2/` (D19), and one process uses one backend. +- **Switch (D26):** `--sessions-v2` on `fx` and `fx ask`, or + `FX_SESSIONS_V2=1` for any host, including ACP launched by an editor and + the E2E suite. It is off by default. Subagents follow their parent's + process, and the wasm build stays on v1 until `storage_js` lands. +- **Side files while the switch exists (D27):** per-session side folders + (tool results, images, command logs, artifacts, background and terminal + state) keep v1's layout under an fx-owned `~/.fx/session-files/{id}/`, + removed with the session. The move to blobs (D6) and to + `~/.fx/terminal/{id}/` (D13) happens before the default flips. +- **Rollback:** + - Before the default flips, switching back to v1 hides v2 sessions but + loses nothing. + - After the conversion, a downgraded fx still sees every v1 session, but + nothing done in v2. +- **Removal condition:** v1, the converter and the v1 reader are deleted one + release after v2 becomes the default. That requires the E2E session suite, + the SDK resume test and a dogfood window to pass with no v2 regression. + +## Reliability And Recovery + +| Left after a crash | Next open | +|---|---| +| Torn or bad-checksum final line | Cut, because it never counted | +| Bad-checksum line that open reads (line 1, the newest snapshot, or after it) | Read-only up to the last good line | +| Bad-checksum line before the newest snapshot | Open does not read it and stays writable; `read` stops there and reports the damage, `verify` finds it, and `recover` forks the good prefix | +| Open turn | `turn_interrupted{reason: crash}`; fx decides whether to offer "continue", which starts a new linked turn (D23) | +| No `closed` line | `clean_exit` is false | +| Lock | Already released by the kernel | +| Child spawned without a log | `child_finished{outcome: lost}`; a named child keeps its name, and its next message starts it fresh (D33) | +| Child with a log but no finish | `child_finished{outcome: interrupted}` | +| Orphan blob, `.tmp` or `.trash` entry | Harmless; removed by rebuild | +| A blob the log names is missing, or its bytes fail their hash | The session is damaged, as for a bad line: resume refuses (`InvalidSessionFormat` in fx), `verify` counts it, and `recover` forks up to the last turn before the first line that names it (D39) | +| Stale index | `list` self-heals entries whose folder is missing; rebuild fixes the rest | + +- **Stickiness:** "ask after an unclean exit" is carried by the last + interrupted turn's `reason: crash` until the user starts a new turn. +- **Diagnostics:** + - `verify` scans a whole log: checksums, seq, and fold equivalence against + the newest snapshot; + - `rebuild` rewrites the index from the logs and sweeps `.tmp` and + `.trash`; + - fx doctor calls both. + +## Decisions + +Settled before the decision reviews: +- **Decision:** build standalone, prove it through the API only, then wire + it into fx next to v1, then replace v1. **Why:** + isolation and discipline. **Alternative:** build inside fx from day one, + which would couple the design to v1 while it is changing. +- **Decision:** one append-only JSONL log per session, one module, an API-only + boundary, compiled into fx. The microservice and JSON-schema ideas describe + the discipline, not a process or call format. **Why:** one owner and one + source of truth. **Alternative:** a separate process, which adds IPC, + startup cost and a new failure mode. +- **Decision:** fork is part of the API. **Why:** requested feature. + +Settled in the 2026-09-27 scope lock: +- **D1 Decision:** an unfinished turn gets `turn_interrupted{reason: crash}` + on reopen and is never cut. **Why:** keeps the log append-only and removes + `recovery.json` and `recovery.asked`. **Alternative:** truncate as v1 does, + losing the partial turn. +- **D2 Decision:** a session folder is created at the first turn; earlier + `set` lines are held in memory and written with it. **Why:** there are no + empty sessions, no startup I/O and no delete-if-empty logic. + **Alternative:** create at the first save of any kind, or at startup as v1 + does. +- **D3 Decision:** a plain `fsync` at durability points only, on every + platform. There is no fsync per line, no `F_FULLFSYNC` and no background + sync. Revised on 2026-09-27. + **Why:** power loss is rare, and stronger syncing is not worth its cost. + This is the simplest and fastest option, 0.12 ms per turn against the v1 + replay's 3.4 ms in the Zig benchmark (the first Python prototype measured + 0.13 ms and 7.1 ms), with v1's guarantee against fx and OS crashes. + **Alternative:** `F_FULLFSYNC` at durability points (power-loss safe on + macOS, about 4 ms per turn), or a background full sync after a plain + `fsync`. The latter needs a sync thread and still loses turns already + reported as saved. +- **D4 Decision:** a CRC32C field ends every line. **Why:** detects silent + damage the way real journals do, and stays valid JSON. **Alternative:** + newline, parse and seq only. +- **D5 Decision:** forks start only at turn boundaries, or turn 0. + **Why:** a fork's log is clean from line 1. **Alternative:** any line, + with an interrupted turn appended; deferred. +- **D6 Decision:** large bodies go through per-session blobs, hard-linked on + fork, replacing fx's four stores. **Why:** one rule for large data, simple + delete, forks that cannot break. **Alternative:** a shared store (reference + counting and GC), or keeping fx's stores. +- **D7 Decision:** snapshots now, after each compaction and every ~64 KB + (tuned by the benchmark; see Performance And Capacity). **Why:** resume + cost is bounded like a filesystem checkpoint, and the transcript is paged + on demand. **Alternative:** defer until measured. +- **D8 Decision:** a one-time background conversion of every v1 session, same + ids, v1 files untouched, v1 reader deleted one release later. **Why:** one + listing path and a clean v1 removal. **Alternative:** convert on first + resume (two listing paths) or don't convert. +- **D9 Decision:** wasm persists through a JS-host L0 over the unchanged + `sessionStore`. **Why:** embedders change nothing. **Alternative:** a new + append-style SDK API, or dropping wasm persistence. +- **D10 Decision:** each completed piece of a turn is appended as it happens, + with no sync until the commit. **Why:** a crash keeps every finished piece, + with no separate recovery snapshot. **Alternative:** one batch at commit, as + v1 does. +- **D11 Decision:** `-c` stays distinct from `--resume last`, using host and + open time in the index. Sessions tied on that time resolve as `list` sorts + them (the smaller id first), so `--resume last` is the list's first entry. + **Why:** keeps v1 behavior without a separate file, and the same state + always resolves the same way. **Alternative:** merge both into "newest session". +- **D12 Decision:** the agent loop gains one callback, `append_turn_piece`. + **Why:** the loop knows exactly when each piece completes, and it removes + the quadratic full-turn rebuild. **Alternative:** diff recovery checkpoints + in the adapter. + +Settled in the second 2026-09-27 review: +- **D13 Decision:** hosted terminal state lives in an fx-owned + `~/.fx/terminal/{session-id}/`, outside the manager. **Why:** it is mutable + runtime state of live shells, not history. Unix keeps these apart + (`/var/log` versus `/run` and `/var/lib/{service}`), and it keeps + screen churn out of the log. **Alternative:** a manager-provided writable + folder inside `{id}/` (breaks the boundary), or rewriting the terminal + store as log events. +- **D14 Decision:** one optional diagnostics callback at manager init, + forwarded by the adapter to `debug_trace`. **Why:** workspace rule 3 (log + dropped state) without importing fx; the SQLite log-callback pattern. + **Alternative:** a separate manager log file, or repairs returned only in + call results. +- **D15 Decision:** fx's session commands keep working with v2 meanings. + `recover` forks at the last good turn and leaves the source untouched. + `migrate` (hidden) runs the conversion and is removed with v1. List, show + and doctor map to `list`, `read`, `verify` and `rebuild`. **Why:** keeps + v1's promise for damaged sessions, reusing fork. **Alternative:** drop + `recover` and `migrate`. +- **D16 Decision** (amends D8): the converter reruns on every v2 start during + the one-release window, skipping ids already in v2. **Why:** older fx + binaries on PATH can create v1 sessions after the first run. + **Alternative:** a one-time run. +- **D17 Decision:** every `item` carries a required `type`, a short name fx + chooses (`user`, `assistant`, `tool_call`, `tool_result`, `steering`, and + any later ones). The manager checks only its form (1 to 32 of `a-z`, `0-9` + and `_`), stores it, and returns it from `read`; it never interprets it + and keeps no list of allowed names, like a file extension the filesystem + stores but never opens. **Why:** logs stay readable with `jq` and `grep`, + readers can filter without parsing fx's `data`, and the converter keeps + v1's kinds by name, while fx still adds a type with no manager change. + **Alternative:** the type only inside + `data`, or one manager-owned kind per message type with ordering rules + (which ties the manager to the agent's message model). +- **D18 Decision:** the conversation language is a `set` key, `language`, a + JSON string of 1 to 24 bytes such as `"es"` or `"und-Latn"`, and the + index lists it next to the title. **Why:** `fx sessions` prints each + session's language in text and JSON (`src/core/output/output_contracts.zig` + lines 978 to 996 and 1098), and `list` reads the index only. + **Alternative:** the adapter opens every listed + session to read it (slow), or `fx sessions` drops the language. +- **D19 Decision:** the v2 root is `~/.fx/sessions/v2/`, inside v1's + sessions folder, so every session stays under `~/.fx/sessions/`. + - v1 treats every folder there whose name is a valid id as a session + (`src/core/session/session_store.zig` lines 385 to 387, and the doctor + scan at lines 2549 to 2555). fx skips `v2` there, as it already skips + `latest`, once v2 is wired in; the converter skips it too. + - Installed older fx versions never learn the rule. Their `fx doctor` + reports a harmless `session v2: canonical_state_invalid`. No v1 path was + found that deletes or rewrites the folder: doctor cleanup never runs on + it, and legacy migration works on one named session at a time. + - Removing `~/.fx/sessions` by hand removes v2 sessions too. + - The path is permanent; moving to plain `~/.fx/sessions/` after v1 is + gone would be another migration. + - The manager creates missing parent folders `0700`, like its own. + **Alternative:** `~/.fx/sessions-v2/`, which v1 never looks inside. + +Settled in the 2026-09-27 pre-wiring API check: +- **D20 Decision:** `State` carries `created_ms` and `updated_ms`, the `ts` + of line 1 and of the newest line (0 before the first turn), and the index + records the same `updated_ms` instead of the clock at the index write. + **Why:** ACP's load and usage recovery need both on resume + (`src/acp/sessions.zig` lines 669 to 679, + `src/core/session/usage_recovery.zig` lines 89 to 107), and a converted + session keeps its original times in the list rather than the conversion + time. **Alternative:** the adapter looks the session up in `list`. +- **D21 Decision:** a host may end a turn with `reason: failed` as well as + `cancel`. **Why:** fx ends turns both ways + (`src/core/shared/types.zig` lines 2243 to 2246), and recording a failure + as a cancel would make `last_interrupted` wrong. TurnLifecycle treats + every reason as one interrupt, so the spec is unchanged. + **Alternative:** only `cancel`, with the difference kept in fx's data. +- **D22 Decision:** the parent's log owns all subagent state. + `child_spawned` and `child_finished` carry optional fx `data` (at most + 4 KiB), `cancelled` joins the outcomes, a child has at most one unfinished + work item, and `State.children` lists every child with its newest work, + outcome, data and seq. **Why:** fx needs the whole list, not only running + work, to continue a named child, detect replaced work and report status + (`src/core/subagent/child_state.zig` lines 42 to 57), and this removes + `children.json` without a second owner. **Alternative:** keep + `children.json` next to v2 for now, which gives the same state two owners. +- **D23 Decision:** "continue" after an interrupted turn starts a new turn + that links back to it; D1 stands and the manager never reopens an ended + turn. **Why:** no manager or spec change, and the log stays append-only. + **Alternative:** let a crashed turn stay open until fx decides, which + changes D1 and TurnLifecycle. +- **D24 Decision:** an ACP session that never gets a prompt is never written + (D2 applies to every host); loading its id after a restart returns + NotFound. **Why:** it holds nothing to lose, and no empty folders appear. + **Alternative:** write every ACP session at creation as v1 does. +- **D25 Decision:** token counters stay inside fx's `usage` value and are + not added to the index or `fx sessions`. **Why:** the list does not show + them today. **Alternative:** index them for the list. + +Settled when wiring started (2026-09-27): +- **D26 Decision:** the switch is `--sessions-v2` plus `FX_SESSIONS_V2=1`, + off by default, instead of a runtime-profile capability flag. **Why:** the + request was for `fx --sessions-v2`, and editors that launch ACP can only + set the environment. **Alternative:** a flag only, which leaves ACP and + the E2E suite out. +- **D27 Decision:** until the default flips, v2 sessions keep side files in + v1's layout under `~/.fx/session-files/{id}/`, a temporary deviation from + D6 and D13. **Why:** wiring and dogfooding can start without first + rewriting four stores and the terminal store. **Alternative:** move to + blobs and `~/.fx/terminal/` before any wiring. + +Settled after the first fault-injection runs (2026-09-27): +- **D28 Decision:** a tool call is saved before it runs, as a + `tool_running` item with no result yet. On resume, each such call that + the turn does not already hold gets a failed result, telling the model + the tool was running when fx stopped and may have partly run. The result + is derived from the log on every resume, never written, and only for a + turn fx did not finish itself; a turn fx ended (a cancel) keeps what fx + saved. **Why:** the model never gets an unpaired call, and it knows a + side effect is uncertain. **Alternative:** v1's behavior, where the + running call is lost with its turn. +- **D29 Decision:** I/O failures keep their kind across the API: + `NoSpaceLeft`, `AccessDenied`, `ReadOnlyFileSystem` and `FileTooBig` join + `Io` in the manager's error sets, and fx shows them as v1 does. The + failed write or sync itself reports its cause; the session is then + failed, and later calls on it report that same cause (D40). **Why:** a + full disk or a read-only folder shows its cause. **Alternative:** `Io` + alone. +- **D30 Decision:** a new session that was renamed but never prompted is + not kept (D2). **Why:** it holds no conversation. **Alternative:** save it + on rename, as v1 keeps it. +- **D31 Decision:** while dogfooding, v2 does not store v1's paused-response + checkpoint behind `--continue-recovery`; an interrupted turn comes back + with the pieces saved so far. Revisit before the flip. **Alternative:** + port the checkpoint now. + +Settled while wiring ACP (2026-09-27): +- **D32 Decision:** the transcript shown on resume and on an ACP load + lists every saved turn, as v1's does, while the model's history still + starts at the newest compaction. The adapter reads the whole log for it, + one turn and one page in memory at a time, and must stay at least as + fast as v1's full history load. `fx session {id}` lists every saved turn + as well, with each compaction's summary where its line sits in the log, + counted as v1's archive counts it: the turns before it, and its place + among the compactions. **Why:** a compaction must not hide old turns + from the person reading them. **Alternative:** show the summary and the + turns after it. +- **D33 Decision:** a named child whose first message was `lost` keeps its + name. The lost message's result tells the parent it was lost, and the + next message to that name is new work for the same child, whose log is + created by that work's first turn (`tla/Subagents.tla` already allows + this). Nothing is resent on its own. **Why:** the parent decides whether + to resend, so no work runs twice. **Alternative:** refuse the name, or + resend the lost message on reopen. +- **D34 Decision:** fx chooses a child's id and names it in the parent's + `child_spawned` before the child exists; `open(.new)` takes that id for + a child session only, with no disk I/O. A child with no log yet keeps its + id, and its first turn creates the log under it (`Subagents.tla` + `ChildStart`); a taken id fails that turn's append, because the publish + rename never replaces a folder. A lost named child's instructions (kept + in its own `prefs`) are lost with it; the parent's log still holds the + call that gave them. **Why:** D33 and v1's flow need an id that exists + before the log. **Alternative:** a fresh id per attempt, which gives one + name several children. + +Settled while wiring side files, `fx sessions` and doctor (2026-09-28): +- **D35 Decision:** with v2 on, `fx session migrate` refuses with a clear + message that it applies to v1 storage until the v1-to-v2 converter + lands; it touches no v1 file. **Why:** one backend per + process (D26), and the converter is its own step. **Alternative:** build + the converter now, or run v1's migration from a v2 process. +- **D36 Decision:** with v2 on, `fx doctor` verifies up to 64 sessions, + v1's bound, says when it stopped early, and reports damage, and removes + only side folders whose session is gone (D27), as v1's doctor removes + stray temporary files. A folder changed in the last 24 hours stays: a new session keeps side files + (an attached image) before its first turn creates its log, so a young + folder may still have an owner. It rebuilds nothing + and forks nothing; `fx session recover` stays the way to salvage a + damaged session. **Why:** doctor stays safe to run at any time. + **Alternative:** report only, or also rebuild and repair. +- **D37 Decision:** `peek(id)` returns a saved session's state and identity + without its lock, folded as the catalog folds it (line 1, the newest + snapshot, the tail); a torn tail is left as it is, and a child needs no + parent to be read. `fx session {id}` and doctor read through it and + `read`, never through a writable open. **Why:** a read-only command must + not take the writer lock or repair anything. **Alternative:** rebuild + the state in fx from `read` pages, a second fold that could drift. No + TLA+ change: it reads, as `list` does. + +Settled on 2026-09-28: +- **D38 Decision:** a resume may set how long it waits for the writer lock + (`lock_wait_ms` on `open(.resume)`); unset keeps the manager's 2 s. fx's + session picker waits for none, as v1's picker does (its + `session_lock_deadline_ms = 0`), so a session open in another fx shows + as busy at once instead of freezing the app for 2 s; every other resume + keeps the 2 s. **Why:** v1's picker contract; found by v1's `tui-resume` + contention test under v2. **Alternative:** one wait per manager, which + either freezes the picker or drops the 2 s other resumes rely on. No + TLA+ change: `WriterLock.tla` models Busy as `Open` being disabled while + the lock is held, and how long a contender retries is outside it. +- **D39 Decision:** a blob the log names that is missing, or whose bytes + fail their hash, damages the session the way a bad line does. Replay + fails with Corrupt (fx: "saved session is unreadable", never "not + found"); `verify` reports how many such blobs it met (doctor shows the + session as damaged); a fork copies only lines whose blobs are present + and whole, so `.last_good` ends before the first turn that names a bad + one and a `.turn` fork past it is refused. **Why:** found by the M1 + fault matrix: resume said NotFound for a session that exists, doctor + said ok, and a recover copy would have named the same missing blob. + **Alternative:** show the piece as unavailable and resume anyway, as fx + does for a missing image; rejected because a blob holds a turn's own + text, which the model would then silently lose. `tla/Fork.tla` gains + `Lose`, and `RefsExist` now allows a missing reference only in the + session that lost it. +- **D40 Decision:** a failed session keeps the cause of the write or sync + that failed it, including a sync that failed on another thread and the + first turn's publish, and every later call on it reports that cause + instead of `Io`. **Why:** found by the M1 fault matrix: fx reports a + failed streamed write only at the turn's commit, so the same full disk + read "FileTooBig" on one run and "Io" on another; the fault grid later + found a new session in a read-only folder reading "Io". **Alternative:** keep `Io` and have every fx host + remember the first error itself. No TLA+ change: the specs model a + session going down, not the name of the error. +- **D41 Decision:** a host switching sessions may open the next session + before it closes the current one. ACP creates or loads the next session + first and closes the current one only once the next is ready, so a + failed switch leaves the current session in place. While a switch is + pending, the current session's turn may still end and its children may + still finish, but no turn or child starts; the current session closes + only after its children are joined, and closing the next one instead + abandons the switch. **Why:** found by the M1 trace check of `Wiring`: + every ACP switch in the E2E runs opened the next session first, which + the spec's single session slot did not allow. **Alternative:** close the + current session first, which leaves ACP without a session when the next + one fails to open. `tla/Wiring.tla` gains `next`, the session being + switched to. +- **D42 Decision:** a resume rewrites the session's index entry, stamped as + opened by the resuming host, instead of appending only an `opened` line. + **Why:** found while porting ACP's load `cwd`: a resume from another + workspace records `set workspace` in the log, but `list` kept the old + workspace until the session closed, so `session/list` and `fx sessions` + showed a moved session under the folder it left; a repaired open turn + left the turn count stale the same way. **Alternative:** write the entry + only when the repair changed the listing, which saves one index line per + resume but needs the repair to report what it wrote. `tla/Catalog.tla` + gains `Refresh`, a put for a live, indexed session, which the title, + workspace and language updates already wrote. +- **D43 Decision:** an ACP session on v2 keeps the client system prompt and + its MCP tool identities in its side folder, through the + `SessionChildCapability` v1 uses, and `session/new` and `session/load` + take the request's `cwd` as v1 does. The prompt is written at + `session/new`, as on v1; closing a session that never got a prompt + removes its side folder (F13), and doctor sweeps one that a crash leaves + (D36). **Why:** main's ACP gained these after the stack was cut; without + them a v2 session silently lost the client's instructions and its replay + detail, and started in the process folder. **Alternative:** hold the + prompt in memory until the first turn, which keeps D24 exact but loses + the prompt when the side write fails after that turn commits. No TLA+ + change: side files are outside the specs. + +Settled while moving off the side folder (2026-10-01): +- **D44 Decision:** a v2 session's large bodies are blobs of that session, + realizing D6 for fx's stores: tool results and tool images, command + replay and web-fetch downloads (an edit's diff stays inside its item, as + v2 already keeps it). Each handle keeps its store's + prefix and extension, and its name is the body's full 64-hex hash: a + tool result is `result-`, the hash and `.txt`, and a command's output is + `fx-command-replay-`, the hash and `.bin`, so no name + index exists and `read_tool_result` still tells text, images and command + output apart. All of a session's blobs are found by hash alone, so each + store reads only handles with its own prefix and reports any other as not + found, as v1's separate folders did; otherwise the result store would + page a command's replay as raw frames. Every blob is listed on an item of the turn that stored it; + one stored outside a turn is listed on the next item the session writes + (only the move's own setting lists blobs, D47). A body is stored only + while the session is on disk: the adapter opens the turn before it + stores one itself, and a subagent child opens its turn when it starts, + as the hosts that stream a turn already do. The store modules keep their callers: the session's + `SessionChildCapability` gains a blob backend on v2 that puts and gets + whole bodies, and only the stores and the two direct readers of replay + files change. A command's output streams to a temporary file outside the + session while it runs and becomes a blob when it is kept, copied from + that file by `Session.putBlobFile` so it is never whole in memory; output + that is never kept goes with the file. A command's own log files, which + its process writes directly, stay in the temporary folder fx uses when no + session is open. Prompt images are captured before the + session is on disk, where no blob can be written, so they are saved + inside the user's item, as libfx saves them; a large item is a blob + already. fx's own size limits stay where they are. **Why:** one folder per session, + forks that hard-link instead of copying, no orphan side folders, and + content addressing that makes a stored body unforgeable. **Alternative:** + keep today's handle names with an index from name to blob, which grows + with every stored result. +- **D45 Decision:** a v2 session's hosted terminal state lives in + `~/.fx/terminal/{id}/` (D13). Deleting the session removes it, `fx + session recover` copies it as it copied side files, and doctor removes a + terminal folder whose session is gone and that is more than a day old + (as D36). **Why:** live shell state is not history, and it no longer + depends on the side folder. **Alternative:** keep it in the side folder. +- **D46 Decision:** the manager gains two setting keys, `client_prompt` and + `tool_identities`, whose values are fx's JSON. fx writes each only when it + changes, at most 64 KiB and 1,024 entries, well under a line. This + replaces D43's side files. **Why:** both are small session settings, and + the side folder goes away. **Alternative:** one generic host key, where a + new tool identity would rewrite the client prompt too. +- **D47 Decision:** an older v2 session moves to this layout on its first + writable open. fx puts each side body its log names as a blob, and the map + from each old handle to its hash as one more blob, then writes one batch: + `set moved_files`, whose value names the map blob and whose line lists + every moved blob, plus the two settings from the old files. The map stays + out of snapshots, which repeat every setting's value. It then + renames the terminal folder and removes the side folder. Each step can be + repeated, so a crash at any point redoes the move on the next open, and an + old handle resolves through the map. A read-only view of a session not + moved yet, such as `fx session {id}`, reads its side files as today; that + read path goes with v1 (M4). The manager lets a `set` line list + blobs, outside a turn, under the same rule as an item: each exists before + the line, a fork hard-links them, and verify checks them. **Why:** + teammates' sessions keep working with no permanent dual path, since an old + handle resolves through one map. **Alternative:** read both layouts until + v1 is removed, or treat old bodies as unavailable. +- **D48 Decision:** with D44 to D47 a v2 session never creates + `~/.fx/session-files/{id}`; D27 is retired. Doctor still removes leftover + side folders. `tla/Fork.tla` gains `set` lines with blobs, and + `tla/MoveSideFiles.tla` models the move under crashes. +- **D49 Decision:** a web-fetch download is a blob, and the model opens it + by path with its own tools, so the manager gives the path of a durable + blob (`Manager.blobPath`) after checking it exists. Blob files are + written read-only (`0400`), so a tool cannot change one by accident; a + fork's hard link shares that mode. The path stays valid after resume, + and `getBlob` still checks the bytes against the name. **Why:** one copy + that outlives the process, and the model's tools work unchanged. + **Alternative:** a temporary copy that goes when fx exits, or plain files + in a downloads folder outside the session, which forks do not carry. + No TLA+ change: a blob is never rewritten in any spec. + +Settled after main's new compactor landed (2026-10-01): +- **D50 Decision:** fx's compactor keeps its records (each compacted tool + call, turn and folded earlier compaction, as `compacted-T12.txt`, + `compacted-M12.txt` and `compacted-L1.txt`) in a named store it can + write, replace, list and read. On v2 each record is a blob, and one + `set compaction_records` setting names a blob holding the map from + record name to blob, as `moved_files` does (D47). The adapter writes + that setting with the session's next batch, listing the map and the + records added since the last one, so the compaction line that cites them + never lands without them: the log keeps a prefix, so the setting needs + no sync of its own. A moved session's old records, under + `tool-results/` in its move map, are listed and read too; a newer record + of the same name wins. **Why:** v2 has no side folder (D48), and a map + in a blob keeps snapshots small. **Alternative:** rebuild records from + the log, which copies the compactor's format into fx's session code, or + a side folder kept only for records, which D48 rules out. `tla/Fork.tla` + `SetBlob` now lists a blob inside a turn as well as outside it, since + compaction runs mid-turn; such a setting is checked as an item is. + +Settled after the first dogfood finding (2026-10-01, F1): +- **D51 Decision:** the message that issues running calls keeps its text + with them. In the batch that first saves a step's calls as running + (D28), one `assistant_running` item holds that message's text; a step + with no text writes none. Replay uses it only when it answers running + calls after a crash: the repaired step carries that text, so the + transcript and the next request show what fx showed before it stopped. + A finished assistant piece clears it, so text that an earlier step + finished with never lands on a later one. The provider replay stays + out: it binds to every call of its message, and a repaired step may + hold only some of them, so it is dropped as fx drops any replay whose + calls changed. **Why:** fx had shown the text, the model had sent it, + and v1 keeps it; without it the plan for an interrupted command is + gone. **Alternative:** stream the assistant piece early, which makes + the finished step's prefix match depend on every later change to that + message. No TLA+ change: the item rides in D28's batch, and no spec + models fx's items. + +Settled after the second dogfood finding (2026-10-02, F2): +- **D52 Decision:** a session's title comes from its first prompt even + when a crash took its first turn. A new session still writes the title + its first prompt gives with its first turn end. A resumed host session + with no stored title keeps the title v1's listing derives from its + restored history (the first usable prompt, an interrupted turn's + included) and writes it with its next turn end; later turns leave it. + A child stays as before. The app's title generation keeps + its gate (an untitled session with no history), so a crash-recovered + session gets the prompt title, not a generated one. **Why:** v2 keeps + the crashed prompt, so the old rule (only a session started in this + process names itself) left such a session untitled for good, while the + app already shows that prompt as its title on resume. **Alternative:** + also generate a title on the first prompt after resume, as v1 does + because it drops the crashed turn; that changes the app's title gate and + resume title cache, which v1 shares. No TLA+ change: a title is a + setting no spec reads. + +Settled for making v2 the only store (2026-10-02): +- **D53 Decision:** v2 becomes the only session store, and the switch goes: + `--sessions-v2` and `FX_SESSIONS_V2` are removed, not kept as no-ops. + **Why:** a no-op flag is dead code, and every host keeps one path. + **Alternative:** accept the flag silently for one release. +- **D54 Decision:** v1's paused-response recovery is removed: + `fx ask --continue-recovery`, the app's offer to continue an interrupted + reply, and the recovery checkpoint files (`recovery.json`, + `recovery.asked`, `owner.live`). This settles D31. v2's interrupted turns + and running-call repair (D1, D28, D51) stay. The orchestrator's + checkpoint save also streams v2's finished pieces, so only its + full-turn rebuild goes. **Why:** v2 keeps every finished piece already, + and the checkpoint is a second recovery path. **Alternative:** port the + checkpoint to v2. +- **D55 Decision (amends D8 and D16):** the converter comes first, on v1's + existing read path, and v1 is removed after it, except that read path. + On every start, the new build imports each v1 session v2 does not hold, + once per id, keeping its id: a family, the root and the children in its + registry, under the v1 lock of every member, staged and then published + children first. A busy family is skipped and retried on a later start; + crash leftovers are swept before an import. A v1 session that changes + after its import is not imported again, and the converter never writes + a v1 file. A fresh v2 session never takes the id of a live v1 session + (R1). `tla/V1Conversion.tla` models this with older builds still + writing v1. **Why:** no window where the new build hides a user's v1 + sessions, and no v1 reader written twice. **Alternative:** remove v1 + first and write a fresh read-only importer; or re-import a v1 session + whose v2 copy got no new turn, which needs a stored fingerprint. + +Confirmed for the converter and the removal (2026-10-02; +D59 replaces D55's import at start with conversion on open): +- **D56 Decision:** besides the conversation and state, the converter + carries what a user would otherwise lose: side files as blobs with old + handles mapped as D47 maps them; ACP client prompts and tool identities + as D46's settings; hosted terminal state into `~/.fx/terminal/{id}` + (D45); `-c`'s remembered app session as v2's last-opened when v2 has + none; unsettled usage markers; and a `recovery.json` open turn as an + interrupted turn with its saved pieces (D1), exactly when v1 would show + it: v1 drops a checkpoint whose turn is not open in its log. **Why:** each is state a + v1 session holds outside `session.json` and its event log. + **Alternative:** convert the conversation only. +- **D57 Decision:** v1 is removed in one step after the converter ships: + the writer, store, listing, catalog, migration, recovery and every host + branch, leaving only the converter's read path. One release later the + converter and that path go too (D8). wasm and libfx persistence is + decided separately and blocks only the JS-host snapshot + store and the codec parts it needs. **Why:** each release ships one + store and no unused code. **Alternative:** remove v1 module by module + across several releases. + +Settled for `/fork` (2026-10-02): +- **D58 Decision:** `/fork` in the interactive app, on v2, opens a menu of + the session's prompts, oldest at the top and the newest selected, each + shown up to three lines and then `…`. Picking one forks the session + before that prompt: the manager's `open(.fork)` copies the log to the + end of the previous turn under a new id and hard-links the blobs (D5), + so the source is never written. The app switches to the fork as a + resume does, opening it before it closes the source (D41), writes + `original session fx --resume` and the source's id in the transcript, + and puts the + prompt back in the input box. The fork's title is the source's with + ` (fork)` once. `/fork` waits for a running turn to end, and without + v2 it says it needs `--sessions-v2`. Subagent children and hosted + terminals stay with the source, since the fold counts children only + after a fork point. The adapter adds two calls: `forkPoints`, each + turn's prompt and number, and `fork(before_turn, …)`. **Why:** the + manager already forks at turn boundaries, so the feature adds no + format and no new way to write a log. **Alternative:** fork after the + chosen turn's reply; or copy the log in fx instead of the manager. + `tla/Fork.tla` models the manager's fork at a boundary with blob links. + `tla/Wiring.tla` gains `Fork`: on v2, between turns and with no child + running, a session that never existed becomes the one to switch to, + and the source is not written (`ForkIsNewSession`, `ForkLeavesSource`, + `ForkBetweenTurns`). Every Bun E2E run of `/fork` is checked by TLC + through `tla/trace/bun_tlc_check.sh`: each process's `wiring` trace + against `Wiring`, and each saved log against `TurnLifecycle` and, for + a fork, `tla/trace/ForkLog.tla`, which accepts only a copy that is the + source's first lines byte for byte, ending at a turn boundary. + +Settled for the converter (2026-10-06): +- **D59 Decision (amends D55 and D57):** a v1 session converts when it + is opened, not at start. Every open (the app's resume, `-c`, the + picker and `/resume`, `fx ask`, ACP `session/load`) goes through one + function: it opens the v2 copy, or converts the family (the root and + the children in its registry, from one v1 state) and then opens it. + Start scans nothing. Listing shows v1 sessions not yet converted next + to v2 ones, v2 winning on an id (D60 dropped a rule for v2 deletions); + listing never converts. A conversion stages the family, writes it with one + fsync, publishes the children first, and ends with a snapshot so the + open after it takes the fast path; the manager gains this staged + import, since an import today syncs every batch. A busy v1 session is + refused as busy; an unreadable one is refused with the reason, its v1 + files untouched and nothing half converted. Later v1 writes by an + older build are ignored (as D55). A dim line says it is converting + only when it takes longer than about 150 ms. A convert-all command + ships with it, for sessions never opened before the converter goes. + Budget: convert plus open, p95 under 50 ms for sessions up to 1K + turns and under 200 ms at 10K turns, on a corpus of real v1 sessions, + gated by a benchmark. In the manager an import holds every batch, its + turns included, framed behind line 1 until `publishImport`, which + writes them through the first turn's staged publish: one write and one + fsync of the log, a folder fsync, the rename, a root fsync. Its blobs + go to `.tmp/{id}/blobs` first, and an abandoned import leaves only that + folder, which the next attempt clears. Batches keep their original + times until a host appends after the publish. `zig build bench`: 1K + turns import in 1.91 ms and 10K in 16.24 ms, half of each budget being + the ceiling. **Why:** no start cost and no background work; a session + pays once, when it is used. **Alternative:** the background import on + every start, as D55 first had it. +- **D60 Decision (amends D55 and D59; 2026-10-07):** once a + family's v2 copy is published and durable, the converter deletes the + family's v1 folders one by one while it still holds their v1 locks, so + a v1 session is kept once, not twice. Each folder is first renamed out + of v1's root into a trash folder neither store lists, so it disappears + in one step, then removed; a later conversion empties that trash. Each v2 member records the fingerprint + of the v1 version it copied. A v1 folder left behind (a crash between + the publish and the delete, or a delete the file system refused) is + deleted by a later open of that session only while its fingerprint + still matches; one an older build changed since is left alone, and + its later writes are ignored as D59 says. A refused delete does not + fail the open. Older fx versions no longer see a converted session. + With the v1 copy gone, a v2 deletion cannot bring it back, so D59's + rule that a v2 deletion hides a v1 id goes: no host deletes a v2 + session, and nothing would exercise it. **Why:** a converted session + should not take its space twice. **Alternative:** keep the v1 copy + until the converter is removed, or delete only from `fx sessions + convert`. +- **D61 Decision (2026-10-07, on the converter design's open + questions):** sessions in v1's older formats (schema 3 and legacy, about + 82% of a real profile) convert too, through v1's older reader; a slow + one shows the slow notice. So do v1 folders an old release left + world-readable (0755), which today's v1 refuses: others could only read + them, the v2 copy is private, and the readable v1 copy is deleted. `--resume last` picks the newest of the + merged listing. `fx session {id}` shows an unconverted v1 session read + only, without converting it. A converted session is a v2 session and + behaves as one: nothing special for converted sessions. The slow notice + shows in the app, on `fx ask`'s stderr, and to ACP clients. `fx + sessions convert` prints `converted N, busy N, unreadable N` and a line + per skipped session, and exits 1 when any was skipped. A damaged session's + error names the file and the reason. Internal, by the same pass: a + registry child whose v1 folder is gone is recorded as lost (D33); + taking a v1 lock may create a missing `session.lock`, which is not + content; a v1 child id opened directly answers SessionNotFound, as v2 + does; the sweep runs under the family's locks, so two processes + converting one family serialize, and `V1Conversion.tla` models two + converters. **Why:** the converter design left these open. **Alternative:** refuse the older formats, + or keep `fx session` v2 only. +- **D62 Decision (2026-10-07, after converting a clone of a + real profile: 13,970 families converted, 13 unreadable):** a conversion + first checks every member keeping nothing, then reads and stages one + member at a time, so memory holds at most one member (a 15-member + family had peaked at 3.6 GB); families with children are read twice. + A side file over v2's per-file limit (one real 16.8 GB command replay) + is left out, named in the trace and the convert output, and the rest of + the family converts. The v2 listing must stay fast at the size + conversion creates (about 14,000 sessions took 1.9 s a page): fixed in + this change, gated by the manager's benchmark. The usage marker move + (publish, the v2 marker, then the v1 marker's removal, then the folder) + is modeled in `V1Conversion.tla`. **Why:** the real run showed each + limit. **Alternative:** keep whole families in memory, refuse the + family, or fix the listing later. + +## Design Risks And Failure Behavior + +- **Stale index.** A crash between publish and the index append hides a + session until rebuild; `list` self-heals missing folders + (`tla/Catalog.tla`). +- **Wrong snapshot.** Snapshots are derived and can be ignored; a test + requires fold equivalence (`tla/ResumeSnapshot.tla`). A state too large + for one line gets no snapshot: the append succeeds, the diagnostic says + so, and resume folds from the previous snapshot. Found in the API check: + the error used to reach the host after its batch was written, skipping + that batch's `fsync`. +- **Seq reuse after a machine crash.** Only a seq past a durability point is + stable (`tla/SessionLog.tla`). +- **Power cut on macOS (accepted by D3).** + - The newest synced turns can be lost. + - A rare damaged middle line opens the session read-only up to the last + good line; damage older than the newest snapshot is found by `read` and + `verify` instead. + - The specs model only the guarantee a plain `fsync` gives: an fx or OS + crash, or a power cut on Linux. +- **Unmodeled wasm locking.** wasm's single writer relies on the embedder + honoring `expectedRevision`. `WriterLock.tla` models only flock; a buggy + embedder store could allow two writers. +- **Converter correctness.** It must handle every v1 format still on disk, + so it is tested against real sessions, including children and interrupted + turns. +- **A session continued in an old binary after conversion** keeps its newer + turns only in the v1 copy (D16). +- **Two locations per session.** The session folder and the terminal folder + (D13). A missed delete leaves an orphan terminal folder, which doctor + removes. +- **Behavior changes.** + - Creation at the first turn means a session-level `/model` or `/rename` + before any prompt is not kept in the session. + - An unused ACP session is not kept, and loading its id after a restart + returns NotFound (D24). + - Handles become hashes. + - The E2E suite must pass unchanged, or each difference must be approved. +- **Hard links.** Same filesystem only, which holds inside the sessions root; + a copy is the fallback. +- **Profile usage recovery.** The markers stay fx's. v2 sessions have their + own folder, `~/.fx/usage-recovery-v2/{id}`, read by the same recovery, + which compares the checkpoint's own time with the marker's instead of file + times (D20). +- **Side folder retired (D27, D48).** A v2 session no longer has side files; + older sessions move on their first writable open (D47). A move cut short + leaves the side folder until the next open, and doctor removes folders + whose session is gone. A missed terminal-folder delete is swept the same + way (D45). + +## Verification + +- **Changed contract:** + - unit tests at each level; + - tests asserting every invariant of the matching `tla/` spec; + - TLC runs of all eight specs plus `tla/mutants.py`; + - a fold-equivalence property test; + - trace validation of the code against the specs, where every trace from + unit tests, the driver and the crash matrix must be accepted by + `tla/trace/validate.sh`. The hook contract is in `tla/trace/README.md`. +- **Integration:** a standalone driver running the four native host thread + models through the API, plus a wasm host double over a fake `sessionStore`. +- **Failure:** + - `kill -9` at every append and durability step; + - a fault-injecting L0 that drops unsynced bytes and tears lines; + - flipped bits for the checksum; + - two processes contending for one session. +- **Migration:** the converter run against real v1 sessions from the current + release, including children, interrupted turns and wasm snapshots; a second + start converts only sessions created since. +- **Commands:** `fx session recover` on a session with a damaged middle line + produces a writable copy up to the last good turn; the source is + unchanged. +- **Permissions:** tests check `0700` folders, `0600` files and `0400` + blobs, and refuse a + symlinked session path. +- **Diagnostics:** every repair in the crash matrix emits exactly one + diagnostics event. +- **Real path:** fx built with v2 on, `./zig-out/bin/fx` exercised + interactively, through `fx ask` and through ACP; the fx E2E session suite + and `sdk/tests/test-term-session-resume.mjs` with v2 on. +- **Regression:** the E2E suite on v1 and on v2; the startup benchmark + unchanged. + +## Implementation Freedom + +- private names and the file split inside each level; +- allocator strategy; +- the JSON encoder; +- the backward-scan block size; +- fsync versus fdatasync on Linux; +- the blob threshold below the hard cap; +- the index rewrite threshold; +- the snapshot distance, tuned to 64 KB by the benchmark; +- test names and fixture layout. diff --git a/src/core/session_manager/tla/Catalog.cfg b/src/core/session_manager/tla/Catalog.cfg new file mode 100644 index 000000000..a34be8212 --- /dev/null +++ b/src/core/session_manager/tla/Catalog.cfg @@ -0,0 +1,9 @@ +SPECIFICATION Spec +CONSTANT Ids = {s1, s2, s3} +INVARIANTS + TypeOK + ListedAreLive + NoResurrection + IndexNamesPublished +PROPERTIES + RebuildIsExact diff --git a/src/core/session_manager/tla/Catalog.tla b/src/core/session_manager/tla/Catalog.tla new file mode 100644 index 000000000..86fcefcf3 --- /dev/null +++ b/src/core/session_manager/tla/Catalog.tla @@ -0,0 +1,156 @@ +----------------------------- MODULE Catalog ----------------------------- +(***************************************************************************) +(* Step: L3 catalog (index.jsonl). *) +(* *) +(* The index is derived. Publishing a folder happens before its index *) +(* put; delete renames the folder to .trash before its tombstone, then *) +(* purges it. A crash can land between any two steps and forgets owed *) +(* index writes. list() filters out entries whose folder is missing and *) +(* appends a tombstone for them (Heal). rebuild() re-derives the index *) +(* from live folders and purges .trash, atomically under index.lock. *) +(* *) +(* Design: system-design.md "Concurrency And Ordering" (index) and *) +(* "Reliability And Recovery". *) +(***************************************************************************) +EXTENDS Naturals, Sequences, FiniteSets + +CONSTANT Ids + +VARIABLES + dir, \* [Ids -> {"none", "live", "trash", "gone"}] + index, \* a sequence of [id, op], op \in {"put", "del"} + pending, \* [Ids -> {"none", "put", "del"}]: index write still owed + everDeleted \* ghost: ids that were ever deleted + +vars == <> + +LastOp(s) == + LET is == {i \in 1..Len(index) : index[i].id = s} IN + IF is = {} THEN "none" + ELSE index[CHOOSE i \in is : \A j \in is : j <= i].op + +Indexed == {s \in Ids : LastOp(s) = "put"} +Live == {s \in Ids : dir[s] = "live"} + +\* What list() returns: indexed entries whose folder exists. +Listed == {s \in Indexed : dir[s] = "live"} + +TypeOK == + /\ dir \in [Ids -> {"none", "live", "trash", "gone"}] + /\ pending \in [Ids -> {"none", "put", "del"}] + /\ everDeleted \subseteq Ids + +Init == + /\ dir = [s \in Ids |-> "none"] + /\ index = <<>> + /\ pending = [s \in Ids |-> "none"] + /\ everDeleted = {} + +\* First save: rename .tmp/{id} to {id}; the index put is owed next. +Publish(s) == + /\ dir[s] = "none" + /\ dir' = [dir EXCEPT ![s] = "live"] + /\ pending' = [pending EXCEPT ![s] = "put"] + /\ UNCHANGED <> + +IndexPut(s) == + /\ pending[s] = "put" + /\ index' = Append(index, [id |-> s, op |-> "put"]) + /\ pending' = [pending EXCEPT ![s] = "none"] + /\ UNCHANGED <> + +\* delete(): rename {id} to .trash/{id}; the tombstone is owed next. +Trash(s) == + /\ dir[s] = "live" + /\ pending[s] = "none" + /\ dir' = [dir EXCEPT ![s] = "trash"] + /\ pending' = [pending EXCEPT ![s] = "del"] + /\ everDeleted' = everDeleted \cup {s} + /\ UNCHANGED index + +IndexDel(s) == + /\ pending[s] = "del" + /\ index' = Append(index, [id |-> s, op |-> "del"]) + /\ pending' = [pending EXCEPT ![s] = "none"] + /\ UNCHANGED <> + +Purge(s) == + /\ dir[s] = "trash" + /\ pending[s] = "none" + /\ dir' = [dir EXCEPT ![s] = "gone"] + /\ UNCHANGED <> + +\* A resume, or a title, workspace or language change, rewrites the entry of +\* a live session (D42). The session holds its writer lock throughout, and +\* delete needs that lock (Busy), so no Trash lands inside it. Over an entry +\* already put, a refresh changes no last op, so the spec leaves that case +\* out; over a missing one, such as a publish put a crash forgot, it heals. +Refresh(s) == + /\ dir[s] = "live" + /\ LastOp(s) # "put" + /\ index' = Append(index, [id |-> s, op |-> "put"]) + /\ UNCHANGED <> + +\* A crash forgets every owed index write. +Crash == + /\ \E s \in Ids : pending[s] # "none" + /\ pending' = [s \in Ids |-> "none"] + /\ UNCHANGED <> + +\* list() self-heal: tombstone an indexed id whose folder is missing. +Heal(s) == + /\ s \in Indexed + /\ dir[s] # "live" + /\ index' = Append(index, [id |-> s, op |-> "del"]) + /\ UNCHANGED <> + +\* rebuild(): a fresh index with one put per live folder, then one del per +\* tombstoned id, each group in any order; .trash is purged. Tombstones +\* survive so a deleted id can never be re-imported or listed again. Owed +\* writes are dropped because the fresh index already reflects the folders. +Tombstoned == {s \in Ids : LastOp(s) = "del"} + +Rebuild == + /\ LET n == Cardinality(Live) + m == Cardinality(Tombstoned) + IN \E order \in [1..n -> Live], gone \in [1..m -> Tombstoned] : + /\ \A i, j \in 1..n : i # j => order[i] # order[j] + /\ \A i, j \in 1..m : i # j => gone[i] # gone[j] + /\ index' = [i \in 1..n |-> [id |-> order[i], op |-> "put"]] + \o [i \in 1..m |-> [id |-> gone[i], op |-> "del"]] + /\ dir' = [s \in Ids |-> IF dir[s] = "trash" THEN "gone" ELSE dir[s]] + /\ pending' = [s \in Ids |-> "none"] + /\ UNCHANGED everDeleted + +Next == + \/ \E s \in Ids : + \/ Publish(s) + \/ IndexPut(s) + \/ Refresh(s) + \/ Trash(s) + \/ IndexDel(s) + \/ Purge(s) + \/ Heal(s) + \/ Crash + \/ Rebuild + +Spec == Init /\ [][Next]_vars + +----------------------------------------------------------------------------- +(* Invariants *) + +\* list() never returns a session whose folder is gone. +ListedAreLive == Listed \subseteq Live + +\* A deleted id never comes back, in the list or on disk. +NoResurrection == + \A s \in everDeleted : s \notin Listed /\ dir[s] # "live" + +\* The index only ever names ids that were published. +IndexNamesPublished == + \A i \in 1..Len(index) : dir[index[i].id] # "none" + +(* Action property: right after rebuild(), the index lists exactly the *) +(* live folders. *) +RebuildIsExact == [][Rebuild => (Indexed' = Live')]_vars +============================================================================= diff --git a/src/core/session_manager/tla/Fork.cfg b/src/core/session_manager/tla/Fork.cfg new file mode 100644 index 000000000..f6b94f0f8 --- /dev/null +++ b/src/core/session_manager/tla/Fork.cfg @@ -0,0 +1,12 @@ +SPECIFICATION Spec +CONSTANTS + Ids = {s1, s2, s3} + Blobs = {b1, b2} + MaxLen = 4 + NoBlob = NoBlob +INVARIANTS + TypeOK + RefsExist + ForkKeepsPrefix + ForkAtBoundary + FirstLine diff --git a/src/core/session_manager/tla/Fork.tla b/src/core/session_manager/tla/Fork.tla new file mode 100644 index 000000000..cc347c3b5 --- /dev/null +++ b/src/core/session_manager/tla/Fork.tla @@ -0,0 +1,159 @@ +------------------------------- MODULE Fork ------------------------------- +(***************************************************************************) +(* Step: L2 fork and blobs. *) +(* *) +(* A blob file lands before any line can reference it. A fork copies *) +(* lines 2..S of its source at a turn boundary and hard-links the *) +(* source's blobs. Deleting a session removes its folder, log and links. *) +(* Invariants: every blob a live log references exists in that session, *) +(* unless the disk lost it there, and a fork keeps its copied prefix *) +(* whatever later happens to its source. A lost blob damages only its *) +(* session: a fork never copies a line that names one (D39). *) +(* *) +(* Design: system-design.md D5, D6 and D39. *) +(***************************************************************************) +EXTENDS Naturals, Sequences, FiniteSets + +CONSTANTS Ids, Blobs, MaxLen, NoBlob + +VARIABLES + st, \* [Ids -> {"none", "live", "deleted"}] + lg, \* [Ids -> Seq(entry)]: each session's log + links, \* [Ids -> SUBSET Blobs]: files present in {id}/blobs/ + base, \* [Ids -> Seq(entry)]: prefix copied at fork time (<<>> for roots) + lost \* [Ids -> SUBSET Blobs]: blob files the disk lost in that session + +vars == <> + +E(k, b) == [k |-> k, b |-> b] + +Count(l, k) == Cardinality({i \in 1..Len(l) : l[i].k = k}) +IsOpen(l) == Count(l, "start") > Count(l, "commit") + +TypeOK == + /\ st \in [Ids -> {"none", "live", "deleted"}] + /\ links \in [Ids -> SUBSET Blobs] + /\ lost \in [Ids -> SUBSET Blobs] + +Init == + /\ st = [s \in Ids |-> "none"] + /\ lg = [s \in Ids |-> <<>>] + /\ links = [s \in Ids |-> {}] + /\ base = [s \in Ids |-> <<>>] + /\ lost = [s \in Ids |-> {}] + +Create(s) == + /\ st[s] = "none" + /\ st' = [st EXCEPT ![s] = "live"] + /\ lg' = [lg EXCEPT ![s] = <>] + /\ UNCHANGED <> + +Start(s) == + /\ st[s] = "live" + /\ Len(lg[s]) < MaxLen + /\ ~IsOpen(lg[s]) + /\ lg' = [lg EXCEPT ![s] = Append(@, E("start", NoBlob))] + /\ UNCHANGED <> + +Commit(s) == + /\ st[s] = "live" + /\ Len(lg[s]) < MaxLen + /\ IsOpen(lg[s]) + /\ lg' = [lg EXCEPT ![s] = Append(@, E("commit", NoBlob))] + /\ UNCHANGED <> + +\* put_blob(): the file is installed before any line can reference it. +PutBlob(s, b) == + /\ st[s] = "live" + /\ b \notin links[s] + /\ links' = [links EXCEPT ![s] = @ \cup {b}] + /\ UNCHANGED <> + +\* append(item{blob}): the manager checks the blob exists in this session. +Item(s, b) == + /\ st[s] = "live" + /\ Len(lg[s]) < MaxLen + /\ IsOpen(lg[s]) + /\ b \in links[s] + /\ lg' = [lg EXCEPT ![s] = Append(@, E("item", b))] + /\ UNCHANGED <> + +\* append(set{blobs}): a setting may list blobs, inside a turn or outside it, +\* under the item's rule: the manager checks the blob exists in this +\* session. fx writes such lines when it moves a session off its side folder +\* (D47) and when its compactor keeps records (D50). One per session bounds +\* the states; more such lines behave as more items do. +SetBlob(s, b) == + /\ st[s] = "live" + /\ Len(lg[s]) < MaxLen + /\ Count(lg[s], "set") = 0 + /\ b \in links[s] + /\ lg' = [lg EXCEPT ![s] = Append(@, E("set", b))] + /\ UNCHANGED <> + +\* open(.fork{src, at}): only at a turn boundary, and only over lines +\* whose blobs the source still has (`.last_good` ends before the first +\* that names a lost one, D39). Line 1 is new; lines 2..at are copied +\* unchanged; every source blob is hard-linked. +Fork(src, f, at) == + /\ st[src] = "live" + /\ st[f] = "none" + /\ at \in 1..Len(lg[src]) + /\ ~IsOpen(SubSeq(lg[src], 1, at)) + /\ \A i \in 2..at : lg[src][i].b # NoBlob => lg[src][i].b \in links[src] + /\ LET copied == SubSeq(lg[src], 2, at) IN + /\ lg' = [lg EXCEPT ![f] = <> \o copied] + /\ base' = [base EXCEPT ![f] = copied] + /\ links' = [links EXCEPT ![f] = links[src]] + /\ st' = [st EXCEPT ![f] = "live"] + /\ UNCHANGED lost + +\* delete(): the folder, its log and its blob links go away. +Delete(s) == + /\ st[s] = "live" + /\ st' = [st EXCEPT ![s] = "deleted"] + /\ lg' = [lg EXCEPT ![s] = <<>>] + /\ links' = [links EXCEPT ![s] = {}] + /\ lost' = [lost EXCEPT ![s] = {}] + /\ UNCHANGED base + +\* The disk loses one blob file of a live session (D39). +Lose(s, b) == + /\ st[s] = "live" + /\ b \in links[s] + /\ links' = [links EXCEPT ![s] = @ \ {b}] + /\ lost' = [lost EXCEPT ![s] = @ \cup {b}] + /\ UNCHANGED <> + +Next == + \E s \in Ids : + \/ Create(s) + \/ Start(s) + \/ Commit(s) + \/ Delete(s) + \/ \E b \in Blobs : PutBlob(s, b) \/ Item(s, b) \/ SetBlob(s, b) \/ Lose(s, b) + \/ \E f \in Ids, at \in 1..MaxLen : Fork(s, f, at) + +Spec == Init /\ [][Next]_vars + +----------------------------------------------------------------------------- +(* Invariants *) + +\* Every blob a live log references is present in that session, unless the +\* disk lost it there: a fork never inherits a missing reference. +RefsExist == + \A s \in Ids : st[s] = "live" => + \A i \in 1..Len(lg[s]) : + lg[s][i].b # NoBlob => lg[s][i].b \in links[s] \cup lost[s] + +\* A fork's copied prefix is intact, whatever happened to its source. +ForkKeepsPrefix == + \A f \in Ids : st[f] = "live" => + SubSeq(lg[f], 2, Len(base[f]) + 1) = base[f] + +\* A fork never starts inside an open turn. +ForkAtBoundary == \A f \in Ids : ~IsOpen(base[f]) + +\* Line 1 of every live log is `created`. +FirstLine == \A s \in Ids : st[s] = "live" => lg[s][1].k = "created" +============================================================================= diff --git a/src/core/session_manager/tla/Lifecycle.cfg b/src/core/session_manager/tla/Lifecycle.cfg new file mode 100644 index 000000000..ded63a515 --- /dev/null +++ b/src/core/session_manager/tla/Lifecycle.cfg @@ -0,0 +1,7 @@ +SPECIFICATION Spec +CONSTANT Ids = {s1, s2} +INVARIANTS + TypeOK + VisibleHasLine1 + AckedIsVisible + NothingBeforeFirstTurn diff --git a/src/core/session_manager/tla/Lifecycle.tla b/src/core/session_manager/tla/Lifecycle.tla new file mode 100644 index 000000000..317542a77 --- /dev/null +++ b/src/core/session_manager/tla/Lifecycle.tla @@ -0,0 +1,135 @@ +---------------------------- MODULE Lifecycle ---------------------------- +(***************************************************************************) +(* Step: L2 lazy creation and publish. *) +(* *) +(* open(.new) touches nothing on disk. The first turn builds .tmp/{id}: *) +(* mkdir, write line 1, fsync the log, rename to {id}, fsync the parent *) +(* directory, and only then returns to the caller. An fx crash stops *) +(* the sequence anywhere. A machine crash can also undo an unsynced rename,*) +(* drop an unsynced mkdir, and drop line 1 if it was not fsynced. *) +(* Rebuild sweeps leftovers in .tmp. *) +(* *) +(* Design: system-design.md D2 and "Durable State And Schema" (publish). *) +(***************************************************************************) +EXTENDS Naturals + +CONSTANT Ids + +Steps == {"idle", "mem", "tmpdir", "written", "synced", "renamed", "done", "dead"} + +VARIABLES + step, \* [Ids -> Steps]: how far the first-turn publish has got + where, \* [Ids -> {"none", "tmp", "visible"}]: the folder on disk + line1, \* [Ids -> {"none", "cached", "durable"}]: line 1 on disk + acked \* [Ids -> BOOLEAN]: the caller was told the save succeeded + +vars == <> + +TypeOK == + /\ step \in [Ids -> Steps] + /\ where \in [Ids -> {"none", "tmp", "visible"}] + /\ line1 \in [Ids -> {"none", "cached", "durable"}] + /\ acked \in [Ids -> BOOLEAN] + +Init == + /\ step = [s \in Ids |-> "idle"] + /\ where = [s \in Ids |-> "none"] + /\ line1 = [s \in Ids |-> "none"] + /\ acked = [s \in Ids |-> FALSE] + +Advance(s, from, to) == + /\ step[s] = from + /\ step' = [step EXCEPT ![s] = to] + +OpenNew(s) == + /\ Advance(s, "idle", "mem") + /\ UNCHANGED <> + +MkTmp(s) == + /\ Advance(s, "mem", "tmpdir") + /\ where' = [where EXCEPT ![s] = "tmp"] + /\ UNCHANGED <> + +WriteLine1(s) == + /\ Advance(s, "tmpdir", "written") + /\ line1' = [line1 EXCEPT ![s] = "cached"] + /\ UNCHANGED <> + +FsyncLog(s) == + /\ Advance(s, "written", "synced") + /\ line1' = [line1 EXCEPT ![s] = "durable"] + /\ UNCHANGED <> + +Rename(s) == + /\ Advance(s, "synced", "renamed") + /\ where' = [where EXCEPT ![s] = "visible"] + /\ UNCHANGED <> + +\* fsync of sessions/v2/ makes the rename durable; then append() returns. +FsyncDirAndAck(s) == + /\ Advance(s, "renamed", "done") + /\ acked' = [acked EXCEPT ![s] = TRUE] + /\ UNCHANGED <> + +\* fx dies: every unfinished first-turn publish stops; the disk keeps what it has. +ProcessCrash == + /\ \E s \in Ids : step[s] \notin {"idle", "done", "dead"} + /\ step' = [s \in Ids |-> IF step[s] \in {"idle", "done"} THEN step[s] ELSE "dead"] + /\ UNCHANGED <> + +\* Machine crash (the PowerLoss action): like an fx crash, and unsynced directory changes and unsynced +\* line 1 bytes may also be lost. An unsynced rename may be undone, and when +\* the mkdir of .tmp/{id} was never synced either, the folder may be gone +\* from both places. Unsynced line 1 bytes may vanish or survive; after the +\* reboot, whatever survived is durable. +PowerLoss == + \E lose \in [Ids -> BOOLEAN], gone \in [Ids -> BOOLEAN], keep \in [Ids -> BOOLEAN] : + LET w == [s \in Ids |-> + CASE step[s] = "renamed" /\ lose[s] -> IF gone[s] THEN "none" ELSE "tmp" + [] where[s] = "tmp" /\ step[s] # "done" /\ lose[s] -> "none" + [] OTHER -> where[s]] + IN /\ where' = w + /\ line1' = [s \in Ids |-> + CASE w[s] = "none" -> "none" + [] line1[s] = "cached" /\ keep[s] -> "durable" + [] line1[s] = "cached" -> "none" + [] OTHER -> line1[s]] + /\ step' = [s \in Ids |-> + IF step[s] \in {"idle", "done"} THEN step[s] ELSE "dead"] + /\ UNCHANGED acked + +\* rebuild(): remove a leftover .tmp folder of a first-turn publish that died. +Sweep(s) == + /\ step[s] = "dead" + /\ where[s] = "tmp" + /\ where' = [where EXCEPT ![s] = "none"] + /\ line1' = [line1 EXCEPT ![s] = "none"] + /\ UNCHANGED <> + +Next == + \/ \E s \in Ids : + \/ OpenNew(s) + \/ MkTmp(s) + \/ WriteLine1(s) + \/ FsyncLog(s) + \/ Rename(s) + \/ FsyncDirAndAck(s) + \/ Sweep(s) + \/ ProcessCrash + \/ PowerLoss + +Spec == Init /\ [][Next]_vars + +----------------------------------------------------------------------------- +(* Invariants *) + +\* A visible session always has a durable first line. +VisibleHasLine1 == \A s \in Ids : where[s] = "visible" => line1[s] = "durable" + +\* An acknowledged first turn stays visible, even after a machine crash. +AckedIsVisible == \A s \in Ids : acked[s] => where[s] = "visible" + +\* open(.new) and settings held before the first turn never create anything on disk. +NothingBeforeFirstTurn == + \A s \in Ids : step[s] \in {"idle", "mem"} => where[s] = "none" +============================================================================= diff --git a/src/core/session_manager/tla/MoveSideFiles.cfg b/src/core/session_manager/tla/MoveSideFiles.cfg new file mode 100644 index 000000000..c8e0890ec --- /dev/null +++ b/src/core/session_manager/tla/MoveSideFiles.cfg @@ -0,0 +1,9 @@ +SPECIFICATION FairSpec +CONSTANT Handles = {h1, h2, h3} +INVARIANTS + TypeOK + Resolvable + TerminalKept + MapComplete +PROPERTIES + EventuallyDone diff --git a/src/core/session_manager/tla/MoveSideFiles.tla b/src/core/session_manager/tla/MoveSideFiles.tla new file mode 100644 index 000000000..35a2857ec --- /dev/null +++ b/src/core/session_manager/tla/MoveSideFiles.tla @@ -0,0 +1,126 @@ +--------------------------- MODULE MoveSideFiles --------------------------- +(***************************************************************************) +(* Step: fx wiring, moving an older v2 session off its side folder (D47). *) +(* *) +(* An older v2 session keeps large bodies and its terminal state in *) +(* ~/.fx/session-files/{id}/. On its first writable open fx puts each *) +(* body as a blob, writes one batch holding the map from old handles to *) +(* blobs and the two settings, renames the terminal folder to *) +(* ~/.fx/terminal/{id}/, and removes the side folder. One writer at a *) +(* time holds the session (WriterLock), and a crash can stop it between *) +(* any two steps; the next open starts again from what the disk holds. *) +(* A reader may resolve any old handle at any moment: through the map *) +(* once it is written, through the side folder before. *) +(* *) +(* Design: system-design.md D44 to D48. *) +(***************************************************************************) +EXTENDS Naturals, FiniteSets + +CONSTANTS Handles + +VARIABLES + side, \* SUBSET Handles: bodies still in the side folder + folder, \* "present" | "removed": the side folder itself + blobs, \* SUBSET Handles: bodies put as blobs of the session + mapped, \* TRUE once the batch with the map and settings is durable + terminal, \* "side" | "moved": where the terminal state lives + open \* TRUE while a writer is running the move + +vars == <> + +TypeOK == + /\ side \subseteq Handles + /\ folder \in {"present", "removed"} + /\ blobs \subseteq Handles + /\ mapped \in BOOLEAN + /\ terminal \in {"side", "moved"} + /\ open \in BOOLEAN + +Init == + /\ side = Handles + /\ folder = "present" + /\ blobs = {} + /\ mapped = FALSE + /\ terminal = "side" + /\ open = FALSE + +\* A writable open takes the session; the move runs inside it. +Open == + /\ ~open + /\ open' = TRUE + /\ UNCHANGED <> + +\* put_blob() of one side body; repeating it is harmless (content addressed). +PutBlob(h) == + /\ open + /\ ~mapped + /\ h \in side + /\ blobs' = blobs \cup {h} + /\ UNCHANGED <> + +\* One durable batch: `set moved_files` listing every blob, and the settings. +WriteMap == + /\ open + /\ ~mapped + /\ blobs = Handles + /\ mapped' = TRUE + /\ UNCHANGED <> + +\* Rename session-files/{id}/terminal to terminal/{id}. +MoveTerminal == + /\ open + /\ mapped + /\ terminal = "side" + /\ terminal' = "moved" + /\ UNCHANGED <> + +\* Remove the side folder and everything left in it. +RemoveSide == + /\ open + /\ mapped + /\ terminal = "moved" + /\ folder = "present" + /\ folder' = "removed" + /\ side' = {} + /\ UNCHANGED <> + +\* The writer stops: a clean close or a crash between any two steps. +Stop == + /\ open + /\ open' = FALSE + /\ UNCHANGED <> + +Done == folder = "removed" + +Next == + \/ Open + \/ \E h \in Handles : PutBlob(h) + \/ WriteMap + \/ MoveTerminal + \/ RemoveSide + \/ Stop + +Spec == Init /\ [][Next]_vars + +\* Writers keep coming back, and a step enabled again and again eventually +\* runs (a crash can stop any one open, not every open). +FairSpec == Spec /\ WF_vars(Open) /\ SF_vars(WriteMap) /\ SF_vars(MoveTerminal) + /\ SF_vars(RemoveSide) /\ \A h \in Handles : SF_vars(PutBlob(h)) + +----------------------------------------------------------------------------- +(* Invariants *) + +\* Every old handle resolves at every moment: through the map once it is +\* written, through the side folder before. +Resolvable == + \A h \in Handles : (mapped /\ h \in blobs) \/ (~mapped /\ h \in side) + +\* The terminal state is never lost: the side folder goes only after it moved. +TerminalKept == folder = "removed" => terminal = "moved" + +\* The map names only bodies that exist as blobs. +MapComplete == mapped => blobs = Handles + +\* Liveness under FairSpec: the move eventually finishes and stays finished. +EventuallyDone == <>[]Done +============================================================================= diff --git a/src/core/session_manager/tla/README.md b/src/core/session_manager/tla/README.md new file mode 100644 index 000000000..649745020 --- /dev/null +++ b/src/core/session_manager/tla/README.md @@ -0,0 +1,148 @@ +# TLA+ models + +One model per step of the design. Each one checks the protocol described in +`../system-design.md`, not the Zig code. The bridge to the code is that every +invariant below also becomes a test assertion for the step it models. + +**Status: all eight specs parse (SANY) and pass TLC. Each one also catches +its planted bugs (`./mutants.py`).** Last run: 2026-09-27, TLC2 2.19 (rev +5a47802), OpenJDK 27 on macOS arm64. + +| Spec | States generated | Distinct states | Search depth | Result | +|---|---|---|---|---| +| `SessionLog` | 686 | 110 | 15 | No error | +| `TurnLifecycle` | 21,684 | 19,352 | 14 | No error | +| `WriterLock` | 3,257 | 1,016 | 24 | No error | +| `ResumeSnapshot` | 5,461 | 5,461 | 7 | No error | +| `Fork` | 375,727 | 51,776 | 16 | No error | +| `Subagents` | 204,097 | 120,297 | 23 | No error | +| `Catalog` | 645,269 | 94,482 | 19 | No error | +| `Lifecycle` | 9,553 | 144 | 13 | No error | + +Every run explored the whole bounded state space (0 states left on the queue). + +`Lifecycle`'s `PowerLoss` was widened on 2026-09-27, when trace validation +compared it with real disk behavior. A renamed but unsynced publish may also +vanish from both folders (when the `mkdir` of `.tmp/{id}` was never synced +either), and unsynced line 1 bytes may survive as well as vanish. The spec +still passes, and both of its mutants are still caught. + +`Catalog`'s `Rebuild` was widened the same day to keep a `del` for every +tombstoned id after its fresh `put` lines, as the code does, so a deleted id +stays deleted through a rebuild and cannot be re-imported. The spec still +passes, and its mutant is still caught. + +`Subagents` was widened on 2026-09-27 for D22 (the pre-wiring API check): +work numbers per child, at most one unfinished work item per child, `failed` +finishes and a parent `cancelled`. `LostMeansNoLog` became an action +property, checked on the step that writes the line, because a persistent +child marked lost for one work item may create its log with a later one. + +`./mutants.py` plants 14 realistic bugs, one to three per spec, and requires +TLC to report the matching invariant or action property as violated. All 14 +are caught: + +- fsync acknowledging a half-written line +- open() keeping a torn tail +- reopen skipping `turn_interrupted` +- accepting an item outside a turn +- open ignoring the flock +- a snapshot with the wrong state +- a fork forgetting blob links +- a fork inside an open turn +- repair marking every child lost +- a spawn while the child's work is open +- reopen skipping child repair +- list skipping the folder check +- rename before the line 1 fsync +- ack before the directory fsync + +## The specs + +| Spec | Step (level) | What it proves | Invariants | +|---|---|---|---| +| `SessionLog.tla` | Log append, fsync, fx crash, machine crash, torn tail (L1) | Acknowledged lines survive a machine crash; only the final line can be torn; open() leaves no torn line | `SeqContiguous`, `OnlyTailTorn`, `AckedSurvive`, `OpenIsClean` | +| `TurnLifecycle.tla` | Turn rules, close, crash, reopen (L2) | The manager only writes valid turn transitions; close and reopen never leave a stale open turn; the log is only ever extended | `StartsWithCreated`, `AtMostOneOpenTurn`, `ItemsInsideTurns`, `EndsCloseATurn`, `ClosedOnlyBetweenTurns`, `NoStaleTurnAfterReopen`, property `AppendOnly` | +| `WriterLock.tla` | flock across processes, Session mutex across threads (L0, L2) | One writing process; file order equals seq order across threads and after takeover | `OneWriter`, `OnlyHolderOpen`, `MutexInsideOpenSession`, `SeqIsPosition` | +| `ResumeSnapshot.tla` | Fold and resume from a snapshot (L2) | Resuming from the newest snapshot equals a full replay; snapshots can be dropped | `ResumeEqualsFullReplay`, `SnapshotsAreIgnorable` | +| `Lifecycle.tla` | Lazy creation and publish (L2) | Nothing on disk before the first turn; a visible session has a durable line 1; an acknowledged first turn survives a machine crash | `VisibleHasLine1`, `AckedIsVisible`, `NothingBeforeFirstTurn` | +| `Fork.tla` | Fork and blobs (L2) | Every referenced blob exists; a fork keeps its prefix after the source changes or is deleted; forks start at turn boundaries | `RefsExist`, `ForkKeepsPrefix`, `ForkAtBoundary`, `FirstLine` | +| `Subagents.tla` | Children, persistent work, cancel, parent crash and repair (L2) | Every work item ends in a known state; one unfinished work item per child; `lost` only without a log; no orphan child logs | `OneOpenWork`, `FinishClosesOpenWork`, `NoOrphanChild`, `NoIndeterminate`, property `LostMeansNoLog` | +| `Catalog.tla` | index.jsonl, list self-heal, delete, rebuild (L3) | list never returns a missing session; a deleted id never comes back; rebuild is exact | `ListedAreLive`, `NoResurrection`, `IndexNamesPublished`, property `RebuildIsExact` | + +Every spec also checks `TypeOK` where one is defined. + +**What the `PowerLoss` action means.** It models a machine crash: the OS +goes down without flushing the page cache, and only synced bytes survive. +With D3's plain `fsync`, that covers: + +- an OS crash (kernel panic or freeze) on every platform; +- a power cut on Linux. + +A power cut on macOS can also lose recently synced data from the drive's own +cache. D3 accepts that, and it is outside these models. The action keeps its +name so the trace event contract and the mutants stay stable. + +## Running + +```sh +./check.sh # all specs +./check.sh SessionLog Fork # some specs +./mutants.py # every planted bug must still be caught +``` + +Requirements: + +- OpenJDK: `brew install openjdk`. It is keg-only, so it is not on PATH; + both scripts find it at `/opt/homebrew/opt/openjdk/bin/java`. +- `tla2tools.jar`: `~/.local/share/tla/tla2tools.jar`. Override the location + with `TLA2TOOLS_JAR`. + +`check.sh` runs TLC with `-deadlock`, because every model is bounded and stops +at its bound, and it keeps TLC's state files outside this folder. When you add +an invariant, add a mutant to `mutants.py` that breaks it. + +## Checking the code, not just the design + +The models above check the design. To check that the Zig code actually +behaves like them, the code writes a trace of its steps in test builds, and +TLC validates that trace against the same specs. See +[trace/README.md](trace/README.md). + +```sh +./trace/validate.sh SessionLog run.ndjson # ACCEPTED, or REJECTED at step N +./trace/selftest.sh # the validator must accept and reject +``` + +## What the models do not cover + +- Byte encoding, JSON parsing and line size caps. Those are covered by unit + tests. +- Byte offsets. `Fork.tla` copies lines as values, so it cannot see that a + snapshot's `compaction_offset` moves when the fork's line 1 is longer; the + driver found that, and the fork now encodes each copied snapshot again + (`session.zig` test "a fork after a compaction and snapshots"). +- Which bytes open reads. `SessionLog.tla` recovers a whole log; the manager + reads only line 1, the newest snapshot and what follows, so older damage + is found by `read` and `verify` (`system-design.md` Reliability And + Recovery; the driver's bit-flip cells cover every region). +- Code paths that no test runs. Trace validation (above) covers only the + runs we execute. +- Performance. That is the benchmark in `../system-design.md` Performance + And Capacity. +- The fx adapter and host policy, such as when to offer "continue". Those are + covered by fx E2E tests. +- Liveness (for example "every child eventually finishes"). The models check + safety only. Liveness would need fairness assumptions about the model + provider, which the manager does not control. +- Model bounds. Small bounds (2 or 3 ids, logs of 4 to 7 lines) find ordering + and crash-window bugs, but they do not prove behavior at every size. Raise + a bound in a spec's `.cfg` when a bug is suspected past it. + +## Keeping the models honest + +When a decision in `../system-design.md` changes, update the spec that models +it in the same change. If TLC finds a counterexample: + +1. If the spec is wrong, fix the spec. +2. If the design is wrong, fix `system-design.md` first, then the spec. diff --git a/src/core/session_manager/tla/ResumeSnapshot.cfg b/src/core/session_manager/tla/ResumeSnapshot.cfg new file mode 100644 index 000000000..25c0be016 --- /dev/null +++ b/src/core/session_manager/tla/ResumeSnapshot.cfg @@ -0,0 +1,8 @@ +SPECIFICATION Spec +CONSTANTS + Vals = {v1, v2} + MaxLen = 6 + NoVal = NoVal +INVARIANTS + ResumeEqualsFullReplay + SnapshotsAreIgnorable diff --git a/src/core/session_manager/tla/ResumeSnapshot.tla b/src/core/session_manager/tla/ResumeSnapshot.tla new file mode 100644 index 000000000..2a9dfc07d --- /dev/null +++ b/src/core/session_manager/tla/ResumeSnapshot.tla @@ -0,0 +1,91 @@ +-------------------------- MODULE ResumeSnapshot -------------------------- +(***************************************************************************) +(* Step: L2 fold and resume. *) +(* *) +(* open(.resume) folds from the newest snapshot instead of line 1. This *) +(* spec states the contract that makes that safe: resuming from the *) +(* newest snapshot gives exactly the state of a full replay, and the *) +(* snapshot lines themselves can be dropped without changing any state. *) +(* The Zig implementation must pass the same two checks as property *) +(* tests. *) +(* *) +(* Design: system-design.md "Fold". *) +(***************************************************************************) +EXTENDS Naturals, Sequences + +CONSTANTS Vals, MaxLen, NoVal + +Empty == [pref |-> NoVal, turns |-> 0, open |-> FALSE] + +\* Every line has the same record shape; `st` is used only by snapshots. +Entry(k, v, s) == [k |-> k, v |-> v, st |-> s] + +Step(s, e) == + CASE e.k = "set" -> [s EXCEPT !.pref = e.v] + [] e.k = "start" -> [s EXCEPT !.open = TRUE] + [] e.k = "commit" -> [s EXCEPT !.open = FALSE, !.turns = @ + 1] + [] OTHER -> s \* snapshot lines change nothing + +RECURSIVE FoldFrom(_, _, _) +FoldFrom(l, i, s) == + IF i > Len(l) THEN s ELSE FoldFrom(l, i + 1, Step(s, l[i])) + +Full(l) == FoldFrom(l, 1, Empty) + +SnapIdx(l) == {i \in 1..Len(l) : l[i].k = "snap"} + +LastSnap(l) == + IF SnapIdx(l) = {} THEN 0 + ELSE CHOOSE i \in SnapIdx(l) : \A j \in SnapIdx(l) : j <= i + +\* What open(.resume) computes: the newest snapshot, then fold the tail. +Resume(l) == + LET j == LastSnap(l) IN + IF j = 0 THEN Full(l) ELSE FoldFrom(l, j + 1, l[j].st) + +RECURSIVE Strip(_) +Strip(l) == + IF l = <<>> THEN <<>> + ELSE IF Head(l).k = "snap" THEN Strip(Tail(l)) + ELSE <> \o Strip(Tail(l)) + +VARIABLES log +vars == <> + +Init == log = <<>> + +Set(v) == + /\ Len(log) < MaxLen + /\ log' = Append(log, Entry("set", v, Empty)) + +Start == + /\ Len(log) < MaxLen + /\ ~Full(log).open + /\ log' = Append(log, Entry("start", NoVal, Empty)) + +Commit == + /\ Len(log) < MaxLen + /\ Full(log).open + /\ log' = Append(log, Entry("commit", NoVal, Empty)) + +\* The manager writes a snapshot of the state folded so far. Snapshots +\* may land anywhere, including inside an open turn. +Snapshot == + /\ Len(log) < MaxLen + /\ log' = Append(log, Entry("snap", NoVal, Full(log))) + +Next == + \/ \E v \in Vals : Set(v) + \/ Start + \/ Commit + \/ Snapshot + +Spec == Init /\ [][Next]_vars + +----------------------------------------------------------------------------- +(* Invariants *) + +ResumeEqualsFullReplay == Resume(log) = Full(log) + +SnapshotsAreIgnorable == Full(Strip(log)) = Full(log) +============================================================================= diff --git a/src/core/session_manager/tla/SessionLog.cfg b/src/core/session_manager/tla/SessionLog.cfg new file mode 100644 index 000000000..137d9f427 --- /dev/null +++ b/src/core/session_manager/tla/SessionLog.cfg @@ -0,0 +1,8 @@ +SPECIFICATION Spec +CONSTANT MaxLines = 4 +INVARIANTS + TypeOK + SeqContiguous + OnlyTailTorn + AckedSurvive + OpenIsClean diff --git a/src/core/session_manager/tla/SessionLog.tla b/src/core/session_manager/tla/SessionLog.tla new file mode 100644 index 000000000..3f5a34cc0 --- /dev/null +++ b/src/core/session_manager/tla/SessionLog.tla @@ -0,0 +1,122 @@ +---------------------------- MODULE SessionLog ---------------------------- +(***************************************************************************) +(* Step: L1 log. One append-only log file. *) +(* *) +(* Models write() into the page cache, fsync at a durability point, an fx *) +(* crash (the kernel keeps every written byte), a machine crash (only the *) +(* fsynced prefix is guaranteed; the rest may be lost and the new last *) +(* line may be torn) and the torn-tail cut plus fsync done by open(). *) +(* *) +(* Design: system-design.md "Line format" and "Durable State And Schema". *) +(***************************************************************************) +EXTENDS Naturals, Sequences + +CONSTANT MaxLines + +VARIABLES + log, \* file contents: a sequence of lines [seq, done] + durable, \* length of the prefix that is on stable storage + acked, \* number of lines a caller was told are durable + status \* "open", "writing" or "down" + +vars == <> + +Line(n, d) == [seq |-> n, done |-> d] + +LastDone == Len(log) = 0 \/ log[Len(log)].done + +TypeOK == + /\ log \in Seq([seq : 1..MaxLines, done : BOOLEAN]) + /\ Len(log) <= MaxLines + /\ durable \in 0..MaxLines + /\ acked \in 0..MaxLines + /\ status \in {"open", "writing", "down"} + +Init == + /\ log = <<>> + /\ durable = 0 + /\ acked = 0 + /\ status = "open" + +(* write() starts: bytes are in the page cache, the newline is not yet. *) +BeginWrite == + /\ status = "open" + /\ Len(log) < MaxLines + /\ log' = Append(log, Line(Len(log) + 1, FALSE)) + /\ status' = "writing" + /\ UNCHANGED <> + +(* write() returns: the whole line, including its newline, is written. *) +FinishWrite == + /\ status = "writing" + /\ log' = [log EXCEPT ![Len(log)].done = TRUE] + /\ status' = "open" + /\ UNCHANGED <> + +(* Durability point: fsync, then acknowledge to the caller. *) +Fsync == + /\ status = "open" + /\ durable' = Len(log) + /\ acked' = Len(log) + /\ UNCHANGED <> + +(* fx dies. The kernel keeps every byte already written. *) +ProcessCrash == + /\ status \in {"open", "writing"} + /\ status' = "down" + /\ UNCHANGED <> + +(* Machine crash (OS crash, or a power cut on Linux; D3 leaves a macOS *) +(* power cut outside the model): bytes after the durable prefix may be *) +(* lost, and the new *) +(* last line may be torn. *) +PowerLoss == + /\ \E k \in durable..Len(log), torn \in BOOLEAN : + LET kept == SubSeq(log, 1, k) IN + log' = IF torn /\ k > durable + THEN [kept EXCEPT ![k].done = FALSE] + ELSE kept + /\ status' = "down" + /\ UNCHANGED <> + +(* open(.resume): cut a torn last line, fsync, accept writes again. *) +Recover == + /\ status = "down" + /\ LET repaired == IF LastDone THEN log ELSE SubSeq(log, 1, Len(log) - 1) + IN /\ log' = repaired + /\ durable' = Len(repaired) + /\ status' = "open" + /\ UNCHANGED acked + +Next == + \/ BeginWrite + \/ FinishWrite + \/ Fsync + \/ ProcessCrash + \/ PowerLoss + \/ Recover + +Spec == Init /\ [][Next]_vars + +----------------------------------------------------------------------------- +(* Invariants *) + +\* seq equals the line's position: no gaps and no duplicates. +SeqContiguous == \A i \in 1..Len(log) : log[i].seq = i + +\* Only the final line can be incomplete. +OnlyTailTorn == \A i \in 1..(Len(log) - 1) : log[i].done + +\* A line the caller was told is durable is never lost or torn. +AckedSurvive == + /\ acked <= durable + /\ durable <= Len(log) + /\ \A i \in 1..acked : log[i].done + +\* An open log never ends in a torn line. +OpenIsClean == status = "open" => LastDone + +(* Note: after a machine crash, a line past `acked` can vanish and its seq *) +(* is handed out again. Hosts must treat only acknowledged seqs as *) +(* stable (system-design.md "Acknowledged seq"). *) +============================================================================= diff --git a/src/core/session_manager/tla/Subagents.cfg b/src/core/session_manager/tla/Subagents.cfg new file mode 100644 index 000000000..336660eff --- /dev/null +++ b/src/core/session_manager/tla/Subagents.cfg @@ -0,0 +1,11 @@ +SPECIFICATION Spec +CONSTANT Children = {c1, c2} +CONSTANT MaxWork = 2 +INVARIANTS + TypeOK + OneOpenWork + FinishClosesOpenWork + NoOrphanChild + NoIndeterminate +PROPERTY + LostMeansNoLog diff --git a/src/core/session_manager/tla/Subagents.tla b/src/core/session_manager/tla/Subagents.tla new file mode 100644 index 000000000..1d92c48ca --- /dev/null +++ b/src/core/session_manager/tla/Subagents.tla @@ -0,0 +1,170 @@ +---------------------------- MODULE Subagents ---------------------------- +(***************************************************************************) +(* Step: L2 children. *) +(* *) +(* The parent log records child_spawned (durable) before the child's work *) +(* starts. A child's first turn creates its own log; a persistent child's *) +(* later work runs in that same log. The child thread appends *) +(* child_finished (ok or failed), or the parent cancels the work *) +(* (cancelled). A crash can land between any two steps. On parent reopen, *) +(* the manager closes every unfinished work item: `lost` if the child has *) +(* no log, `interrupted` if it has one. *) +(* *) +(* A child has at most one unfinished work item (D22); its later work *) +(* items are new spawn/finish pairs with the next work number. fx's *) +(* `data` on these lines is opaque to the manager and not modeled. *) +(* *) +(* Design: system-design.md kinds table, "Reliability And Recovery" and *) +(* D22. *) +(***************************************************************************) +EXTENDS Naturals, Sequences, FiniteSets + +CONSTANTS Children, MaxWork + +VARIABLES + plog, \* parent log: a sequence of [k, c, w, o] + childLog, \* [Children -> BOOLEAN]: {c}/log.jsonl exists + thread, \* [Children -> {"none", "starting", "running"}], in memory + up, \* the fx process is running + repairing \* reopen repair is in progress + +vars == <> + +Outcomes == {"ok", "failed", "cancelled", "interrupted", "lost"} + +Count(s, k, c) == Cardinality({i \in 1..Len(s) : s[i].k = k /\ s[i].c = c}) +Works(c) == Count(plog, "spawned", c) +Unfinished(c) == Works(c) > Count(plog, "finished", c) +Spawned(c) == Works(c) > 0 + +TypeOK == + /\ \A i \in 1..Len(plog) : + /\ plog[i].k \in {"spawned", "finished"} + /\ plog[i].c \in Children + /\ plog[i].w \in 1..MaxWork + /\ plog[i].o \in Outcomes \cup {"none"} + /\ childLog \in [Children -> BOOLEAN] + /\ thread \in [Children -> {"none", "starting", "running"}] + /\ up \in BOOLEAN + /\ repairing \in BOOLEAN + +Init == + /\ plog = <<>> + /\ childLog = [c \in Children |-> FALSE] + /\ thread = [c \in Children |-> "none"] + /\ up = TRUE + /\ repairing = FALSE + +Normal == up /\ ~repairing + +\* 1. The parent appends child_spawned (fsynced), then starts the thread. +\* Refused while the child still has unfinished work. +Spawn(c) == + /\ Normal + /\ ~Unfinished(c) + /\ Works(c) < MaxWork + /\ plog' = Append(plog, [k |-> "spawned", c |-> c, w |-> Works(c) + 1, o |-> "none"]) + /\ thread' = [thread EXCEPT ![c] = "starting"] + /\ UNCHANGED <> + +\* 2. The child's work starts a turn; the first one publishes its log. +ChildStart(c) == + /\ Normal + /\ thread[c] = "starting" + /\ childLog' = [childLog EXCEPT ![c] = TRUE] + /\ thread' = [thread EXCEPT ![c] = "running"] + /\ UNCHANGED <> + +\* 3. The child finishes and appends child_finished to the parent. +ChildFinish(c) == + /\ Normal + /\ thread[c] = "running" + /\ \E o \in {"ok", "failed"} : + plog' = Append(plog, [k |-> "finished", c |-> c, w |-> Works(c), o |-> o]) + /\ thread' = [thread EXCEPT ![c] = "none"] + /\ UNCHANGED <> + +\* 3'. The parent cancels the child's unfinished work and stops its thread. +Cancel(c) == + /\ Normal + /\ thread[c] \in {"starting", "running"} + /\ plog' = Append(plog, [k |-> "finished", c |-> c, w |-> Works(c), o |-> "cancelled"]) + /\ thread' = [thread EXCEPT ![c] = "none"] + /\ UNCHANGED <> + +\* The process dies anywhere. Durable lines stay; threads are gone. +Crash == + /\ up + /\ up' = FALSE + /\ thread' = [c \in Children |-> "none"] + /\ repairing' = FALSE + /\ UNCHANGED <> + +\* Parent reopen: repair runs before any normal work. +Reopen == + /\ ~up + /\ up' = TRUE + /\ repairing' = TRUE + /\ UNCHANGED <> + +RepairChild(c) == + /\ up + /\ repairing + /\ Unfinished(c) + /\ plog' = Append(plog, [k |-> "finished", c |-> c, w |-> Works(c), + o |-> IF childLog[c] THEN "interrupted" ELSE "lost"]) + /\ UNCHANGED <> + +RepairDone == + /\ up + /\ repairing + /\ \A c \in Children : ~Unfinished(c) + /\ repairing' = FALSE + /\ UNCHANGED <> + +Next == + \/ \E c \in Children : + \/ Spawn(c) + \/ ChildStart(c) + \/ ChildFinish(c) + \/ Cancel(c) + \/ RepairChild(c) + \/ Crash + \/ Reopen + \/ RepairDone + +Spec == Init /\ [][Next]_vars + +----------------------------------------------------------------------------- +(* Invariants *) + +\* A child has at most one unfinished work item. +OneOpenWork == + \A c \in Children : + Count(plog, "finished", c) <= Works(c) /\ Works(c) <= Count(plog, "finished", c) + 1 + +\* Every child_finished closes that child's newest work item, which was +\* unfinished until then: no finish before its spawn, none twice. +FinishClosesOpenWork == + \A i \in 1..Len(plog) : + plog[i].k = "finished" => + LET p == SubSeq(plog, 1, i - 1) IN + /\ Count(p, "spawned", plog[i].c) = Count(p, "finished", plog[i].c) + 1 + /\ plog[i].w = Count(p, "spawned", plog[i].c) + +\* A child log never exists without a spawn line in the parent. +NoOrphanChild == \A c \in Children : childLog[c] => Spawned(c) + +\* `lost` is recorded only when the child really has no log at that moment. +\* An action property: a persistent child marked lost for one work item may +\* create its log with a later one. +LostMeansNoLog == + [][\A i \in (Len(plog) + 1)..Len(plog') : + (plog'[i].k = "finished" /\ plog'[i].o = "lost") => ~childLog[plog'[i].c]]_vars + +\* Outside repair, every unfinished work item has a live thread: no child +\* is ever left in an unknown state. +NoIndeterminate == + Normal => \A c \in Children : + Unfinished(c) => thread[c] \in {"starting", "running"} +============================================================================= diff --git a/src/core/session_manager/tla/TurnLifecycle.cfg b/src/core/session_manager/tla/TurnLifecycle.cfg new file mode 100644 index 000000000..3576de3fe --- /dev/null +++ b/src/core/session_manager/tla/TurnLifecycle.cfg @@ -0,0 +1,12 @@ +SPECIFICATION Spec +CONSTANT MaxLen = 7 +INVARIANTS + TypeOK + StartsWithCreated + AtMostOneOpenTurn + ItemsInsideTurns + EndsCloseATurn + ClosedOnlyBetweenTurns + NoStaleTurnAfterReopen +PROPERTIES + AppendOnly diff --git a/src/core/session_manager/tla/TurnLifecycle.tla b/src/core/session_manager/tla/TurnLifecycle.tla new file mode 100644 index 000000000..843363c59 --- /dev/null +++ b/src/core/session_manager/tla/TurnLifecycle.tla @@ -0,0 +1,127 @@ +--------------------------- MODULE TurnLifecycle --------------------------- +(***************************************************************************) +(* Step: L2 turn rules, close, crash and reopen repair. *) +(* *) +(* A host may ask for any kind in any order. The manager appends only *) +(* valid transitions and rejects the rest (InvalidTransition). close() *) +(* interrupts an open turn before `closed`. open(.resume) interrupts a *) +(* turn left open by a crash. Byte-level durability is SessionLog.tla's *) +(* job; here a crash keeps the log exactly as written. Every interrupt *) +(* reason (host: cancel, failed; manager: closed, crash) is one *) +(* "interrupt": the turn rules do not depend on it (D21). *) +(* *) +(* Design: system-design.md kinds table and "Fold". *) +(***************************************************************************) +EXTENDS Naturals, Sequences, FiniteSets + +CONSTANT MaxLen + +HostKinds == {"start", "item", "compacted", "commit", "interrupt", "set"} +Kinds == HostKinds \cup {"created", "closed"} + +VARIABLES + log, \* the session log as a sequence of kinds + status, \* "new", "open", "closed" or "down" + fresh \* TRUE right after open(.resume), until the next turn starts + +vars == <> + +Count(l, k) == Cardinality({i \in 1..Len(l) : l[i] = k}) +Ends(l) == Count(l, "commit") + Count(l, "interrupt") +IsOpen(l) == Count(l, "start") > Ends(l) + +Prefix(a, b) == Len(a) <= Len(b) /\ SubSeq(b, 1, Len(a)) = a + +\* What the manager accepts from a host. +Valid(l, k) == + CASE k = "start" -> ~IsOpen(l) + [] k = "item" -> IsOpen(l) + [] k = "commit" -> IsOpen(l) + [] k = "interrupt" -> IsOpen(l) + [] k = "compacted" -> TRUE + [] k = "set" -> TRUE + +TypeOK == + /\ log \in Seq(Kinds) + /\ status \in {"new", "open", "closed", "down"} + /\ fresh \in BOOLEAN + +Init == + /\ log = <<>> + /\ status = "new" + /\ fresh = FALSE + +\* The first turn publishes the session with line 1 (D2). +Create == + /\ status = "new" + /\ log' = <<"created">> + /\ status' = "open" + /\ UNCHANGED fresh + +\* A host asks to append k; only valid kinds are written. +Write(k) == + /\ status = "open" + /\ Len(log) < MaxLen + /\ Valid(log, k) + /\ log' = Append(log, k) + /\ fresh' = (fresh /\ k # "start") + /\ UNCHANGED status + +\* close(): an open turn is interrupted, then `closed` is appended. +Close == + /\ status = "open" + /\ Len(log) + 2 <= MaxLen + /\ log' = IF IsOpen(log) + THEN log \o <<"interrupt", "closed">> + ELSE Append(log, "closed") + /\ status' = "closed" + /\ fresh' = FALSE + +\* fx dies with the session open. +Crash == + /\ status = "open" + /\ status' = "down" + /\ UNCHANGED <> + +\* open(.resume): a turn left open by a crash gets turn_interrupted. +Reopen == + /\ status \in {"closed", "down"} + /\ Len(log) < MaxLen + /\ log' = IF IsOpen(log) THEN Append(log, "interrupt") ELSE log + /\ status' = "open" + /\ fresh' = TRUE + +Next == + \/ Create + \/ \E k \in HostKinds : Write(k) + \/ Close + \/ Crash + \/ Reopen + +Spec == Init /\ [][Next]_vars + +----------------------------------------------------------------------------- +(* Invariants *) + +StartsWithCreated == Len(log) > 0 => log[1] = "created" + +AtMostOneOpenTurn == Count(log, "start") - Ends(log) \in {0, 1} + +ItemsInsideTurns == + \A i \in 1..Len(log) : + log[i] = "item" => IsOpen(SubSeq(log, 1, i - 1)) + +EndsCloseATurn == + \A i \in 1..Len(log) : + log[i] \in {"commit", "interrupt"} => IsOpen(SubSeq(log, 1, i - 1)) + +ClosedOnlyBetweenTurns == + \A i \in 1..Len(log) : + log[i] = "closed" => ~IsOpen(SubSeq(log, 1, i - 1)) + +\* After open(.resume), no turn from the previous owner is still open. +NoStaleTurnAfterReopen == fresh => ~IsOpen(log) + +(* Action property: the log is only ever extended, never rewritten. *) +AppendOnly == [][Prefix(log, log')]_vars +============================================================================= diff --git a/src/core/session_manager/tla/V1Conversion.cfg b/src/core/session_manager/tla/V1Conversion.cfg new file mode 100644 index 000000000..9adc290ea --- /dev/null +++ b/src/core/session_manager/tla/V1Conversion.cfg @@ -0,0 +1,36 @@ +SPECIFICATION FairSpec +CONSTANTS + Procs = {p1, p2} + RootId = RootId + ChildId = ChildId + NewIds = {n} + None = None + Torn = Torn + MaxV = 2 + MaxLocks = 2 + MaxExtra = 1 + MaxCrash = 2 + MaxReq = 3 + AvoidV1Ids = TRUE +INVARIANTS + TypeOK + LockHeld + NoStaleConvLock + CopyIsCurrent + NoTornImport + NoShadow + ChildrenLanded + OrphansKeepV1 + UsageKept + NoDanglingMark +PROPERTIES + AnsweredWhole + NoFalseNotFound + NothingHalfConverted + NoLossOnDelete + LeftoversGone + ConverterOnlyDeletes + ConvertsOnlyOnRequest + RootsStick + ChildrenStick + RequestsAnswered diff --git a/src/core/session_manager/tla/V1Conversion.mutants.cfg b/src/core/session_manager/tla/V1Conversion.mutants.cfg new file mode 100644 index 000000000..90abff4c1 --- /dev/null +++ b/src/core/session_manager/tla/V1Conversion.mutants.cfg @@ -0,0 +1,36 @@ +SPECIFICATION FairSpec +CONSTANTS + Procs = {p1, p2} + RootId = RootId + ChildId = ChildId + NewIds = {n} + None = None + Torn = Torn + MaxV = 2 + MaxLocks = 1 + MaxExtra = 1 + MaxCrash = 1 + MaxReq = 2 + AvoidV1Ids = TRUE +INVARIANTS + TypeOK + LockHeld + NoStaleConvLock + CopyIsCurrent + NoTornImport + NoShadow + ChildrenLanded + OrphansKeepV1 + UsageKept + NoDanglingMark +PROPERTIES + AnsweredWhole + NoFalseNotFound + NothingHalfConverted + NoLossOnDelete + LeftoversGone + ConverterOnlyDeletes + ConvertsOnlyOnRequest + RootsStick + ChildrenStick + RequestsAnswered diff --git a/src/core/session_manager/tla/V1Conversion.tla b/src/core/session_manager/tla/V1Conversion.tla new file mode 100644 index 000000000..10b0d96a7 --- /dev/null +++ b/src/core/session_manager/tla/V1Conversion.tla @@ -0,0 +1,612 @@ +---------------------------- MODULE V1Conversion ---------------------------- +(***************************************************************************) +(* Step: v1 sessions convert to v2 when they are opened (D55, D56, D59, *) +(* D60, D61). *) +(* *) +(* Processes of the new build (Procs) each ask to open a root id, or the *) +(* convert-all command asks for it. If v2 holds the id, the request is *) +(* answered at once, after deleting any v1 folder of the family a crash *) +(* left behind that is unchanged since it was copied. If only v1 holds *) +(* it, the process converts the family, the root and the child sessions *) +(* in its registry, before it answers: it takes the v1 lock of every *) +(* member (a held one answers "busy"), and only then clears the family's *) +(* crash leftovers in .tmp and stages a copy of each member (an *) +(* unreadable member answers "unreadable" and drops the staging). A *) +(* child an earlier, crashed conversion already published is reused as *) +(* it is. It publishes the children and then the root, deletes each *) +(* member's v1 folder under its lock while that folder is the version *) +(* its copy holds (D60), and releases the locks. A delete the file *) +(* system refuses leaves the folder and still answers. Nothing converts *) +(* without a request, and the converter writes no v1 file: it only *) +(* deletes a folder whose copy is published. *) +(* *) +(* Older builds keep writing v1 sessions throughout: a writer holds a *) +(* session's lock while it has the session open, and a write in progress *) +(* leaves the files torn. The new build creates fresh v2 sessions and *) +(* appends to any v2 root. Any process can crash at any step: a crash *) +(* drops every lock it held and leaves staging, published children and *) +(* undeleted v1 folders behind. *) +(* *) +(* Rule R1 (AvoidV1Ids): a fresh v2 session never takes the id of a live *) +(* v1 session. Assumption A1: an older build never creates a v1 session *) +(* under an id v2 holds (ids are 72 random bits). *) +(* *) +(* Converted once per id (D55): a v1 folder an older build changed after *) +(* its copy was made is never converted again or deleted, so v1ver may *) +(* run ahead of base. *) +(* *) +(* Design: system-design.md D53 to D57 and D59 to D61. *) +(***************************************************************************) +EXTENDS Naturals, FiniteSets + +CONSTANTS + Procs, \* processes of the new build + RootId, \* a v1 root session + ChildId, \* a child session in that root's registry + NewIds, \* ids only fresh v2 sessions can take + None, + Torn, \* the copy of a member read while a writer was mid-write + MaxV, \* versions a v1 session reaches + MaxLocks, \* times a writer opens one session + MaxExtra, \* v2 turns appended to one session + MaxCrash, \* crashes and refused deletes in one behavior + MaxReq, \* open and convert-all requests in one behavior + AvoidV1Ids \* rule R1 + +Ids == {RootId, ChildId} +Parent == [i \in Ids |-> IF i = ChildId THEN RootId ELSE None] +ASSUME RootId # ChildId /\ Ids \cap NewIds = {} /\ Procs \cap {"free", "writer"} = {} + +AllIds == Ids \cup NewIds +Roots == {i \in Ids : Parent[i] = None} +Children(r) == {c \in Ids : Parent[c] = r} +Fam(r) == {r} \cup Children(r) + +Kinds == {"none", "open", "all"} +Answers == {"none", "opened", "converted", "busy", "unreadable", "notfound"} +Status == {"none", "import", "fresh"} + +VARIABLES + v1ver, \* [Ids -> 0..MaxV]: 0 absent, else the version of its files + v1lock, \* [Ids -> {"free", "writer"} \cup Procs] + writing, \* [Ids -> BOOLEAN]: a writer is mid-write; the files are torn + locks, \* [Ids -> 0..MaxLocks]: times a writer took the lock + bad, \* [Ids -> BOOLEAN]: the member's v1 files cannot be read + pub, \* [AllIds -> Status]: the id in v2 + base, \* [AllIds -> 0..MaxV \cup {Torn}]: the version a conversion + \* copied, which the v2 copy records as its fingerprint + staged, \* [Ids -> BOOLEAN]: a copy in .tmp + stagedBase, \* [Ids -> 0..MaxV \cup {Torn}] + extra, \* [AllIds -> 0..MaxExtra]: v2 turns appended since publish + conv, \* [Procs -> the converter: pc, the family root, its locked + \* members, and those it copied in this run] + req, \* [Procs -> the request being answered: kind and root] + out, \* [Procs -> the answer to the latest request: ans and root] + refused, \* [Procs -> SUBSET Ids]: deletes refused in the current request + reqs, \* requests made + crashes, + famOf, \* [Roots -> SUBSET Ids]: the members a root's conversion covered + mark1, \* [Ids -> BOOLEAN]: v1's usage marker, ~/.fx/usage-recovery/{id} + mark2, \* [Ids -> BOOLEAN]: v2's usage marker, ~/.fx/usage-recovery-v2/{id} + owed \* [Ids -> BOOLEAN]: ghost: the member has usage still to settle + +vars == <> + +marks == <> + +Idle == [pc |-> "idle", root |-> None, members |-> {}, copied |-> {}] +NoReq == [kind |-> "none", root |-> None] + +TypeOK == + /\ v1ver \in [Ids -> 0..MaxV] + /\ v1lock \in [Ids -> {"free", "writer"} \cup Procs] + /\ writing \in [Ids -> BOOLEAN] + /\ locks \in [Ids -> 0..MaxLocks] + /\ bad \in [Ids -> BOOLEAN] + /\ pub \in [AllIds -> Status] + /\ base \in [AllIds -> (0..MaxV) \cup {Torn}] + /\ staged \in [Ids -> BOOLEAN] + /\ stagedBase \in [Ids -> (0..MaxV) \cup {Torn}] + /\ extra \in [AllIds -> 0..MaxExtra] + /\ \A p \in Procs : + /\ conv[p].pc \in {"idle", "locked", "staged", "published"} + /\ conv[p].root \in Roots \cup {None} + /\ conv[p].members \subseteq Ids /\ conv[p].copied \subseteq conv[p].members + /\ req[p].kind \in Kinds /\ req[p].root \in Roots \cup {None} + /\ out[p].ans \in Answers /\ out[p].root \in Roots \cup {None} + /\ refused[p] \subseteq Ids + /\ reqs \in 0..MaxReq + /\ crashes \in 0..MaxCrash + /\ famOf \in [Roots -> SUBSET Ids] + /\ mark1 \in [Ids -> BOOLEAN] /\ mark2 \in [Ids -> BOOLEAN] /\ owed \in [Ids -> BOOLEAN] + +Live(i) == pub[i] \in {"import", "fresh"} + +\* A published child whose root is not published: a crash's leftover, which +\* the next conversion of its family reuses as it is. +Orphan(i) == Parent[i] # None /\ pub[i] = "import" /\ pub[Parent[i]] = "none" +Dirty == \E i \in Ids : staged[i] + +\* A v1 folder a crash or a refused delete left behind, unchanged since its +\* copy (damage changes its fingerprint too), free, and not refused in p's +\* current request: p's open deletes it. +Leftover(p, i) == + /\ pub[i] = "import" /\ v1ver[i] > 0 /\ v1ver[i] = base[i] /\ ~bad[i] + /\ v1lock[i] = "free" /\ i \notin refused[p] + +\* What the picker and `fx sessions` list: v2 roots, and v1 roots v2 does not +\* hold; children are internal. +Listed == + {r \in Roots : Live(r) \/ (pub[r] = "none" /\ v1ver[r] > 0)} + \cup {n \in NewIds : Live(n)} + +Init == + /\ v1ver = [i \in Ids |-> 0] + /\ v1lock = [i \in Ids |-> "free"] + /\ writing = [i \in Ids |-> FALSE] + /\ locks = [i \in Ids |-> 0] + /\ bad = [i \in Ids |-> FALSE] + /\ pub = [i \in AllIds |-> "none"] + /\ base = [i \in AllIds |-> 0] + /\ staged = [i \in Ids |-> FALSE] + /\ stagedBase = [i \in Ids |-> 0] + /\ extra = [i \in AllIds |-> 0] + /\ conv = [p \in Procs |-> Idle] + /\ req = [p \in Procs |-> NoReq] + /\ out = [p \in Procs |-> [ans |-> "none", root |-> None]] + /\ refused = [p \in Procs |-> {}] + /\ reqs = 0 + /\ crashes = 0 + /\ famOf = [r \in Roots |-> {}] + /\ mark1 = [i \in Ids |-> FALSE] + /\ mark2 = [i \in Ids |-> FALSE] + /\ owed = [i \in Ids |-> FALSE] + +(* -- v1 writers: older builds *) + +WCreate(i) == + /\ v1ver[i] = 0 + /\ Parent[i] # None => v1ver[Parent[i]] > 0 + /\ pub[i] = "none" \* A1 + /\ v1ver' = [v1ver EXCEPT ![i] = 1] + /\ UNCHANGED <> + /\ UNCHANGED marks + +WLock(i) == + /\ v1ver[i] > 0 + /\ v1lock[i] = "free" + /\ locks[i] < MaxLocks + /\ v1lock' = [v1lock EXCEPT ![i] = "writer"] + /\ locks' = [locks EXCEPT ![i] = @ + 1] + /\ UNCHANGED <> + /\ UNCHANGED marks + +WBegin(i) == + /\ v1lock[i] = "writer" + /\ ~writing[i] + /\ v1ver[i] < MaxV + /\ writing' = [writing EXCEPT ![i] = TRUE] + /\ UNCHANGED <> + /\ UNCHANGED marks + +WEnd(i) == + /\ writing[i] + /\ writing' = [writing EXCEPT ![i] = FALSE] + /\ v1ver' = [v1ver EXCEPT ![i] = @ + 1] + /\ UNCHANGED <> + /\ UNCHANGED marks + +WUnlock(i) == + /\ v1lock[i] = "writer" + /\ ~writing[i] + /\ v1lock' = [v1lock EXCEPT ![i] = "free"] + /\ UNCHANGED <> + /\ UNCHANGED marks + +\* A writer dies: the kernel drops its lock, and v1's own open repairs a torn +\* write back to the last whole version. +WCrash(i) == + /\ v1lock[i] = "writer" + /\ crashes < MaxCrash + /\ v1lock' = [v1lock EXCEPT ![i] = "free"] + /\ writing' = [writing EXCEPT ![i] = FALSE] + /\ crashes' = crashes + 1 + /\ UNCHANGED <> + /\ UNCHANGED marks + +\* An older build ends a turn whose usage is not settled yet: it keeps v1's +\* usage marker, under its lock. +WMark(i) == + /\ v1lock[i] = "writer" + /\ ~mark1[i] + /\ mark1' = [mark1 EXCEPT ![i] = TRUE] + /\ owed' = [owed EXCEPT ![i] = TRUE] + /\ UNCHANGED <> + +\* A member's v1 files become unreadable: damage from outside fx. +Damage(i) == + /\ v1ver[i] > 0 + /\ ~bad[i] + /\ bad' = [bad EXCEPT ![i] = TRUE] + /\ UNCHANGED <> + /\ UNCHANGED marks + +(* -- the new build's own v2 sessions *) + +FCreate(i) == + /\ i \in NewIds \/ (i \in Roots /\ (AvoidV1Ids => v1ver[i] = 0)) + /\ pub[i] = "none" + /\ i \in Ids => ~staged[i] + /\ pub' = [pub EXCEPT ![i] = "fresh"] + /\ UNCHANGED <> + /\ UNCHANGED marks + +FAppend(i) == + /\ Live(i) + /\ i \in NewIds \/ i \in Roots + /\ extra[i] < MaxExtra + /\ extra' = [extra EXCEPT ![i] = @ + 1] + /\ UNCHANGED <> + /\ UNCHANGED marks + +(* -- requests and the converter, in each requesting process *) + +Request(p, k, r) == + /\ k \in {"open", "all"} + /\ req[p] = NoReq + /\ conv[p] = Idle + /\ reqs < MaxReq + /\ req' = [req EXCEPT ![p] = [kind |-> k, root |-> r]] + /\ out' = [out EXCEPT ![p] = [ans |-> "none", root |-> r]] + /\ refused' = [refused EXCEPT ![p] = {}] + /\ reqs' = reqs + 1 + /\ UNCHANGED <> + /\ UNCHANGED marks + +Answer(p, a) == + /\ req' = [req EXCEPT ![p] = NoReq] + /\ out' = [out EXCEPT ![p] = [ans |-> a, root |-> req[p].root]] + +Done(p) == IF req[p].kind = "open" THEN "opened" ELSE "converted" + +Waiting(p) == req[p] # NoReq /\ conv[p] = Idle + +\* v2 already holds the id: any leftover of its family is cleaned first. +AHeld(p) == + /\ Waiting(p) + /\ Live(req[p].root) + /\ ~\E i \in Fam(req[p].root) : Leftover(p, i) + /\ Answer(p, Done(p)) + /\ UNCHANGED <> + /\ UNCHANGED marks + +\* A leftover v1 folder, unchanged since its copy, is deleted under its lock. +CClean(p, i) == + /\ Waiting(p) + /\ Live(req[p].root) + /\ i \in Fam(req[p].root) + /\ Leftover(p, i) /\ ~mark1[i] + /\ v1ver' = [v1ver EXCEPT ![i] = 0] + /\ UNCHANGED <> + /\ UNCHANGED marks + +\* The file system refuses that delete: the folder stays, the open goes on. +CCleanRefused(p, i) == + /\ Waiting(p) + /\ Live(req[p].root) + /\ i \in Fam(req[p].root) + /\ Leftover(p, i) + /\ crashes < MaxCrash + /\ refused' = [refused EXCEPT ![p] = @ \cup {i}] + /\ crashes' = crashes + 1 + /\ UNCHANGED <> + /\ UNCHANGED marks + +\* Neither store holds it. +AMissing(p) == + /\ Waiting(p) + /\ pub[req[p].root] = "none" /\ v1ver[req[p].root] = 0 + /\ Answer(p, IF req[p].kind = "open" THEN "notfound" ELSE "converted") + /\ UNCHANGED <> + /\ UNCHANGED marks + +\* Takes every present member's lock, or answers "busy" holding none. The +\* check that v2 does not hold the root is made under the locks: another +\* process may have converted it while this one waited. +CBegin(p) == + LET r == req[p].root + present == {i \in Fam(r) : v1ver[i] > 0} IN + /\ Waiting(p) + /\ pub[r] = "none" /\ v1ver[r] > 0 + /\ IF \A i \in present : v1lock[i] = "free" + THEN /\ v1lock' = [i \in Ids |-> IF i \in present THEN p ELSE v1lock[i]] + /\ conv' = [conv EXCEPT ![p] = [pc |-> "locked", root |-> r, members |-> present, copied |-> {}]] + /\ UNCHANGED <> + ELSE /\ Answer(p, "busy") + /\ UNCHANGED <> + /\ UNCHANGED <> + /\ UNCHANGED marks + +\* Under the locks: the family's staging leftovers go, and each member not +\* already published gets a fresh copy in .tmp; an unreadable member drops +\* the staging and answers "unreadable". +CStage(p) == + LET m == conv[p].members + copy == {i \in m : pub[i] = "none"} IN + /\ conv[p].pc = "locked" + /\ IF \E i \in copy : bad[i] + THEN /\ v1lock' = [i \in Ids |-> IF i \in m THEN "free" ELSE v1lock[i]] + /\ staged' = [i \in Ids |-> IF i \in Fam(conv[p].root) THEN FALSE ELSE staged[i]] + /\ conv' = [conv EXCEPT ![p] = Idle] + /\ Answer(p, "unreadable") + /\ UNCHANGED stagedBase + ELSE /\ staged' = [i \in Ids |-> IF i \in Fam(conv[p].root) THEN i \in copy ELSE staged[i]] + /\ stagedBase' = [i \in Ids |-> + IF i \in copy + THEN (IF writing[i] THEN Torn ELSE v1ver[i]) + ELSE stagedBase[i]] + /\ conv' = [conv EXCEPT ![p].pc = "staged", ![p].copied = copy] + /\ UNCHANGED <> + /\ UNCHANGED <> + /\ UNCHANGED marks + +\* Publishing is the manager's atomic rename. +CPublishChild(p, c) == + /\ conv[p].pc = "staged" + /\ c \in conv[p].members \ {conv[p].root} + /\ staged[c] + /\ staged' = [staged EXCEPT ![c] = FALSE] + /\ pub' = [pub EXCEPT ![c] = "import"] + /\ base' = [base EXCEPT ![c] = stagedBase[c]] + /\ UNCHANGED <> + /\ UNCHANGED marks + +CPublishRoot(p) == + LET r == conv[p].root IN + /\ conv[p].pc = "staged" + /\ \A c \in conv[p].members \ {r} : ~staged[c] + /\ staged' = [staged EXCEPT ![r] = FALSE] + /\ pub' = [pub EXCEPT ![r] = "import"] + /\ base' = [base EXCEPT ![r] = stagedBase[r]] + /\ conv' = [conv EXCEPT ![p].pc = "published"] + /\ famOf' = [famOf EXCEPT ![r] = conv[p].members] + /\ UNCHANGED <> + /\ UNCHANGED marks + +\* A member whose v1 state p may move to v2 and remove: one it copied in +\* this run, or a reused child still at its copy's version and fingerprint. +Unchanged(p, i) == + /\ i \in conv[p].members /\ v1ver[i] > 0 /\ v1ver[i] = base[i] + /\ i \in conv[p].copied \/ ~bad[i] + +\* Its folder goes once its usage marker has moved (D62). +Deletable(p, i) == Unchanged(p, i) /\ ~mark1[i] + +\* Where p moves a member's usage marker: after it published that member's +\* family, or for a leftover of a family v2 already holds. +MarkScope(p, i) == + \/ conv[p].pc = "published" /\ Unchanged(p, i) + \/ Waiting(p) /\ Live(req[p].root) /\ i \in Fam(req[p].root) /\ Leftover(p, i) + +\* The v2 marker is written first, then v1's is removed: usage to settle is +\* always behind one of them, and settling both is idempotent. +MoveMark(p, i) == + /\ MarkScope(p, i) + /\ mark1[i] /\ ~mark2[i] + /\ mark2' = [mark2 EXCEPT ![i] = TRUE] + /\ UNCHANGED <> + +DropMark(p, i) == + /\ MarkScope(p, i) + /\ mark1[i] /\ mark2[i] + /\ mark1' = [mark1 EXCEPT ![i] = FALSE] + /\ UNCHANGED <> + +\* D60: with the copy durable, each member's v1 folder goes, still locked. +CDelete(p, i) == + /\ conv[p].pc = "published" + /\ Deletable(p, i) + /\ i \notin refused[p] + /\ v1ver' = [v1ver EXCEPT ![i] = 0] + /\ UNCHANGED <> + /\ UNCHANGED marks + +\* The file system refuses that delete, or the marker move: the folder +\* stays as a leftover. +CDeleteRefused(p, i) == + /\ conv[p].pc = "published" + /\ Unchanged(p, i) + /\ i \notin refused[p] + /\ crashes < MaxCrash + /\ refused' = [refused EXCEPT ![p] = @ \cup {i}] + /\ crashes' = crashes + 1 + /\ UNCHANGED <> + /\ UNCHANGED marks + +\* Every member's folder is gone, refused, or not deletable (a reused child +\* an older build changed or that was damaged): the locks go, it answers. +CFinish(p) == + /\ conv[p].pc = "published" + /\ \A i \in conv[p].members : ~Unchanged(p, i) \/ i \in refused[p] + /\ v1lock' = [i \in Ids |-> IF i \in conv[p].members THEN "free" ELSE v1lock[i]] + /\ conv' = [conv EXCEPT ![p] = Idle] + /\ Answer(p, Done(p)) + /\ UNCHANGED <> + /\ UNCHANGED marks + +\* The process dies: no answer, and its locks go with it. +CCrash(p) == + /\ req[p] # NoReq + /\ crashes < MaxCrash + /\ v1lock' = [i \in Ids |-> IF v1lock[i] = p THEN "free" ELSE v1lock[i]] + /\ conv' = [conv EXCEPT ![p] = Idle] + /\ req' = [req EXCEPT ![p] = NoReq] + /\ out' = [out EXCEPT ![p] = [ans |-> "none", root |-> req[p].root]] + /\ crashes' = crashes + 1 + /\ UNCHANGED <> + /\ UNCHANGED marks + +\* A converter's steps, without its faults. +ConvWork(p) == + \/ AHeld(p) \/ AMissing(p) \/ CBegin(p) \/ CStage(p) \/ CPublishRoot(p) \/ CFinish(p) + \/ \E c \in Ids : CPublishChild(p, c) \/ CDelete(p, c) \/ CClean(p, c) \/ MoveMark(p, c) \/ DropMark(p, c) + +\* Faults: a refused delete. +ConvRefused(p) == \E c \in Ids : CDeleteRefused(p, c) \/ CCleanRefused(p, c) + +ConvStep(p) == ConvWork(p) \/ ConvRefused(p) \/ CCrash(p) + +WriterStep(i) == WCreate(i) \/ WLock(i) \/ WBegin(i) \/ WEnd(i) \/ WUnlock(i) \/ WCrash(i) \/ WMark(i) + +Next == + \/ \E p \in Procs : + \/ ConvStep(p) + \/ \E k \in {"open", "all"}, r \in Roots : Request(p, k, r) + \/ \E i \in Ids : WriterStep(i) \/ Damage(i) + \/ \E i \in AllIds : FCreate(i) \/ FAppend(i) + +Spec == Init /\ [][Next]_vars + +\* Each converter keeps going on a request it holds, and writers release +\* their locks; requests, crashes, writes and opens are bounded. +FairSpec == + /\ Spec + /\ \A p \in Procs : + /\ WF_vars(AHeld(p)) /\ WF_vars(AMissing(p)) /\ WF_vars(CBegin(p)) + /\ WF_vars(CStage(p)) /\ WF_vars(CPublishRoot(p)) /\ WF_vars(CFinish(p)) + /\ \A c \in Ids : WF_vars(CPublishChild(p, c)) /\ WF_vars(CDelete(p, c)) /\ WF_vars(CClean(p, c)) + /\ \A c \in Ids : WF_vars(MoveMark(p, c)) /\ WF_vars(DropMark(p, c)) + /\ \A i \in Ids : WF_vars(WUnlock(i)) /\ WF_vars(WEnd(i)) + +(* -- properties *) + +\* A converter holds every member's lock from staging to the delete, so the +\* copy it publishes is the version v1 has, never a torn one, and the +\* folder it deletes is that version. +LockHeld == + \A p \in Procs : + conv[p].pc \in {"locked", "staged", "published"} => + \A i \in conv[p].members : v1lock[i] = p +CopyIsCurrent == + \A p \in Procs : + conv[p].pc = "staged" => + \A i \in conv[p].members : staged[i] => stagedBase[i] = v1ver[i] +NoTornImport == \A i \in Ids : pub[i] = "import" => base[i] # Torn + +\* A converter's locks never outlive its conversion. +NoStaleConvLock == \A p \in Procs : conv[p].pc = "idle" => \A i \in Ids : v1lock[i] # p + +\* A fresh v2 session never takes a live v1 root's id, which would hide that +\* v1 session for good. +NoShadow == \A r \in Roots : v1ver[r] > 0 => pub[r] # "fresh" + +\* A published root's conversion covered every member present when it +\* began, and each of those children is published. +ChildrenLanded == + \A r \in Roots : pub[r] = "import" => \A c \in famOf[r] \ {r} : pub[c] = "import" + +\* A child whose root never landed still has its v1 folder: no delete +\* happens before the whole family is published. +OrphansKeepV1 == \A i \in Ids : Orphan(i) => v1ver[i] > 0 + +\* Usage still to settle always has a marker, v1's or v2's (D62). +UsageKept == \A i \in Ids : owed[i] => (mark1[i] \/ mark2[i]) + +\* v1's marker never outlives its folder: recovery would then read a +\* session that is gone. +NoDanglingMark == \A i \in Ids : mark1[i] => v1ver[i] > 0 + +\* The step at which p answers; each answer is judged when it is given. +AnswerStep(p) == req[p] # NoReq /\ req'[p] = NoReq /\ out'[p].ans # "none" + +\* "Opened" or "converted" means v2 holds the root (its children by +\* ChildrenLanded), or there is nothing to convert. +AnsweredWhole == + [][\A p \in Procs : + (AnswerStep(p) /\ out'[p].ans \in {"opened", "converted"}) => + (pub'[req[p].root] \in {"import", "fresh"} \/ v1ver'[req[p].root] = 0)]_vars + +\* A live v1 session is never reported missing. +NoFalseNotFound == + [][\A p \in Procs : + (AnswerStep(p) /\ out'[p].ans = "notfound") => + (pub'[req[p].root] = "none" /\ v1ver'[req[p].root] = 0)]_vars + +\* A refused request converts nothing: "busy" changes no staging and takes +\* no lock; "unreadable" leaves no staging of the family and no lock. +NothingHalfConverted == + [][\A p \in Procs : + /\ (AnswerStep(p) /\ out'[p].ans = "busy") => + (staged' = staged /\ pub' = pub /\ \A i \in Ids : v1lock'[i] # p) + /\ (AnswerStep(p) /\ out'[p].ans = "unreadable") => + (pub' = pub /\ \A i \in Fam(req[p].root) : ~staged'[i] /\ v1lock'[i] # p)]_vars + +\* D60: a v1 folder goes only once its v2 copy is published and is that +\* folder's version, under its converter's lock or free; no writer deletes. +NoLossOnDelete == + [][\A i \in Ids : + (v1ver[i] > 0 /\ v1ver'[i] = 0) => + /\ pub[i] = "import" /\ pub'[i] = "import" + /\ base[i] = v1ver[i] /\ ~writing[i] + /\ v1lock[i] # "writer"]_vars + +\* An answered open or conversion leaves no v1 folder of the family that +\* equals its copy, except one held by a writer or by another converter +\* (which deletes it as it finishes), damaged since, or whose delete was +\* refused. +LeftoversGone == + [][\A p \in Procs : + (AnswerStep(p) /\ out'[p].ans \in {"opened", "converted"}) => + \A i \in Fam(req[p].root) : + (pub'[i] = "import" /\ v1ver'[i] > 0 /\ v1ver'[i] = base'[i]) + => (v1lock'[i] \in {"writer"} \cup (Procs \ {p}) \/ bad'[i] \/ i \in refused'[p])]_vars + +\* The converter writes no v1 file: it only deletes v1 folders. +ConverterOnlyDeletes == + [][(\E p \in Procs : ConvStep(p)) => + /\ \A i \in Ids : v1ver'[i] \in {v1ver[i], 0} + /\ UNCHANGED <>]_vars + +\* Nothing converts without a request for that root: no background work. +ConvertsOnlyOnRequest == + [][\A r \in Roots : + (pub[r] = "none" /\ pub'[r] = "import") => \E p \in Procs : req[p].root = r]_vars + +\* A live v2 root is never replaced, and a conversion is never redone, nor +\* is a published child's copy, reused or not: once per id. +RootsStick == + [][\A i \in Roots \cup NewIds : + Live(i) => (pub'[i] = pub[i] /\ base'[i] = base[i])]_vars +ChildrenStick == + [][\A c \in Ids : + (Parent[c] # None /\ pub[c] = "import") => (pub'[c] = "import" /\ base'[c] = base[c])]_vars + +\* Every request is answered, unless its process dies. +RequestsAnswered == \A p \in Procs : (req[p] # NoReq) ~> (req[p] = NoReq) +============================================================================= diff --git a/src/core/session_manager/tla/Wiring.cfg b/src/core/session_manager/tla/Wiring.cfg new file mode 100644 index 000000000..f5f25963a --- /dev/null +++ b/src/core/session_manager/tla/Wiring.cfg @@ -0,0 +1,13 @@ +SPECIFICATION Spec +CONSTANT Sessions = {a, b, c} +INVARIANTS + TypeOK + OneBackend + ParentOutlivesChildren + UsageNeverSilent + ContinueLinksInterrupted + SwitchIsTwoSessions +PROPERTIES + ForkIsNewSession + ForkLeavesSource + ForkBetweenTurns diff --git a/src/core/session_manager/tla/Wiring.tla b/src/core/session_manager/tla/Wiring.tla new file mode 100644 index 000000000..c1cf0bc37 --- /dev/null +++ b/src/core/session_manager/tla/Wiring.tla @@ -0,0 +1,305 @@ +------------------------------ MODULE Wiring ------------------------------ +(***************************************************************************) +(* Step: fx wiring, through the adapter. *) +(* *) +(* One fx process at a time. It picks its backend once at start *) +(* (`--sessions-v2` or FX_SESSIONS_V2, D26) and keeps it until it exits. *) +(* The host has one session slot: it opens a session through the adapter, *) +(* runs turns, may switch to another session, and closes it at exit. To *) +(* switch it may open the next session before closing the current one *) +(* (D41), which fills a second slot, `next`, until the current closes. A *) +(* turn may spawn a child thread, whose finish is appended through the *) +(* parent's Session. Usage is charged to the profile as it happens and *) +(* reaches the session log with the next durable batch; the profile's *) +(* usage-recovery marker covers the gap. "Continue" starts a new turn *) +(* linked to an interrupted one (D23). `/fork` (D58) makes a new session *) +(* from the current one's log before a prompt and switches to it. The *) +(* process can crash anywhere. *) +(* *) +(* The manager's own rules are modeled elsewhere (TurnLifecycle.tla, *) +(* Subagents.tla, WriterLock.tla); here a reopen simply ends a turn a *) +(* crash left open as interrupted (D1). *) +(* *) +(* Design: system-design.md "fx mapping" and D20 to D27. *) +(***************************************************************************) +EXTENDS Naturals, FiniteSets + +CONSTANT Sessions + +Backends == {"v1", "v2"} +Ends == {"none", "commit", "interrupt"} + +VARIABLES + up, \* the fx process is running + backend, \* the backend this process chose at start + wrote, \* backends this process has written since it started + cur, \* the session open in the host slot, or "none" + turnOpen, \* [Sessions -> BOOLEAN]: the log has an open turn + lastEnd, \* [Sessions -> Ends]: how the newest ended turn ended + linked, \* [Sessions -> Ends]: how the turn a continuation continues ended + child, \* "none" or "running": the one child thread + childOf, \* the session whose turn spawned the child, or "none" + usageSplit, \* [Sessions -> BOOLEAN]: the profile and the log may disagree on usage + marker, \* [Sessions -> BOOLEAN]: the profile's usage-recovery marker exists + next, \* the session opened to switch to, or "none" (D41) + made, \* [Sessions -> BOOLEAN]: the session exists on disk + forkOf \* [Sessions -> Sessions \cup {"none"}]: the session a fork came from + +vars == <> + +\* Every component uses the backend the process chose (D26). +ChildBackend == backend +UsageBackend == backend + +TypeOK == + /\ up \in BOOLEAN + /\ backend \in Backends + /\ wrote \subseteq Backends + /\ cur \in Sessions \cup {"none"} + /\ turnOpen \in [Sessions -> BOOLEAN] + /\ lastEnd \in [Sessions -> Ends] + /\ linked \in [Sessions -> Ends] + /\ child \in {"none", "running"} + /\ childOf \in Sessions \cup {"none"} + /\ usageSplit \in [Sessions -> BOOLEAN] + /\ marker \in [Sessions -> BOOLEAN] + /\ next \in Sessions \cup {"none"} + /\ made \in [Sessions -> BOOLEAN] + /\ forkOf \in [Sessions -> Sessions \cup {"none"}] + +Init == + /\ up = FALSE + /\ backend = "v1" + /\ wrote = {} + /\ cur = "none" + /\ turnOpen = [s \in Sessions |-> FALSE] + /\ lastEnd = [s \in Sessions |-> "none"] + /\ linked = [s \in Sessions |-> "none"] + /\ child = "none" + /\ childOf = "none" + /\ usageSplit = [s \in Sessions |-> FALSE] + /\ marker = [s \in Sessions |-> FALSE] + /\ next = "none" + /\ made = [s \in Sessions |-> FALSE] + /\ forkOf = [s \in Sessions |-> "none"] + +Active == up /\ cur # "none" + +\* fx starts and picks its backend, once. +Start(b) == + /\ ~up + /\ up' = TRUE + /\ backend' = b + /\ wrote' = {} + /\ UNCHANGED <> + +\* Startup usage recovery: a marker left by a crash is reconciled, then removed. +RecoverUsage(s) == + /\ up + /\ marker[s] + /\ usageSplit' = [usageSplit EXCEPT ![s] = FALSE] + /\ marker' = [marker EXCEPT ![s] = FALSE] + /\ UNCHANGED <> + +\* The adapter opens a session: into the slot, or, while one is open, as the +\* session to switch to (D41). A turn a crash left open ends as interrupted. +Open(s) == + /\ up + /\ next = "none" + /\ s # cur + /\ IF cur = "none" THEN cur' = s /\ next' = "none" ELSE cur' = cur /\ next' = s + /\ wrote' = wrote \cup {backend} + /\ turnOpen' = [turnOpen EXCEPT ![s] = FALSE] + /\ lastEnd' = IF turnOpen[s] THEN [lastEnd EXCEPT ![s] = "interrupt"] ELSE lastEnd + /\ made' = [made EXCEPT ![s] = TRUE] + /\ UNCHANGED <> + +\* New work needs a session and no switch pending. +Idle == Active /\ next = "none" + +BeginTurn == + /\ Idle + /\ ~turnOpen[cur] + /\ turnOpen' = [turnOpen EXCEPT ![cur] = TRUE] + /\ linked' = [linked EXCEPT ![cur] = "none"] + /\ wrote' = wrote \cup {backend} + /\ UNCHANGED <> + +\* "Continue" (D23): a new turn whose first item links to the newest ended +\* turn, which must have been interrupted. +Continue == + /\ Idle + /\ ~turnOpen[cur] + /\ lastEnd[cur] = "interrupt" + /\ turnOpen' = [turnOpen EXCEPT ![cur] = TRUE] + /\ linked' = [linked EXCEPT ![cur] = lastEnd[cur]] + /\ wrote' = wrote \cup {backend} + /\ UNCHANGED <> + +\* Before a model request is charged, the marker is written. +MarkUsage == + /\ Active + /\ turnOpen[cur] + /\ ~marker[cur] + /\ marker' = [marker EXCEPT ![cur] = TRUE] + /\ UNCHANGED <> + +\* The request is charged to the profile; the log has not caught up yet. +Charge == + /\ Active + /\ turnOpen[cur] + /\ marker[cur] + /\ usageSplit' = [usageSplit EXCEPT ![cur] = TRUE] + /\ UNCHANGED <> + +\* A usage checkpoint mid-turn: `set usage` is a durability point, so the +\* log catches up with the profile once the append returns. +PersistUsage == + /\ Active + /\ usageSplit[cur] + /\ usageSplit' = [usageSplit EXCEPT ![cur] = FALSE] + /\ wrote' = wrote \cup {UsageBackend} + /\ UNCHANGED <> + +\* The turn ends, also while a switch is pending (a cancelled turn); the +\* usage so far is written in the same durable batch. +EndTurn(e) == + /\ Active + /\ turnOpen[cur] + /\ turnOpen' = [turnOpen EXCEPT ![cur] = FALSE] + /\ lastEnd' = [lastEnd EXCEPT ![cur] = e] + /\ usageSplit' = [usageSplit EXCEPT ![cur] = FALSE] + /\ wrote' = wrote \cup {UsageBackend} + /\ UNCHANGED <> + +\* Once a durable batch carried the usage, the marker goes. +ClearMarker(s) == + /\ up + /\ marker[s] + /\ ~usageSplit[s] + /\ marker' = [marker EXCEPT ![s] = FALSE] + /\ UNCHANGED <> + +\* A turn spawns a child thread (child_spawned through the parent). +Spawn == + /\ Idle + /\ turnOpen[cur] + /\ child = "none" + /\ child' = "running" + /\ childOf' = cur + /\ wrote' = wrote \cup {backend, ChildBackend} + /\ UNCHANGED <> + +\* The child's thread appends child_finished through the parent's Session, +\* or the parent cancels it; either way through an open parent. +ChildDone == + /\ up + /\ child = "running" + /\ cur = childOf + /\ child' = "none" + /\ childOf' = "none" + /\ wrote' = wrote \cup {backend} + /\ UNCHANGED <> + +\* The host closes a session, to switch or to exit: children are finished +\* and joined first, then close interrupts an open turn and carries usage. +\* Closing the current session hands the slot to the one switched to; +\* closing that one instead abandons the switch (D41). +Close(s) == + /\ up + /\ s \in {cur, next} \ {"none"} + /\ child = "none" + /\ cur' = IF s = cur THEN next ELSE cur + /\ next' = "none" + /\ turnOpen' = [turnOpen EXCEPT ![s] = FALSE] + /\ lastEnd' = IF turnOpen[s] THEN [lastEnd EXCEPT ![s] = "interrupt"] ELSE lastEnd + /\ usageSplit' = [usageSplit EXCEPT ![s] = FALSE] + /\ wrote' = wrote \cup {backend} + /\ UNCHANGED <> + +\* /fork (D58): a new session holding the current one's log before a chosen +\* prompt becomes the session to switch to, and Close then hands it the +\* slot. Only on v2, between turns and with no child running; the source +\* is never written. The fork's newest ended turn is whichever the source +\* had before that prompt. +Fork(f) == + /\ Idle + /\ backend = "v2" + /\ child = "none" + /\ f \notin {cur, next} + /\ ~made[f] + /\ ~turnOpen[cur] + /\ next' = f + /\ made' = [made EXCEPT ![f] = TRUE] + /\ forkOf' = [forkOf EXCEPT ![f] = cur] + /\ \E e \in Ends : lastEnd' = [lastEnd EXCEPT ![f] = e] + /\ wrote' = wrote \cup {backend} + /\ UNCHANGED <> + +Exit == + /\ up + /\ cur = "none" + /\ next = "none" + /\ child = "none" + /\ up' = FALSE + /\ UNCHANGED <> + +\* The process dies anywhere: memory and threads are gone; the logs, the +\* profile ledger and the marker stay. +Crash == + /\ up + /\ up' = FALSE + /\ cur' = "none" + /\ next' = "none" + /\ child' = "none" + /\ childOf' = "none" + /\ UNCHANGED <> + +Next == + \/ \E b \in Backends : Start(b) + \/ \E s \in Sessions : RecoverUsage(s) \/ Open(s) \/ ClearMarker(s) \/ Close(s) + \/ BeginTurn \/ Continue + \/ MarkUsage \/ Charge \/ PersistUsage + \/ \E e \in {"commit", "interrupt"} : EndTurn(e) + \/ Spawn \/ ChildDone + \/ \E f \in Sessions : Fork(f) + \/ Exit \/ Crash + +Spec == Init /\ [][Next]_vars + +----------------------------------------------------------------------------- +(* Invariants *) + +\* A process writes one backend only: no dual writes. +OneBackend == Cardinality(wrote) <= 1 + +\* A child thread runs only while its parent's Session is open. +ParentOutlivesChildren == child = "running" => (up /\ cur = childOf) + +\* Whenever the profile and the log may disagree on usage, the marker says so. +UsageNeverSilent == \A s \in Sessions : usageSplit[s] => marker[s] + +\* A pending switch names a second session, never the current one (D41). +SwitchIsTwoSessions == next # "none" => (cur # "none" /\ cur # next) + +\* A continuation always continues an interrupted turn. +ContinueLinksInterrupted == \A s \in Sessions : linked[s] \in {"none", "interrupt"} + +(* Properties of /fork (D58) *) + +ForkStep(f) == forkOf'[f] # forkOf[f] + +\* A fork is a session that never existed: it never replaces one. +ForkIsNewSession == [][\A f \in Sessions : ForkStep(f) => ~made[f]]_vars + +\* The fork step leaves the source as it was. +ForkLeavesSource == + [][\A f \in Sessions : ForkStep(f) => + /\ turnOpen'[cur] = turnOpen[cur] /\ lastEnd'[cur] = lastEnd[cur] + /\ linked'[cur] = linked[cur] /\ usageSplit'[cur] = usageSplit[cur]]_vars + +\* A fork happens on v2, between turns, with no child running. +ForkBetweenTurns == + [][\A f \in Sessions : ForkStep(f) => + (backend = "v2" /\ ~turnOpen[cur] /\ child = "none")]_vars +============================================================================= diff --git a/src/core/session_manager/tla/WriterLock.cfg b/src/core/session_manager/tla/WriterLock.cfg new file mode 100644 index 000000000..73b1e612e --- /dev/null +++ b/src/core/session_manager/tla/WriterLock.cfg @@ -0,0 +1,12 @@ +SPECIFICATION Spec +CONSTANTS + Procs = {p1, p2} + Threads = {t1, t2} + MaxLines = 4 + None = None +INVARIANTS + TypeOK + OneWriter + OnlyHolderOpen + MutexInsideOpenSession + SeqIsPosition diff --git a/src/core/session_manager/tla/WriterLock.tla b/src/core/session_manager/tla/WriterLock.tla new file mode 100644 index 000000000..6f054b54c --- /dev/null +++ b/src/core/session_manager/tla/WriterLock.tla @@ -0,0 +1,122 @@ +---------------------------- MODULE WriterLock ---------------------------- +(***************************************************************************) +(* Step: L0 flock plus the L2 per-session mutex. *) +(* *) +(* One writing process per session (flock on {id}/lock) and many threads *) +(* per process (the Session mutex inside the manager). The kernel drops *) +(* the flock when a process dies. Hosts never lock anything; Acquire and *) +(* WriteAndRelease happen inside append(). Busy is modeled as Open being *) +(* disabled while another process holds the lock. *) +(* *) +(* Design: system-design.md "Concurrency And Ordering". *) +(***************************************************************************) +EXTENDS Naturals, Sequences + +CONSTANTS Procs, Threads, MaxLines, None + +VARIABLES + holder, \* process holding the flock, or None + alive, \* [Procs -> BOOLEAN] + opened, \* [Procs -> BOOLEAN]: the process has an open Session + nextSeq, \* [Procs -> Nat]: the Session's in-memory next seq + mutex, \* [Procs -> Threads \cup {None}]: thread inside append() + file \* the log: a sequence of [seq, by] + +vars == <> + +TypeOK == + /\ holder \in Procs \cup {None} + /\ alive \in [Procs -> BOOLEAN] + /\ opened \in [Procs -> BOOLEAN] + /\ nextSeq \in [Procs -> 1..(MaxLines + 1)] + /\ mutex \in [Procs -> Threads \cup {None}] + /\ file \in Seq([seq : 1..MaxLines, by : Procs]) + +Init == + /\ holder = None + /\ alive = [p \in Procs |-> TRUE] + /\ opened = [p \in Procs |-> FALSE] + /\ nextSeq = [p \in Procs |-> 1] + /\ mutex = [p \in Procs |-> None] + /\ file = <<>> + +\* open(): flock succeeds only when nobody holds it; otherwise Busy. +\* The Session learns the next seq from the file it just locked. +Open(p) == + /\ alive[p] + /\ ~opened[p] + /\ holder = None + /\ holder' = p + /\ opened' = [opened EXCEPT ![p] = TRUE] + /\ nextSeq' = [nextSeq EXCEPT ![p] = Len(file) + 1] + /\ UNCHANGED <> + +\* A thread calls append(); the manager takes the Session mutex. +Acquire(p, t) == + /\ alive[p] + /\ opened[p] + /\ mutex[p] = None + /\ mutex' = [mutex EXCEPT ![p] = t] + /\ UNCHANGED <> + +\* Under the mutex: assign seq, write the line, release the mutex. +WriteAndRelease(p, t) == + /\ alive[p] + /\ opened[p] + /\ mutex[p] = t + /\ Len(file) < MaxLines + /\ file' = Append(file, [seq |-> nextSeq[p], by |-> p]) + /\ nextSeq' = [nextSeq EXCEPT ![p] = @ + 1] + /\ mutex' = [mutex EXCEPT ![p] = None] + /\ UNCHANGED <> + +\* close(): waits for the mutex, then releases the flock. +Close(p) == + /\ alive[p] + /\ opened[p] + /\ mutex[p] = None + /\ holder = p + /\ holder' = None + /\ opened' = [opened EXCEPT ![p] = FALSE] + /\ UNCHANGED <> + +\* The process dies; the kernel releases its flock. +Crash(p) == + /\ alive[p] + /\ alive' = [alive EXCEPT ![p] = FALSE] + /\ opened' = [opened EXCEPT ![p] = FALSE] + /\ mutex' = [mutex EXCEPT ![p] = None] + /\ holder' = IF holder = p THEN None ELSE holder + /\ UNCHANGED <> + +Restart(p) == + /\ ~alive[p] + /\ alive' = [alive EXCEPT ![p] = TRUE] + /\ UNCHANGED <> + +Next == + \E p \in Procs : + \/ Open(p) + \/ Close(p) + \/ Crash(p) + \/ Restart(p) + \/ \E t \in Threads : Acquire(p, t) \/ WriteAndRelease(p, t) + +Spec == Init /\ [][Next]_vars + +----------------------------------------------------------------------------- +(* Invariants *) + +\* At most one process has the session open for writing. +OneWriter == \A p, q \in Procs : opened[p] /\ opened[q] => p = q + +\* Only the flock holder has an open Session. +OnlyHolderOpen == \A p \in Procs : opened[p] => holder = p + +\* A thread inside append() always belongs to an open Session. +MutexInsideOpenSession == \A p \in Procs : mutex[p] # None => opened[p] + +\* File order is seq order: no duplicates, no gaps, across threads and +\* across processes taking over after a crash. +SeqIsPosition == \A i \in 1..Len(file) : file[i].seq = i +============================================================================= diff --git a/src/core/session_manager/tla/check.sh b/src/core/session_manager/tla/check.sh new file mode 100755 index 000000000..ac38baafd --- /dev/null +++ b/src/core/session_manager/tla/check.sh @@ -0,0 +1,58 @@ +#!/bin/sh +# Model-check every session-manager spec with TLC. +# +# Needs Java 11+ and tla2tools.jar: +# brew install openjdk +# mkdir -p ~/.local/share/tla +# curl -fL -o ~/.local/share/tla/tla2tools.jar \ +# https://github.com/tlaplus/tlaplus/releases/latest/download/tla2tools.jar +# +# Usage: +# ./check.sh # every spec +# ./check.sh SessionLog Fork # selected specs +# TLA2TOOLS_JAR=/path/tla2tools.jar ./check.sh +set -eu + +cd "$(dirname "$0")" + +jar="${TLA2TOOLS_JAR:-$HOME/.local/share/tla/tla2tools.jar}" +if [ ! -f "$jar" ]; then + echo "tla2tools.jar not found at $jar (set TLA2TOOLS_JAR)" >&2 + exit 2 +fi +# Prefer JAVA_HOME, then Homebrew's keg-only openjdk, then java on PATH. +java="" +for candidate in \ + "${JAVA_HOME:+$JAVA_HOME/bin/java}" \ + /opt/homebrew/opt/openjdk/bin/java \ + /usr/local/opt/openjdk/bin/java \ + "$(command -v java 2>/dev/null || true)"; do + if [ -n "$candidate" ] && [ -x "$candidate" ] && "$candidate" -version >/dev/null 2>&1; then + java="$candidate" + break + fi +done +if [ -z "$java" ]; then + echo "no working Java runtime (set JAVA_HOME or brew install openjdk)" >&2 + exit 2 +fi + +all="SessionLog TurnLifecycle WriterLock ResumeSnapshot Fork Subagents Catalog Lifecycle Wiring MoveSideFiles V1Conversion" +specs="${*:-$all}" +work="${TMPDIR:-/tmp}/session-manager-tlc" +mkdir -p "$work" + +status=0 +for spec in $specs; do + echo "== $spec" + # -deadlock: do not report states with no enabled action. Every spec is + # bounded (MaxLen, MaxLines, finite id sets), so terminal states are + # expected at the bound. + if ! "$java" -XX:+UseParallelGC -cp "$jar" tlc2.TLC \ + -deadlock -workers auto -cleanup \ + -metadir "$work/$spec" \ + -config "$spec.cfg" "$spec.tla"; then + status=1 + fi +done +exit "$status" diff --git a/src/core/session_manager/tla/mutants.py b/src/core/session_manager/tla/mutants.py new file mode 100755 index 000000000..2f802eb9f --- /dev/null +++ b/src/core/session_manager/tla/mutants.py @@ -0,0 +1,199 @@ +#!/usr/bin/env python3 +"""Check that every spec still catches the bugs it exists to catch. + +Each mutant plants one realistic design bug in a temporary copy of a spec +and runs TLC on it. The run passes only if TLC reports the expected +invariant as violated. Run after changing any spec: + + ./mutants.py + +Needs the same Java runtime and tla2tools.jar as check.sh. +""" +import os +import pathlib +import shutil +import subprocess +import sys +import tempfile + +HERE = pathlib.Path(__file__).resolve().parent +JAR = os.environ.get("TLA2TOOLS_JAR", os.path.expanduser("~/.local/share/tla/tla2tools.jar")) + +# (spec, bug description, text to replace, replacement, invariant that must fail) +MUTANTS = [ + ("Wiring", "a fork reuses a session that exists", + " /\\ f \\notin {cur, next}\n /\\ ~made[f]\n", + " /\\ f \\notin {cur, next}\n", + "ForkIsNewSession"), + ("Wiring", "a fork while a turn is open", + " /\\ ~made[f]\n /\\ ~turnOpen[cur]\n /\\ next' = f", + " /\\ ~made[f]\n /\\ next' = f", + "ForkBetweenTurns"), + ("Wiring", "the fork step writes the source", + " /\\ \\E e \\in Ends : lastEnd' = [lastEnd EXCEPT ![f] = e]", + " /\\ \\E e \\in Ends : lastEnd' = [lastEnd EXCEPT ![f] = e, ![cur] = \"interrupt\"]", + "ForkLeavesSource"), + ('V1Conversion', 'a converter takes locks another process holds', ' /\\ IF \\A i \\in present : v1lock[i] = "free"\n', ' /\\ IF TRUE\n', 'LockHeld'), + ('V1Conversion', 'a fresh v2 session takes a live v1 id', '(AvoidV1Ids => v1ver[i] = 0)', 'TRUE', 'NoShadow'), + ('V1Conversion', 'the root lands before its children', ' /\\ \\A c \\in conv[p].members \\ {r} : ~staged[c]\n', '', 'ChildrenLanded'), + ('V1Conversion', "a busy answer sweeps another process's staging", ' ELSE /\\ Answer(p, "busy")\n /\\ UNCHANGED <>\n /\\ UNCHANGED <>\n /\\ staged\' = [i \\in Ids |-> FALSE]\n /\\ UNCHANGED < IF v1lock[i] = p THEN "free" ELSE v1lock[i]]\n', " /\\ v1lock' = v1lock\n", 'NoStaleConvLock'), + ('V1Conversion', 'an open reports a live v1 session missing', ' /\\ pub[req[p].root] = "none" /\\ v1ver[req[p].root] = 0\n /\\ Answer(p, IF', ' /\\ ~Live(req[p].root)\n /\\ Answer(p, IF', 'NoFalseNotFound'), + ('V1Conversion', 'a conversion starts without a request', ' LET r == req[p].root\n present == {i \\in Fam(r) : v1ver[i] > 0} IN\n /\\ Waiting(p)\n', ' LET r == RootId\n present == {i \\in Fam(r) : v1ver[i] > 0} IN\n /\\ conv[p] = Idle\n', 'ConvertsOnlyOnRequest'), + ('V1Conversion', 'an unreadable member leaves its staging', " /\\ staged' = [i \\in Ids |-> IF i \\in Fam(conv[p].root) THEN FALSE ELSE staged[i]]\n", " /\\ staged' = [i \\in Ids |-> IF i \\in copy THEN TRUE ELSE staged[i]]\n", 'NothingHalfConverted'), + ('V1Conversion', 'a busy answer keeps the locks it took', ' ELSE /\\ Answer(p, "busy")\n /\\ UNCHANGED <>', ' ELSE /\\ Answer(p, "busy")\n /\\ v1lock\' = [i \\in Ids |-> IF i \\in present /\\ v1lock[i] = "free" THEN p ELSE v1lock[i]]\n /\\ UNCHANGED conv', 'NoStaleConvLock'), + ('V1Conversion', 'a child loses its v1 folder before its root is published', " /\\ base' = [base EXCEPT ![c] = stagedBase[c]]\n /\\ UNCHANGED < 0 /\\ v1ver[i] = base[i] /\\ ~bad[i]\n', ' /\\ pub[i] = "import" /\\ v1ver[i] > 0 /\\ ~bad[i]\n', 'NoLossOnDelete'), + ('V1Conversion', "a cleanup ignores a writer's lock", ' /\\ v1lock[i] = "free" /\\ i \\notin refused[p]', ' /\\ i \\notin refused[p]', 'NoLossOnDelete'), + ('V1Conversion', 'a conversion keeps the v1 folders', ' /\\ \\A i \\in conv[p].members : ~Unchanged(p, i) \\/ i \\in refused[p]\n', '', 'LeftoversGone'), + ('V1Conversion', 'an open skips the leftover cleanup', ' /\\ ~\\E i \\in Fam(req[p].root) : Leftover(p, i)\n', '', 'LeftoversGone'), + ('V1Conversion', 'the locks go before the delete', ' /\\ UNCHANGED <>', ' /\\ v1lock\' = [i \\in Ids |-> IF i \\in conv[p].members THEN "free" ELSE v1lock[i]]\n /\\ UNCHANGED <>', 'LockHeld'), + ('V1Conversion', 'the converter writes a v1 file', ' /\\ UNCHANGED <>', " /\\ bad' = [i \\in Ids |-> IF i \\in conv[p].members THEN TRUE ELSE bad[i]]\n /\\ UNCHANGED <>", 'ConverterOnlyDeletes'), + ('V1Conversion', 'a reused child is deleted after an older build changed it', ' /\\ i \\in conv[p].members /\\ v1ver[i] > 0 /\\ v1ver[i] = base[i]\n /\\ i \\in conv[p].copied', ' /\\ i \\in conv[p].members /\\ v1ver[i] > 0\n /\\ i \\in conv[p].copied', 'NoLossOnDelete'), + ('V1Conversion', 'the v1 usage marker goes before the v2 one is written', " /\\ mark1[i] /\\ mark2[i]\n /\\ mark1' = [mark1 EXCEPT ![i] = FALSE]", " /\\ mark1[i]\n /\\ mark1' = [mark1 EXCEPT ![i] = FALSE]", 'UsageKept'), + ('V1Conversion', 'a folder goes before its usage marker moved', 'Deletable(p, i) == Unchanged(p, i) /\\ ~mark1[i]', 'Deletable(p, i) == Unchanged(p, i)', 'NoDanglingMark'), + ('V1Conversion', 'a leftover is cleaned before its usage marker moved', " /\\ Leftover(p, i) /\\ ~mark1[i]\n /\\ v1ver' = [v1ver EXCEPT ![i] = 0]", " /\\ Leftover(p, i)\n /\\ v1ver' = [v1ver EXCEPT ![i] = 0]", 'NoDanglingMark'), + ('V1Conversion', 'a reused child is copied again', ' copy == {i \\in m : pub[i] = "none"} IN', ' copy == m IN', 'ChildrenStick'), + ("SessionLog", "fsync acks a half-written line", + 'Fsync ==\n /\\ status = "open"', + 'Fsync ==\n /\\ status \\in {"open", "writing"}', + "AckedSurvive"), + ("SessionLog", "open() keeps a torn tail", + "IF LastDone THEN log ELSE SubSeq(log, 1, Len(log) - 1)", "log", + "OpenIsClean"), + ("TurnLifecycle", "reopen skips turn_interrupted", + "log' = IF IsOpen(log) THEN Append(log, \"interrupt\") ELSE log", "log' = log", + "NoStaleTurnAfterReopen"), + ("TurnLifecycle", "manager accepts an item outside a turn", + '[] k = "item" -> IsOpen(l)', '[] k = "item" -> TRUE', + "ItemsInsideTurns"), + ("WriterLock", "open ignores the flock", + " /\\ holder = None\n /\\ holder' = p", " /\\ holder' = p", + "OneWriter"), + ("ResumeSnapshot", "snapshot stores the wrong state", + 'Entry("snap", NoVal, Full(log))', 'Entry("snap", NoVal, Empty)', + "ResumeEqualsFullReplay"), + ("Fork", "fork forgets blob links", + "links' = [links EXCEPT ![f] = links[src]]", "links' = links", + "RefsExist"), + ("Fork", "fork copies a line whose blob was lost", + " /\\ \\A i \\in 2..at : lg[src][i].b # NoBlob => lg[src][i].b \\in links[src]\n", "", + "RefsExist"), + ("Fork", "fork allowed inside an open turn", + " /\\ ~IsOpen(SubSeq(lg[src], 1, at))\n", "", + "ForkAtBoundary"), + ("Subagents", "repair marks every child lost", + 'o |-> IF childLog[c] THEN "interrupted" ELSE "lost"', 'o |-> "lost"', + "LostMeansNoLog"), + ("Subagents", "spawn while the child's work is open", + " /\\ ~Unfinished(c)\n /\\ Works(c) < MaxWork", + " /\\ Works(c) < MaxWork", + "OneOpenWork"), + ("Wiring", "a subagent opens its session on v1", + "ChildBackend == backend", 'ChildBackend == "v1"', + "OneBackend"), + ("Wiring", "close without joining child threads", + " /\\ child = \"none\"\n /\\ cur' = IF s = cur", + " /\\ cur' = IF s = cur", + "ParentOutlivesChildren"), + ("Wiring", "switch to the session already open", + " /\\ s # cur\n", + "", + "SwitchIsTwoSessions"), + ("Wiring", "charge usage before writing the marker", + " /\\ marker[cur]\n /\\ usageSplit'", + " /\\ usageSplit'", + "UsageNeverSilent"), + ("Wiring", "clear the marker before usage is durable", + " /\\ marker[s]\n /\\ ~usageSplit[s]\n", + " /\\ marker[s]\n", + "UsageNeverSilent"), + ("Wiring", "continue a committed turn", + " /\\ lastEnd[cur] = \"interrupt\"\n", + "", + "ContinueLinksInterrupted"), + ("Subagents", "reopen skips child repair", + " /\\ repairing' = TRUE\n /\\ UNCHANGED <>", + " /\\ repairing' = FALSE\n /\\ UNCHANGED <>", + "NoIndeterminate"), + ("Catalog", "list skips the folder check", + 'Listed == {s \\in Indexed : dir[s] = "live"}', "Listed == Indexed", + "ListedAreLive"), + ("Fork", "a setting lists a blob the session lacks", + " /\\ b \\in links[s]\n /\\ lg' = [lg EXCEPT ![s] = Append(@, E(\"set\", b))]", + " /\\ lg' = [lg EXCEPT ![s] = Append(@, E(\"set\", b))]", + "RefsExist"), + ("MoveSideFiles", "the map is written before every body is a blob", + " /\\ ~mapped\n /\\ blobs = Handles\n /\\ mapped' = TRUE", + " /\\ ~mapped\n /\\ mapped' = TRUE", + "Resolvable"), + ("MoveSideFiles", "the side folder goes before the terminal moved", + " /\\ mapped\n /\\ terminal = \"moved\"\n /\\ folder = \"present\"", + " /\\ mapped\n /\\ folder = \"present\"", + "TerminalKept"), + ("Catalog", "an index refresh for a session never published", + 'Refresh(s) ==\n /\\ dir[s] = "live"', "Refresh(s) ==\n /\\ TRUE", + "IndexNamesPublished"), + ("Lifecycle", "rename before fsync of line 1", + 'Advance(s, "synced", "renamed")', 'Advance(s, "written", "renamed")', + "VisibleHasLine1"), + ("Lifecycle", "ack before fsync of the directory", + 'Advance(s, "renamed", "done")', 'Advance(s, "synced", "done")', + "AckedIsVisible"), +] + + +def find_java(): + candidates = [] + if os.environ.get("JAVA_HOME"): + candidates.append(os.path.join(os.environ["JAVA_HOME"], "bin", "java")) + candidates += ["/opt/homebrew/opt/openjdk/bin/java", "/usr/local/opt/openjdk/bin/java"] + on_path = shutil.which("java") + if on_path: + candidates.append(on_path) + for candidate in candidates: + if os.access(candidate, os.X_OK): + probe = subprocess.run([candidate, "-version"], capture_output=True) + if probe.returncode == 0: + return candidate + return None + + +def main(): + java = find_java() + if java is None or not os.path.isfile(JAR): + print("needs a Java runtime and tla2tools.jar (see check.sh)", file=sys.stderr) + return 2 + survivors = 0 + with tempfile.TemporaryDirectory(prefix="session-manager-mutants-") as tmp: + for index, (spec, desc, old, new, expected) in enumerate(MUTANTS): + work = pathlib.Path(tmp) / f"{index:02d}-{spec}" + work.mkdir() + text = (HERE / f"{spec}.tla").read_text() + if old not in text: + print(f"{spec:15s} {desc:42s} STALE: mutation no longer applies") + survivors += 1 + continue + (work / f"{spec}.tla").write_text(text.replace(old, new, 1)) + # A smaller model, when the full one is too large to search per mutant. + small = HERE / f"{spec}.mutants.cfg" + shutil.copy(small if small.exists() else HERE / f"{spec}.cfg", work / f"{spec}.cfg") + run = subprocess.run( + [java, "-XX:+UseParallelGC", "-cp", JAR, "tlc2.TLC", "-deadlock", + "-workers", "auto", "-cleanup", "-metadir", str(work / "states"), + "-config", f"{spec}.cfg", f"{spec}.tla"], + cwd=work, capture_output=True, text=True, timeout=900, + ) + output = run.stdout + run.stderr + if (f"Invariant {expected} is violated" in output + or f"Action property {expected} is violated" in output): + print(f"{spec:15s} {desc:42s} caught by {expected}") + else: + print(f"{spec:15s} {desc:42s} SURVIVED (expected {expected} to fail)") + survivors += 1 + print("all mutants caught" if survivors == 0 else f"{survivors} mutant(s) survived") + return 0 if survivors == 0 else 1 + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/src/core/session_manager/tla/trace/CatalogTrace.cfg b/src/core/session_manager/tla/trace/CatalogTrace.cfg new file mode 100644 index 000000000..daef0463d --- /dev/null +++ b/src/core/session_manager/tla/trace/CatalogTrace.cfg @@ -0,0 +1,4 @@ +SPECIFICATION TraceSpec +CONSTANT Ids <- TraceIds +CONSTRAINT Progress +INVARIANT TraceIncomplete diff --git a/src/core/session_manager/tla/trace/CatalogTrace.tla b/src/core/session_manager/tla/trace/CatalogTrace.tla new file mode 100644 index 000000000..e7718ba1b --- /dev/null +++ b/src/core/session_manager/tla/trace/CatalogTrace.tla @@ -0,0 +1,57 @@ +---------------------------- MODULE CatalogTrace ---------------------------- +(***************************************************************************) +(* Trace validation for Catalog.tla (index.jsonl, delete, heal, rebuild). *) +(* *) +(* One trace line per action: *) +(* event Publish | IndexPut | Trash | IndexDel | Purge | Heal (with *) +(* s) | Crash | Rebuild *) +(* s "s1" | "s2" | "s3" *) +(* dir per session, from the folders: "live" ({id}/), "trash" *) +(* (.trash/{id}/), else "gone" once published, else "none" *) +(* index [id, op] per put or del line of index.jsonl, in file order; *) +(* a put that follows a put for the same id only updates the *) +(* summary and is left out, as are `opened` lines *) +(* pending, everDeleted what the code still owes, and a ghost *) +(***************************************************************************) +EXTENDS Catalog, TraceData, TLC + +VARIABLE l +tvars == <> + +TraceIds == {"s1", "s2", "s3"} + +ASSUME TLCSet(1, 0) + +Matches(e) == + /\ dir' = e.dir + /\ index' = e.index + /\ pending' = e.pending + /\ everDeleted' = e.everDeleted + +Act(e) == + CASE e.event = "Publish" -> Publish(e.s) + [] e.event = "IndexPut" -> IndexPut(e.s) + [] e.event = "Trash" -> Trash(e.s) + [] e.event = "IndexDel" -> IndexDel(e.s) + [] e.event = "Purge" -> Purge(e.s) + [] e.event = "Heal" -> Heal(e.s) + [] e.event = "Crash" -> Crash + [] e.event = "Rebuild" -> Rebuild + +TraceInit == Init /\ l = 1 + +TraceNext == + /\ l <= Len(Trace) + /\ Act(Trace[l]) + /\ Matches(Trace[l]) + /\ l' = l + 1 + +TraceSpec == TraceInit /\ [][TraceNext]_tvars + +Progress == + IF l - 1 > TLCGet(1) + THEN TLCSet(1, l - 1) /\ PrintT(<<"matched_lines", l - 1>>) + ELSE TRUE + +TraceIncomplete == l <= Len(Trace) +============================================================================= diff --git a/src/core/session_manager/tla/trace/ForkLog.tla b/src/core/session_manager/tla/trace/ForkLog.tla new file mode 100644 index 000000000..96da25cd8 --- /dev/null +++ b/src/core/session_manager/tla/trace/ForkLog.tla @@ -0,0 +1,31 @@ +------------------------------ MODULE ForkLog ------------------------------ +(***************************************************************************) +(* A saved fork against its saved source (D5, D58). *) +(* *) +(* `Copied` is the fork's lines after line 1 up to its `forked_from.seq`, *) +(* the lines the manager copied; `Source` is the source's lines after *) +(* line 1. Both leave out snapshots, which a fork encodes again. Each line *) +(* is a record [k, h]: k its kind as TurnLifecycleLog names kinds, h a *) +(* hash of its exact bytes. Accepted when the copied lines are exactly the *) +(* source's first lines, byte for byte, and end at a turn boundary: every *) +(* turn they start, they also end. `NotWritten` then fails. *) +(***************************************************************************) +EXTENDS Naturals, Sequences, FiniteSets, SavedFork + +VARIABLE checked + +Starts(s) == {i \in 1..Len(s) : s[i].k = "start"} +Ends(s) == {i \in 1..Len(s) : s[i].k \in {"commit", "interrupt"}} + +IsPrefix == + /\ Len(Copied) <= Len(Source) + /\ \A i \in 1..Len(Copied) : Copied[i] = Source[i] + +AtBoundary == Cardinality(Starts(Copied)) = Cardinality(Ends(Copied)) + +LogInit == checked = FALSE +LogNext == ~checked /\ IsPrefix /\ AtBoundary /\ checked' = TRUE +LogSpec == LogInit /\ [][LogNext]_checked + +NotWritten == ~checked +============================================================================= diff --git a/src/core/session_manager/tla/trace/ForkTrace.cfg b/src/core/session_manager/tla/trace/ForkTrace.cfg new file mode 100644 index 000000000..1dc735c5e --- /dev/null +++ b/src/core/session_manager/tla/trace/ForkTrace.cfg @@ -0,0 +1,8 @@ +SPECIFICATION TraceSpec +CONSTANTS + Ids <- TraceIds + Blobs <- TraceBlobs + MaxLen <- TraceMaxLen + NoBlob <- TraceNoBlob +CONSTRAINT Progress +INVARIANT TraceIncomplete diff --git a/src/core/session_manager/tla/trace/ForkTrace.tla b/src/core/session_manager/tla/trace/ForkTrace.tla new file mode 100644 index 000000000..e989e0c00 --- /dev/null +++ b/src/core/session_manager/tla/trace/ForkTrace.tla @@ -0,0 +1,58 @@ +----------------------------- MODULE ForkTrace ----------------------------- +(***************************************************************************) +(* Trace validation for Fork.tla (blobs, fork at a boundary, delete). *) +(* *) +(* One trace line per action: *) +(* event Create | Start | Commit | Delete (with s) | PutBlob | Item *) +(* (with s and b) | Fork (with src, f, at) *) +(* s, src, f "s1" | "s2" | "s3"; b "b1" | "b2"; at the fork's S *) +(* st per session: "none" | "live" | "deleted" *) +(* lg per session, parsed from its log.jsonl: [k, b] for every *) +(* created, start, commit and item line; b is the item's blob *) +(* links per session: the blob files in its blobs/ folder *) +(* base per session: the prefix a fork copied, as the code copied it *) +(***************************************************************************) +EXTENDS Fork, TraceData, TLC + +VARIABLE l +tvars == <> + +TraceIds == {"s1", "s2", "s3"} +TraceBlobs == {"b1", "b2"} +TraceMaxLen == 32 +TraceNoBlob == "none" + +ASSUME TLCSet(1, 0) + +Matches(e) == + /\ st' = e.st + /\ lg' = e.lg + /\ links' = e.links + /\ base' = e.base + +Act(e) == + CASE e.event = "Create" -> Create(e.s) + [] e.event = "Start" -> Start(e.s) + [] e.event = "Commit" -> Commit(e.s) + [] e.event = "Delete" -> Delete(e.s) + [] e.event = "PutBlob" -> PutBlob(e.s, e.b) + [] e.event = "Item" -> Item(e.s, e.b) + [] e.event = "Fork" -> Fork(e.src, e.f, e.at) + +TraceInit == Init /\ l = 1 + +TraceNext == + /\ l <= Len(Trace) + /\ Act(Trace[l]) + /\ Matches(Trace[l]) + /\ l' = l + 1 + +TraceSpec == TraceInit /\ [][TraceNext]_tvars + +Progress == + IF l - 1 > TLCGet(1) + THEN TLCSet(1, l - 1) /\ PrintT(<<"matched_lines", l - 1>>) + ELSE TRUE + +TraceIncomplete == l <= Len(Trace) +============================================================================= diff --git a/src/core/session_manager/tla/trace/LifecycleTrace.cfg b/src/core/session_manager/tla/trace/LifecycleTrace.cfg new file mode 100644 index 000000000..daef0463d --- /dev/null +++ b/src/core/session_manager/tla/trace/LifecycleTrace.cfg @@ -0,0 +1,4 @@ +SPECIFICATION TraceSpec +CONSTANT Ids <- TraceIds +CONSTRAINT Progress +INVARIANT TraceIncomplete diff --git a/src/core/session_manager/tla/trace/LifecycleTrace.tla b/src/core/session_manager/tla/trace/LifecycleTrace.tla new file mode 100644 index 000000000..69ddef865 --- /dev/null +++ b/src/core/session_manager/tla/trace/LifecycleTrace.tla @@ -0,0 +1,58 @@ +-------------------------- MODULE LifecycleTrace -------------------------- +(***************************************************************************) +(* Trace validation for Lifecycle.tla (lazy creation and the first-turn *) +(* publish). *) +(* *) +(* One trace line per action: *) +(* event OpenNew | MkTmp | WriteLine1 | FsyncLog | Rename | *) +(* FsyncDirAndAck | Sweep (with s) | ProcessCrash | PowerLoss *) +(* s "s1" or "s2", for the per-session actions *) +(* step [s1 |-> ..., s2 |-> ...], how far each publish has got *) +(* where per session: "none" | "tmp" | "visible", from the folders *) +(* line1 per session: "none" | "cached" | "durable", from the log file *) +(* and the fault layer's record of what was synced *) +(* acked per session: the caller was told the first turn was saved *) +(***************************************************************************) +EXTENDS Lifecycle, Sequences, TraceData, TLC + +VARIABLE l +tvars == <> + +TraceIds == {"s1", "s2"} + +ASSUME TLCSet(1, 0) + +Matches(e) == + /\ step' = e.step + /\ where' = e.where + /\ line1' = e.line1 + /\ acked' = e.acked + +Act(e) == + CASE e.event = "OpenNew" -> OpenNew(e.s) + [] e.event = "MkTmp" -> MkTmp(e.s) + [] e.event = "WriteLine1" -> WriteLine1(e.s) + [] e.event = "FsyncLog" -> FsyncLog(e.s) + [] e.event = "Rename" -> Rename(e.s) + [] e.event = "FsyncDirAndAck" -> FsyncDirAndAck(e.s) + [] e.event = "Sweep" -> Sweep(e.s) + [] e.event = "ProcessCrash" -> ProcessCrash + [] e.event = "PowerLoss" -> PowerLoss + +TraceInit == Init /\ l = 1 + +TraceNext == + /\ l <= Len(Trace) + /\ Act(Trace[l]) + /\ Matches(Trace[l]) + /\ l' = l + 1 + +TraceSpec == TraceInit /\ [][TraceNext]_tvars + +Progress == + IF l - 1 > TLCGet(1) + THEN TLCSet(1, l - 1) /\ PrintT(<<"matched_lines", l - 1>>) + ELSE TRUE + +TraceIncomplete == l <= Len(Trace) +============================================================================= diff --git a/src/core/session_manager/tla/trace/README.md b/src/core/session_manager/tla/trace/README.md new file mode 100644 index 000000000..5c52b4dc2 --- /dev/null +++ b/src/core/session_manager/tla/trace/README.md @@ -0,0 +1,145 @@ +# Trace validation: checking the code against the specs + +TLC cannot read Zig. Instead, the implementation writes one JSON line per +step it takes, and TLC checks that the whole sequence is a behavior the spec +allows. A trace is **accepted** only if some behavior of the spec produces +exactly the logged states, step by step. Otherwise it is **rejected**, and +`validate.sh` names the first step the spec does not allow. + +The models in `..` check the design exhaustively within their bounds. Trace +validation checks that the real code stays inside the design on every run +we execute: unit tests, the standalone driver, and the `kill -9` and +machine-crash matrix. + +## How it works + +```text +Zig test build trace.ndjson to_tla.py TLC +------------------ -------------- --------- --- +each L1/L2 step -------> {"event": "Fsync", --> TraceData.tla --> SpecTrace.tla +emits one line "log_len": 2, ...} (Trace == <<...>>) EXTENDS Spec, TraceData + step l must be action + Trace[l].event, and the + next state must equal + Trace[l]'s fields +``` + +- `SpecTrace.tla` extends the spec unchanged. It adds a counter `l` over the + trace, and each TLC step must be the action named by `Trace[l].event`, + landing in a state whose variables equal that line's fields. +- Nondeterministic actions such as `PowerLoss` are resolved by the logged + state: TLC tries every choice and keeps the ones that match. +- The trick for the verdict: the invariant `TraceIncomplete == l <= Len(Trace)` + is violated exactly when the whole trace was matched, so TLC reporting a + violation means ACCEPTED. A state constraint prints the furthest line + matched, which names the rejected step. + +## Files + +| File | Purpose | +|---|---| +| `validate.sh SPEC trace.ndjson` | Runs the check in a temp directory. Exit 0 accepted, 1 rejected, 2 tool error | +| `to_tla.py` | Converts JSON lines into `TraceData.tla`. Lists become sequences, objects records, `{"$set": [...]}` sets | +| `SessionLogTrace.tla`, `.cfg` | Wrapper for `SessionLog.tla`. The event contract is in its header | +| `stand_in_log.py` | A small Python stand-in for L1, used only to self-test this tooling | +| `check_saved_logs.py ROOT...` | Checks logs fx saved (`{id}/log.jsonl` under each ROOT) after the fact: every log against `TurnLifecycle`, every parent with child lines against `Subagents`, and every fork against its source with `ForkLog`. `--selftest` requires 7 good and 9 planted logs to get their verdicts | +| `ForkLog.tla` | A fork's copied lines against its source's: accepted only when they are the source's first lines byte for byte (snapshots aside, which a fork encodes again) and end at a turn boundary | +| `TurnLifecycleLog.tla`, `SubagentsLog.tla` | Its wrappers. Only the disk is known, so TLC searches the process state between lines; accepted when some behavior writes exactly the saved lines | +| `check_wiring_traces.py LOG...` | Checks the adapter's `wiring` trace lines (a run with `FX_TRACE_SCOPES=wiring`) against `Wiring.tla`: each process's lines become Start, the host steps and Exit, or Crash when it stops without Exit. A log where two processes overlap is skipped. `--selftest` requires 6 good and 8 planted traces to get their verdicts, the fork cases included | +| `WiringTrace.tla` | Its wrapper. Accepted when every step is allowed in turn; the usage steps change nothing a traced step reads, so they are left out | +| `bun_tlc_check.sh FX_WORKTREE [FILE [PATTERN]]` | Runs fx's E2E tests under Bun with `FX_E2E_TLA_DIR` set, then checks every kept run with TLC: the `wiring` traces with `check_wiring_traces.py` and the saved logs with `check_saved_logs.py`. Exit 0 only when all are ACCEPTED and at least `MIN_FORKS` (default 1) fork steps and saved forks were checked; a skipped trace counts as a failure | +| `check_conversion.py --request R --report D` | Checks a v1-to-v2 conversion run against `V1Conversion.tla` (D59). The request comes from the pipeline harness suite `session-conversion-tlc`, which drives the real binary step by step (older-build v1 writes, opens, `fx sessions convert`, holds, damage, a crash mid-conversion) and observes each step's result on disk and through fx's own readers and listing. Exit 0 ACCEPTED only when TLC matched every observation, 1 REJECTED, 2 INCONCLUSIVE, 3 TOOL_ERROR. `--selftest` requires 6 good and 7 planted runs to get their verdicts | +| `V1ConversionTrace.tla` | Its wrapper. Each observation's step kind limits the model actions that may run before it; a request step makes exactly one request, and only a writer an earlier hold step left running may write during it | +| `selftest.sh` | Proves the tooling both accepts and rejects (below) | + +## Self-test + +`./selftest.sh` runs the stand-in three ways and requires these verdicts: + +| Case | Required verdict | +|---|---| +| Correct stand-in (writes, fsync, a crash in the middle of a write, recovery, a machine crash that tears a line, recovery) | ACCEPTED, 15 steps | +| Recovery keeps a torn tail (planted bug) | REJECTED at step 8, the `Recover` | +| Good trace with `acked` changed from 2 to 3 on line 5 | REJECTED at step 5 | + +Last run: 2026-09-27, TLC2 2.19. All three verdicts matched. + +## The contract for the Zig trace hook + +These rules apply to the test-only trace hook, `../../trace.zig`: + +1. **Test builds only.** The hook is behind a build option and compiles to + nothing in release builds, so it adds no cost and no I/O to fx. +2. **One line per spec action,** named exactly like the action in the spec + (`BeginWrite`, `Fsync`, `Recover`, ...), with one field per spec variable + under the names in the wrapper header. +3. **Real state, not bookkeeping.** Fields that model the disk (line count, + torn tail, seq numbers, which folders exist) are computed by reading the + actual files after the step. Fields that model memory (status, acked, open + turn) come from the manager's own state. A trace built only from the + writer's counters would agree with itself and prove nothing. +4. **One order.** Steps inside a Session are emitted while holding the + Session mutex, so the trace order is the real order. Multi-process tests + (`WriterLock`) run through the standalone driver, which serializes the + steps of all processes into one trace. +5. **Crashes are logged by the driver.** A killed process cannot log its own + crash. After `kill -9` or a simulated machine crash, the driver appends the + `ProcessCrash` or `PowerLoss` line, reading the disk state itself. +6. **Every trace gets checked.** The driver runs `validate.sh` on every trace + it produces, and any rejection fails the run. + +## Adding a wrapper for another spec + +Copy `SessionLogTrace.tla` and change three things: + +- `EXTENDS` names the new spec. +- `Matches(e)` compares every variable of that spec with the fields of `e`. +- `Act(e)` maps each event name to the spec's action. For an action with + parameters, such as `Write(k)` or `Open(p)`, the line carries the argument, + and `Act` passes it on, for example + `[] e.event = "Write" -> Write(e.kind)`. + +Keep `TraceInit`, `TraceNext`, `Progress` and `TraceIncomplete` as they are, +and copy the `.cfg`, setting the spec's constants large enough for real +traces. Then add a stand-in case, or a real Zig test, that the new wrapper +must reject. A wrapper that has never rejected anything is not yet trusted. + +Each of these wrappers has rejected its planted bug: `TurnLifecycleTrace`, +`WriterLockTrace`, `ResumeSnapshotTrace`, `LifecycleTrace`, `ForkTrace`, +`SubagentsTrace` and `CatalogTrace`. + +## Limits + +- **Guard with IF, never with `\/`, inside `Matches`.** Within an action, + TLC explores both sides of a disjunction, so + `Len(log') = 0 \/ log'[Len(log')].done` still indexes an empty sequence and + ends in a tool error. The first Zig traces (an `Fsync` and a `Recover` on an + empty log) found this in `SessionLogTrace.tla`; it now uses IF. + +- **Give every TLC run its own `java.io.tmpdir`.** TLC unpacks `TLC.tla`, + `Naturals.tla` and the other standard modules there. With a shared + folder, parallel checks read each other's half-written copies and fail + with "Fatal errors while parsing". `validate.sh` points it into the + run's private work folder, and `check_saved_logs.py` and + `check_wiring_traces.py` give each parallel check its own (`JOBS`, + default 6). +- **A batch is one write; trace views end at the observed line.** The + manager writes each batch in one append, observed or not, so traced runs + and the crash matrix see production's write pattern (a process kill never + splits a batch). Its lines are observed one by one after the write, so + a tracer that reads the log bounds its view by the observed line's seq. +- **Only what runs is checked.** Trace validation checks the runs we + execute. That is why the driver's crash matrix matters: it decides which + code paths get traced. +- **The mapping from files to spec state must be right.** A wrong mapping can + hide a bug. Keep it small, and read the real files (rule 3). +- **Traces must fit the model's constants.** `SessionLogTrace.cfg` raises + `MaxLines` to 64 for that reason, and `TurnLifecycleTrace.tla` sets + `TraceMaxLen` to 4096 for the driver's host models, whose logs run to + hundreds of lines. A longer trace is rejected at the bound, so raise the + constant or split the trace. In a trace check the bound adds no states: + the trace fixes every step. +- **TLC 2.19 plus the Community Modules jar crashes** + (`NoClassDefFoundError: tlc2/value/impl/KSubsetValue`). That is why the + converter exists instead of `Json!ndJsonDeserialize`. Revisit when a TLC + release matches the modules jar. diff --git a/src/core/session_manager/tla/trace/ResumeSnapshotTrace.cfg b/src/core/session_manager/tla/trace/ResumeSnapshotTrace.cfg new file mode 100644 index 000000000..7200672c4 --- /dev/null +++ b/src/core/session_manager/tla/trace/ResumeSnapshotTrace.cfg @@ -0,0 +1,7 @@ +SPECIFICATION TraceSpec +CONSTANTS + Vals <- TraceVals + MaxLen <- TraceMaxLen + NoVal <- TraceNoVal +CONSTRAINT Progress +INVARIANT TraceIncomplete diff --git a/src/core/session_manager/tla/trace/ResumeSnapshotTrace.tla b/src/core/session_manager/tla/trace/ResumeSnapshotTrace.tla new file mode 100644 index 000000000..c27fc2402 --- /dev/null +++ b/src/core/session_manager/tla/trace/ResumeSnapshotTrace.tla @@ -0,0 +1,51 @@ +------------------------ MODULE ResumeSnapshotTrace ------------------------ +(***************************************************************************) +(* Trace validation for ResumeSnapshot.tla (the fold and its snapshots). *) +(* *) +(* One trace line per action: *) +(* event Set (with v) | Start | Commit | Snapshot *) +(* v for Set: "v1" | "v2", the prefs value written *) +(* log every modeled line on disk, parsed from log.jsonl: *) +(* [k |-> "set" | "start" | "commit" | "snap", v, st]. For a *) +(* snapshot, st is read from the snapshot's own state object: *) +(* [pref, turns (committed), open]. Other kinds are outside this *) +(* spec and left out. *) +(* The Snapshot action requires st to equal the full fold at that point, *) +(* so a snapshot that stores the wrong state is rejected. *) +(***************************************************************************) +EXTENDS ResumeSnapshot, TraceData, TLC + +VARIABLE l +tvars == <> + +TraceVals == {"v1", "v2"} +TraceMaxLen == 64 +TraceNoVal == "none" + +ASSUME TLCSet(1, 0) + +Matches(e) == log' = e.log + +Act(e) == + CASE e.event = "Set" -> Set(e.v) + [] e.event = "Start" -> Start + [] e.event = "Commit" -> Commit + [] e.event = "Snapshot" -> Snapshot + +TraceInit == Init /\ l = 1 + +TraceNext == + /\ l <= Len(Trace) + /\ Act(Trace[l]) + /\ Matches(Trace[l]) + /\ l' = l + 1 + +TraceSpec == TraceInit /\ [][TraceNext]_tvars + +Progress == + IF l - 1 > TLCGet(1) + THEN TLCSet(1, l - 1) /\ PrintT(<<"matched_lines", l - 1>>) + ELSE TRUE + +TraceIncomplete == l <= Len(Trace) +============================================================================= diff --git a/src/core/session_manager/tla/trace/SessionLogTrace.cfg b/src/core/session_manager/tla/trace/SessionLogTrace.cfg new file mode 100644 index 000000000..9380352b9 --- /dev/null +++ b/src/core/session_manager/tla/trace/SessionLogTrace.cfg @@ -0,0 +1,4 @@ +SPECIFICATION TraceSpec +CONSTANT MaxLines = 64 +CONSTRAINT Progress +INVARIANT TraceIncomplete diff --git a/src/core/session_manager/tla/trace/SessionLogTrace.tla b/src/core/session_manager/tla/trace/SessionLogTrace.tla new file mode 100644 index 000000000..0ebe4a26a --- /dev/null +++ b/src/core/session_manager/tla/trace/SessionLogTrace.tla @@ -0,0 +1,66 @@ +------------------------- MODULE SessionLogTrace ------------------------- +(***************************************************************************) +(* Trace validation for SessionLog.tla. *) +(* *) +(* TLC accepts an implementation trace only if some behavior of SessionLog *) +(* produces exactly the logged states, step by step. TraceData.tla is *) +(* generated from the implementation's JSON-lines trace by to_tla.py. *) +(* *) +(* One trace line per L1 step: *) +(* event BeginWrite | FinishWrite | Fsync | ProcessCrash | *) +(* PowerLoss | Recover *) +(* log_len lines in log.jsonl, counting a torn final line *) +(* tail_done whether the file ends in "\n" *) +(* seqs seq of every complete line, parsed from the file bytes *) +(* durable lines covered by the last fsync *) +(* acked lines acknowledged to callers as durable *) +(* status "open" | "writing" | "down" *) +(* log_len, tail_done and seqs must come from reading the real file, not *) +(* from the writer's own counters. *) +(***************************************************************************) +EXTENDS SessionLog, TraceData, TLC + +VARIABLE l +tvars == <> + +ASSUME TLCSet(1, 0) + +\* IF, not \/: inside an action TLC explores both sides of a disjunction, +\* so `Len(log') = 0 \/ log'[Len(log')].done` would index an empty log. +Matches(e) == + /\ Len(log') = e.log_len + /\ IF Len(log') = 0 THEN e.tail_done ELSE log'[Len(log')].done = e.tail_done + /\ Len(e.seqs) <= Len(log') + /\ \A i \in 1..Len(e.seqs) : log'[i].seq = e.seqs[i] + /\ durable' = e.durable + /\ acked' = e.acked + /\ status' = e.status + +Act(e) == + CASE e.event = "BeginWrite" -> BeginWrite + [] e.event = "FinishWrite" -> FinishWrite + [] e.event = "Fsync" -> Fsync + [] e.event = "ProcessCrash" -> ProcessCrash + [] e.event = "PowerLoss" -> PowerLoss + [] e.event = "Recover" -> Recover + +TraceInit == Init /\ l = 1 + +TraceNext == + /\ l <= Len(Trace) + /\ Act(Trace[l]) + /\ Matches(Trace[l]) + /\ l' = l + 1 + +TraceSpec == TraceInit /\ [][TraceNext]_tvars + +\* State constraint: prints each new furthest trace line matched. +Progress == + IF l - 1 > TLCGet(1) + THEN TLCSet(1, l - 1) /\ PrintT(<<"matched_lines", l - 1>>) + ELSE TRUE + +\* Violated exactly when the whole trace was matched: TLC reporting this +\* invariant as violated means ACCEPTED. +TraceIncomplete == l <= Len(Trace) +============================================================================= diff --git a/src/core/session_manager/tla/trace/SubagentsLog.tla b/src/core/session_manager/tla/trace/SubagentsLog.tla new file mode 100644 index 000000000..e647a5da5 --- /dev/null +++ b/src/core/session_manager/tla/trace/SubagentsLog.tla @@ -0,0 +1,31 @@ +--------------------------- MODULE SubagentsLog --------------------------- +(***************************************************************************) +(* Checks a parent log fx saved against Subagents.tla, after the fact. *) +(* *) +(* Only the disk is known: the parent's child lines, in order (`Target`, *) +(* records [k, c, w, o]), and which children have a log at the end *) +(* (`FinalChildLog`), both from SavedChildren.tla. Threads, crashes, *) +(* reopens and when each child's log appeared are left to TLC. Accepted *) +(* when some behavior of the spec writes exactly these lines and ends *) +(* with those child logs: the invariant `NotWritten` then fails. *) +(* *) +(* check_saved_logs.py writes SavedChildren.tla and runs this. *) +(***************************************************************************) +EXTENDS Subagents, SavedChildren, TLC + +ASSUME TLCSet(1, 0) + +LogNext == + /\ Next + /\ Len(plog') <= Len(Target) + /\ plog' = SubSeq(Target, 1, Len(plog')) + +LogSpec == Init /\ [][LogNext]_vars + +Progress == + IF Len(plog) > TLCGet(1) + THEN TLCSet(1, Len(plog)) /\ PrintT(<<"matched_lines", Len(plog)>>) + ELSE TRUE + +NotWritten == ~(plog = Target /\ childLog = FinalChildLog) +============================================================================= diff --git a/src/core/session_manager/tla/trace/SubagentsTrace.cfg b/src/core/session_manager/tla/trace/SubagentsTrace.cfg new file mode 100644 index 000000000..16a2aa4c4 --- /dev/null +++ b/src/core/session_manager/tla/trace/SubagentsTrace.cfg @@ -0,0 +1,5 @@ +SPECIFICATION TraceSpec +CONSTANT Children <- TraceChildren +CONSTANT MaxWork <- TraceMaxWork +CONSTRAINT Progress +INVARIANT TraceIncomplete diff --git a/src/core/session_manager/tla/trace/SubagentsTrace.tla b/src/core/session_manager/tla/trace/SubagentsTrace.tla new file mode 100644 index 000000000..cf2fcc75b --- /dev/null +++ b/src/core/session_manager/tla/trace/SubagentsTrace.tla @@ -0,0 +1,58 @@ +--------------------------- MODULE SubagentsTrace --------------------------- +(***************************************************************************) +(* Trace validation for Subagents.tla (children and parent reopen repair).*) +(* *) +(* One trace line per action: *) +(* event Spawn | ChildStart | ChildFinish | Cancel | RepairChild *) +(* (with c) | Crash | Reopen | RepairDone *) +(* c "c1" | "c2" *) +(* plog the parent's child lines, parsed from its log.jsonl: *) +(* [k |-> "spawned" | "finished", c, w (the child's work *) +(* number, counted from its spawn lines), o] *) +(* childLog per child: {child}/log.jsonl exists *) +(* thread, up, repairing the process's own state, as the code runs it *) +(***************************************************************************) +EXTENDS Subagents, TraceData, TLC + +VARIABLE l +tvars == <> + +TraceChildren == {"c1", "c2"} +TraceMaxWork == 2 + +ASSUME TLCSet(1, 0) + +Matches(e) == + /\ plog' = e.plog + /\ childLog' = e.childLog + /\ thread' = e.thread + /\ up' = e.up + /\ repairing' = e.repairing + +Act(e) == + CASE e.event = "Spawn" -> Spawn(e.c) + [] e.event = "ChildStart" -> ChildStart(e.c) + [] e.event = "ChildFinish" -> ChildFinish(e.c) + [] e.event = "Cancel" -> Cancel(e.c) + [] e.event = "RepairChild" -> RepairChild(e.c) + [] e.event = "Crash" -> Crash + [] e.event = "Reopen" -> Reopen + [] e.event = "RepairDone" -> RepairDone + +TraceInit == Init /\ l = 1 + +TraceNext == + /\ l <= Len(Trace) + /\ Act(Trace[l]) + /\ Matches(Trace[l]) + /\ l' = l + 1 + +TraceSpec == TraceInit /\ [][TraceNext]_tvars + +Progress == + IF l - 1 > TLCGet(1) + THEN TLCSet(1, l - 1) /\ PrintT(<<"matched_lines", l - 1>>) + ELSE TRUE + +TraceIncomplete == l <= Len(Trace) +============================================================================= diff --git a/src/core/session_manager/tla/trace/TurnLifecycleLog.tla b/src/core/session_manager/tla/trace/TurnLifecycleLog.tla new file mode 100644 index 000000000..3400e8f25 --- /dev/null +++ b/src/core/session_manager/tla/trace/TurnLifecycleLog.tla @@ -0,0 +1,29 @@ +------------------------- MODULE TurnLifecycleLog ------------------------- +(***************************************************************************) +(* Checks a log fx saved against TurnLifecycle.tla, after the fact. *) +(* *) +(* Only the disk is known: the log's kinds, in order (`Target`, from *) +(* SavedLog.tla). The process state (status, fresh), and with it every *) +(* close, crash and reopen that wrote no line, is left to TLC. The log is *) +(* accepted when some behavior of the spec writes exactly these lines: *) +(* every step keeps the log a prefix of `Target`, and the invariant *) +(* `NotWritten` fails once the whole log is written. *) +(* *) +(* check_saved_logs.py writes SavedLog.tla and runs this. *) +(***************************************************************************) +EXTENDS TurnLifecycle, SavedLog, TLC + +ASSUME TLCSet(1, 0) + +LogNext == Next /\ Prefix(log', Target) + +LogSpec == Init /\ [][LogNext]_vars + +\* Prints the longest prefix written, which names the rejected line. +Progress == + IF Len(log) > TLCGet(1) + THEN TLCSet(1, Len(log)) /\ PrintT(<<"matched_lines", Len(log)>>) + ELSE TRUE + +NotWritten == log # Target +============================================================================= diff --git a/src/core/session_manager/tla/trace/TurnLifecycleTrace.cfg b/src/core/session_manager/tla/trace/TurnLifecycleTrace.cfg new file mode 100644 index 000000000..c5ef342d7 --- /dev/null +++ b/src/core/session_manager/tla/trace/TurnLifecycleTrace.cfg @@ -0,0 +1,4 @@ +SPECIFICATION TraceSpec +CONSTANT MaxLen <- TraceMaxLen +CONSTRAINT Progress +INVARIANT TraceIncomplete diff --git a/src/core/session_manager/tla/trace/TurnLifecycleTrace.tla b/src/core/session_manager/tla/trace/TurnLifecycleTrace.tla new file mode 100644 index 000000000..779e191b7 --- /dev/null +++ b/src/core/session_manager/tla/trace/TurnLifecycleTrace.tla @@ -0,0 +1,53 @@ +------------------------ MODULE TurnLifecycleTrace ------------------------ +(***************************************************************************) +(* Trace validation for TurnLifecycle.tla (turn rules, close, reopen). *) +(* *) +(* One trace line per action: *) +(* event Create | Write (with kind) | Close | Crash | Reopen *) +(* kind for Write: start | item | compacted | commit | interrupt | set *) +(* log the kinds on disk, in order, parsed from log.jsonl; snapshot *) +(* and child lines are outside this spec and left out *) +(* status "new" | "open" | "closed" | "down" *) +(* fresh TRUE from a reopen until the next turn starts *) +(***************************************************************************) +EXTENDS TurnLifecycle, TraceData, TLC + +VARIABLE l +tvars == <> + +\* Only bounds the log a trace may build; the trace fixes every step, so +\* a large bound adds no states. The driver's host models run to hundreds +\* of lines. +TraceMaxLen == 4096 + +ASSUME TLCSet(1, 0) + +Matches(e) == + /\ log' = e.log + /\ status' = e.status + /\ fresh' = e.fresh + +Act(e) == + CASE e.event = "Create" -> Create + [] e.event = "Write" -> Write(e.kind) + [] e.event = "Close" -> Close + [] e.event = "Crash" -> Crash + [] e.event = "Reopen" -> Reopen + +TraceInit == Init /\ l = 1 + +TraceNext == + /\ l <= Len(Trace) + /\ Act(Trace[l]) + /\ Matches(Trace[l]) + /\ l' = l + 1 + +TraceSpec == TraceInit /\ [][TraceNext]_tvars + +Progress == + IF l - 1 > TLCGet(1) + THEN TLCSet(1, l - 1) /\ PrintT(<<"matched_lines", l - 1>>) + ELSE TRUE + +TraceIncomplete == l <= Len(Trace) +============================================================================= diff --git a/src/core/session_manager/tla/trace/V1ConversionTrace.tla b/src/core/session_manager/tla/trace/V1ConversionTrace.tla new file mode 100644 index 000000000..f5471409b --- /dev/null +++ b/src/core/session_manager/tla/trace/V1ConversionTrace.tla @@ -0,0 +1,108 @@ +--------------------------- MODULE V1ConversionTrace --------------------------- +(***************************************************************************) +(* Trace validation for V1Conversion.tla from what real fx runs leave. *) +(* *) +(* A driver runs real fx processes one step at a time and observes the *) +(* result after each (`Obs`, from ConversionData.tla), a record with *) +(* k the step: create | write | hold | release (older-build v1 *) +(* writers), open | all | crash (a request, the last one killed *) +(* mid-request), open2 (two processes opening the same root at *) +(* once), damage, fresh (a new v2 session), list *) +(* r the requested root ("none" for other steps) *) +(* ans the request's answer: opened | converted | busy | unreadable *) +(* | notfound, or none; ans2 the second process's, for open2 *) +(* v1 [Ids -> version]: each v1 member's distinct contents in order *) +(* of first appearance, 0 absent *) +(* pub [AllIds -> Status]: each id in v2 *) +(* base [AllIds -> version]: for a converted id, the v1 version its *) +(* copy equals, -1 when it equals none *) +(* extra [AllIds -> Nat]: v2 turns after the copied ones *) +(* dirty conversion leftovers in .tmp *) +(* listed the ids the listing shows *) +(* bad [Ids -> BOOLEAN]: members the driver made unreadable *) +(* held the members a still-running older build has open *) +(* denied the driver made the file system refuse deletes in this step *) +(* Between observations, only the actions of that step's kind may run, *) +(* any number of them; a request step makes exactly its requests, by *) +(* process p1 (and p2 for open2). Accepted when some behavior of *) +(* V1Conversion passes through every observation in order: `NotDone` *) +(* then fails. *) +(***************************************************************************) +EXTENDS V1Conversion, ConversionData, Sequences, TLC + +VARIABLE l +tvars == <> + +ASSUME TLCSet(1, 0) + +P1 == "p1" +P2 == "p2" + +\* The requests observation `j` makes. +Made(o) == CASE o.k = "open2" -> 2 [] o.k \in {"open", "all", "crash"} -> 1 [] OTHER -> 0 +RECURSIVE ReqCount(_) +ReqCount(n) == IF n = 0 THEN 0 ELSE Made(Obs[n]) + ReqCount(n - 1) + +\* A refused delete is a fault only a step that injected it may show. +ConvAllowed(p, o) == ConvWork(p) \/ (o.denied /\ ConvRefused(p)) + +\* During a request, an older build may write only if an earlier hold step +\* left it holding the session; it cannot take a lock there. +HolderStep(i) == WBegin(i) \/ WEnd(i) \/ WMark(i) + +\* The actions a step of kind `o.k` may take, at observation index `n`. +Hidden(o, n) == + CASE o.k \in {"create", "write", "hold", "release"} -> + \E i \in Ids : WriterStep(i) + [] o.k = "damage" -> \E i \in Ids : Damage(i) + [] o.k = "fresh" -> \E i \in NewIds : FCreate(i) \/ FAppend(i) + [] o.k \in {"open", "all"} -> + \/ reqs < ReqCount(n) /\ Request(P1, o.k, o.r) + \/ ConvAllowed(P1, o) + \/ \E i \in Ids : HolderStep(i) + \/ req[P1] = NoReq /\ reqs = ReqCount(n) /\ \E i \in AllIds : FAppend(i) + [] o.k = "open2" -> + \/ reqs = ReqCount(n) - 2 /\ Request(P1, "open", o.r) + \/ reqs = ReqCount(n) - 1 /\ Request(P2, "open", o.r) + \/ \E p \in {P1, P2} : ConvAllowed(p, o) + \/ \E i \in Ids : HolderStep(i) + \/ req[P1] = NoReq /\ req[P2] = NoReq /\ reqs = ReqCount(n) /\ \E i \in AllIds : FAppend(i) + [] o.k = "crash" -> + \/ reqs < ReqCount(n) /\ \E kk \in {"open", "all"} : Request(P1, kk, o.r) + \/ ConvAllowed(P1, o) \/ CCrash(P1) + \/ \E i \in Ids : HolderStep(i) + [] OTHER -> FALSE + +Match(o, n) == + /\ v1ver = o.v1 + /\ pub = o.pub + /\ \A i \in AllIds : pub[i] = "import" => base[i] = o.base[i] + /\ extra = o.extra + /\ Dirty = o.dirty + /\ Listed = o.listed + /\ bad = o.bad + /\ {i \in Ids : v1lock[i] = "writer"} = o.held + /\ reqs = ReqCount(n) + /\ \A p \in Procs : req[p] = NoReq /\ conv[p] = Idle + /\ o.k \in {"open", "all"} => out[P1].ans = o.ans + /\ o.k = "open2" => + \/ out[P1].ans = o.ans /\ out[P2].ans = o.ans2 + \/ out[P1].ans = o.ans2 /\ out[P2].ans = o.ans + /\ o.k = "crash" => out[P1].ans = "none" + +TraceInit == Init /\ l = 1 + +TraceNext == + /\ l <= Len(Obs) + /\ \/ Hidden(Obs[l], l) /\ UNCHANGED l + \/ Match(Obs[l], l) /\ l' = l + 1 /\ UNCHANGED vars + +TraceSpec == TraceInit /\ [][TraceNext]_tvars + +Progress == + IF l - 1 > TLCGet(1) + THEN TLCSet(1, l - 1) /\ PrintT(<<"matched_lines", l - 1>>) + ELSE TRUE + +NotDone == l <= Len(Obs) +============================================================================= diff --git a/src/core/session_manager/tla/trace/WiringTrace.tla b/src/core/session_manager/tla/trace/WiringTrace.tla new file mode 100644 index 000000000..c09f04d7b --- /dev/null +++ b/src/core/session_manager/tla/trace/WiringTrace.tla @@ -0,0 +1,55 @@ +------------------------------ MODULE WiringTrace ------------------------------ +(***************************************************************************) +(* Trace validation for Wiring.tla, from fx's `wiring` trace lines. *) +(* *) +(* One trace line per step the adapter logs, in order (`Trace`, from *) +(* WiringData.tla): a record [a, s, e] with *) +(* a Start | Open | BeginTurn | EndTurn | Spawn | ChildDone | Close *) +(* | Fork | Exit | Crash *) +(* s the session, "s1".. (Open, Close, and Fork's new session), else *) +(* "none" *) +(* e "commit" | "interrupt" (EndTurn only), else "none" *) +(* Start and Exit are the store's first open and last close in a process *) +(* (a process whose tracing starts after its store opened starts at its *) +(* first line); *) +(* Crash is added by check_wiring_traces.py when a process's lines stop *) +(* without Exit. The usage steps (the marker, charges, checkpoints) happen *) +(* in code the adapter does not see; they change only `usageSplit` and *) +(* `marker`, which no traced step reads, so they are left out. Accepted *) +(* when every line is an allowed step in turn: `NotDone` then fails. *) +(***************************************************************************) +EXTENDS Wiring, WiringData, Sequences, TLC + +VARIABLE l +tvars == <> + +ASSUME TLCSet(1, 0) + +Act(e) == + CASE e.a = "Start" -> Start("v2") + [] e.a = "Open" -> Open(e.s) + [] e.a = "BeginTurn" -> BeginTurn + [] e.a = "EndTurn" -> EndTurn(e.e) + [] e.a = "Spawn" -> Spawn + [] e.a = "ChildDone" -> ChildDone + [] e.a = "Close" -> Close(e.s) + [] e.a = "Fork" -> Fork(e.s) + [] e.a = "Exit" -> Exit + [] e.a = "Crash" -> Crash + +TraceInit == Init /\ l = 1 + +TraceNext == + /\ l <= Len(Trace) + /\ Act(Trace[l]) + /\ l' = l + 1 + +TraceSpec == TraceInit /\ [][TraceNext]_tvars + +Progress == + IF l - 1 > TLCGet(1) + THEN TLCSet(1, l - 1) /\ PrintT(<<"matched_lines", l - 1>>) + ELSE TRUE + +NotDone == l <= Len(Trace) +============================================================================= diff --git a/src/core/session_manager/tla/trace/WriterLockTrace.cfg b/src/core/session_manager/tla/trace/WriterLockTrace.cfg new file mode 100644 index 000000000..c2225ef50 --- /dev/null +++ b/src/core/session_manager/tla/trace/WriterLockTrace.cfg @@ -0,0 +1,8 @@ +SPECIFICATION TraceSpec +CONSTANTS + Procs <- TraceProcs + Threads <- TraceThreads + MaxLines <- TraceMaxLines + None <- TraceNone +CONSTRAINT Progress +INVARIANT TraceIncomplete diff --git a/src/core/session_manager/tla/trace/WriterLockTrace.tla b/src/core/session_manager/tla/trace/WriterLockTrace.tla new file mode 100644 index 000000000..7562b6801 --- /dev/null +++ b/src/core/session_manager/tla/trace/WriterLockTrace.tla @@ -0,0 +1,62 @@ +-------------------------- MODULE WriterLockTrace -------------------------- +(***************************************************************************) +(* Trace validation for WriterLock.tla (flock plus the Session mutex). *) +(* *) +(* One trace line per action: *) +(* event Open | Close | Crash | Restart (with p) | *) +(* Acquire | WriteAndRelease (with p and t) *) +(* p, t "p1" | "p2" and "t1" | "t2" *) +(* holder the process holding the flock, or "none" *) +(* alive, opened, nextSeq, mutex per process *) +(* file [seq, by] for each line written since the trace began, *) +(* parsed from log.jsonl: seq counts from 1 at the first traced *) +(* line, `by` is the writer named in the line. `closed` lines *) +(* are bookkeeping outside this spec and are left out, and the *) +(* seqs after them shift down, so a skipped or duplicated seq *) +(* still shows as a mismatch. *) +(***************************************************************************) +EXTENDS WriterLock, TraceData, TLC + +VARIABLE l +tvars == <> + +TraceProcs == {"p1", "p2"} +TraceThreads == {"t1", "t2"} +TraceMaxLines == 64 +TraceNone == "none" + +ASSUME TLCSet(1, 0) + +Matches(e) == + /\ holder' = e.holder + /\ alive' = e.alive + /\ opened' = e.opened + /\ nextSeq' = e.nextSeq + /\ mutex' = e.mutex + /\ file' = e.file + +Act(e) == + CASE e.event = "Open" -> Open(e.p) + [] e.event = "Close" -> Close(e.p) + [] e.event = "Crash" -> Crash(e.p) + [] e.event = "Restart" -> Restart(e.p) + [] e.event = "Acquire" -> Acquire(e.p, e.t) + [] e.event = "WriteAndRelease" -> WriteAndRelease(e.p, e.t) + +TraceInit == Init /\ l = 1 + +TraceNext == + /\ l <= Len(Trace) + /\ Act(Trace[l]) + /\ Matches(Trace[l]) + /\ l' = l + 1 + +TraceSpec == TraceInit /\ [][TraceNext]_tvars + +Progress == + IF l - 1 > TLCGet(1) + THEN TLCSet(1, l - 1) /\ PrintT(<<"matched_lines", l - 1>>) + ELSE TRUE + +TraceIncomplete == l <= Len(Trace) +============================================================================= diff --git a/src/core/session_manager/tla/trace/bun_tlc_check.sh b/src/core/session_manager/tla/trace/bun_tlc_check.sh new file mode 100755 index 000000000..b213e316c --- /dev/null +++ b/src/core/session_manager/tla/trace/bun_tlc_check.sh @@ -0,0 +1,60 @@ +#!/usr/bin/env bash +# Runs fx's E2E tests under Bun with traces kept, then checks every run with +# TLC: each process's `wiring` trace against Wiring.tla, and each saved log +# against TurnLifecycle, Subagents and, for a fork, ForkLog. Exits 0 only when +# every check is ACCEPTED and the runs held at least MIN_FORKS fork steps. +# +# bun_tlc_check.sh FX_WORKTREE [TEST_FILE [TEST_NAME_PATTERN]] +# +# FX_WORKTREE is an fx checkout whose zig-out/bin/fx is built. MIN_FORKS +# (default 1) guards against a run that never reached the code under check. +set -euo pipefail + +here="$(cd "$(dirname "$0")" && pwd)" +fx="${1:?usage: bun_tlc_check.sh FX_WORKTREE [TEST_FILE [TEST_NAME_PATTERN]]}" +file="${2:-sessions-v2.test.ts}" +pattern="${3:-fork}" +min_forks="${MIN_FORKS:-1}" + +[ -x "$fx/zig-out/bin/fx" ] || { echo "build fx first: $fx/zig-out/bin/fx" >&2; exit 2; } +out="$(mktemp -d "${TMPDIR:-/tmp}/fx-bun-tlc.XXXXXX")" +echo "runs kept in $out" + +(cd "$fx/tests/e2e" && env -u AI_GATEWAY_API_KEY -u AI_GATEWAY_TEST_API_KEY \ + FX_E2E_TLA_DIR="$out" bun test "$file" -t "$pattern") || { + echo "bun: the tests failed; TLC not run" >&2 + exit 1 +} + +traces=() +while IFS= read -r f; do traces+=("$f"); done < <(find "$out" -name '*.wiring.log' | sort) +roots=() +while IFS= read -r d; do roots+=("$d"); done < <(find "$out" -type d -name 'sessions-v2' | sort) +[ "${#traces[@]}" -gt 0 ] || { echo "no wiring traces kept: is FX_E2E_TLA_DIR honored?" >&2; exit 1; } +[ "${#roots[@]}" -gt 0 ] || { echo "no saved logs kept" >&2; exit 1; } + +forks="$(cat "${traces[@]}" | grep -c 'action=Fork ' || true)" +echo "traces ${#traces[@]}, saved roots ${#roots[@]}, fork steps $forks" +[ "$forks" -ge "$min_forks" ] || { echo "fewer than $min_forks fork steps reached TLC" >&2; exit 1; } + +status=0 +echo "== wiring traces against Wiring.tla" +wiring="$(python3 "$here/check_wiring_traces.py" "${traces[@]}")" || status=1 +echo "$wiring" +if echo "$wiring" | grep -q -E '^(REJECTED|SKIPPED|TOOL ERROR) +/'; then status=1; fi +# An empty trace is right only for a run on v1, which saves no v2 sessions. +while IFS= read -r path; do + [ -n "$path" ] || continue + if [ -d "$(dirname "$path")/sessions-v2" ]; then + echo "a v2 run left an empty trace: $path" >&2 + status=1 + fi +done < <(echo "$wiring" | sed -n -E 's/^EMPTY +(.*): no wiring lines$/\1/p') +echo "$wiring" | grep -q -E '^ACCEPTED +[1-9]' || { echo "no trace was accepted" >&2; status=1; } +echo "== saved logs against TurnLifecycle, Subagents and ForkLog" +saved="$(python3 "$here/check_saved_logs.py" "${roots[@]}")" || status=1 +echo "$saved" +fork_jobs="$(echo "$saved" | awk '$1 == "fork" && $2 == "ACCEPTED" {print $3}')" +[ "${fork_jobs:-0}" -ge "$min_forks" ] || { echo "fewer than $min_forks saved forks checked" >&2; status=1; } +[ "$status" -eq 0 ] && echo "ALL ACCEPTED" || echo "NOT ALL ACCEPTED" +exit "$status" diff --git a/src/core/session_manager/tla/trace/check_conversion.py b/src/core/session_manager/tla/trace/check_conversion.py new file mode 100644 index 000000000..71ad74c0d --- /dev/null +++ b/src/core/session_manager/tla/trace/check_conversion.py @@ -0,0 +1,311 @@ +#!/usr/bin/env python3 +"""Check what real fx runs did against V1Conversion.tla, with TLC. + + check_conversion.py --request REQUEST.json --report DIR + check_conversion.py --selftest + +REQUEST is written by the Bun driver: {"version": 1, "ids": {"root": ID, +"child": ID or null, "fresh": [ID, ...]}, "observations": [...]}, one +observation per real step, as V1ConversionTrace.tla describes. The verdict +is printed as JSON and kept in DIR with TLC's log and its generated inputs: +ACCEPTED (exit 0) only when TLC reached its sentinel with every observation +matched; REJECTED (1) when TLC ran to the end without matching them all; +INCONCLUSIVE (2) for malformed or empty evidence; TOOL_ERROR (3) otherwise. +""" +import argparse +import hashlib +import json +import os +import pwd +import re +import shutil +import subprocess +import sys +from pathlib import Path + +HERE = Path(__file__).resolve().parent +TLA = HERE.parent +JAVA = os.environ.get("JAVA", "/opt/homebrew/opt/openjdk/bin/java") +# The account's home, not $HOME: drivers run fx under a disposable HOME. +JAR = os.environ.get("TLA_JAR", os.path.join(pwd.getpwuid(os.getuid()).pw_dir, ".local/share/tla/tla2tools.jar")) + +KINDS = {"create", "write", "hold", "release", "open", "all", "crash", "open2", "damage", "fresh", "list"} +REQUESTS = {"open", "all", "crash", "open2"} +ANSWERS = {"none", "opened", "converted", "busy", "unreadable", "notfound"} +STATUS = {"none", "import", "fresh"} +EXIT = {"ACCEPTED": 0, "REJECTED": 1, "INCONCLUSIVE": 2, "TOOL_ERROR": 3} + + +class Inconclusive(Exception): + pass + + +def tla_str(s): + return '"' + s.replace("\\", "\\\\").replace('"', '\\"') + '"' + + +def tla_fun(mapping, render): + return "(" + " @@ ".join(f"{tla_str(k)} :> {render(v)}" for k, v in mapping.items()) + ")" + + +def model_ids(ids): + """Real id -> model id: the root "r", the child "c", fresh sessions "n1"..""" + root, child, fresh = ids.get("root"), ids.get("child"), ids.get("fresh", []) + if not isinstance(root, str) or not root: + raise Inconclusive("the request names no root id") + names = {root: "r"} + if child: + names[child] = "c" + for n, fid in enumerate(fresh, 1): + names[fid] = f"n{n}" + if len(names) != 1 + bool(child) + len(fresh): + raise Inconclusive("ids repeat") + return names + + +def model_obs(request): + names = model_ids(request.get("ids", {})) + obs = request.get("observations") + if not isinstance(obs, list) or not obs: + raise Inconclusive("no observations") + if not any(o.get("k") in REQUESTS for o in obs): + raise Inconclusive("no request step was observed") + member = ["r", "c"] + every = member + sorted(v for v in names.values() if v.startswith("n")) + out = [] + for n, o in enumerate(obs, 1): + try: + k, ans, ans2 = o["k"], o.get("ans", "none"), o.get("ans2", "none") + if k not in KINDS or ans not in ANSWERS or ans2 not in ANSWERS: + raise Inconclusive(f"observation {n}: unknown step or answer") + r = names.get(o.get("r"), "none") if k in REQUESTS else "none" + if k in REQUESTS and r != "r": + raise Inconclusive(f"observation {n}: a request names no known root") + + def by_model(field, default, check): + got = {names[i]: v for i, v in o[field].items() if i in names} + if len(got) != len(o[field]): + raise Inconclusive(f"observation {n}: {field} names an unknown id") + for v in got.values(): + check(v) + return got, default + + def nat(v): + if not isinstance(v, int) or v < -1: + raise Inconclusive(f"observation {n}: a count is not an integer") + + def status(v): + if v not in STATUS: + raise Inconclusive(f"observation {n}: unknown v2 status {v!r}") + + def flag(v): + if not isinstance(v, bool): + raise Inconclusive(f"observation {n}: a flag is not a boolean") + + v1, _ = by_model("v1", 0, nat) + pub, _ = by_model("pub", "none", status) + base, _ = by_model("base", 0, nat) + extra, _ = by_model("extra", 0, nat) + bad, _ = by_model("bad", False, flag) + listed, held, denied = o["listed"], o.get("held", []), o.get("denied", False) + if not isinstance(o["dirty"], bool) or not isinstance(listed, list) or not isinstance(held, list) \ + or not isinstance(denied, bool): + raise Inconclusive(f"observation {n}: dirty, listed, held or denied is malformed") + if denied and k not in REQUESTS: + raise Inconclusive(f"observation {n}: deletes can only be refused during a request") + if any(names.get(i) not in member for i in held): + raise Inconclusive(f"observation {n}: held names an id that is not a v1 member") + unknown = [i for i in listed if i not in names] + out.append({ + "k": k, "r": r, "ans": ans, "ans2": ans2, + "v1": {i: v1.get(i, 0) for i in member}, + "pub": {i: pub.get(i, "none") for i in every}, + "base": {i: base.get(i, 0) for i in every}, + "extra": {i: extra.get(i, 0) for i in every}, + "bad": {i: bad.get(i, False) for i in member}, + "dirty": o["dirty"], + "denied": denied, + "held": sorted(names[i] for i in held), + # An id the run does not know can never match the model's listing. + "listed": sorted({names[i] for i in listed if i in names} | ({"unknown"} if unknown else set())), + }) + except KeyError as missing: + raise Inconclusive(f"observation {n}: missing {missing}") + return out, [v for v in every if v.startswith("n")] + + +def data_module(obs): + def rec(o): + return ("[k |-> " + tla_str(o["k"]) + ", r |-> " + tla_str(o["r"]) + ", ans |-> " + tla_str(o["ans"]) + + ", ans2 |-> " + tla_str(o["ans2"]) + + ", v1 |-> " + tla_fun(o["v1"], str) + ", pub |-> " + tla_fun(o["pub"], tla_str) + + ", base |-> " + tla_fun(o["base"], str) + ", extra |-> " + tla_fun(o["extra"], str) + + ", bad |-> " + tla_fun(o["bad"], lambda b: "TRUE" if b else "FALSE") + + ", dirty |-> " + ("TRUE" if o["dirty"] else "FALSE") + + ", denied |-> " + ("TRUE" if o["denied"] else "FALSE") + + ", held |-> {" + ", ".join(tla_str(i) for i in o["held"]) + "}" + + ", listed |-> {" + ", ".join(tla_str(i) for i in o["listed"]) + "}]") + body = ",\n ".join(rec(o) for o in obs) + return f"---- MODULE ConversionData ----\nEXTENDS TLC, Integers, FiniteSets\nObs == <<\n {body}\n>>\n====\n" + + +def config(obs, fresh): + kinds = [o["k"] for o in obs] + max_v = max([1] + [v for o in obs for v in o["v1"].values()]) + max_extra = max([1] + [v for o in obs for v in o["extra"].values()]) + writes = sum(k in {"create", "write", "hold"} for k in kinds) + 1 + crashes = sum(k in {"crash", "release"} for k in kinds) + 3 * sum(o["denied"] for o in obs) + 1 + reqs = sum(2 if k == "open2" else 1 for k in kinds if k in REQUESTS) + fresh_set = "{" + ", ".join(tla_str(f) for f in fresh) + "}" + return (f'CONSTANTS\n Procs = {{"p1", "p2"}}\n RootId = "r"\n ChildId = "c"\n NewIds = {fresh_set}\n None = None\n' + f" Torn = Torn\n MaxV = {max_v}\n MaxLocks = {writes}\n MaxExtra = {max_extra}\n" + f" MaxCrash = {crashes}\n MaxReq = {reqs}\n AvoidV1Ids = TRUE\n" + "SPECIFICATION TraceSpec\nINVARIANT NotDone\nCONSTRAINT Progress\n") + + +def sha256(path): + return hashlib.sha256(Path(path).read_bytes()).hexdigest() + + +def run_tlc(obs, fresh, work): + work.mkdir(parents=True) + (work / "tmp").mkdir() + for name in ("V1Conversion.tla",): + shutil.copyfile(TLA / name, work / name) + shutil.copyfile(HERE / "V1ConversionTrace.tla", work / "V1ConversionTrace.tla") + (work / "ConversionData.tla").write_text(data_module(obs)) + (work / "V1ConversionTrace.cfg").write_text(config(obs, fresh)) + command = [JAVA, "-XX:+UseParallelGC", f"-Djava.io.tmpdir={work / 'tmp'}", "-cp", JAR, "tlc2.TLC", + "-workers", "1", "-deadlock", "-metadir", str(work / "states"), + "-config", "V1ConversionTrace.cfg", "V1ConversionTrace"] + with (work / "tlc.log").open("w") as log: + code = subprocess.run(command, cwd=work, stdout=log, stderr=subprocess.STDOUT, timeout=600).returncode + text = (work / "tlc.log").read_text(errors="replace") + matched = max([int(m) for m in re.findall(r'"matched_lines", (\d+)', text)] or [0]) + expected = len(obs) + if code == 12 and "Invariant NotDone is violated" in text and matched == expected: + verdict = "ACCEPTED" + elif code == 0 and "No error has been found" in text and matched < expected: + verdict = "REJECTED" + else: + verdict = "TOOL_ERROR" + shutil.rmtree(work / "states", ignore_errors=True) + shutil.rmtree(work / "tmp", ignore_errors=True) + return {"verdict": verdict, "matched": matched, "expected": expected, "exitCode": code, + "log": str(work / "tlc.log"), + "modelHashes": {n: sha256(work / n) for n in ("V1Conversion.tla", "V1ConversionTrace.tla")}} + + +def verify(request, report): + if request.get("version") != 1: + raise Inconclusive("version 1 required") + obs, fresh = model_obs(request) + result = run_tlc(obs, fresh, report / "tlc") + if result["verdict"] == "REJECTED": + step = obs[result["matched"]] + result["detail"] = (f"observations 1..{result['matched']} match; observation {result['matched'] + 1} " + f"({step['k']}, answer {step['ans']}) is not a behavior of V1Conversion") + return result + + +def selftest(): + """Planted observation sequences: each must get its verdict.""" + ids = {"root": "R", "child": None, "fresh": []} + + def ob(k, v1=0, pub="none", base=0, extra=0, ans="none", dirty=False, listed=None, bad=False, r="R", held=(), + denied=False, ans2="none"): + return {"k": k, "r": r, "ans": ans, "ans2": ans2, "v1": {"R": v1}, "pub": {"R": pub}, "base": {"R": base}, + "extra": {"R": extra}, "bad": {"R": bad}, "dirty": dirty, "held": list(held), + "listed": ["R"] if listed is None else listed, "denied": denied} + made = ob("create", v1=1) + kept = ob("open", v1=1, pub="import", base=1, ans="opened", denied=True) + cases = [ + ("an open converts the v1 session and deletes it, then a turn lands in v2", + [made, ob("open", pub="import", base=1, extra=1, ans="opened")], "ACCEPTED"), + ("convert-all, then an open of the converted session", + [made, ob("all", pub="import", base=1, ans="converted"), + ob("open", pub="import", base=1, ans="opened")], "ACCEPTED"), + ("busy while an older build holds it, opened once released", + [made, ob("hold", v1=1, held=["R"]), ob("open", v1=1, ans="busy", held=["R"]), ob("release", v1=1), + ob("open", pub="import", base=1, ans="opened")], "ACCEPTED"), + ("unreadable: refused, nothing converted or deleted", + [made, ob("damage", v1=1, bad=True), ob("open", v1=1, bad=True, ans="unreadable")], "ACCEPTED"), + ("a refused delete leaves the folder; the next open deletes it", + [made, kept, ob("open", pub="import", base=1, ans="opened")], "ACCEPTED"), + ("an older build changes a leftover; the next open keeps it, and v2 keeps its copy", + [made, kept, ob("write", v1=2, pub="import", base=1), + ob("open", v1=2, pub="import", base=1, ans="opened")], "ACCEPTED"), + ("a crash mid-conversion leaves staging; the next open sweeps it", + [made, ob("crash", v1=1, dirty=True), ob("open", pub="import", base=1, ans="opened")], "ACCEPTED"), + ("two processes open it at once: one converts, both open the copy", + [made, ob("open2", pub="import", base=1, ans="opened", ans2="opened")], "ACCEPTED"), + ("planted: of two processes opening it at once, one calls it unreadable", + [made, ob("open2", pub="import", base=1, ans="opened", ans2="unreadable")], "REJECTED"), + ("planted: a live v1 session reported missing", + [made, ob("open", v1=1, ans="notfound")], "REJECTED"), + ("planted: the copy matches no v1 version", + [made, ob("open", pub="import", base=-1, ans="opened")], "REJECTED"), + ("planted: busy with no holder", + [made, ob("open", v1=1, ans="busy")], "REJECTED"), + ("planted: the listing hides an unconverted v1 session", + [made, ob("list", v1=1, listed=[]), ob("open", pub="import", base=1, ans="opened")], "REJECTED"), + ("planted: unreadable, yet half converted", + [made, ob("damage", v1=1, bad=True), ob("open", v1=1, bad=True, dirty=True, ans="unreadable")], "REJECTED"), + ("planted: an older build's later write reaches the v2 copy", + [made, kept, ob("write", v1=2, pub="import", base=2)], "REJECTED"), + ("planted: converted with no request", + [made, ob("list", v1=1, pub="import", base=1), ob("open", pub="import", base=1, ans="opened")], "REJECTED"), + ("planted: the v1 folder stays though no delete was refused", + [made, ob("open", v1=1, pub="import", base=1, ans="opened")], "REJECTED"), + ("planted: a leftover an older build changed is deleted", + [made, kept, ob("write", v1=2, pub="import", base=1), ob("open", pub="import", base=1, ans="opened")], + "REJECTED"), + ("planted: the v1 folder deleted before its copy was published", + [made, ob("crash", dirty=True)], "REJECTED"), + ] + bad = 0 + root = Path(os.environ.get("TMPDIR", "/tmp")) / f"check-conversion-selftest-{os.getpid()}" + for n, (label, observations, want) in enumerate(cases, 1): + try: + got = verify({"version": 1, "ids": ids, "observations": observations}, root / str(n)) + verdict = got["verdict"] + except Inconclusive as why: + verdict = f"INCONCLUSIVE ({why})" + ok = verdict == want + bad += not ok + print(f"{'ok ' if ok else 'FAIL'} {label}: {verdict}, wanted {want}") + print(f"selftest: {len(cases) - bad}/{len(cases)} verdicts as required") + if not bad: + shutil.rmtree(root, ignore_errors=True) + return 1 if bad else 0 + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--request", type=Path) + parser.add_argument("--report", type=Path) + parser.add_argument("--selftest", action="store_true") + args = parser.parse_args() + if args.selftest: + return selftest() + if not args.request or not args.report: + parser.error("--request and --report are required") + report = args.report.resolve() + report.mkdir(parents=True, exist_ok=False) + try: + raw = args.request.read_bytes() + (report / "request.json").write_bytes(raw) + result = verify(json.loads(raw), report) + except Inconclusive as why: + result = {"verdict": "INCONCLUSIVE", "detail": str(why)} + except (OSError, ValueError, subprocess.SubprocessError) as error: + result = {"verdict": "TOOL_ERROR", "detail": str(error)} + result["version"] = 1 + result["report"] = str(report) + (report / "verdict.json").write_text(json.dumps(result, indent=2) + "\n") + print(json.dumps(result)) + return EXIT[result["verdict"]] + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/src/core/session_manager/tla/trace/check_saved_logs.py b/src/core/session_manager/tla/trace/check_saved_logs.py new file mode 100644 index 000000000..ae842f176 --- /dev/null +++ b/src/core/session_manager/tla/trace/check_saved_logs.py @@ -0,0 +1,298 @@ +#!/usr/bin/env python3 +"""Checks logs fx saved against TurnLifecycle.tla and Subagents.tla. + +usage: check_saved_logs.py ROOT... each ROOT holds session folders + ({id}/log.jsonl), as ~/.fx/sessions/v2 + check_saved_logs.py --selftest planted logs: each must get its verdict + +JOBS=N runs N TLC checks at once (default 6). + +Every session's log is checked against TurnLifecycle (TurnLifecycleLog.tla); +a log with child lines is also checked against Subagents (SubagentsLog.tla), +with each child's log existence read at the end. Only the disk is known, so +TLC searches the process state in between (see the two wrappers). A torn +tail is left out, as the manager reads it. A log that does not parse is +reported as unreadable, not checked. Exit 0 when every readable log is +accepted. +""" +import hashlib +import json +import os +import pwd +import re +import shutil +import subprocess +import sys +import tempfile +from concurrent.futures import ThreadPoolExecutor + +HERE = os.path.dirname(os.path.abspath(__file__)) +TLA = os.path.dirname(HERE) +JAVA = os.environ.get("JAVA", "/opt/homebrew/opt/openjdk/bin/java") +# The account's home, not $HOME: drivers run fx under a disposable HOME. +JAR = os.environ.get("TLA_JAR", os.path.join(pwd.getpwuid(os.getuid()).pw_dir, ".local/share/tla/tla2tools.jar")) + +TURN_KINDS = { + "session_created": "created", + "set": "set", + "turn_started": "start", + "item": "item", + "compacted": "compacted", + "turn_committed": "commit", + "turn_interrupted": "interrupt", + "closed": "closed", +} +CHILD_KINDS = {"child_spawned", "child_finished"} +OUTSIDE = {"snapshot"} | CHILD_KINDS + + +class Unreadable(Exception): + pass + + +def read_lines(path, raw=False): + """The log's whole lines; a torn tail is left out. With `raw`, each line + comes with its exact bytes.""" + data = open(path, "rb").read() + end = data.rfind(b"\n") + out = [] + for n, line in enumerate(data[: end + 1].split(b"\n")[:-1], 1): + try: + value = json.loads(line) + except ValueError: + raise Unreadable(f"line {n} is not JSON") + out.append((value, line) if raw else value) + return out + + +def fork_records(lines, upto=None): + """[k, h] records of lines 2.. (those with seq <= `upto`), snapshots left + out: a fork encodes its copied snapshots again.""" + out = [] + for value, line in lines[1:]: + if upto is not None and value.get("seq", 0) > upto: + break + kind = value.get("kind") + if kind == "snapshot": + continue + out.append({"k": TURN_KINDS.get(kind, kind), "h": hashlib.sha256(line).hexdigest()[:16]}) + return out + + +def fork_target(lines, root): + """For a fork, its copied lines and its source's lines; else None.""" + origin = lines[0][0].get("forked_from") + if not origin: + return None + source = os.path.join(root, origin["id"], "log.jsonl") + if not os.path.isfile(source): + raise Unreadable(f"fork source {origin['id']} is not in this root") + return fork_records(lines, origin["seq"]), fork_records(read_lines(source, raw=True)) + + +def turn_target(lines): + target = [] + for n, line in enumerate(lines, 1): + kind = line.get("kind") + if kind in OUTSIDE: + continue + if kind not in TURN_KINDS: + raise Unreadable(f"line {n} has unknown kind {kind!r}") + target.append(TURN_KINDS[kind]) + return target + + +def child_target(lines, root): + names, works, target = {}, {}, [] + for line in lines: + kind = line.get("kind") + if kind not in CHILD_KINDS: + continue + child = line["child"] + c = names.setdefault(child, f"c{len(names) + 1}") + if kind == "child_spawned": + works[c] = works.get(c, 0) + 1 + target.append({"k": "spawned", "c": c, "w": works[c], "o": "none"}) + else: + target.append({"k": "finished", "c": c, "w": works.get(c, 0), "o": line["outcome"]}) + final = {c: os.path.exists(os.path.join(root, child, "log.jsonl")) for child, c in names.items()} + return target, final + + +def tla_str(s): + return '"' + s.replace("\\", "\\\\").replace('"', '\\"') + '"' + + +def tla_record(r): + return "[" + ", ".join(f"{k} |-> {tla_str(v) if isinstance(v, str) else v}" for k, v in r.items()) + "]" + + +def run_tlc(module, spec_files, generated, cfg, invariant="NotWritten"): + work = tempfile.mkdtemp(prefix="fx-log-check-") + try: + for f in spec_files: + shutil.copy(f, work) + for name, text in generated.items(): + open(os.path.join(work, name), "w").write(text) + open(os.path.join(work, module + ".cfg"), "w").write(cfg) + proc = subprocess.run( + # Its own java.io.tmpdir: TLC unpacks its standard modules there, + # and parallel runs sharing one folder read each other's + # half-written files. + [JAVA, "-XX:+UseParallelGC", f"-Djava.io.tmpdir={work}", "-cp", JAR, "tlc2.TLC", "-workers", "1", "-deadlock", + "-metadir", os.path.join(work, "states"), "-config", module + ".cfg", module], + cwd=work, capture_output=True, text=True, timeout=600, + ) + out = proc.stdout + proc.stderr + matched = max([int(m) for m in re.findall(r'"matched_lines", (\d+)', out)] or [0]) + if f"Invariant {invariant} is violated" in out: + return "ACCEPTED", matched + if "No error has been found" in out: + return "REJECTED", matched + return "TOOL ERROR", out[-600:] + finally: + shutil.rmtree(work, ignore_errors=True) + + +def check_turns(target): + body = ", ".join(tla_str(k) for k in target) + saved = f"---- MODULE SavedLog ----\nTarget == <<{body}>>\n====\n" + cfg = (f"CONSTANT MaxLen = {len(target) + 2}\nSPECIFICATION LogSpec\n" + "INVARIANT NotWritten\nCONSTRAINT Progress\n") + specs = [os.path.join(TLA, "TurnLifecycle.tla"), os.path.join(HERE, "TurnLifecycleLog.tla")] + return run_tlc("TurnLifecycleLog", specs, {"SavedLog.tla": saved}, cfg) + + +def check_children(target, final): + children = sorted(final) + body = ", ".join(tla_record(r) for r in target) + fin = " @@ ".join(f"{tla_str(c)} :> {'TRUE' if final[c] else 'FALSE'}" for c in children) + saved = (f"---- MODULE SavedChildren ----\nEXTENDS TLC\nTarget == <<{body}>>\n" + f"FinalChildLog == {fin}\n====\n") + max_work = max([r["w"] for r in target] or [1]) + cfg = ("CONSTANTS Children = {" + ", ".join(tla_str(c) for c in children) + "}\n" + f" MaxWork = {max_work}\nSPECIFICATION LogSpec\n" + "INVARIANT NotWritten\nCONSTRAINT Progress\n") + specs = [os.path.join(TLA, "Subagents.tla"), os.path.join(HERE, "SubagentsLog.tla")] + return run_tlc("SubagentsLog", specs, {"SavedChildren.tla": saved}, cfg) + + +def check_fork(copied, source): + def seq(rs): + return ", ".join(tla_record(r) for r in rs) + saved = f"---- MODULE SavedFork ----\nCopied == <<{seq(copied)}>>\nSource == <<{seq(source)}>>\n====\n" + cfg = "SPECIFICATION LogSpec\nINVARIANT NotWritten\n" + verdict, _ = run_tlc("ForkLog", [os.path.join(HERE, "ForkLog.tla")], {"SavedFork.tla": saved}, cfg) + return verdict, len(copied) + + +def jobs_for(roots): + jobs = [] + for root in roots: + for sid in sorted(os.listdir(root)): + path = os.path.join(root, sid, "log.jsonl") + if not os.path.isfile(path): + continue + name = f"{os.path.basename(os.path.dirname(root.rstrip('/')))}/{sid}" + try: + raw = read_lines(path, raw=True) + lines = [value for value, _ in raw] + turns = turn_target(lines) + children = child_target(lines, root) + fork = fork_target(raw, root) + except Unreadable as err: + jobs.append((name, "unreadable", str(err))) + continue + jobs.append((name, "turns", turns)) + if children[0]: + jobs.append((name, "children", children)) + if fork: + jobs.append((name, "fork", fork)) + return jobs + + +def run(job): + name, what, arg = job + if what == "unreadable": + return name, what, "UNREADABLE", arg + if what == "turns": + verdict, detail = check_turns(arg) + elif what == "fork": + verdict, detail = check_fork(*arg) + else: + verdict, detail = check_children(*arg) + size = len(arg) if what == "turns" else len(arg[0]) + return name, what, verdict, f"{detail}/{size} lines" if verdict != "TOOL ERROR" else detail + + +def selftest(): + cases = [ + ("turns: a committed turn, then close", "turns", ["created", "set", "start", "item", "commit", "closed"], "ACCEPTED"), + ("turns: crash, reopen interrupts, next turn", "turns", ["created", "start", "item", "interrupt", "start", "commit"], "ACCEPTED"), + ("turns: close interrupts the open turn", "turns", ["created", "start", "interrupt", "closed", "start", "commit"], "ACCEPTED"), + ("planted: item outside a turn", "turns", ["created", "item"], "REJECTED"), + ("planted: two open turns", "turns", ["created", "start", "start"], "REJECTED"), + ("planted: closed inside a turn", "turns", ["created", "start", "closed"], "REJECTED"), + ("planted: commit without a start", "turns", ["created", "set", "commit"], "REJECTED"), + ("children: spawn, finish ok", + "children", ([{"k": "spawned", "c": "c1", "w": 1, "o": "none"}, {"k": "finished", "c": "c1", "w": 1, "o": "ok"}], {"c1": True}), "ACCEPTED"), + ("children: lost, then a fresh start (D33)", + "children", ([{"k": "spawned", "c": "c1", "w": 1, "o": "none"}, {"k": "finished", "c": "c1", "w": 1, "o": "lost"}, + {"k": "spawned", "c": "c1", "w": 2, "o": "none"}, {"k": "finished", "c": "c1", "w": 2, "o": "ok"}], {"c1": True}), "ACCEPTED"), + ("planted: lost, yet the child has a log", + "children", ([{"k": "spawned", "c": "c1", "w": 1, "o": "none"}, {"k": "finished", "c": "c1", "w": 1, "o": "lost"}], {"c1": True}), "REJECTED"), + ("planted: interrupted, yet the child has no log", + "children", ([{"k": "spawned", "c": "c1", "w": 1, "o": "none"}, {"k": "finished", "c": "c1", "w": 1, "o": "interrupted"}], {"c1": False}), "REJECTED"), + ("planted: a finish with no spawn", + "children", ([{"k": "finished", "c": "c1", "w": 0, "o": "ok"}], {"c1": False}), "REJECTED"), + ] + def rec(k, h): + return {"k": k, "h": h} + src = [rec("set", "p"), rec("start", "a"), rec("item", "b"), rec("commit", "c"), rec("start", "d"), rec("commit", "e")] + cases += [ + ("fork: the source's lines to the end of turn 1", "fork", (src[:4], src), "ACCEPTED"), + ("fork: before the first turn", "fork", (src[:1], src), "ACCEPTED"), + ("planted: a copied line differs from the source's", "fork", (src[:2] + [rec("item", "x"), src[3]], src), "REJECTED"), + ("planted: the copy ends inside a turn", "fork", (src[:3], src), "REJECTED"), + ] + bad = 0 + + def verdict_of(c): + if c[1] == "turns": + return check_turns(c[2]) + if c[1] == "fork": + return check_fork(*c[2]) + return check_children(*c[2]) + with ThreadPoolExecutor(int(os.environ.get("JOBS", "6"))) as pool: + results = pool.map(lambda c: (c, verdict_of(c)), cases) + for (label, _, _, want), (verdict, detail) in results: + ok = verdict == want + bad += not ok + print(f"{'ok ' if ok else 'FAIL'} {label}: {verdict} (matched {detail}), wanted {want}") + print(f"selftest: {len(cases) - bad}/{len(cases)} verdicts as required") + return 1 if bad else 0 + + +def main(argv): + if argv[1:] == ["--selftest"]: + return selftest() + if len(argv) < 2: + print(__doc__) + return 2 + jobs = jobs_for(argv[1:]) + counts = {} + failed = 0 + with ThreadPoolExecutor(int(os.environ.get("JOBS", "6"))) as pool: + for name, what, verdict, detail in pool.map(run, jobs): + counts[(what, verdict)] = counts.get((what, verdict), 0) + 1 + if verdict not in ("ACCEPTED", "UNREADABLE"): + failed += 1 + if verdict != "ACCEPTED": + print(f"{verdict:10} {what:9} {name}: {detail}") + for (what, verdict), n in sorted(counts.items()): + print(f"{what:9} {verdict:10} {n}") + return 1 if failed else 0 + + +if __name__ == "__main__": + sys.exit(main(sys.argv)) diff --git a/src/core/session_manager/tla/trace/check_wiring_traces.py b/src/core/session_manager/tla/trace/check_wiring_traces.py new file mode 100644 index 000000000..83cfd0cb0 --- /dev/null +++ b/src/core/session_manager/tla/trace/check_wiring_traces.py @@ -0,0 +1,155 @@ +#!/usr/bin/env python3 +"""Checks fx's `wiring` trace lines against Wiring.tla (WiringTrace.tla). + +usage: check_wiring_traces.py FILE... trace logs written with FX_TRACE=1, + FX_TRACE_SCOPES=wiring, FX_TRACE_LOG + check_wiring_traces.py --selftest + +JOBS=N runs N TLC checks at once (default 6). + +The adapter writes one line per step (`action=... session=... pid=...`). +Each process's first store open and last close become Start and Exit; a +process whose lines stop without Exit gets a Crash. Wiring.tla models one fx +process at a time, so a file whose processes overlap is skipped and named. +Exit 0 when every checked trace is accepted. +""" +import os +import re +import sys +from concurrent.futures import ThreadPoolExecutor + +sys.path.insert(0, os.path.dirname(os.path.abspath(__file__))) +from check_saved_logs import HERE, TLA, run_tlc, tla_str # noqa: E402 + +LINE = re.compile(r"^\d+ \[wiring\] action=(\w+) session=(\S+)(?: end=(\w+))? pid=(-?\d+)$") + + +class Skip(Exception): + pass + + +def parse(path): + events = [] + for raw in open(path, errors="replace"): + m = LINE.match(raw.rstrip("\n")) + if m: + events.append((int(m.group(4)), m.group(1), m.group(2), m.group(3))) + return events + + +def steps_for(events): + """The Wiring steps, and the sessions they name.""" + order, seen = [], set() + for pid, *_ in events: + if pid in seen and order[-1] != pid: + raise Skip("processes overlap") + if pid not in seen: + seen.add(pid) + order.append(pid) + names, steps = {}, [] + for pid in order: + depth = 0 + mine = [e for e in events if e[0] == pid] + # ACP opens its store before tracing starts: its first line is + # then a later step, and the process started just before it. + if mine[0][1] != "StoreOpen": + steps.append(("Start", "none", "none")) + depth = 1 + for p, action, session, end in mine: + if action == "StoreOpen": + if depth == 0: + steps.append(("Start", "none", "none")) + depth += 1 + elif action == "StoreClose": + depth -= 1 + if depth == 0: + steps.append(("Exit", "none", "none")) + elif depth == 0: + raise Skip(f"{action} outside an open store") + elif action in ("Open", "Close", "Fork"): + steps.append((action, names.setdefault(session, f"s{len(names) + 1}"), "none")) + elif action == "EndTurn": + steps.append(("EndTurn", "none", end)) + else: + steps.append((action, "none", "none")) + if depth > 0: + steps.append(("Crash", "none", "none")) + return steps, sorted(names.values()) or ["s1"] + + +def check(steps, sessions): + body = ", ".join(f"[a |-> {tla_str(a)}, s |-> {tla_str(s)}, e |-> {tla_str(e)}]" for a, s, e in steps) + data = f"---- MODULE WiringData ----\nTrace == <<{body}>>\n====\n" + cfg = ("CONSTANT Sessions = {" + ", ".join(tla_str(s) for s in sessions) + "}\n" + "SPECIFICATION TraceSpec\nINVARIANT NotDone\nCONSTRAINT Progress\n") + specs = [os.path.join(TLA, "Wiring.tla"), os.path.join(HERE, "WiringTrace.tla")] + verdict, detail = run_tlc("WiringTrace", specs, {"WiringData.tla": data}, cfg, invariant="NotDone") + return verdict, detail + + +def run(path): + events = parse(path) + if not events: + return path, "EMPTY", "no wiring lines" + try: + steps, sessions = steps_for(events) + except Skip as why: + return path, "SKIPPED", str(why) + verdict, detail = check(steps, sessions) + if verdict == "REJECTED": + step = steps[detail] if detail < len(steps) else None + return path, verdict, f"steps 1..{detail} match; step {detail + 1} {step} is not allowed ({len(steps)} steps)" + return path, verdict, f"{detail}/{len(steps)} steps" if verdict == "ACCEPTED" else detail + + +def selftest(): + S, O, B, C, X = ("Start", "none", "none"), ("Open", "s1", "none"), ("BeginTurn", "none", "none"), ("Close", "s1", "none"), ("Exit", "none", "none") + O2, C2 = ("Open", "s2", "none"), ("Close", "s2", "none") + commit, crash = ("EndTurn", "none", "commit"), ("Crash", "none", "none") + spawn, done = ("Spawn", "none", "none"), ("ChildDone", "none", "none") + cases = [ + ("a turn, then close and exit", [S, O, B, commit, C, X], ["s1"], "ACCEPTED"), + ("a crash mid-turn, then a resume", [S, O, B, crash, S, O, B, commit, C, X], ["s1"], "ACCEPTED"), + ("a child inside a turn", [S, O, B, spawn, done, commit, C, X], ["s1"], "ACCEPTED"), + ("planted: close while a child runs", [S, O, B, spawn, C], ["s1"], "REJECTED"), + ("a switch: the next session opens before the current closes (D41)", [S, O, B, commit, O2, C, B, commit, C2, X], ["s1", "s2"], "ACCEPTED"), + ("a failed switch closes the next session and keeps the current", [S, O, O2, C2, B, commit, C, X], ["s1", "s2"], "ACCEPTED"), + ("planted: a third open while a switch is pending", [S, O, O2, ("Open", "s3", "none")], ["s1", "s2", "s3"], "REJECTED"), + ("planted: a turn starts while a switch is pending", [S, O, O2, B], ["s1", "s2"], "REJECTED"), + ("planted: a turn ends that never began", [S, O, commit], ["s1"], "REJECTED"), + ("planted: exit with a session open", [S, O, X], ["s1"], "REJECTED"), + ("planted: a child done after its parent closed", [S, O, B, spawn, commit, C, done], ["s1"], "REJECTED"), + ("a fork becomes the next session, and closing the source switches to it (D58)", [S, O, B, commit, ("Fork", "s2", "none"), C, B, commit, C2, X], ["s1", "s2"], "ACCEPTED"), + ("planted: a fork while a turn is open", [S, O, B, ("Fork", "s2", "none")], ["s1", "s2"], "REJECTED"), + ("planted: a fork into a session that exists", [S, O2, C2, O, ("Fork", "s2", "none")], ["s1", "s2"], "REJECTED"), + ] + bad = 0 + with ThreadPoolExecutor(int(os.environ.get("JOBS", "6"))) as pool: + for (label, _, _, want), (verdict, detail) in zip(cases, pool.map(lambda c: check(c[1], c[2]), cases)): + ok = verdict == want + bad += not ok + print(f"{'ok ' if ok else 'FAIL'} {label}: {verdict} (matched {detail}), wanted {want}") + print(f"selftest: {len(cases) - bad}/{len(cases)} verdicts as required") + return 1 if bad else 0 + + +def main(argv): + if argv[1:] == ["--selftest"]: + return selftest() + if len(argv) < 2: + print(__doc__) + return 2 + counts, failed = {}, 0 + with ThreadPoolExecutor(int(os.environ.get("JOBS", "6"))) as pool: + for path, verdict, detail in pool.map(run, argv[1:]): + counts[verdict] = counts.get(verdict, 0) + 1 + failed += verdict in ("REJECTED", "TOOL ERROR") + if verdict != "ACCEPTED": + print(f"{verdict:10} {path}: {detail}") + for verdict, n in sorted(counts.items()): + print(f"{verdict:10} {n}") + return 1 if failed else 0 + + +if __name__ == "__main__": + sys.exit(main(sys.argv)) diff --git a/src/core/session_manager/tla/trace/selftest.sh b/src/core/session_manager/tla/trace/selftest.sh new file mode 100755 index 000000000..437b8ffc8 --- /dev/null +++ b/src/core/session_manager/tla/trace/selftest.sh @@ -0,0 +1,42 @@ +#!/bin/sh +# Prove the trace tooling can both accept and reject. +# +# Runs the Python stand-in log three ways and checks the verdicts: +# correct implementation -> ACCEPTED +# recovery keeps a torn tail (bug) -> REJECTED at step 8 (the Recover) +# one field changed in a good trace -> REJECTED at step 5 (acked 2 -> 3) +set -eu + +here=$(cd "$(dirname "$0")" && pwd) +tmp=$(mktemp -d "${TMPDIR:-/tmp}/session-manager-selftest.XXXXXX") +trap 'rm -rf "$tmp"' EXIT + +python3 "$here/stand_in_log.py" "$tmp/good.log" "$tmp/good.ndjson" +python3 "$here/stand_in_log.py" "$tmp/bad.log" "$tmp/bad.ndjson" keep_torn_tail +sed '5s/"acked": 2/"acked": 3/' "$tmp/good.ndjson" > "$tmp/tampered.ndjson" + +failures=0 +expect() { # name trace wanted_exit wanted_text + set +e + got=$("$here/validate.sh" SessionLog "$2" 2>&1) + code=$? + set -e + if [ "$code" -eq "$3" ] && printf '%s' "$got" | grep -q "$4"; then + echo "ok $1: $(printf '%s' "$got" | head -1)" + else + echo "FAIL $1: exit $code, wanted $3 and '$4'" + printf '%s\n' "$got" | sed 's/^/ /' + failures=$((failures + 1)) + fi +} + +expect "correct implementation" "$tmp/good.ndjson" 0 "ACCEPTED" +expect "recovery keeps a torn tail" "$tmp/bad.ndjson" 1 "step 8 of" +expect "tampered acked field" "$tmp/tampered.ndjson" 1 "step 5 of" + +if [ "$failures" -eq 0 ]; then + echo "trace selftest passed" + exit 0 +fi +echo "trace selftest failed: $failures case(s)" +exit 1 diff --git a/src/core/session_manager/tla/trace/stand_in_log.py b/src/core/session_manager/tla/trace/stand_in_log.py new file mode 100755 index 000000000..32ad61be4 --- /dev/null +++ b/src/core/session_manager/tla/trace/stand_in_log.py @@ -0,0 +1,115 @@ +#!/usr/bin/env python3 +"""A small stand-in for the L1 log, used only to self-test the trace tooling. + +It writes a real file with O_APPEND, fsync and simulated crashes, and emits +one trace line per step. The state in each line is read back from the actual +file bytes, the same way the Zig trace hook must do it. Not a design +reference for the Zig code. + +usage: stand_in_log.py LOG_PATH TRACE_PATH [keep_torn_tail] +""" +import json +import os +import sys + + +class Log: + def __init__(self, path, trace, bug=None): + self.path, self.trace, self.bug = path, trace, bug + self.fd = os.open(path, os.O_WRONLY | os.O_CREAT | os.O_APPEND, 0o600) + self.durable = self.acked = 0 + self.status, self.pending, self.seq = "open", None, 0 + + def disk(self): + """Abstraction function: file bytes -> (line count, tail done, seqs).""" + with open(self.path, "rb") as f: + data = f.read() + torn = len(data) > 0 and not data.endswith(b"\n") + complete = data.split(b"\n")[: data.count(b"\n")] + seqs = [] + for raw in complete: + try: + seqs.append(int(json.loads(raw)["seq"])) + except (ValueError, KeyError, TypeError): + seqs.append(-1) + return len(complete) + (1 if torn else 0), not torn, seqs + + def emit(self, event): + n, done, seqs = self.disk() + self.trace.write(json.dumps({ + "event": event, "log_len": n, "tail_done": done, "seqs": seqs, + "durable": self.durable, "acked": self.acked, "status": self.status, + }) + "\n") + + def begin_write(self): + """First half of one write(): the newline is not on disk yet.""" + self.seq += 1 + line = json.dumps({"v": 1, "seq": self.seq, "kind": "item"}).encode() + b"\n" + half = len(line) // 2 + os.write(self.fd, line[:half]) + self.pending = line[half:] + self.status = "writing" + self.emit("BeginWrite") + + def finish_write(self): + os.write(self.fd, self.pending) + self.pending = None + self.status = "open" + self.emit("FinishWrite") + + def fsync(self): + os.fsync(self.fd) + self.durable = self.acked = self.disk()[0] + self.emit("Fsync") + + def process_crash(self): + os.close(self.fd) + self.status = "down" + self.emit("ProcessCrash") + + def power_loss(self, keep, tear): + """Simulated: keep `keep` complete lines (at least durable), then tear + the last kept line if it was never fsynced.""" + if self.status != "down": + os.close(self.fd) + with open(self.path, "rb") as f: + data = f.read() + kept = b"".join(p + b"\n" for p in data.split(b"\n")[:keep]) + if tear and keep > self.durable: + kept = kept[:-3] + with open(self.path, "wb") as f: + f.write(kept) + self.status = "down" + self.emit("PowerLoss") + + def recover(self): + """open(.resume): cut a torn tail, fsync, reopen for append.""" + with open(self.path, "rb") as f: + data = f.read() + if data and not data.endswith(b"\n") and self.bug != "keep_torn_tail": + data = data[: data.rfind(b"\n") + 1] + with open(self.path, "wb") as f: + f.write(data) + self.fd = os.open(self.path, os.O_WRONLY | os.O_APPEND) + os.fsync(self.fd) + self.durable = self.disk()[0] + self.seq = data.count(b"\n") + self.status = "open" + self.emit("Recover") + + +def scenario(path, trace_path, bug=None): + with open(trace_path, "w") as trace: + log = Log(path, trace, bug) + log.begin_write(); log.finish_write() + log.begin_write(); log.finish_write(); log.fsync() # 2 acknowledged lines + log.begin_write(); log.process_crash() # torn 3rd line + log.recover() # must cut it + log.begin_write(); log.finish_write() # new 3rd line, not fsynced + log.power_loss(keep=3, tear=True) # machine crash tears it + log.recover() + log.begin_write(); log.finish_write(); log.fsync() + + +if __name__ == "__main__": + scenario(sys.argv[1], sys.argv[2], sys.argv[3] if len(sys.argv) > 3 else None) diff --git a/src/core/session_manager/tla/trace/to_tla.py b/src/core/session_manager/tla/trace/to_tla.py new file mode 100755 index 000000000..5f2e2ea08 --- /dev/null +++ b/src/core/session_manager/tla/trace/to_tla.py @@ -0,0 +1,59 @@ +#!/usr/bin/env python3 +"""Convert an implementation trace (JSON lines) into the TLA+ module TraceData. + +usage: to_tla.py trace.ndjson TraceData.tla + +Each JSON line becomes one record in `Trace == << ... >>`. Values map as: + true/false -> TRUE/FALSE, integers -> integers, strings -> strings, + lists -> sequences, objects -> records, {"$set": [...]} -> a set. +Floats and null are rejected: the specs have no use for them. +""" +import json +import sys + + +def value(v): + if isinstance(v, bool): + return "TRUE" if v else "FALSE" + if isinstance(v, int): + return str(v) + if isinstance(v, str): + return json.dumps(v) + if isinstance(v, list): + return "<<" + ", ".join(value(x) for x in v) + ">>" + if isinstance(v, dict): + if set(v) == {"$set"}: + return "{" + ", ".join(value(x) for x in v["$set"]) + "}" + if not v: + raise ValueError("empty objects have no TLA+ record form") + return "[" + ", ".join(f"{k} |-> {value(x)}" for k, x in v.items()) + "]" + raise ValueError(f"unsupported trace value: {v!r}") + + +def main(): + if len(sys.argv) != 3: + print(__doc__.strip().splitlines()[2], file=sys.stderr) + return 2 + records = [] + with open(sys.argv[1]) as trace: + for number, line in enumerate(trace, start=1): + if not line.strip(): + continue + try: + records.append(value(json.loads(line))) + except (ValueError, json.JSONDecodeError) as err: + print(f"trace line {number}: {err}", file=sys.stderr) + return 2 + body = ",\n ".join(records) + with open(sys.argv[2], "w") as out: + out.write("---- MODULE TraceData ----\n") + # Integers gives negative literals (for example a seq of -1 for a + # line the implementation could not parse). + out.write("EXTENDS Integers\n") + out.write(f"Trace == <<\n {body}\n>>\n" if records else "Trace == <<>>\n") + out.write("====\n") + return 0 + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/src/core/session_manager/tla/trace/validate.sh b/src/core/session_manager/tla/trace/validate.sh new file mode 100755 index 000000000..468790f26 --- /dev/null +++ b/src/core/session_manager/tla/trace/validate.sh @@ -0,0 +1,79 @@ +#!/bin/sh +# Check that an implementation trace is a behavior of a spec. +# +# usage: ./validate.sh SPEC trace.ndjson +# SPEC is a spec with a trace wrapper here, for example SessionLog. +# Needs ../SPEC.tla, ./SPECTrace.tla and ./SPECTrace.cfg. +# +# Exit codes: 0 accepted, 1 rejected (prints the first step the spec does +# not allow), 2 tool or usage error. +set -u + +if [ "$#" -ne 2 ]; then + echo "usage: $0 SPEC trace.ndjson" >&2 + exit 2 +fi +spec=$1 +here=$(cd "$(dirname "$0")" && pwd) +trace=$(cd "$(dirname "$2")" && pwd)/$(basename "$2") + +for f in "$here/../$spec.tla" "$here/${spec}Trace.tla" "$here/${spec}Trace.cfg" "$trace"; do + if [ ! -f "$f" ]; then + echo "missing $f" >&2 + exit 2 + fi +done + +jar="${TLA2TOOLS_JAR:-$HOME/.local/share/tla/tla2tools.jar}" +java="" +for candidate in \ + "${JAVA_HOME:+$JAVA_HOME/bin/java}" \ + /opt/homebrew/opt/openjdk/bin/java \ + /usr/local/opt/openjdk/bin/java \ + "$(command -v java 2>/dev/null || true)"; do + if [ -n "$candidate" ] && [ -x "$candidate" ] && "$candidate" -version >/dev/null 2>&1; then + java="$candidate" + break + fi +done +if [ -z "$java" ] || [ ! -f "$jar" ]; then + echo "needs a Java runtime and tla2tools.jar (see ../check.sh)" >&2 + exit 2 +fi + +work=$(mktemp -d "${TMPDIR:-/tmp}/session-manager-trace.XXXXXX") +trap 'rm -rf "$work"' EXIT +cp "$here/../$spec.tla" "$here/${spec}Trace.tla" "$here/${spec}Trace.cfg" "$work/" +python3 "$here/to_tla.py" "$trace" "$work/TraceData.tla" || exit 2 +steps=$(grep -c . "$trace" || true) + +# One worker: the progress register (TLCSet/TLCGet) is per worker. TLC +# unpacks its standard modules into java.io.tmpdir; a private one lets +# several checks run at once. +mkdir "$work/java-tmp" +out=$(cd "$work" && "$java" -Djava.io.tmpdir="$work/java-tmp" -cp "$jar" tlc2.TLC -deadlock -workers 1 -cleanup \ + -metadir "$work/states" -config "${spec}Trace.cfg" "${spec}Trace.tla" 2>&1) + +# Match with case, not a pipe into grep -q: grep exits at the first match +# and a large TLC output then fails printf with a broken pipe. +case $out in + *'Invariant TraceIncomplete is violated'*) verdict=accepted ;; + *'No error has been found'*) verdict=rejected ;; + *) verdict=unfinished ;; +esac + +if [ "$verdict" = accepted ]; then + echo "ACCEPTED: all $steps steps are a behavior of $spec" + exit 0 +fi +if [ "$verdict" = rejected ]; then + matched=$(printf '%s\n' "$out" | sed -n 's/.*"matched_lines", \([0-9]*\)>>.*/\1/p' | tail -1) + matched=${matched:-0} + bad=$((matched + 1)) + echo "REJECTED: steps 1..$matched match; step $bad of $steps is not allowed by $spec:" + sed -n "${bad}p" "$trace" + exit 1 +fi +printf '%s\n' "$out" | tail -15 +echo "TOOL ERROR: TLC did not finish the trace check" >&2 +exit 2 diff --git a/src/core/session_manager/trace.zig b/src/core/session_manager/trace.zig index ce21578f9..3da5cdd16 100644 --- a/src/core/session_manager/trace.zig +++ b/src/core/session_manager/trace.zig @@ -2,7 +2,7 @@ //! //! Each traced run writes `zig-out/traces/SPEC--CASE.ndjson`: one JSON line //! per spec action, named like the action, with one field per spec variable -//! (`docs/session-manager/tla/trace/README.md`). Fields that model the disk +//! (`tla/trace/README.md`). Fields that model the disk //! are read back from the real files after the step; fields that model //! memory come from the code's own state. //! diff --git a/src/core/subagent/tool_host.zig b/src/core/subagent/tool_host.zig index 6a4534001..8ab79add1 100644 --- a/src/core/subagent/tool_host.zig +++ b/src/core/subagent/tool_host.zig @@ -153,7 +153,7 @@ pub const Runtime = struct { /// A host over a v2 parent, whose children live in its log (D22). /// Borrows `children` and the callback contexts until deinit; the - /// parent stays open until then (`tla/Wiring.tla` + /// parent stays open until then (`src/core/session_manager/tla/Wiring.tla` /// ParentOutlivesChildren). pub fn createV2( alloc: Allocator, diff --git a/src/mcp/io/trace.zig b/src/mcp/io/trace.zig index 39e2e240a..784c47f25 100644 --- a/src/mcp/io/trace.zig +++ b/src/mcp/io/trace.zig @@ -1,4 +1,4 @@ -//! JSONL trace of core steps (docs/approach.md §6, format version 1). +//! JSONL trace of core steps (format version 1). //! //! The I/O layer writes one line per `step` call when tracing is on. The Bun //! bridge turns a trace into a TLA+ observation and asks TLC whether it is a diff --git a/src/mcp/mcp.zig b/src/mcp/mcp.zig index a2e6431f5..b78eb4139 100644 --- a/src/mcp/mcp.zig +++ b/src/mcp/mcp.zig @@ -1,7 +1,7 @@ //! MCPv2 module root and public API. //! //! Files under `src/mcp/` import only `std` and each other. The host passes in -//! `std.Io` and everything else through `host.zig`. See `docs/approach.md`. +//! `std.Io` and everything else through `host.zig`. const std = @import("std"); diff --git a/tests/e2e/sessions-v2.test.ts b/tests/e2e/sessions-v2.test.ts index 8064ce932..d527fb584 100644 --- a/tests/e2e/sessions-v2.test.ts +++ b/tests/e2e/sessions-v2.test.ts @@ -2025,9 +2025,9 @@ test("a crash while a named subagent works records it interrupted, and its next expect(JSON.parse(resumed.stdout).output).toBe("AFTER_LOST_DONE"); // The reopen recorded the started work as interrupted, as - // `tla/Subagents.tla` repairs a child with a log; the next message is new - // work for the same child. A child streams no pieces, so its log holds - // nothing of the lost work. + // `src/core/session_manager/tla/Subagents.tla` repairs a child with a + // log; the next message is new work for the same child. A child streams + // no pieces, so its log holds nothing of the lost work. const lines = childLines(fixture, id); expect(lines.map((line) => [line.kind, line.outcome ?? null])).toEqual([ ["child_spawned", null], ["child_finished", "interrupted"], ["child_spawned", null], ["child_finished", "ok"],