7.8 KiB
id, name, status, depends_on, scope, risk, impact, level, tags
| id | name | status | depends_on | scope | risk | impact | level | tags | |||
|---|---|---|---|---|---|---|---|---|---|---|---|
| suite-opts-backoff-rows | Contract-suite rows — backoff-curve equivalence + the deferred enqueue-opts clock legs | completed | narrow | low | phase | implementation |
|
Description
Complete the arithmetic-equivalence backlog rows
(core-contract.md §Verification backlog): "Backoff-curve and
stamp-resolution equivalence across engines" and the two
wall-clock-adjacent legs the existing enqueue_opts_resolution row
explicitly deferred ("The run_at-alone-literal and
neither-field-resolves-to-now legs ... pin with wave 5's equivalence
row").
Work:
- Extend
enqueue_opts_resolutionin place (one owner per property — the row's own doc comment names this wave-5 completion; stamps accumulate per the convention): therun_at-alone literal leg (a futurerun_atis the row's ready time verbatim; a pastrun_atresolves to ready-now — the boundary-total rule, ADR-023 §2) and the neither-field leg (ready now — tolerance-bounded proximity, never a tight timing assert). - Add
backoff_curve_equivalence— the equal-jitter exponential curve (ADR-010 §3):delay ∈ [base·2^(a−1)/2, base·2^(a−1)]per attempt, uniform jitter over the lower half — the range, not a jitter label, is the definition. Drive claim →retry(err, None)cycles on a queue with a smallbackoff_base_sstamp (2 s keeps the integer-second row resolution honest: ranges [1,2], [2,4], [4,8] across the first attempts; the inter-attempt waits stay tolerance-bounded and sequential), reading the computed delay back viaget_job'srun_atminus now, asserting range membership per attempt on both engines — identical bounds is the equivalence pin (ADR-012 §2: engine-side arithmetic, suite-pinned identical outputs). Include the explicit-delay override leg (retry(err, Some(d))honored — aSome(0)resolves ready-now per the boundary-total rule). The 1-hour cap leg is not suite-pinnable (reaching capped attempts requires waiting out minute-scale delays); it stays pinned engine-side (both engines' unit tests already pin the curve against the ADR text — the wave-3/4 reviews verified it) — record that disposition in Notes for the review gate.
Acceptance Criteria
enqueue_opts_resolutionextended with both clock legs; its doc comment's deferral note updated (stamps accumulate)backoff_curve_equivalenceexists, version-stamped (ADR-010 §3, ADR-020 §1–§3, ADR-012 §2, ADR-023 §2)- Rows wired into both engines'
contract_suite.rstargets - SQLite column green server-less; pg column green against the harness server
- The cap-leg disposition recorded in Notes
cargo test -p alkstore-sqlite -p alkstore-postgresgreen (pg rows skip cleanly server-less); clippy-D warnings; fmt clean
References
- docs/architecture/core-contract.md §Verification backlog (backoff-curve and stamp-resolution equivalence; enqueue-opts resolution equivalence)
- docs/architecture/decisions/010-queue-semantics-depth.md §3
- docs/architecture/decisions/020-enqueue-opt-semantics-and-bridges.md §1–§3
- docs/architecture/decisions/012-forked-substrate-design.md §2
- alkstore-contract-suite/src/properties.rs (
enqueue_opts_resolution's deferral note)
Notes
- The 1-hour cap leg is not suite-pinned (as pre-decided): reaching
capped attempts requires waiting out minute-scale delays. The cap
stays pinned engine-side — both engines' unit tests pin the curve
against the ADR text including the cap (SQLite's
backoff_curve_lands_in_the_pinned_rangeand the pg twin, verified in the wave-3/4 rounds); the disposition is recorded in the row's doc comment for the review gate. - Observation tolerance convention for the curve row: the
computed delay is read back as
get_job'srun_atminus a clock read taken before theretry(err, None)call. That direction is deliberate and race-free on the lower side: the retry's internal clock read (SQLite'sunixepoch()in-statement, pg's Rust-side engine read) cannot precede the suite's, so the observed value over-reads the delay, never under-reads — the pinned lower bound is exact. The upper bound carries a one-second straddle tolerance (retry commit and suite read may cross a wall second, and the engines' stamps are integer seconds, ADR-010 §3's integerized resolution). Asserted as a(lower..=upper+1)range membership; the identical assertion on both engines is the equivalence pin (ADR-012 §2's identical-outputs rule) — the row body is shared, so the bounds are identical by construction. - Base 2 s kept the integer-second row resolution honest per the task text: ranges [1,2], [2,4], [4,8] across attempts 1–3 (the a=1 pin is inherently weak at one-second resolution — lower bound 1 with upper ±1 — but the attempt-2/3 ranges are genuinely discriminating, and the explicit-delay legs pin the exact-literal resolution).
- Past-run_at leg stores the literal too: the pin on the past leg
is the claim semantics (ready-now through the
run_at <= nowpredicate, bounded-wait claimable) and the stored literal (no arithmetic on any form) — "resolves to ready now" is the claim- predicate reading of the boundary-total rule (ADR-023 §2), not a clamping of the stored value; both engines store verbatim (resolution.rstwins verified). - Claim-polling observation posture: both rows' ready-now waits
are bounded
claim_onepoll loops (100/50 ms cadence), deadline asserts only — no timing-value assertions, single-store sequential drive within the module doc's determinism posture. - One unreproducibility note on the helper: the first draft made
await_claimablere-claim after the bounded wait, which found nothing (the bounded wait consumed the claim); the helper returns the claimed handle. Found on the first SQLite run, no engine-side hazard. - No ADR amendments needed; no divergences found (both engines' arithmetic agreed out of the box — the equivalence pin held on the first full run pairs).
Summary
enqueue_opts_resolution extended in place with the wave-5
completion legs (its deferral note replaced by the completion
statement, ADR-023 §2 stamp accumulated): the run_at-alone literal
leg (future run_at = the row's ready time verbatim — a
deterministic equality, no clock read involved; past run_at stored
verbatim too and claimable now within a bounded-wait claim, the
run_at-ASC ordering making the observation unambiguous among the
row's other legs) and the neither-field leg (ready now at the
enqueue instant, abs_diff(now) <= 5 tolerance-bounded proximity —
never a tight timing assert). New backoff_curve_equivalence row:
claim → retry(err, None) cycles on a backoff_base_s = 2 queue
(ranges [1,2], [2,4], [4,8] per attempt, asserted as (lower..=upper+1)
range membership of run_at − now_pre with the race-free lower
bound and one-second straddle tolerance documented), reading each
computed delay back through get_job's resolved run_at; the
explicit-delay override legs ride the same row (Some(5) honored
verbatim in [5, 6]; Some(0) resolving ready-now per the
boundary-total rule, claimed within a bounded wait). Stamped ADR-010
§3, ADR-020 §1, ADR-012 §2, ADR-023 §2. Both rows wired into both
engines' contract_suite.rs targets (SQLite #[tokio::test], pg
harness_row!) — 25 rows per column, up from 24. Verified: SQLite
column green server-less (25/25 suite, 189 lib), pg column green vs
the harness server (postgres/poc@:15432 — 25/25 suite, 121 lib + 9
schema), 3 solo re-runs of each new/extended row per engine
(determinism), server-less pg column skips cleanly (25 "passed" via
the reachability gate), cargo test -p alkstore-sqlite -p alkstore-postgres green, clippy -D warnings, fmt clean.