Validate Jepsen conflict deaths against independent claim evidence - #19
Open
jeregrine wants to merge 3 commits into
Open
Validate Jepsen conflict deaths against independent claim evidence#19jeregrine wants to merge 3 commits into
jeregrine wants to merge 3 commits into
Conversation
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.
Problem
The Jepsen driver trusted every
{:group_registry_conflict, key, winner_meta}exit. It removed the owner's intent and credited conflict coverage without checking whether that process actually lost a registry conflict. Killing a revision-99 owner with a nonexistent key and an invented revision -100 winner could therefore leave an apparently valid empty terminal state.Fix
Retain conflict deaths as oracle obligations. An independent, restart-persistent harness journal records registration invocations before calling Group, their outcomes, and intent removal. The Clojure checker reconstructs the victim's possible registrations and requires the reported winner to have a strictly higher
{revision, token}rank and matching historical claim evidence for the same cluster and key. Only independently justified deaths contribute conflict coverage; invalid deaths fail the history even after Group has cleaned up every row.Registration calls interrupted before their reply remain possible claims, while definitive
:takenresults exclude attempts. Historical evidence remains available after the winning owner unregisters, dies, or the BEAM restarts. Permanently retired nodes' journals are archived through the stopped-container collector and replayed alongside every snapshot, preserving both winning claims and invalid deaths without treating retired owners as live.Before each new history, DB setup resets the running recorder's disk and memory together. Mid-history restarts preserve evidence, while repeated histories cannot inherit earlier conflict coverage. Qualification consumes EDN emitted by the actual Owner/Driver harness and the archive decoder.
Supporting information
Stacked on #23 (
fix-jepsen-retired-evidence) to extend its lifecycle collector rather than duplicate it. This changes only the Jepsen harness and oracle, not Group's conflict semantics.The oracle proves independently witnessed possible winners, not the exact instant a replica learned each claim. Local journal order rejects winners first attempted after a death; it does not assume synchronized cross-node clocks or that a remote unregister was already delivered.
Conflict archives use small append-only workload records, a 64 MiB collection bound, and ten-second command deadlines. Missing, truncated, unreadable, or malformed archives fail qualification. Checker qualification and retired-journal decoding require Elixir/Mix and the repository dependencies on the controller host.