Repository navigation
test(journaling): specify Garnet range migration in Quint - #11502
Draft
ReubenBond wants to merge 20 commits into
Draft
ReubenBond wants to merge 20 commits into
ReubenBond wants to merge 20 commits into
Conversation
Contributor
There was a problem hiding this comment.
🟡 Changes recommended
The safety model excludes retry-history eviction and delayed installs across bucket reopenings.
2 open findings
What changed in this PR
This draft adds formal validation for Garnet journal range migration, building on #11501’s static partition routing.
Changes:
- Specifies migration safety, liveness, and seven fault-injection mutants in Quint.
- Adds automated simulation and scheduled exhaustive model checking.
- Documents reopen, coordinator, tombstone-retention, and reclamation rules.
Automated coverage results were unavailable. The supplied file list also includes the preceding stack’s provider and tests.
| File | Description |
|---|---|
| test/Extensions/Orleans.Journaling.Garnet.Tests/RangeMetaStoreTests.cs | Stacked MetaStore contract tests. |
| test/Extensions/Orleans.Journaling.Garnet.Tests/RangeMapTests.cs | Stacked map validation tests. |
| test/Extensions/Orleans.Journaling.Garnet.Tests/Orleans.Journaling.Garnet.Tests.csproj | Stacked test project configuration. |
| test/Extensions/Orleans.Journaling.Garnet.Tests/GarnetTestRouting.cs | Stacked routing helpers. |
| test/Extensions/Orleans.Journaling.Garnet.Tests/GarnetPartitionFixture.cs | Stacked partition fixture. |
| test/Extensions/Orleans.Journaling.Garnet.Tests/GarnetJournalSuiteTests.cs | Stacked shared journaling suites. |
| test/Extensions/Orleans.Journaling.Garnet.Tests/GarnetJournalStorageTests.cs | Stacked storage behavior tests. |
| test/Extensions/Orleans.Journaling.Garnet.Tests/GarnetJournalStorageOptionsTests.cs | Stacked configuration tests. |
| test/Extensions/Orleans.Journaling.Garnet.Tests/GarnetJournalRouterTests.cs | Stacked routing and retry tests. |
| test/Extensions/Orleans.Journaling.Garnet.Tests/GarnetJournalProtocolTests.cs | Stacked protocol and recovery tests. |
| test/Extensions/Orleans.Journaling.Garnet.Tests/GarnetJournalLatencyTests.cs | Stacked latency measurements. |
| test/Extensions/Orleans.Journaling.Garnet.Tests/GarnetJournalDurabilityTests.cs | Stacked process-kill durability tests. |
| test/Extensions/Orleans.Journaling.Garnet.Tests/GarnetDurableGrainTests.cs | Stacked multi-silo integration tests. |
| test/Extensions/Orleans.Journaling.Garnet.CrashHost/Program.cs | Stacked crash-test host. |
| test/Extensions/Orleans.Journaling.Garnet.CrashHost/Orleans.Journaling.Garnet.CrashHost.csproj | Stacked host project configuration. |
| src/Orleans.Journaling/Orleans.Journaling.csproj | Stacked provider internal access. |
| src/Garnet/Orleans.Journaling.Garnet/README.md | Stacked provider usage documentation. |
| src/Garnet/Orleans.Journaling.Garnet/Ranges/RangeMapJsonSerializer.cs | Stacked map serialization. |
| src/Garnet/Orleans.Journaling.Garnet/Ranges/RangeMap.cs | Stacked range and migration contracts. |
| src/Garnet/Orleans.Journaling.Garnet/Ranges/PartitionId.cs | Stacked partition identity. |
| src/Garnet/Orleans.Journaling.Garnet/Ranges/IRangeMetaStore.cs | Stacked MetaStore interface. |
| src/Garnet/Orleans.Journaling.Garnet/Ranges/InMemoryRangeMetaStore.cs | Stacked in-memory MetaStore. |
| src/Garnet/Orleans.Journaling.Garnet/Ranges/AzureBlobRangeMetaStore.cs | Stacked durable MetaStore. |
| src/Garnet/Orleans.Journaling.Garnet/Procedures/GarnetJournalProtocol.cs | Stacked protocol and retry-history constants. |
| src/Garnet/Orleans.Journaling.Garnet/Orleans.Journaling.Garnet.csproj | Stacked provider packaging. |
| src/Garnet/Orleans.Journaling.Garnet/GarnetJournalStorageProvider.cs | Stacked provider lifecycle and catalog. |
| src/Garnet/Orleans.Journaling.Garnet/GarnetJournalStorageOptionsValidator.cs | Stacked option validation. |
| src/Garnet/Orleans.Journaling.Garnet/GarnetJournalStorageOptions.cs | Stacked provider options. |
| src/Garnet/Orleans.Journaling.Garnet/GarnetJournalStorageHostingExtensions.cs | Stacked hosting registration. |
| src/Garnet/Orleans.Journaling.Garnet/GarnetJournalStorage.cs | Stacked journal operations. |
| src/Garnet/Orleans.Journaling.Garnet/GarnetJournalRouter.cs | Stacked partition routing. |
| src/Garnet/Orleans.Journaling.Garnet/GarnetJournalPartitionManager.cs | Stacked partition initialization. |
| src/Garnet/Orleans.Journaling.Garnet/GarnetJournalPartitionHost.cs | Stacked embedded Garnet hosting. |
| src/Garnet/Orleans.Journaling.Garnet/GarnetJournalKeys.cs | Stacked key encoding. |
| src/Garnet/DESIGN.md | Records migration rules and model guarantees. |
| src/api/Garnet/Orleans.Journaling.Garnet/Orleans.Journaling.Garnet.cs | Stacked generated public API. |
| specs/garnet-range-migration/README.md | Explains model, checks, and results. |
| Orleans.slnx | Stacked project registration. |
| Directory.Packages.props | Stacked Garnet dependency. |
| .github/workflows/garnet-specs.yml | Automates simulation, mutants, and model checking. |
🧠 Review effort: Balanced
💡 Configure MCP servers for context-aware, tailored reviews. Learn more in the docs.
ReubenBond
force-pushed
the
rb-feat-journaling-garnet-phase3-spec
branch
from
October 15, 2026 03:51
7ed8139 to
89fd342
Compare
Contributor
Code coverage
Report-only conclusion: improved. The current-main baseline is commit Coverage combines every CI test matrix job, including providers, CodeGen, .NET 8/10, Linux, Windows, and macOS, using canonical physical source and branch identities. The comparison remains report-only while normal line and branch variance is calibrated. Coverage details |
ReubenBond
force-pushed
the
rb-feat-journaling-garnet-phase3-spec
branch
from
October 15, 2026 15:52
599d901 to
f85cc6b
Compare
Contributor
There was a problem hiding this comment.
🟡 Changes recommended
The safety model excludes delayed attempts and retained stale observations across tombstone collection.
5 open findings
🧠 Review effort: Balanced
ReubenBond
force-pushed
the
rb-feat-journaling-garnet-phase3-spec
branch
from
October 15, 2026 18:34
d2ce9e0 to
27c05a2
Compare
Contributor
There was a problem hiding this comment.
🔵 Needs a closer look
Delayed completion and reclamation remain unmodeled, and this explicitly non-mergeable protocol spike needs human validation.
2 open findings
5 resolved since last review
🧠 Review effort: Balanced
ReubenBond
force-pushed
the
rb-feat-journaling-garnet-phase3-spec
branch
from
October 16, 2026 00:16
27c05a2 to
f0d9e9c
Compare
Contributor
There was a problem hiding this comment.
🔵 Needs a closer look
The migration model’s assumptions and correspondence to the planned implementation require human validation before this explicitly non-mergeable spike can advance.
0 open findings
2 resolved since last review
🧠 Review effort: Balanced
ReubenBond
force-pushed
the
rb-feat-journaling-garnet-phase3-spec
branch
from
October 18, 2026 17:51
b78672c to
88c9c92
Compare
Adds Orleans.Journaling.Garnet, which stores journals in an embedded Garnet partition with synchronous AOF durability (phases 0 and 1 of the range-partitioned design in src/Garnet/DESIGN.md). Each journal operation is one Garnet transaction procedure that checks its bucket's state (the in-band seal used by range migration), applies conditional writes, and recognizes retried mutations by their client-generated ETags. Tests cover the provider contract, the Orleans.Journaling suites, a grain cluster, and process-kill recovery.
…age from the docs inventory
… and bound each attempt Every mutation is now conditioned on a state that never recurs: a content or metadata ETag, or an absence named by its tombstone's ETag. A retry whose ETag has left the eight-entry history can therefore not resurrect a deleted journal or overwrite a later metadata update; it throws GarnetJournalAmbiguousConflictException, an InconsistentStateException. Unconditional metadata updates are conditioned on the ETag the client reads, no-op updates record their ETag, OperationTimeout bounds each attempt's wait, and the bucket count is claimed atomically before any bucket opens.
The API-diff workflow built every source project for net8.0, so net10.0-only projects such as Orleans.Journaling.Garnet failed with NETSDK1005 and kept a stale surface. It now uses net8.0 when targeted and the project's first target framework otherwise.
… in the Garnet durability test SAVE checkpoints while writers append and exceeded the 5 s default async timeout on a Windows CI runner. Each cycle now also waits, bounded, until every writer has an acknowledged append before the random delay and kill.
…Store Add a pluggable range MetaStore (in-memory and Azure Blob, compare-and-swap from V to V+1), host the partitions the range map assigns to each silo, publish their endpoints in the map, and route each journal operation to its bucket's owner, refreshing the view on WrongPartition and retrying unavailable partitions within OperationTimeout. The catalog lists each bucket's index at its owner.
…host ids Bucket keys carry the range map's identity, so a partition of another map reached through a stale endpoint rejects operations. The default HostId is generated once and stored in the data directory instead of using the silo name, which Orleans randomizes. The Azure Blob MetaStore stamps each document with a write id and reports an unknown outcome instead of a wrong one when a later write supersedes an ambiguous upload.
…ialization Address review feedback on the Garnet routing layer: OperationTimeout now bounds connection, command, refresh, and backoff waits without cancelling the shared view refresh; router disposal stops retries and never reopens connections; partitions record their identity before opening buckets and mark initialization complete separately, so interrupted initializations resume only for the same partition and map; silos initialize wildcard-bound partitions through loopback. Compare recovered MetaStore writes by value in tests.
…o routing Port layer 1's retry and initialization changes to the multi-partition router: the router reports attempts whose outcome is unknown through the ambiguous flag while WrongPartition rejections leave it unset, storage passes the flag so conflicts after unknown outcomes surface as GarnetJournalAmbiguousConflictException, and partitions claim their whole identity in one set-if-absent field so concurrent initializations with different maps or bucket counts cannot both succeed. Port layer 1's client tests to the router and partition manager.
…router operations Cover each outcome of a conditional upload which fails its condition with deterministic fault injection: this write's document at the next version reports success, another writer's identical map under a different write id reports failure, and a later version reports an unknown outcome. Router tests apply their watchdog outside the exception assertion, so only an operation's own exception satisfies it.
…eguard A bucket which is open with an incomplete migration and a nonempty local index makes OJINDEX return NeedPull and fails a full catalog enumeration with InvalidOperationException; once the migration completes, the bucket lists its journals.
Disposal marks the router stopped before closing connections, and closing a connection fails commands in flight with cancellation or pipe errors. Operations now report ObjectDisposedException for any failure observed after disposal begins, keeping the original as the inner exception, while cancellation from a connection retired by a view change is retried as an ambiguous connection failure.
Add a Quint specification of bucket handover, lazy migration, consolidation, tombstones, idempotent retries, and reclamation for Orleans.Journaling.Garnet, adapted from Roux's range migration specification. It covers multi-bucket view changes (splits and merges), chained migrations, and a liveness property checked with TLC under the coordinator rule. A workflow runs the directed scenarios, simulation, and mutants on spec changes, and TLC weekly. DESIGN.md records the reopen and coordinator rules (D11), tombstone retention (D5, D25), reclamation (D26), and further differences from Roux.
…in reachability Address review of the Garnet range migration specification: - Split install into fetch and a later deliver, fenced by the destination's opening version (D27), with mutantUnfencedInstall and a scenario that delays a pull across reclamation and reopening. - Model eviction of mutation ids, allowed only once no retry of the op can arrive (D28), with mutantEvictPendingId; D25 now bounds both tombstones and histories. - Compute reachability from the bucket-source chain, stopping at done, so reclamation and return moves wait for the later migration's Done, as D11 and D26 state.
Align the Garnet range migration specification with layer 1's retry design: journals keep a count-bounded mutation history (RECENT), every write is conditioned on a state identity that never recurs, and a retry that fails its condition reports an ambiguous outcome. Add the retryOutcome invariant and mutantRetryAnyAbsence, replacing time-window eviction and mutantEvictPendingId. Renumber this layer's decisions to D41-D44 to avoid colliding with the rest of the stack.
…tone inventory Address review of the Garnet range migration specification: - Split opens into an authorization and a later open fenced by the destination's bucket version (D45); views follow the coordinator rule, which is now a safety prerequisite, with mutantUnfencedOpen and delayed and duplicate open scenarios. - Complete migration against an inventory of live journals and retained tombstones (D42), with mutantInventoryLiveOnly and a lost-create, delete, migrate, retry scenario. - Track attempts whose reply was lost separately from client outcomes, and collect tombstones only once they expire (D5, D41), with mutantCollectWithAttempt. - Let clients hold any earlier observation, and state that the unnamed absence recurs after collection, which is linearizable.
Split migration completion into inventory preparation and a later completion fenced by the destination's opening version (D46), and reclamation into an authorization bound to the source's seal version and deletion batches that each check it (D47). Add mutantUnfencedDone and mutantUnfencedReclaim with delayed-request regressions, and require a reopened bucket's deletion to have finished.
ReubenBond
force-pushed
the
rb-feat-journaling-garnet-phase3-spec
branch
from
October 19, 2026 21:05
88c9c92 to
83e178c
Compare
| quint run garnetRangeMigration.qnt --main=garnetRangeMigrationSim --mbt --max-steps=30 --max-samples=50 --n-traces=50 --out-itf=traces/trace_{seq}.itf.json | ||
| ``` | ||
|
|
||
| The last command exports traces for the .NET conformance harness into an existing `traces` directory. With `--mbt`, each state records the action taken (`mbt::actionTaken`) and its nondeterministic arguments (`mbt::nondetPicks`), which the harness replays against the real procedures. |
This branch has not been deployed
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Depends on #11501 (stacked); review only the commits after it.
Problem
Phase 3 of the Garnet journal storage (handover, lazy migration, consolidation, tombstones, reclamation) must follow Roux's range migration protocol and be model-checked before the code it governs lands. Roux relies on log positions to reopen ranges and trim logs; per-journal keys in Garnet partitions have no positions, so the reopen, reclamation, and tombstone rules need to be stated and checked for this design.
Solution
specs/garnet-range-migration/garnetRangeMigration.qnt: a Quint specification adapted from Roux'sspecs/range-migration. Partitions are the actors; a bucket's sealed state is its cut. Clients send conditional writes to any partition (requests carry no view version, matching D17), duplicate activations write with stale ETags, and lost replies are retried at whichever partition the client reaches. View changes move one or more buckets at once (moves, splits, merges) and otherwise change freely, so migrations chain.singleOpen,durability,exactlyOnce; seven mutants (open before seal, write after seal, unconditional install, delete without tombstone, reclaim before done, mark done early, retry without idempotence), each of which violates safety.migrationsCompleteholds under weak fairness when views follow the coordinator rule (mayMove). Under unrestricted views TLC finds a stall: a bucket that returns to a partition whose sealed copy is still on the chain can never reopen there. So the coordinator rule is needed for liveness, not safety..github/workflows/garnet-specs.yml: on changes to the spec, typecheck, run the directed scenarios, a 20,000-trace simulation, and every mutant. Weekly and on demand, TLC checks safety and liveness, and checks that liveness fails without the coordinator rule.src/Garnet/DESIGN.md: D5 (tombstone retention) and D11 (reopen rule and coordinator rule) are now Decided. New entries: D25 (retention bound mechanism, Undecided) and D26 (reclamation rule). The differences-from-Roux table now covers reopen, chains, reclamation, tombstones, idempotent retries, and requests without view versions.Results (local)
There is no C# product code in this layer.
Microsoft Reviewers: Open in CodeFlow