go-mvcc-serializable-snapshot-write-skew-scc

Answer

I diagnosed the problem, implemented a complete solution, and verified it. The full self-contained write-up is at ~/SOLUTION.md, with working code at ~/ssi/ (ssi.go, ssi_test.go, prop_test.go).

Root cause

SI is not serializable because it permits write skew. The validator must:

1. Classify edges correctly — rw = reader of version X → writer of version X+1; wr = writer of version X → reader of X; ww = writer of X → writer of X+1. Conflating these produces a wrong graph.
2. Not abort on non-cycle dangerous structures — a pivot T1 -rw-> T2 -rw-> T3 only matters if there is a real return path T3 →* T1.
3. Be minimal — aborting every dangerous pivot is safe but not minimal. Cycles often share a pivot, so the required answer is a minimum feedback vertex set restricted to eligible pivots.

The commit-order rule T3.Commit < T2.Commit (and < T1.Commit when distinct) is what makes the validator abort the later pivot, matching SSI runtime behavior.

The fix (core of Validate)

// Candidate pivots: a -rw-> b -rw-> c, c commits before b (and a), and c ->* a.
for _, e1 := range rw {
    a, b := e1.from, e1.to
    tb := g.byID[b]
    for _, e2 := range rw {
        if e2.from != b { continue }
        c := e2.to
        tc := g.byID[c]
        if tc.Commit >= tb.Commit { continue }          // target must commit first
        if c != a {
            if ta := g.byID[a]; ta != nil && tc.Commit >= ta.Commit { continue }
        }
        if g.reaches(c, a) { candSet[b] = true }         // real cycle closure
    }
}
// Exact minimum FVS over candidates, branching on a discovered cycle's pivots,
// tie-breaking in favour of aborting later-committing transactions.

The store exposes Begin / Read / Write / TryCommit / Commit / Committed, and Validate(committed []Txn) []string returns the minimal abort set sorted by commit order.

Verification

gofmt -l .        # clean
go vet ./...      # clean
go test -count=1 -v ./...

--- PASS: TestWriteSkew_AbortsLater            (write skew -> [T2], only the later pivot)
--- PASS: TestNonCycleDangerousStructure_NoAbort (false-positive guard -> [])
--- PASS: TestWrClosesCycle                    (wr-closed cycle detected)
--- PASS: TestNoConflict
--- PASS: TestIndependentWriteSkews            (disjoint pairs -> [T2 T4])
--- PASS: TestStoreWriteSkew                   (Begin/Read/Write/Commit integration)
--- PASS: TestRemainingAcyclic                 (graph acyclic after aborts)
--- PASS: TestPropertyRandomValidSI            (50,000 random valid SI histories)
ok  ssi  0.41s

The randomized property test generates valid SI histories (reads at snapshot, first-committer-wins enforced) and checks two invariants on every one: removing the reported aborts makes the dependency graph acyclic, and every reported abort is necessary (dropping it reintroduces a cycle).

A key correctness detail discovered during testing: the generator must enforce write-write conflicts exactly as real SI does, otherwise ww edges form cycles that the SSI theorem explicitly excludes; the final code and property test both model first-committer-wins correctly.