Formal and empirical verification of the single-writer designs by tobiajo · Pull Request #835 · evolution-gaming/kafka-flow

tobiajo · 2026-06-22T13:30:43Z

Stacked on (merge first): #834

Why

The single-writer designs are concurrency mechanisms, and both halves of their correctness hold badly in prose review: the external behaviour they lean on (what the group coordinator, the broker fetch path, and Cassandra LWT actually guarantee — and when), and the mechanism details where removing one piece quietly voids the guarantee. Scrutiny in this form caught real defects in code that had already passed review and its test suite. This PR keeps that scrutiny: the external facts pinned to sources, the mechanisms model-checked, the protocol claims corroborated against a real broker. Three parts.

TLA+ models — `models/`

One abstract SingleWriterStore spec (the durable store is always a correct, non-stale fold); a backend is correct iff it refines it, checked by TLC refinement mapping. 15 specs, 75 configurations (40 of them negative controls), all run in CI (models.yml) — green at 75/75.

Cassandra ✓ — offset compare-and-set + offset-carrying tombstone + replay-window monotone buffer, with CasFirstWrite beneath it (the non-atomic first-write compound against its atomic equivalent).
Kafka ✓ — generation fence + capture coupling + offset seed + atomic offset binding, with GroupCommit beneath it (write-orchestration termination and offset ordering).
Epoch ✗ — the rejected producer-epoch design, encoded as a refinement theorem that must fail.
Every load-bearing detail has a negative-control configuration that must break checking — a green suite means the details are load-bearing, not merely present.
RecoveryRead (with RecoveryReadAtomic / RecoveryDeadline) — the recovery-read completeness and stall analysis: the high-watermark read bound and the no-progress deadline.

The design docs gain Formal models sections. The models verify behaviour under the researched assumptions; they do not re-derive them — that is the corpus's job.

Research — `research/`

12 documents, entered through README.md — the report itself: it presents the design, the verification method, the findings and lessons, and the open work, routing to the detail files behind it:

External behaviour, source-verified (external-semantics.md, kafka-rebalance-semantics.md) — the coordinator's generation/epoch validation gates (including the negative-generation skip the publish guard mirrors), read_committed/LSO behaviour, initTransactions resolution, and rebalance-callback semantics with a bytecode-audited KIP-848 addendum.
Findings log and claims register (findings.md, claims.md) for both backends — each claim tracked to confirmed, corrected, or refuted.
Cassandra report (cassandra-report.md) — the Cassandra seams and test audit, and the generation study (kafka-generation-study.md), which also carries the realized KIP-848 experiment.
Recovery-read remedy and stall operations (850-remedy-decision.md, 849-stall-operations.md) — the read-bound remedy comparison (bounded-wait vs stable per-partition id) and the operational analysis of a stalled recovery read (detection, playbooks, deadline budget).
Model fidelity (model-fidelity.md) — every design claim tied to the spec or test that checks it.
Implementation requirements (implementation-requirements.md) — the register of what each arm must carry, and the dispositions of the findings against the open PRs.
Advisory review (advisory-review.md) — the external, fresh-context reviews of the research.

KIP-848 experiment

skafka is swapped for a source-vendored fork (lib/skafka), replacing the published 20.2.0 artifact for the whole build: upstream sources verbatim plus group.protocol selection in ConsumerConfig, on kafka-clients 4.3.0. On top of it, Kip848ConsumerProtocolSpec runs against a consumer-protocol broker: the stale transactional commit is fenced and aborts under both protocols, and the silent no-callback epoch bump is observed. The vendoring is the reproducibility vehicle until skafka ships the flag; Kip848ConfigSpec pins the config plumbing. The fork is kept verbatim — excluded from scalafmt (.scalafmt.conf) and Codacy (.codacy.yml) — so it stays a minimal diff from upstream.

Brings models/ (run.sh, SnapshotFlow/Cassandra/Kafka/... .tla and the .cfg suite) onto this branch so the tombstone replay-window finding can be modelled and TLC-checked here. This is a verbatim copy of the models PR's directory; the model fix follows in the next commit. When integrating, this scaffold commit is dropped and the model fix lands on the models PR (evolution-gaming#835). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01LKDTc4XC9EdHTZ7n5q7Cve

