Merge dbsp/source-trait into dbsp/model-over-source
# Conflicts: # context/test-evidence/core.md
This commit is contained in:
@@ -119,6 +119,14 @@ dead host's replies are refused. A duplicate answer also prunes every queued ent
|
||||
and moves `seen` onto the live epoch, so a late notice from a dead host costs one extra round and cannot
|
||||
livelock `sync`.
|
||||
|
||||
**The host that answers a request is live, whatever the client believed.** `left` is a guess, because
|
||||
epochs of different hosts are unordered: a late reply from a host the client never joined moves it onto
|
||||
that host, and writes off the live one. Refusing the live host's answers as "left" then strands the client
|
||||
(`sync` returned `Exhausted`, found by the property test). So `apply_answer`, which `sync` and `poll` use
|
||||
for the reply to a request they just sent, takes an epoch off `left` before it applies. `apply` is for a
|
||||
reply that arrives on its own, and keeps the guard. A stale reply can still move the client for one round;
|
||||
the next request it makes is answered by the live host and brings it back.
|
||||
|
||||
`poll` hands a pulled notice only to the shape it asked about. A notice carries only that shape's keys,
|
||||
and applying it to another tracked shape would advance that shape past keys it never saw.
|
||||
|
||||
@@ -182,7 +190,9 @@ counts comparisons on a counting item type rather than reading a clock.
|
||||
**The host instance** is a random id, never a time (`Host::new` takes one from `RandomState`).
|
||||
`RandomState` has no entropy on `wasm32-unknown-unknown`, so a worker must pass a real one through
|
||||
`Host::with_instance`. A restarted host with the same id would accept a stale watermark as current.
|
||||
`Worker` still calls `Host::new` (improvise-bw4p.7).
|
||||
`Worker` still calls `Host::new` (improvise-bw4p.7). Such a restart, with the same instance id and
|
||||
generation 0, is not recognised as a restart: the client's `older` guard refuses its replies as coming from
|
||||
an older generation of the host it is on (improvise-bw4p.7).
|
||||
|
||||
**Eviction** (`evict_idle`) takes a local count and an idle length in the same unit, never a wall clock
|
||||
compared across machines. An evicted key is announced in the next notice and forgotten; naming it again
|
||||
@@ -207,6 +217,13 @@ The token in a request is carried and echoed by the client and never read by the
|
||||
|
||||
## 8. Edge adapters
|
||||
|
||||
**Transport contract.** A reply must reach the call that made the request. `Request` and `Correction`
|
||||
carry no id, so the client cannot tell a late reply from an answer on its own; `sync` and `poll` treat
|
||||
whatever `Edge::call` returns as the answer (`apply_answer`), and only a reply handed to `apply` is
|
||||
treated as late. A transport that reorders or duplicates replies must therefore correlate them itself
|
||||
or drop the strays (improvise-bw4p.10 adds the id to the frames).
|
||||
|
||||
|
||||
`Edge` is one end of a stream: `call(Request) -> Result<Reply, EdgeError>`. `InProcess` is the
|
||||
function call; `WireEdge` passes request and reply through JSON text, the adapter at a wire boundary,
|
||||
so the lossless properties are exercised by every test that uses it. Neither adds a `ClientFrame` or
|
||||
|
||||
@@ -87,3 +87,9 @@ implementation, written as a query engine with no index would answer, sharing on
|
||||
`DataStore`. `the_store_and_a_scanned_table_answer_every_select_alike` asks both every select over a
|
||||
fixture (every subset of every stored key as a base, with no span, one span of each of six item
|
||||
lists, and two), at both widths and for all five functions: over 5,000 triples.
|
||||
|
||||
## Building a `Summary` from an engine's answer
|
||||
|
||||
`Summary::from_parts(Numbers::from_parts(count, exact_sum, least, greatest), Agreement)`. `Agreement`
|
||||
is what the non-number values hold: `None`, `One(v)` or `Mixed`. `from_parts` drops extremes that
|
||||
contradict the count or are NaN, so a source cannot hand the evaluator a state `add` could not reach.
|
||||
|
||||
@@ -33,11 +33,13 @@ link, so they call the `extern "C"` functions as plain functions.
|
||||
4. **Failure leaves the Z-set unchanged.** `add`, `sub`, `neg`, `scale` and `decode_add`
|
||||
compute a new value and then assign it, so an overflow half way through cannot leave a
|
||||
half-applied update (`zs_zset_insert` is one addition, so it has no half).
|
||||
5. **A failed step poisons the circuit.** A panic in `step` leaves operator state half
|
||||
updated, and the circuit has no rollback (ADR 009 clause 11 is the host's; `zset.md`). So the first
|
||||
failure in a step, or in a rebuild step, marks the circuit poisoned, and every later call
|
||||
that uses it returns `ZS_ERR_POISONED`. A caller drops it and builds another. Ids that do
|
||||
not exist, and malformed arguments, are refused before any state changes and do not poison.
|
||||
5. **A failed step poisons the circuit, and a rollback revives it.** A panic in `step` leaves
|
||||
operator state half updated. So the first failure in a step, or in a rebuild step, marks
|
||||
the circuit poisoned, and every later call that uses it returns `ZS_ERR_POISONED`. The one
|
||||
way out is `zs_circuit_rollback` of a transaction that the failed step ran in
|
||||
(decision 13); a poison from outside a transaction is permanent, and the caller drops the
|
||||
circuit and builds another. Ids that do not exist, and malformed arguments, are refused
|
||||
before any state changes and do not poison.
|
||||
6. **Buffers.** The caller owns every buffer it passes and may reuse it once the call
|
||||
returns; the library copies. The library hands out no memory except handles. Output of
|
||||
variable size uses a two-call protocol: `zs_zset_encode(z, buf, cap, &needed)` always sets
|
||||
@@ -83,6 +85,20 @@ link, so they call the `extern "C"` functions as plain functions.
|
||||
12. **Versioning.** `zs_abi_version()` and `ZS_ABI_VERSION` are 1. A change that breaks a
|
||||
signature or a code bumps it.
|
||||
|
||||
13. **Transactions** (improvise-bw4p.5; `zset.md`, "Transactions"). `zs_circuit_begin`,
|
||||
`zs_circuit_commit` and `zs_circuit_rollback` wrap `Circuit::begin/commit/rollback`; a
|
||||
handle-returning `snapshot` was not chosen, because the circuit logs what changes and there
|
||||
is no snapshot object to free. The new code is `ZS_ERR_TRANSACTION` (10) for a `begin` on an
|
||||
open transaction, a `commit` or `rollback` with none open, and a `zs_circuit_take` while
|
||||
one is open (take after commit: a rollback subtracts the step's output from the sink).
|
||||
`begin` on a poisoned circuit is `ZS_ERR_POISONED`, and so is `commit` after a failed step:
|
||||
the host rolls back. `rollback` is the only call that clears the poison, and only a poison
|
||||
that came from a step inside the transaction. This is additive, so `ZS_ABI_VERSION` stays 1.
|
||||
What a rollback cannot undo is a callback's own side effects and a `ZsRebuild` stepped in the
|
||||
transaction, finished or not (it answers `ZS_ERR_INTERRUPTED` after, and the host starts another job; `rollback_abi.rs`). A
|
||||
circuit left mid-step by a non-local exit answers `ZS_ERR_POISONED` to a rollback like to
|
||||
everything else: the frames are skipped and the engine is not touched.
|
||||
|
||||
A rebuild is one logical tick however many `zs_rebuild_step` calls it takes (`zset.md`,
|
||||
decision 8): a `delay` fed by it shows the previous tick once, and `done` is 1 as soon as the
|
||||
last chunk ran, whatever the deadline callback says.
|
||||
@@ -108,7 +124,7 @@ resolve to whatever is current, and only the nightly date is fixed. It passed at
|
||||
this commit (about 12s):
|
||||
|
||||
```
|
||||
nix shell --impure --expr 'let p = import <nixpkgs> { overlays = [ (builtins.getFlake "github:oxalica/rust-overlay").overlays.default ]; }; in p.rust-bin.nightly."2026-09-24".default.override { extensions = [ "miri" "rust-src" ]; }' --command cargo miri test -p zset-ffi --lib --test abi
|
||||
nix shell --impure --expr 'let p = import <nixpkgs> { overlays = [ (builtins.getFlake "github:oxalica/rust-overlay").overlays.default ]; }; in p.rust-bin.nightly."2026-09-24".default.override { extensions = [ "miri" "rust-src" ]; }' --command cargo miri test -p zset-ffi --lib --test abi --test rollback_abi
|
||||
```
|
||||
|
||||
It is not a CI job. A proposed one: a `miri` job in `.github/workflows/ci.yml` that takes the
|
||||
|
||||
+84
-4
@@ -124,6 +124,7 @@ Clause 1's deferred scope, built without ADR 008. The ADR is not edited; this is
|
||||
| `aggregate`, `aggregate_in` | group-by, re-folds only touched keys (`AggregateState`) |
|
||||
| `Trace`, `MemTrace` | operator state behind lookup, range, apply |
|
||||
| `Rebuild`, `Progress` | a snapshot loaded as a resumable job |
|
||||
| `begin`, `commit`, `rollback` | an undo-log transaction over the circuit's state (below) |
|
||||
|
||||
Decisions, where the ADR left a choice:
|
||||
|
||||
@@ -185,7 +186,86 @@ Decisions, where the ADR left a choice:
|
||||
The tests are `crates/zset/tests/circuit.rs`; the rivals and where they failed are in
|
||||
`context/test-evidence/zset.md`.
|
||||
|
||||
A panic inside `step` (a weight overflow in an operator, say) leaves the circuit unusable:
|
||||
nodes ahead of the panic have updated their state and the rest have not, and there is no
|
||||
rollback. Drop the circuit and build another. ADR 009 clause 11's per-command snapshot and
|
||||
restore is the host's job, not this crate's; `zset-ffi` poisons the circuit for this reason.
|
||||
## Transactions (improvise-bw4p.5)
|
||||
|
||||
A panic inside `step` (a weight overflow in an operator, say) leaves nodes ahead of the panic
|
||||
updated and the rest not. ADR 009 clause 11 says each command snapshots the circuit for
|
||||
rollback; `Circuit::begin`, `commit` and `rollback` are that, and the ADR is not amended (the
|
||||
clause's wording stands; this is how the crate reads it).
|
||||
|
||||
1. **An undo log, not a snapshot.** The ADR budgets memory, and a clone of the circuit's state
|
||||
is the size of the circuit. `begin` instead makes every stateful node start logging, and
|
||||
the log holds what the steps touch: the cost of a transaction is the keys a step touches,
|
||||
not the circuit's size (`a_transaction_costs_the_keys_a_step_touches_and_not_the_size_of_the_circuit`
|
||||
measures it in key clones: 16 extra for `begin; step; commit`, 22 for `rollback`, the same at
|
||||
10 and at 300 keys of state, with an `integrate` in the pipeline). Outside a transaction
|
||||
nothing is logged and nothing extra is cloned. Two costs are the circuit's size, and are
|
||||
limits, not features:
|
||||
- **A split tick.** A `step_continue` that is the first publish of an edge in a transaction
|
||||
clones that edge's whole value (2009 key clones against 1006 outside one, at N=1000;
|
||||
`a_split_tick_in_a_transaction_costs_the_size_of_the_edge`).
|
||||
- **Memory held until `commit`.** Every edge's previous value is moved into the slot's undo
|
||||
record and kept, so an `integrate -> delay` pipeline holds 4022 live keys during a
|
||||
transaction against 2014 without one (N=1000). An integrate edge is back to three copies
|
||||
of its integral for the length of the transaction.
|
||||
2. **What is logged, per node.** Each integrated Z-set (`integrate`, `distinct`, a sink's sum)
|
||||
keeps `(key, weight)` for every addition it applied; each trace (the join's two, the
|
||||
aggregate's groups) keeps `(key, value, weight)` for every `apply`, through `Undoable`, a
|
||||
wrapper over the caller's `Trace`; a `Delay` keeps one clone of what it holds on its first
|
||||
eval, which is the previous tick's input; a `Source` keeps a clone of what was pending at
|
||||
`begin`; an edge (`Slot`) keeps the `(piece, whole)` its first publish replaced, moved and
|
||||
not cloned, except for a continued piece, which clones the edge once. `ticks` is restored.
|
||||
3. **Rollback replays newest first.** Each undo is the exact inverse of an addition that
|
||||
succeeded, so it never leaves `i64`, but only in this order: a key at `MAX` lowered and
|
||||
raised again would reach `MAX + 1` undone oldest first
|
||||
(`rollback_undoes_newest_first_so_no_undo_leaves_i64`). `i64::MIN` has no negation; a
|
||||
trace undoes it as `MAX` then `1` (the weight before was non-negative, so neither leaves
|
||||
`i64`), and a Z-set undoes it by `adjust(.., subtract)`.
|
||||
4. **An entry is built before its change and logged after it.** An overflow panics before a
|
||||
key changes (`insert` is one checked addition), and the entry's clones are made first, so
|
||||
a panicking `Clone` changes nothing either (`c1_a_clone_panic_anywhere_in_a_step_is_rolled_back`
|
||||
sweeps a panic over every key clone in a step). A step that dies half way has therefore
|
||||
logged exactly the keys it applied. A custom `Trace` must do the same: a panicking `apply`
|
||||
leaves the trace as it was. `MemTrace` does, since it makes every clone before it touches
|
||||
its map (`a_panicking_value_clone_leaves_a_memtrace_unchanged`).
|
||||
5. **The edge's two copies.** An integrate stream's piece is also its output, so a second copy
|
||||
(the whole-tick value) only exists while a tick is split. `Slot::whole` is `None` otherwise
|
||||
and `current()` reads the piece. `piece()` lends a borrow rather than a clone
|
||||
(improvise-bw4p.11). An integrate stream now holds its integral twice (the node's `acc`
|
||||
and the stream's piece), not three times; sharing those two needs an `Rc` in the slot and
|
||||
was not done.
|
||||
6. **What a transaction does not undo.**
|
||||
- A closure's captured state (a `map` function that counts, an FFI callback's side
|
||||
effects). Operators that keep state keep it in the crate's own types for this reason.
|
||||
- A `Rebuild`: it owns an iterator over its snapshot, so a rolled-back chunk leaves the job
|
||||
ahead of the circuit. The clock cannot tell: `rollback` rewinds `ticks`, which can make
|
||||
a dead job's recorded tick current again. So the circuit also counts the rollbacks that
|
||||
undid a step or piece (`undone`, never rewound), and a job records the count when it first
|
||||
runs, before its first chunk can panic. The chunk's `push` is marked as a step too, since it
|
||||
can overflow the pending delta before any step runs (`p1_a_chunk_whose_push_panics_in_a_txn_is_counted`). A later count makes `interrupted` true for good,
|
||||
finished or not (`rollback_rebuild.rs`: begun before the transaction and continued inside,
|
||||
finished inside, a first chunk that panicked, and a dead job revived by a later step).
|
||||
- An `Output::take` made inside the transaction: a rollback subtracts the step's output
|
||||
from the sink, which a `take` has emptied. Take after `commit`; `zset-ffi` refuses to take
|
||||
while a transaction is open.
|
||||
7. **Pushes.** `Input::push` is not logged (a handle has no circuit). `rollback` puts the
|
||||
pending delta back to what it was at `begin`, so a push made after `begin` is dropped, and
|
||||
one made before it is pending again. Operators built after `begin` start logging at once
|
||||
and go back to empty; they are not removed.
|
||||
8. **One transaction at a time, and misuse panics** like an overflow does: `begin` while open,
|
||||
`commit` or `rollback` with none open. `zset-ffi` answers with a code instead.
|
||||
|
||||
The tests are `tests/rollback.rs` (the property: a step that panics half way, then a rollback,
|
||||
leaves every stream and sink as before and the later ticks equal to a circuit that never ran
|
||||
the step) and `tests/cost.rs`. A step that panics outside a transaction still leaves the
|
||||
circuit unusable: drop it and build another.
|
||||
|
||||
## Rebuilds and circuits (improvise-bw4p.12)
|
||||
|
||||
A `Rebuild` takes its circuit's identity from its `Input`: the circuit holds an `Rc<()>` and every
|
||||
`Input` it makes holds a clone, so `Rebuild::belongs_to(&circuit)` is a pointer comparison and no
|
||||
global counter is needed. `Rebuild::step` on another circuit panics, where it used to report
|
||||
`Done` and land its chunk in that circuit's next tick. An interrupted job (decision 8 above) can
|
||||
never finish: `interrupted` stays true however many steps follow, because a split tick cannot
|
||||
be mended and a rollback that took a chunk is counted forever (decision 6 above). Drop it and start another job from the same snapshot; the host keeps the
|
||||
snapshot.
|
||||
|
||||
@@ -2380,3 +2380,20 @@ branch reads the owned store; it fails here.
|
||||
|
||||
`set_cell` on a model over a source panics in a debug build, naming the reason. Without the assert the
|
||||
write goes to the owned store and nothing reads it.
|
||||
|
||||
### a_summary_built_from_an_engines_parts_reduces_as_one_built_from_the_values
|
||||
|
||||
Review of #356 (Codex): an engine outside core could not build a `Summary` without replaying rows. The
|
||||
parts (count, exact sum, extremes, agreement of the non-numbers) are computed in the test without
|
||||
`Summary::of`, for the 585 sequences of the reference test. Rivals: the greatest taken from the least;
|
||||
a NaN allowed as an extreme. Each fails it.
|
||||
|
||||
### parts_that_contradict_themselves_are_made_consistent
|
||||
|
||||
Extremes with no numbers, and a NaN as an extreme, are dropped by `Numbers::from_parts`.
|
||||
|
||||
### keys_of_a_store_are_its_cells_keys_without_the_values
|
||||
|
||||
Review of #356 (Codex): `DataStore::keys` went through `cells` and cloned every value. It reads keys
|
||||
only now; the test pins the keys and their order against `cells`. No clone-count test: a value clone is
|
||||
not observable from outside, so the equality is all that can be asserted.
|
||||
|
||||
@@ -172,3 +172,23 @@ host, and the old reply then arrives. Rival: the `left` check removed.
|
||||
every restart and swap. Rival: the `left` check removed fails it. The older-generation guard on its own is
|
||||
not separable from `left` in the histories the property reaches, so it is held by
|
||||
`a_late_window_reply_from_an_older_generation_does_not_regress` alone.
|
||||
|
||||
## The left-epoch livelock
|
||||
|
||||
### a_late_reply_from_a_host_the_client_never_joined_cannot_strand_it
|
||||
|
||||
The property test failed with `Exhausted` on a shrunk history of two restarts and four writes. Cause: the
|
||||
client was on host 3, never having joined host 2; a late host-2 reply was applied (an unknown epoch is
|
||||
accepted), which wrote host 3 into `left`, and every later answer from the live host 3 was then refused as
|
||||
a duplicate. The test replays that history by hand: three hosts, the host-2 reply lost in flight, the client
|
||||
settling on host 3, the late reply applied, the connection lost, and a sync that must settle on host 3's
|
||||
grid. Rival: `apply_answer` treated like `apply` (the `left.retain` removed) fails this test. **The random
|
||||
property does not catch it**: it passed 11 of 11 runs under that fault, and again after the late reply was
|
||||
made an explicit event (a stashed reply from a host the client never joined, replayed before a lost
|
||||
connection), because the property rarely produces a reply from a host the client never joined. This
|
||||
test is the pin. Rival: the left-epoch guard removed fails
|
||||
`a_reply_held_across_a_host_restart_cannot_pull_the_client_back` and the property, as before.
|
||||
|
||||
The property's invariant changed with it. "The watermark never returns to an epoch it left" was false by
|
||||
design once an unknown-epoch reply can move the client, so the property now checks the narrower, true
|
||||
rule: a replayed reply from an epoch the client was in and has left must be a duplicate.
|
||||
|
||||
@@ -166,3 +166,58 @@ A job outlives its circuit; sixty-four new circuits (some at the old address) al
|
||||
|
||||
Retyping `ZsKeepFn`'s return in the header fails. The `unary_op!` signatures are now read
|
||||
from the macro body rather than written into the test.
|
||||
|
||||
## Transactions (improvise-bw4p.5)
|
||||
|
||||
Rivals were injected one at a time in `engine.rs` and watched fail by name; Miri passes on `abi`.
|
||||
|
||||
### a_rollback_after_a_failed_step_revives_the_circuit_in_its_old_state
|
||||
|
||||
An integrate held at `i64::MAX`; inside a transaction a step overflows (`ZS_ERR_OVERFLOW`, then
|
||||
`ZS_ERR_POISONED`), `commit` of it is refused as poisoned, and `rollback` revives the circuit with
|
||||
the integral where it was: `-1` then gives `MAX - 1`, with neither the failed `+1` nor the key
|
||||
added beside it. Rivals: a rollback that leaves the poison on, and one that does not roll the
|
||||
circuit back, fail this test and the callback one; a `commit` that does not check the poison
|
||||
fails this test.
|
||||
|
||||
### a_committed_transaction_keeps_its_steps_and_a_new_one_may_follow
|
||||
|
||||
`commit` keeps the step and its sink, and a later transaction can be opened and rolled back.
|
||||
|
||||
### a_failed_callback_step_is_rolled_back_too
|
||||
|
||||
A failure the callback only reports (the step returns, the fault is noted) is rolled back like a
|
||||
panic: the sink holds nothing after the rollback.
|
||||
|
||||
### transaction_misuse_is_a_code_and_changes_nothing
|
||||
|
||||
`ZS_ERR_TRANSACTION` for `commit` or `rollback` with none open, a second `begin`, and a `take`
|
||||
while one is open (nothing written to the out-pointer). A rollback after a poison from outside any
|
||||
transaction is also refused and the circuit stays poisoned. Rivals: `take` allowed in a
|
||||
transaction, and a second `begin` allowed, each fail this test.
|
||||
|
||||
## Review of #355 at 51438911
|
||||
|
||||
### f1_rebuild_begun_before_a_txn_continued_inside_and_rolled_back
|
||||
|
||||
Through the ABI, a job continued inside a rolled-back transaction returned 0 with `done` 1 and
|
||||
a partial load. It is now `ZS_ERR_INTERRUPTED`.
|
||||
|
||||
### f4_a_failed_rebuild_step_in_a_txn_then_rollback_then_resume
|
||||
|
||||
A job whose first chunk failed inside the transaction resumed without that chunk; now
|
||||
`ZS_ERR_INTERRUPTED`.
|
||||
|
||||
### f2_a_rollback_from_inside_a_callback_is_refused_and_the_txn_stays_open
|
||||
|
||||
`ZS_ERR_POISONED` from the callback's rollback, and the transaction still commits.
|
||||
|
||||
### f3_begin_on_a_circuit_poisoned_outside_a_txn_is_poisoned
|
||||
|
||||
`begin` is `ZS_ERR_POISONED`; `commit` and `rollback` are `ZS_ERR_TRANSACTION`.
|
||||
|
||||
### f5_a_chunk_whose_push_overflows_in_a_txn_then_rollback_is_interrupted
|
||||
|
||||
The same path through the ABI: `zs_rebuild_step` returns `ZS_ERR_OVERFLOW` from the chunk's
|
||||
push, `zs_circuit_rollback` succeeds, and the next `zs_rebuild_step` was a silent success; it is
|
||||
now `ZS_ERR_INTERRUPTED`. Rival: the mark before the push removed fails `[f5]`.
|
||||
|
||||
@@ -429,3 +429,170 @@ A second job's first chunk is a tick, so the first job's next call panics.
|
||||
### a_finished_rebuild_and_an_interrupted_check_do_not_trip_on_later_ticks
|
||||
|
||||
A finished job is never interrupted, and steps afterwards do not make it panic.
|
||||
|
||||
## `crates/zset/tests/{cost,rollback,rebuild}.rs`: rollback, the borrowed piece, the bound rebuild (improvise-bw4p.5, .11, .12)
|
||||
|
||||
Every rival below was injected one at a time and watched fail by test name (and tag where one
|
||||
exists) before being reverted; the whole suite was re-run clean afterwards. Costs are counted
|
||||
in key clones and live keys of a `Counted` key type, never in time, so they hold on any machine.
|
||||
|
||||
### an_eval_borrows_its_input_instead_of_cloning_it
|
||||
|
||||
bw4p.11. `input -> map(|k| k.0) -> output` over 100 keys makes **0** key clones in a step; before
|
||||
the change it made 200 (the source's whole-tick copy and `piece()`'s clone). Rival: `Unary::eval`
|
||||
clones the piece again fails `[piece]`.
|
||||
|
||||
### an_integrate_stream_holds_its_integral_twice_when_the_tick_is_whole
|
||||
|
||||
bw4p.11. After one step an `input -> integrate` pipeline holds 3N live keys (the input's
|
||||
piece, the integral, the integrate stream's piece), where it held 5N before: the whole-tick copy
|
||||
that duplicated the piece is kept only while a tick is split (`Slot::whole` is an `Option`).
|
||||
Rival: a publish that always stores `whole = Some(v.clone())` fails `[whole]` (and the clone test).
|
||||
|
||||
### a_transaction_costs_the_keys_a_step_touches_and_not_the_size_of_the_circuit
|
||||
|
||||
bw4p.5. A pipeline with `distinct`, `delay`, `join_indexed`, `aggregate` and three sinks is
|
||||
loaded with 10, then 300 keys, then given a two-key delta in each of two inputs. The extra key
|
||||
clones of `begin; step; commit` over the same step outside a transaction are **16** at both
|
||||
sizes (22 for `rollback`; the plain step is 20). Rival: `DistinctState::begin` clones what it
|
||||
holds (a snapshot of the world) fails `[cost]` with 28 against 318. A `delay` clones what it
|
||||
holds, the previous tick's input, so the test steps a small delta after the load. Review of
|
||||
#355: the pipeline now includes an `integrate`; a rival `Acc::begin` that clones the integral
|
||||
fails `[cost]`. (An `integrate` whose output is sunk is left out: its output is the integral,
|
||||
so the sink logs all of it, which is the delta and not an overhead.)
|
||||
|
||||
### a_rolled_back_step_leaves_the_circuit_as_it_was_and_the_ticks_after_unchanged
|
||||
|
||||
bw4p.5, the property. A rig with every stateful operator (integrate, delay, differentiate,
|
||||
distinct, join, aggregate, plus and eight sinks) runs a random prefix, then a key preloaded at
|
||||
`i64::MAX - 1`. The failing step adds `(0,0): 1` and then `BIG: 5`, so operators have applied
|
||||
the first key when the second overflows (the test asserts the step panicked iff it was meant
|
||||
to). After `rollback`, every stream's `current()` and every sink equal what they were (`[rollback]`),
|
||||
and the ticks after equal a reference circuit that never saw the step (`[post]`). The same test
|
||||
rolls back a step that succeeds. `carry` is pending at `begin` and must stay pending.
|
||||
Rivals, each failing this test: rollback that skips every node (`[rollback]`, and
|
||||
`an_operator_built_inside_a_transaction_goes_back_to_empty`); an integrate log not undone
|
||||
(`[post]`); a stream slot not restored (`[rollback]`); a `delay`'s held value not restored
|
||||
(`[post]`); a source's pending delta not restored (`[post]`); a sink not undone (`[rollback]`);
|
||||
`DistinctState` not undone (`[post]`); a trace not undone (`[post]`); an undo that drops the sign
|
||||
(`[post]`); a log that records nothing (`[rollback]`, `[built]`).
|
||||
|
||||
### a_committed_transaction_equals_the_same_steps_outside_one
|
||||
|
||||
bw4p.5. A circuit that commits some of its steps equals one that never opened a transaction,
|
||||
state and output, tick by tick. Rival: `commit` rolls back fails `[commit]`.
|
||||
|
||||
### rollback_undoes_the_clock
|
||||
|
||||
bw4p.5. A rolled-back step does not count as a tick. Rival: `ticks` not restored fails `[ticks]`.
|
||||
|
||||
### an_operator_built_inside_a_transaction_goes_back_to_empty
|
||||
|
||||
bw4p.5. An `integrate` built after `begin`, stepped, then rolled back, forgets the step
|
||||
(`[built]`). Without the "a node built in a transaction starts recording" rule it kept it.
|
||||
|
||||
### rollback_undoes_newest_first_so_no_undo_leaves_i64
|
||||
|
||||
bw4p.5. A key at `i64::MAX` lowered by one and raised by one in one transaction. Undone oldest
|
||||
first the first undo would reach `MAX + 1` and panic; undone newest first nothing leaves
|
||||
`i64`. Rival: the log replayed oldest first fails this test (and no other: the property above
|
||||
cannot see it, since its keys never sit at the boundary).
|
||||
|
||||
### a_minimum_weight_applied_to_every_kind_of_state_is_taken_back
|
||||
|
||||
bw4p.5. `i64::MIN` has no negation, so a trace undoes it as `i64::MAX` then `1`. Rival: the
|
||||
second application dropped fails `[min]`.
|
||||
|
||||
### a_second_begin_is_refused_loudly
|
||||
|
||||
bw4p.5, with `a_rollback_with_nothing_open_is_refused_loudly` and
|
||||
`a_commit_with_nothing_open_is_refused_loudly`: misuse panics, as an overflow does.
|
||||
|
||||
### a_rebuild_stepped_on_a_foreign_circuit_is_refused_loudly
|
||||
|
||||
bw4p.12. A job made from circuit A's input, stepped on circuit B, used to report Done and land
|
||||
its chunk in B's next tick. It now panics. Rival: the check removed fails this test.
|
||||
|
||||
### a_rebuild_knows_the_circuit_its_input_came_from
|
||||
|
||||
bw4p.12. `Rebuild::belongs_to`, the question a host asks before the panic. Rival: always true
|
||||
fails `[owner]`.
|
||||
|
||||
### an_interrupted_rebuild_stays_interrupted_and_a_new_job_loads_the_snapshot
|
||||
|
||||
bw4p.12. Documents, and pins, that an interrupted job can never finish: later steps never
|
||||
clear it, and a new job over the same snapshot loads it. It did not fail before: the behaviour
|
||||
was right and unstated.
|
||||
|
||||
## Review of #355 at 51438911 (improvise-bw4p.5, .12)
|
||||
|
||||
An adversarial review found a rebuild across a rollback losing data, a panicking `Clone`
|
||||
mutating unlogged state, and two cost claims that did not hold. Its reproductions are adopted
|
||||
as tests; each rival below was injected and watched fail by name.
|
||||
|
||||
### r1_rebuild_begun_before_txn_continued_inside_then_rolled_back_reports_interrupted
|
||||
|
||||
A job begun outside a transaction and continued inside, then rolled back, was not interrupted;
|
||||
finishing it gave `{1,3,4}` for the snapshot `{1,2,3,4}`. Rival: `rollback` does not count the
|
||||
undone step fails this and r2 to r4.
|
||||
|
||||
### r2_rebuild_finished_inside_a_rolled_back_txn_is_reported_done_with_nothing_loaded
|
||||
|
||||
A job that finished inside a rolled-back transaction was Done with an empty integral and not
|
||||
interrupted.
|
||||
|
||||
### r3_an_interrupted_rebuild_resurrects_after_rollback_and_a_later_step
|
||||
|
||||
`rollback` rewinds `ticks`, so a later `step` made a dead job's recorded tick current again and
|
||||
it continued without its first chunk.
|
||||
|
||||
### r4_rebuild_whose_first_chunk_panics_in_a_txn_then_rolled_back
|
||||
|
||||
A first chunk that panicked left `began_at` unset, and the job resumed without it. The count is
|
||||
now recorded before the chunk runs. Rival: recording it never (the `get_or_insert` removed)
|
||||
fails all four; a rival recording it after the chunk was not run separately.
|
||||
|
||||
### b1_a_closure_that_reads_a_stream_during_eval_does_not_panic
|
||||
|
||||
The borrowed `piece()` does not conflict with a closure that reads streams during an eval,
|
||||
including its own source, inside a transaction. It passed before and after.
|
||||
|
||||
### c1_a_clone_panic_anywhere_in_a_step_is_rolled_back
|
||||
|
||||
Sweeps a panic over every key clone of one transactional step through `integrate`, `distinct`,
|
||||
`join`, `delay`, `aggregate` and sinks; 138 panic points left state that differed after the
|
||||
rollback. The post-rollback tick now pushes the keys the failed step touched, because a leaked
|
||||
key is only visible when it is touched again (a rival that mutated `DistinctState` before
|
||||
cloning its entry survived the first version). Rivals, each failing it: `add_logged`,
|
||||
`DistinctState::step` and `Undoable::apply` each mutating before cloning the entry.
|
||||
|
||||
### a_panicking_value_clone_leaves_a_memtrace_unchanged
|
||||
|
||||
`MemTrace::apply` inserted an empty group before cloning the value. Rival: that order restored
|
||||
fails `[c2]`.
|
||||
|
||||
### reviewer_rollback_matches_a_circuit_that_never_ran_the_step
|
||||
|
||||
The reviewer's model-based property (random circuits over every public operator, a custom
|
||||
panicking trace, random push/step/continue/begin/commit/rollback histories, operators built in
|
||||
a transaction), at the default 256 cases here (30,000 passed in review). Rival: the continued
|
||||
path saving the slot without its `whole` fails it.
|
||||
|
||||
### a_rollback_across_a_split_tick_restores_the_whole_value
|
||||
|
||||
The tick is split before the transaction opens, so every edge holds a `whole` when the first
|
||||
continued piece saves it. Rival: that save dropping `whole` fails `[split]` (an earlier version
|
||||
split the tick inside the transaction and never reached the save).
|
||||
|
||||
### a_split_tick_in_a_transaction_costs_the_size_of_the_edge
|
||||
|
||||
Pins the limit `zset.md` states: a first continued piece in a transaction clones the edge's
|
||||
whole value, growing with the state.
|
||||
|
||||
|
||||
### p1_a_chunk_whose_push_panics_in_a_txn_is_counted
|
||||
|
||||
Delta review of #355 at b2445fed. `Rebuild::step` takes the chunk from its iterator and pushes
|
||||
it before stepping; a push that overflows the pending delta panicked with no step run, so
|
||||
`undone` was not bumped and the resumed job silently dropped the chunk (key 1's `+1`). The step
|
||||
is now marked before the push. Rival: that mark removed fails `[p1]`.
|
||||
|
||||
Reference in New Issue
Block a user