Documentation
¶
Overview ¶
Package interleave is RFC-199 Tier 2's concurrent-open-transaction interleaving driver.
Every hunt workload before it is single-writer — each transaction runs and commits alone — so SimFDB's serializable-snapshot-isolation resolver never had to resolve an actual conflict: not one real not_committed(1020) ever fired. Tier 1's conflict resolution was an *unexercised checkbox*. This driver fills that gap. It holds several transactions open at once, interleaves their reads/writes/atomic-adds through a single deterministic goroutine, and commits them through SimFDB's serialized resolver — which is exactly what makes 1020 fire.
The workload is two contrasting operations on a small hot keyspace:
- RMW-increment v := Get(k); Set(k, v+1) reads k (a read conflict) then writes it. Two of these racing on the same key is the classic lost update — and under SSI the loser does not lose its write silently, it ABORTS with 1020.
- atomic-add Add(k, delta) writes k with no read conflict. Atomic adds never conflict with each other, so they commute and always commit — the FDB idiom that exists precisely to avoid the RMW abort. Running the two side by side exercises both paths.
Two intrinsic oracles judge each run, neither needing an external reference:
- VERDICT oracle — independently recompute the SSI verdict for every commit from point-key read/write sets and a model version counter kept in lockstep with SimFDB's, and compare to SimFDB's actual verdict. A disagreement is either a MISSED CONFLICT (SimFDB committed a transaction whose read was overwritten after its read version — a lost update) or a SPURIOUS ABORT (SimFDB aborted a transaction with no conflicting committed writer). The model resolves at the point-key level while SimFDB resolves over byte-ranges; that representation gap is what gives the oracle teeth against the range arithmetic (keyAfter / rangesOverlap / conflict extents).
- STATE oracle — retry every aborted transaction to a single successful commit (true rollback discarded the aborted attempt, so each program applies exactly once), then assert the final keyspace equals the seed-derived sum of every program's effect (each increment +1, each add +delta). This is fully independent of SimFDB's storage: it catches a lost update, a rolled-back-write LEAK (a rollback that failed to discard a mutation), and any atomic-add miscount.
By default the driver runs fault-free: the resolver itself is under test. Setting Faults > 0 activates SimFDB's commit BUGGIFY, which adds the fault dimension the record workload's single writer cannot reach — a commit_unknown(1021) transaction RACING with other open transactions. 1021 has two real branches: the writes are durable but the answer was lost, or the commit never reached the proxy. The state oracle is unchanged (every program still applies exactly once: an APPLIED 1021 is not retried; a DISCARDED 1021, a 1020, or a 1007 applied nothing and is retry-drained), and the verdict oracle goes one-directional (a real conflict still surfaces as 1020 because the resolver runs before fault injection, but an injected fault on a clean transaction is not predicted). This is what proves a 1021 transaction correctly PARTICIPATES in concurrent conflict detection and applies exactly once — a property no single-writer workload exercises.
Which branch a 1021 took is simulator ground truth (SimDB.LastCommitUnknownApplied) and is read only by the oracle, never by the transactions themselves: a real client cannot know, which is the whole reason the error exists.
Index ¶
Constants ¶
This section is empty.
Variables ¶
This section is empty.
Functions ¶
Types ¶
type Result ¶
type Result struct {
Report *hunt.Report
Conflicts int // phase-1 transactions SimFDB aborted with 1020 (real + injected)
Predicted int // phase-1 transactions the verdict oracle predicted would abort
Applied1021 int // phase-1 transactions whose commit_unknown(1021) took the APPLIED branch
Discarded1021 int // phase-1 transactions whose commit_unknown(1021) took the DISCARDED branch
Txns int
// contains filtered or unexported fields
}
Result is the driver's rich outcome: the standard hunt.Report (violations / error / fingerprint) plus resolver-exercise metrics the tests assert on (Conflicts must be > 0 for the RMW profile — the NO-FAKE-CHECKBOX proof that 1020 truly fires).
type Workload ¶
type Workload struct {
Keys int // counter keyspace size; smaller = more contention = more conflicts (default 4)
Txns int // transactions held open and interleaved per run (default 4)
OpsPerTxn int // steps in each transaction's program (default 3)
AddPct int // percent of steps that are atomic-add vs RMW-increment, in [0,100] (default 40)
// Faults, when > 0, activates SimFDB's commit BUGGIFY at that probability so commits are hit by
// injected not_committed(1020) / transaction_too_old(1007) BEFORE apply and commit_unknown(1021)
// on either of its two branches. 0 (default) is the clean, fault-free path — the pristine
// resolver oracle. With faults on, the 1021 path is the point: on the APPLIED branch the
// transaction took a commit version, so it must participate in later conflict detection, count
// once toward the state total, and NOT be retried (retrying would double-apply its atomic adds);
// on the DISCARDED branch it applied nothing and must be drained like a 1020. See the package
// doc's fault-mode note.
Faults float64
}
Workload is the concurrent-open-transaction interleaving driver, a hunt.Workload. Its knobs are self-contained (it ignores the record-oriented hunt.Config).
Source Files