Cassandra.tla's OwnerRecover/Handover set recoveredAt = store.offset unconditionally, so a tombstone-recovered owner always "knew" the high-water X and the replay-window livelock for a deleted key was abstracted away - the model only ever encoded the fixed code, never the bug. Add a TombFloor constant and a RecoveredFloor helper: a recovery surfaces a tombstone's offset as the floor only when TombFloor is set (the code fix: SnapshotDatabase.recover -> Recovered.Deleted, held by Snapshots as the buffer floor). Without it a deleted key recovers with no floor (0) and self-fences in the replay window exactly like Fix=FALSE, but reached through a tombstone rather than a live snapshot. A live recovery is unaffected, so with TombFloor=TRUE the spec is identical to before. - cassandra_tombstone_replay.cfg (new): TombFloor=FALSE, everything else on -> VIOLATES-TEMPORAL RefLive (the livelock), the paired negative control to cassandra_replay_fixoff but via a tombstone. - existing cassandra_*.cfg: TombFloor=TRUE (the shipped/fixed behavior), so they hold exactly as before. TLC: full suite 25/25 pass their declared expectations (cassandra_refines HOLDS, cassandra_tombstone_replay VIOLATES RefLive). This is the paired model side of the recovery code fix on this branch; when integrating, it lands on the models PR (evolution-gaming#835) and the scaffold import commit is dropped. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01LKDTc4XC9EdHTZ7n5q7Cve

…st-only Snapshot persistence for the transactional Kafka mode was last-write-wins, so a stale writer (a zombie that lost its partition but is still flushing) could overwrite a newer snapshot. Guard the persist path with a compare-and-set on the offset: a write lands only if it advances the stored offset, so a stale writer's flush is rejected rather than clobbering the owner's state. This is the persist-only slice; delete stays plain last-write-wins. A guard-expired row (present with a null offset, left by a partial write whose TTL expired) is repaired by a persist claiming it via IF offset = null, which breaks the INSERT-IF-NOT-EXISTS conflict-forever deadlock. The design doc (docs/cassandra-single-writer-design.md, titled ": persist only") is rewritten around the choices and their learnings: why the offset, not the consumer generation, is the fence token, and where the subtlety lives. FlowSpec is adapted to the PartitionAssignment API. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01PGxViqVaLYb1xQyveED6Hs

…d-set fence) Extend the persist-only compare-and-set to the full snapshot fence: both persist and delete are offset-fenced, closing the stale-writer overwrite for deletes as well. A fenced delete always writes a tombstone, even for a never-persisted key, so a later replay of an already-deleted record cannot revive it. Events recovery is guarded against the journal revive: the replay-window floor is seeded from the snapshot store and initPersisted is routed through the monotonic cell, so a recovery that replays events cannot regress the floor below an existing snapshot's offset. The guard-expired row is read as absent and repaired via IF offset = null. The Cassandra design doc is made self-consistent for the full fence (why the consumer generation cannot replace the offset in the token, and where the subtlety lives); persistence.md and the kafka design doc get the matching updates. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01PGxViqVaLYb1xQyveED6Hs

…key serialization Cover the full-fence behaviour: the compare-and-set test suite, the replay- fencing spec (a replayed delete after its tombstone was TTL-reaped stays a fence), the per-key serialization race (the flushCell lost-write), the read-state floor gate, and the TTL-edge timing. The Cassandra integration tests pin the image above the mode's version floor and harden the TTL-edge timing. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01PGxViqVaLYb1xQyveED6Hs

The published skafka has no typed group.protocol=consumer support, so the consumer-protocol runtime experiment needs a source fork. Vendored under lib/skafka (a minimal diff over upstream, kept verbatim - excluded from scalafmt and Codacy) and wired as a local sbt project in place of the managed dependency.

Runtime evidence for the design exploration that was otherwise analytical: the single-writer fence under the KIP-848 consumer protocol against a real 4.3.0 broker (silent epoch bump; zombie fence), and the revoke-time flush outcome under a real sticky-assignor rebalance (fenced cooperative, committed eager).

Model-check the design as a refinement tower - one abstract SingleWriterStore that each backend refines - with negative controls that break the refinement when a fence is removed. Both design docs gain a Formal models section bridging to models/.

The requirements register, findings ledger, external-semantics pins, remedy-decision analysis and review record behind the single-writer work.

Testing section cited only explicit-generation suites (RevokeTimeFlushSpec and Kip848ConsumerProtocolSpec drive live rebalances); the modelled-assumption list said one open transaction per partition (per id lineage).

