Repository navigation
Conversation
Nothing bounded journal growth. A job that loops for weeks accumulates a row per step, every attempt reads all of them, and steps/2 grows with the job. map_children only helps for fan-out, not a long sequential run. Deleting rows is the obvious fix and the obvious way to corrupt a job: steps memoize by name, so a missing row makes step/4 run the body again. For a step that charged a card, that is the worst failure this library has. Two facts make the safe set decidable. A step's body is the only place its nested steps are requested, and a journaled step returns its memo without running its body. So every descendant of a journaled step is unreachable, and nothing else is. collapse_journal/1 drops exactly that set, transitively. Modelled before implementing, per verify/README.md. NestedCollapse.tla checks the complete state graph (24 states, depth 8) for NoStepRunsTwice and RemovedOnlyUnderPresentAncestor. The mutant drops the ordering guard — collapse before the parent commits, which is the natural implementation if you collapse eagerly while the body unwinds — and reaches a twice-run body in four states. Both are wired into verify/check.sh, which now proves five mutants fail. Implementation: a dynamic step-scope stack in the runner records each step's parent, so a helper called from inside a body nests correctly with no API change. Storage keeps it in a new nullable belay_steps.parent column, and both adapters compute the full descendant closure before deleting, so removing a child cannot hide its own children from the sweep. Migration 4, the first since 1.0. Additive and nullable: 2.1.x nodes keep working against a migrated database, so it is rollback-safe. The contract major stays 1, which is what postgres_schema_test now asserts. Spend accumulates on the job row rather than summing step rows, so budgets are untouched — there is a test for that specifically. What is lost is history: collapsed steps leave steps/2 and any replay fixture. Collapse inherits replay's determinism assumption, and the docs say so in all three places, pointing at mix belay.replay --check-determinism. 213 tests on Memory, 231 on PostgreSQL.
|
Extra verification, since this stack touches
So the cumulative runner changes across #6–#10 — duplicate detection, the request log, the step-scope stack, parent recording, version checks — do not move observable engine behaviour on any recorded scenario. Since both the traces and I did try to run the optional Full formal suite with the model checker: both canonical models verify, five mutants produce their expected counterexamples. |
ATTEST_BIN is an escript and runs under whatever escript is first on PATH. Attest pins a newer Erlang than Belay builds against, so loading its beams on the older VM fails with 'corrupt atom table' — which reads as a corrupt binary and is not one. It cost me a wrong diagnosis; the README now names it. Also corrects the mutant count (five, not four) and records that CI does not set ATTEST_BIN, so trace admission is a local step.
|
Correcting my previous comment: attest is not broken, and the trace-check now runs.
Full suite, end to end, on this branch: So all 60 recorded events of the real engine still satisfy Pushed a |
Stacked on #9. The nested-step design, done spec-first.
The problem, and why the obvious fix is dangerous
Nothing bounded journal growth. A job that loops for weeks accumulates a row per step, every attempt reads all of them, and
steps/2grows with the job.map_childrenonly helps for fan-out, not a long sequential run.Deleting rows is the obvious fix and the obvious way to corrupt a job. Steps memoize by name: a missing row makes
step/4see:noneand run the body again. For a step that charged a card, that is the worst failure this library has.The rule
Two facts make the safe set decidable:
So every descendant of a journaled step is unreachable, and nothing else is.
collapse_journal/1drops exactly that set, transitively.Modelled before implemented
verify/README.mdsays to model protocol changes before writing them, so I did that first.verify/nested_collapse/NestedCollapse.tlaexplores the complete state graph — 24 distinct states, depth 8, zero violations — forNoStepRunsTwiceandRemovedOnlyUnderPresentAncestor.The mutant is the part worth reading. It drops the ordering guard so children may be collapsed before the parent's journal write commits — which is the natural implementation if you collapse eagerly while the body unwinds. Checked against
NoStepRunsTwicealone, so what it proves is the consequence rather than a restatement of the rule:Four states from
Initto a repeated side effect. Both are wired intoverify/check.sh, which now proves five mutants fail rather than four.Implementation
A dynamic step-scope stack in the runner records each step's parent, so a helper function called from inside a body nests correctly with no API change. Storage keeps it in a new nullable
belay_steps.parent; both adapters compute the full descendant closure before deleting, so removing a child cannot hide its own children from the sweep.Migration — the first since 1.0
This is why it opens a 2.2.0 section rather than joining 2.1.0, which advertises no migration.
Migration 4 adds one nullable column. Additive, so 2.1.x nodes keep working against a migrated database and it is rollback-safe. The contract major stays 1 —
postgres_schema_testnow asserts[[4, 1]]and says why.Two properties I tested explicitly
Budgets are untouched. Spend accumulates on the job row rather than summing step rows, so dropping rows cannot move it. There is a test for exactly that, because it would be a quiet and nasty regression.
A retry after collapse does not re-run a collapsed body. Attempt 1 collapses then raises; attempt 2 must get
outerfrom the journal and never re-enter its body. That is the model's invariant, checked against the real engine.What it costs
History. Collapsed steps leave
steps/2and anymix belay.replayfixture. That is a real trade and the docs say so in all three places.It also inherits replay's determinism assumption: if a later attempt asks for a nested step name outside its parent, that row is gone and the body runs again.
mix belay.replay --check-determinismfrom #9 exists to find precisely that, and all three doc sites point at it.213 tests on Memory, 231 on PostgreSQL, both green; format and docs clean; full formal suite green. No version bump.