Saga Extractor

Saga Extractor

Cut a distributed transaction out of a monolith, and prove the compensations actually put the world back.

When six operations run inside one TransactionScope, rollback is a promise the database keeps. Split them across five services and the promise is gone, but the code that relied on it usually keeps its shape: a try/catch, a few "undo" calls written from memory, and an assumption that failure means an exception. It does not. Failure now means rejected or timed out, and those are not the same thing -- the second one is the source of nearly every bug in this repository.

This tool takes the operations, derives a saga from them, and then exhaustively explores every reachable execution -- every rejection, every timeout, every orchestrator crash within a budget -- looking for executions where the saga reports that it rolled back and did not.

What it does

Extraction. Given operations with a declared reversibility and their reads/writes, produce an ordering with the saga shape: compensatable work, then one pivot, then work guaranteed to succeed. It is a topological sort over data dependencies with a reversibility tie-break, and it says out loud where reordering cannot save you.

Checking. Breadth-first exploration of the reachable state space, with seven safety properties. Because the search is BFS, every counterexample it reports is the shortest path to that failure -- there is no shorter explanation.

Reporting. docs/results.md is generated by the code, and a test byte-compares it against a fresh render, so it cannot drift from what the checker actually does.

The properties

The first three are algebraic and cost nothing -- they hold or fail without any exploration. The last four need the state space.

Running it

.\test.ps1          # six stages: format, build, tests, report freshness, design mutations, secrets
.\demo.ps1          # the seven-version progression, narrated
dotnet run --project src/Sagas.Report -c Release            # regenerate docs/results.md
dotnet run --project src/Sagas.Report -c Release -- --stdout # print it instead

87 tests. docs/results.md is the substance of the project; this README is the map.

What the checker found

The interesting output of a project like this is not that it works, it is the list of things that were wrong before it did. Six of them are in docs/portfolio/04-bugs-the-checker-found.md; each one is a defect in the model that took a round of calibration to see, and each one corresponds to a mistake that is easy to make in a real orchestrator.

Two results are worth pulling out here.

The careful-sounding policy is the unsafe one. When a step times out, you do not know whether it ran. Skipping its compensation -- on the grounds that compensating something that never happened is itself a change -- reintroduces two dirty aborts into an otherwise flawless saga. Compensating anyway is safe, because "compensate unconditionally" and "compensations must be idempotent" are the same requirement viewed from two directions.

Two of the seven properties were dead. A test asks whether every property is reachable from some design. When it was first written the answer was no: nothing in the catalogue or the mutation set could violate DeclaredIdempotenceIsFalse or ReverseOrderDoesNotRecover. Both were real checks, correctly implemented, and one of them was fully written and never called from anywhere. They were found by a test whose entire purpose was to ask a question nobody asks.

What it does not do

One orchestrator, one saga instance. Two concurrent orders competing for the last unit of stock are not explored -- that is a real class of bug and it is out of scope, not solved.

Exhaustiveness is bounded by a crash budget, and docs/results.md shows that bound is not a formality: a defective saga gains new violations at budget 2 and again at budget 3. The honest summary of a clean run is "no counterexample exists with at most three crashes".

And it checks a design, not an implementation. It says that if the payment service's capture endpoint is idempotent, the saga is sound. It converts that from an unexamined assumption into a written, checkable claim, which is a real improvement and is not the same as verifying it.

See docs/known-limitations.md.

Layout

src/Sagas.Core/
  WorldState.cs       schema and immutable state vector
  Saga.cs             steps, kinds, shape rules
  Execution.cs        configuration, phases, checker options
  Checker.cs          BFS, properties, shortest counterexamples
  Catalogue.cs        one saga in seven versions
  Extractor.cs        transaction -> saga
  DesignMutations.cs  revert one fix at a time; inject two lies
  Report.cs           a document that refuses results without predictions
  Experiments.cs      every number in results.md
src/Sagas.Report/     CLI entry point
tests/Sagas.Tests/    87 tests
docs/adr/             five decisions and why
docs/portfolio/       the essays