…amport conventions The suite was a flat directory of 15 modules. The directories now mirror the refinement tower itself -- one folder per spec, a refining model beneath the spec it refines: SingleWriterStore/ THE spec (+ SnapshotFlow, the shared base) |- Cassandra/ | `- CasFirstWriteAtomic/ the atomic CAS spec ... | `- CasFirstWrite/ ... refined by the first-write compound |- Kafka/ | |- GroupCommit/ GroupCommitLanes/ RecoveryDeadline/ TokenSync/ FlowsAlive/ | `- RecoveryReadAtomic/ the atomic read spec ... | `- RecoveryRead/ ... refined by the read compound `- Epoch/ FlushCell/ the A4 assumption control (outside the tower) Cross-folder EXTENDS resolve via -DTLA-Library, which TLC honors only for a spec given by an absolute path -- the runner passes one. The modules are also reformatted to the conventions encoded in the TLA+ Toolbox: a 77-column right margin (EDITOR_RIGHT_MARGIN_DEFAULT), header dashes from the new-module template's max(4, (77 - len(name) - 9) / 2), 77-character footers, comment boxes squared to the margin, ASCII only. Pure re-wrapping, verified by dumping SANY's concrete syntax tree before and after: identical for all 15 modules, so no junction list re-grouped (TLA+ conjunction lists are indentation-sensitive, and a re-grouped list still parses). The comment-only exceptions are corrections the reformat surfaced: - Cassandra "THREE hazards" over four bullets -> FOUR - Kafka "two load-bearing client-side details" over three -> three; glossary gained the undocumented `overwrote`; a cross- reference named CasFirstWrite, a Cassandra model, where RecoveryRead => RecoveryReadAtomic was meant - Epoch glossary gained `rebalanced`; ZombieCommit no longer implies its guard restricts the offset (it does not -- the regression is what the counterexample exhibits) - RecoveryRead "Results (eleven configs)" listed 11 of 13, omitting the two Foreign-knob positives that carry its own conclusion - CasFirstWrite pc[w] showed one path of three; AbstractPc omitted "u1" - FlushCell said three register ops without noting the model merges the first two

Each of the 75 runs is now the standard MC pair, beside the spec it checks: MC_<name>.tla a wrapper module that EXTENDS the spec and declares the expected outcome inline (\* expect:, optional \* flags:) MC_<name>.cfg its TLC configuration Two reasons over the old scheme (a bare <name>.cfg carrying a \* spec: directive naming its module). The pair is the layout the tooling already speaks, so the VS Code TLA+ extension model-checks any wrapper with no extra step; and the prose that justified each config now lives in a module the reader opens next to the spec, rather than in a config file. Config short names are unchanged, so every citation across models/README.md, docs/ and research/ still resolves. Conversion verified as a 75-way bijection with token-level identity of every config body, the sole intended differences being the dropped \* spec: directive (now implied by EXTENDS and location), directives and prose moved into the wrapper, and long CONSTANTS lines split one assignment per line to fit the margin. Ten negative controls lose their TypeOK invariant. Outcomes are asserted by TLC exit code (next commit), and an invariant violation is exit 12 whichever invariant broke -- so a negative control co-checking TypeOK would let "the control worked" and "the model is type-broken" report the same PASS. Each of the ten was re-run under its old config to confirm TLC reported the target invariant and not TypeOK, and every paired positive still checks TypeOK, so no family loses the coverage. The VIOLATES-TEMPORAL and VIOLATES-REFINEMENT controls keep theirs: those expect exit 13, so an invariant break is a different code and fails the run rather than masquerading as the expectation.

run.sh classified each run by grepping TLC's output. That coupled the harness to one TLC's phrasing: the pinned pre-2.17 build emits an unnamed temporal violation report, so the matchers carried a special case for it (F-5), and a newer TLC could not be adopted without matcher surgery -- recorded in the corpus as an open gap. Outcomes are now taken from the exit status alone (tlc2.output.EC$ExitStatus, stable across versions): HOLDS => 0, VIOLATES => 12, VIOLATES-TEMPORAL and VIOLATES-REFINEMENT => 13. TLC's output is captured only to print on an unexpected result. Every other status (10 ASSUMPTION, 11 DEADLOCK, 14 ASSERT, 150/151 parse, 255) matches no expectation and so fails loudly. An exit code names a class, not a property, so identity is structural: an expected-violation config must declare exactly one name of the expected class, and it must be the name its directive states. Both are enforced. Names are collected per cfg SECTION rather than per line -- TLC's grammar lets a second same-class check ride a continuation line, and a line-scoped count misses it, which is how a wrapper whose declared invariant HOLDS could be made to report PASS off another invariant's violation. A HOLDS config declaring no invariant or property now fails too, instead of passing vacuously, and only -deadlock is accepted in \* flags: (-simulate would change what "checked" means silently). Also enforced here: the 77-column margin and ASCII-only, so the formatting convention cannot erode. The pin moves to tlaplus release v1.7.4 (jar self-reports TLC 2.19 rev 5a47802) -- safe now that no matcher depends on output phrasing, and verified by a full re-run. The suite also passes on a build newer than the pin, and the ExitStatus constants are identical from 2.15 through the 2026 nightly. tla2tools.jar was tracked despite being listed in .gitignore since the commit that added both; it is untracked here, which is what the download-on-first-run path in run.sh always assumed. .gitignore also picks up the VS Code TLA+ extension's per-run artifacts (*.out, *_trace_*.tlc) and drops three patterns this TLC no longer produces.

…test comment Documentation follow-up to the models migration, plus one unrelated correction found on the way. models/README.md: the new layout and MC-pair format, the exit-code contract and the structural-identity rule behind it, the v1.7.4 pin, and the VS Code setup (tlaplus.moduleSearchPaths, the three folders referenced across directories). The suite-wide assumptions are now numbered A1-A6, with A1-A4 matching the Cassandra design doc's four in the same order -- so A4, the only label cited across the corpus, means per-key serialization everywhere. A3 (per-key independence) had been missing from the list although every model relies on it to check a single key. research/: the toolchain facts move to the current pin, and the open "needs matcher work before a newer TLC" gap is discharged, since the harness no longer reads TLC's output at all. F-5 keeps its finding and loses only the stale implication that its fix is how the runner works today. advisory-review.md is a dated record, so its findings stand as written and the later facts go in a marked addendum after the snapshot line rather than into the findings' prose. model-fidelity.md gains an accepted coverage gap: R-849.2's budget (transaction timeout + abort scan < recoveryStallTimeout < max.poll.interval.ms) is stated as a MUST and checked by the timing model, but no code enforces either bound -- it holds because the defaults clear them and the scaladoc says to keep it that way. Unlike F-12's groupId/autoCommit contract, there is no chokepoint to force it at: R-849.2a records that both comparisons rest on values the module cannot see, which is why the wiring-time check was built and then reversed. Accepted, not overlooked. SnapshotReplayFencingSpec: the tick-delete-during-replay test claimed a persist=false delete "never touches the offset-gated store". It does -- Snapshots.delete writes whenever the store is fenced, and snapshotsOf always fences -- but the buffer's high-water raises the tombstone back to the recovered offset, so the write is an idempotent rewrite AT that offset, which the gate admits by equality. The test pins something real; only its explanation was wrong. Comment and assertion message only, no behavioural change.

…prove A cross-check of the two design docs' model-checking sections against the actual suite found the config names and outcomes all correct, but three claims that overstate what is established. Kafka, the zombie fence. The section credited "the group-metadata capture coupled to flow teardown" as a load-bearing detail pinned by `kafka_decoupled` -- while the same document's rejected alternatives explain that capturing the generation in a rebalance callback is exactly what the design does NOT do (the bump that matters fires no callback under two of three protocol/assignor combinations), and `Consumer.scala` has no capture at all. `Kafka.tla`'s `Coupled` knob conflates two mechanisms the code keeps separate: shipped, the fence is unconditional teardown-on-revoke plus the post-poll refresh. The section now says so, and names the bridge as argued rather than mechanized -- gap M5, which research/model-fidelity.md already recorded but the design doc did not surface. Kafka, the evolution-gaming#850 remedies. "Holds under either remedy" is true only within the partition's id lineage. Out of lineage the two split -- `recoveryread_hw_foreign` HOLDS while `recoveryread_lso_foreign` VIOLATES the refinement -- and that split is the mechanized reason A is required and B is optional. Stating them as co-equal inverted the decision the remedy analysis reached. Kafka, GroupCommit. Called a "refinement"; it has no INSTANCE, no refinement mapping and no Ref* property -- it checks `Termination` and `INV_OffsetWithinDurable`. Now described as what it is. Also: the tower seam is a documented correspondence, not a TLC-checked substitution (README says so; the doc implied otherwise); the Kafka assumption list dropped A6, the un-mechanized takeover-abort visibility half of ext(K5), and kept only the contract half that is folded into the model; "checked under every interleaving" is bounded at two writers; the rejected designs are one, `Epoch`, the other 39 expected failures being removed-guard controls; `cassandra_events_revive_reentry` is F-7's paired negative, not a non-vacuity control (that is `casfw_refines_vacuous`); and the Cassandra A4 assumption now points at `FlushCell`/`serial_race`, the checked sibling it gained.

The section named Kafka, GroupCommit, RecoveryRead/RecoveryReadAtomic and Epoch, but not RecoveryDeadline, TokenSync, GroupCommitLanes or FlowsAlive -- so four of the arm's models, and 19 of its configs, were invisible to a reader of the design doc. RecoveryDeadline was the conspicuous one: the same document discusses the evolution-gaming#849 deadline at length without mentioning the model that mechanizes it. Each is stated through what its negative controls cost, matching the section's existing shape: RecoveryDeadline no tripwire at all -> silent eviction (recoverydeadline_notrip); one that fires too late -> eviction still wins (_late); one keyed on total elapsed rather than consecutive no-progress -> fails a read that is progressing (_total) TokenSync the 2x2 that shows refresh subsumes capture -- capture alone cannot see a silent bump (tokensync_capture, the KIP-848 case), which is the model-side reason capture was removed GroupCommitLanes the two real lanes: no shared budget (gclanes_shared), the marker lane self-triggers (gclanes_starve), the offset stays gated on durability across commit and abort FlowsAlive what the generation fence does NOT give you -- KIP-447 validates member and generation, never per-partition ownership, so the awaited teardown in the revoke callback is the whole zombie fence (flowsalive_race breaks it) FlowsAlive also gets a pointer back to the Kafka bullet, since it carries the shipped zombie fence that Kafka.tla folds into its Coupled knob.

…commit surface Two additions to the Kafka arm, both from re-examining the transactional mode against a real broker. The real-eviction teardown experiment (kafka-generation-study.md). Every retained pin of the write fence supplies the hazard's cause itself: the transactional IT hands a stale PartitionFlow a staleGeneration token, and the KIP-848 zombie-fence IT fabricates current-1, already disclosed there as synthetic. This experiment supplies none of it - a real broker evicts a real member past max.poll.interval.ms and reassigns its partition - so it is the only place the handover is real. The route is teardown, not the revoke callback: an error escapes the poll loop and TopicFlow's teardown release drops every cached PartitionFlow including the reassigned one, so flushOnRevoke flushes stale state. That is the flows-alive invariant's eviction boundary (KF8, S-3) reached rather than argued, and the fence holds end to end. It also corrects that claim's eviction-path clause, which named member validation (UNKNOWN_MEMBER_ID) as the closer. The evicted member's writer, wrapped to record every broker-answered call, recorded exactly one - send-ack rejected on the producer epoch - and no sendOffsetsToTransaction, so member validation never ran. ext(K5) already pins that ordering from source; what is new is corroboration on the eviction route, and that composing it with commitBatch's shape makes member validation unreachable there for any batch carrying a write. Recorded as claim KF17; KF9 is unaffected, since nothing relies on the epoch. The ambiguous-commit surface as ext(K16). A commitTransaction that times out client-side while the broker may already have committed had no entry, though it decides whether commitBatch's abort-on-every-failure is a defect: review had reported that the abort poisons the producer, and it does not. The entry pins the javadoc, the client's IllegalStateException-before-transition behavior, and the measured consequences - the abort aborts nothing, the transaction still lands with snapshot and bound offset both visible under read_committed, and the producer refuses every later transaction. Consequences recorded: the blanket abort is inert where it cannot help and effective where it can, so the narrowing review proposed changes no outcome; nothing is lost, since the offset rides the same transaction; and retrying in place is rejected because each attempt blocks up to a user-configured max.block.ms inside the poll cycle. Both are graded by provenance rather than uniformly. Neither harness is retained: they pin a client contract or a route-coupled assertion rather than kafka-flow behavior a regression could reach, so each is recorded as an experiment with its branch cited for re-running.

An advisory reviewer argued the spent producer self-heals in the background - the Sender completing the EndTxn with Errors.NONE resets the transaction state, so the next beginTransaction would succeed without a rebalance. Read against kafka-clients 4.3.1 that is refuted, and the entry now carries the mechanism rather than a claim carried from the measuring spec: pendingTransition is nulled only in throwIfPendingState and handleCachedTransactionRequestResult, only when result.isAcked(), and isAcked is set only inside TransactionalRequestResult.await on the app thread - the Sender merely calls done(), and resetTransactionState never touches pendingTransition. The state does reset; the guard is consulted first and still fails. Provenance upgraded accordingly. The same review found the freeze's end overstated, and that half holds: 'until the next rebalance' misses that under persistPeriodicallyAndUnloadOrphaned a swallowed persist still lets canUnload remove the key, and the freed offset's commit through the spent producer runs on PartitionFlow's deliberately unhandled path, which rebuilds the producer sooner. Corrected here and in the user-facing doc.

tobiajo force-pushed the tj/address-partition-ownership-overlap-possiblity-models branch 11 times, most recently from 62ef814 to ce7b881 Compare June 22, 2026 23:21

tobiajo changed the title ~~Add TLA+ formal models for the single-writer snapshot designs~~ Add TLA+ formal models for the single-writer snapshot designs [SKIP] Jun 22, 2026

tobiajo mentioned this pull request Jun 24, 2026

Protect Cassandra snapshot writes from stale writers (full compare-and-set fence) #834

Draft

tobiajo force-pushed the tj/address-partition-ownership-overlap-possiblity-models branch from 40891bf to 894597d Compare June 24, 2026 09:24

tobiajo force-pushed the tj/address-partition-ownership-overlap-possiblity-models branch from 894597d to 211d2b8 Compare June 25, 2026 14:17

tobiajo force-pushed the tj/address-partition-ownership-overlap-possiblity-models branch from 211d2b8 to 6eca0a2 Compare June 25, 2026 15:26

tobiajo force-pushed the tj/address-partition-ownership-overlap-possiblity-models branch from 6eca0a2 to 72cefc6 Compare June 25, 2026 15:50

tobiajo force-pushed the tj/address-partition-ownership-overlap-possiblity-models branch from 72cefc6 to 141b127 Compare June 25, 2026 18:23

tobiajo force-pushed the tj/address-partition-ownership-overlap-possiblity-models branch from 141b127 to 246ebf6 Compare June 25, 2026 18:31

tobiajo force-pushed the tj/address-partition-ownership-overlap-possiblity-models branch from 246ebf6 to 9adba27 Compare June 25, 2026 19:31

tobiajo mentioned this pull request Jul 11, 2026

Refresh consumer group metadata on poll #854

Merged

tobiajo changed the title ~~Add TLA+ formal models for the single-writer snapshot designs [SKIPPED]~~ Formal and empirical verification of the single-writer designs Jul 11, 2026

tobiajo reopened this Jul 11, 2026

tobiajo force-pushed the tj/address-partition-ownership-overlap-possiblity-models branch 6 times, most recently from 14ebb01 to 9bbf4ef Compare July 15, 2026 15:16

This was referenced Jul 17, 2026

Recover transactional snapshots completely, with a bounded read tobiajo/kafka-flow#16

Closed

Recover transactional snapshots completely, with a bounded read #857

Merged

Partition ownership overlap during unideal circumstances #732

Open

tobiajo and others added 14 commits July 22, 2026 21:47

Add the TLA+ single-writer models

153003a

Model-check the design as a refinement tower - one abstract SingleWriterStore that each backend refines - with negative controls that break the refinement when a fence is removed. Both design docs gain a Formal models section bridging to models/.

Add the verification research corpus

ee008d2

The requirements register, findings ledger, external-semantics pins, remedy-decision analysis and review record behind the single-writer work.

Correct two claims in the Kafka single-writer design doc

95fadbf

Testing section cited only explicit-generation suites (RevokeTimeFlushSpec and Kip848ConsumerProtocolSpec drive live rebalances); the modelled-assumption list said one open transaction per partition (per id lineage).

This was referenced Aug 4, 2026

Pair the unfenced teardown-flush defect (#732 shape) with its transactional prevention, and pin the ambiguous-commit contract tobiajo/kafka-flow#25

Closed

Document the unanswered-commit case in transactional persistence tobiajo/kafka-flow#26

Open

tobiajo added 2 commits August 4, 2026 20:01

Navigation Menu

Uh oh!

Formal and empirical verification of the single-writer designs - #835

Formal and empirical verification of the single-writer designs#835
tobiajo wants to merge 16 commits into
evolution-gaming:masterfrom
tobiajo:tj/address-partition-ownership-overlap-possiblity-models

tobiajo commented Jun 22, 2026 •

edited

Loading

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Uh oh!

Conversation

tobiajo commented Jun 22, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Why

TLA+ models — models/

Research — research/

KIP-848 experiment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

tobiajo commented Jun 22, 2026 •

edited

Loading

TLA+ models — `models/`

Research — `research/`