feat(network): sound cycle-quantized long-link CQF bound + synthesizer (REQ-TSN-SYNTH-CQF-LONGLINK-001)#311
Merged
Merged
Conversation
…cles (REQ-TSN-SYNTH-CQF-LONGLINK-001)
Soundness core of the long-link CQF delay bound (the prior spec was UNSOUND —
its interval inverted on long links). Model finalized from draft-ietf-detnet-tcqf
/ draft-eckert-detnet-tcqf-05, advisor-confirmed:
- cqf_hop_advance_cycles: k_i = 2 + floor((d_i − DT)/T_c) (Euclidean div). Dead
time DT sits at the cycle END so it EASES same-cycle delivery — it subtracts.
d_i < DT ⇒ k_i = 1 (classic single-cycle hop).
- cqf_delay_max_longlink_ps: D_max = T_c + T_c·Σ k_i(d_i^max).
- cqf_delay_min_longlink_ps: D_min = T_c·Σ_{i<H} k_i(d_i^min) (H−1 intermediate
hops + last-hop floor 0). The asymmetry makes (H±1)·T_c emerge AND guarantees
D_min ≤ D_max always (prior spec inverted for lack of the last-hop term).
- cqf_cycle_budget_bits_with_dead_time: csize = (T_c − DT)·rate (only the
transmittable window; collapses to shipped T_c·rate at DT=0).
- cqf_buffer_count + LinkDelay: B = max(3, max_i((k_i^max−k_i^min)+2)); Err past
the 7-cycle cap (never a silent down-clamp → no undersized buffers).
3 non-circular oracles (all green): (A) degeneracy — all d_i<DT reproduces the
externally-pinned shipped (H±1)·T_c (24-hop→250/230µs); (B) discrimination —
3-hop [1,25,8]µs gives D_max=80µs while naive (H+1)T_c=40µs under-bounds it 2×;
(C) optimism/inversion guard — H=2 both 15µs gives 70µs>naive 30µs, plus a grid
property asserting D_min≤D_max never inverts. csize + buffer oracles too.
Additive API only (functions not yet wired into synthesize_cqf / the AADL
bridge — that integration + requirement rewrite follows). 12 cqf tests pass;
clippy clean.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…Q-TSN-SYNTH-CQF-LONGLINK-001)
Integration layer over the cycle-quantized bound core:
- CqfFlow gains `link_delays: Vec<LinkDelay>` (per-hop min/max one-way latency),
parallel to `path`. EMPTY = all-short, so existing `synthesize_cqf` and the
AADL bridge are unchanged (backward compatible).
- `synthesize_cqf_longlink(flows, rate, dead_time_ps, buffer_cap)` →
`CqfLongLinkSchedule { cycle_time_ps, dead_time_ps, csize_bits, per_link_bits,
buffers }`. Baseline scope = the "cycle dominates links" regime (T_c > every
link ⇒ k_i ∈ {1,2}, D_max monotonic in T_c, closed-form cycle selection). It
picks the largest whole-ns T_c meeting every flow's long-link D_max ≤ deadline,
admits against csize=(T_c−DT)·rate, sizes buffers, and self-certifies against
the exact bound before returning. Deadlines that would need a cycle SHORTER
than a link (multi-cycle-per-hop regime) return LongLinkDeadlineTooTight rather
than an unsound config — that regime is a documented follow-up.
- New errors: DeadTimeTooLarge, LinkDelayLenMismatch, BufferBudgetExceeded,
LongLinkDeadlineTooTight. (In the cycle-dominates regime buffers are always the
3-cycle floor, so BufferBudgetExceeded only fires on a misconfigured cap<3.)
4 synth oracles (feasible-in-regime, sub-link-cycle rejection, all-short matches
hop-count synthesize_cqf, buffer/len-mismatch guards) + the 5 bound oracles all
green. 165 spar-network + 899 spar-analysis tests pass; clippy + fmt clean.
Follow-up: the AADL bridge (cqf_synth.rs) still emits empty link_delays; reading
per-hop Spar_Network::Latency to feed the long-link path end-to-end is next.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…spec + TEST-TSN-SYNTH-CQF-LONGLINK
Rewrites the requirement from the deferred UNSOUND spec (interval inverted on
long links) to the finalized cycle-quantized model: kᵢ=2+⌊(dᵢ−DT)/T_c⌋,
D_max=T_c+T_c·Σkᵢ(dᵢᵐᵃˣ), D_min=T_c·Σ_{i<H}kᵢ(dᵢᵐⁱⁿ) (asymmetry ⇒ no
inversion), jitter-keyed buffers, csize=(T_c−DT)·rate; degeneracy dᵢ<DT ⇒
(H±1)·T_c. Status → implemented, release v0.23.0. Adds TEST-TSN-SYNTH-CQF-LONGLINK
(satisfies + verifies) documenting the 3 non-circular oracles. Both CI rivet
gates (v0.4.3, v0.7.0) PASS.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…dness (REQ-TSN-SYNTH-CQF-LONGLINK-001)
The three existing long-link oracles (degeneracy, discrimination, inversion
guard) all re-apply the kᵢ = 2 + ⌊(dᵢ−DT)/T_c⌋ closed form, so a subtle
optimistic error (wrong sign, floor direction, off-by-one) could pass every
one of them AND survive mutation. Add an INDEPENDENT discrete-event
simulation oracle (longlink_dmax_upper_bounds_discrete_event_sim) that plays
frames through an explicit CQF cycle timeline deriving each hop's advance from
floor(arrival/T_c) — never calling the k formula — and asserts D_max upper-
bounds every observed delay across a full-cycle source-phase sweep over
profiles driving kᵢ ∈ {1..4}. This is the anti-optimism gate; a clean-room
re-derivation (delay = T_c·Σk + (ρ−φ) < T_c·(1+Σk)) plus a 200k-config ×
97-phase sweep found 0 violations.
Mutation-harden the long-link functions to 0-missed: add targeted oracles for
the d==DT boundary (k=2 not 1), tie-break flow-id selection, admission
oversubscribe + exact-csize boundary, per-field degeneracy disjunction,
self-cert slack-below-deadline, and inclusive buffer cap.
Also harden the co-located v0.20 hop-count CQF baseline (surfaced by full-file
mutation since the file is under change): Display coverage for every
CqfSynthError variant, and an exact-csize admission-boundary test that kills
the oversubscription `>`→`>=`/`==` mutants in both synthesize_cqf and
self_check. Accepted survivors documented inline: the min_by_key diagnostic
id-selection (417/419, cosmetic — only names which flow appears in a
DeadlineTooTight message) and the whole-body self_check replacement (461,
equivalent — a defensive guard unreachable on a filtered schedule).
Reword D_min honestly: it is the draft's nominal (H−1)·T_c figure, NOT a
universal lower bound (a frame released just before a boundary is delivered a
fraction of T_c sooner — the sim reaches 49µs where D_min=50µs). Safe because
D_min has NO buffer-sizing or minimum-latency consumer (only the lib re-export
for jitter reporting); buffers key off per-hop k. Artifacts updated to match:
D_max soundness now validated by the independent sim rather than asserted
"advisor-confirmed".
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Rivet verification gate✅ 20/20 passed
Filter: Failed artifacts(none) Updated automatically by |
Codecov Report❌ Patch coverage is
📢 Thoughts on this report? Let us know! |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
What & why
The shipped hop-count CQF bound
(H±1)·T_cis optimistic once a link's one-way latency is significant relative to the cycle (long / WAN DetNet links): a frame can miss the next cycle boundary and be delayed by extra whole cycles. This rebuilds long-link CQF on a sound cycle-quantized model (draft-ietf-detnet-tcqf / draft-eckert-detnet-tcqf-05), superseding the earlier spec whose interval inverted on long links.Per-hop cycle advance
kᵢ = 2 + ⌊(dᵢ − DT)/T_c⌋(Euclidean division; dead timeDTat the cycle end subtracts). Bounds:D_max = T_c + T_c·Σᵢ kᵢ(dᵢᵐᵃˣ)— the safety-critical upper boundD_min = T_c·Σ_{i<H} kᵢ(dᵢᵐⁱⁿ)— nominal(H−1)·T_cfigure (see disclaimer below)Admission budget shrinks by the dead time:
csize = (T_c − DT)·rate. Buffers key off jitterBᵢ = (kᵢᵐᵃˣ − kᵢᵐⁱⁿ) + 2,B = max(3, maxᵢ Bᵢ), Err past cap — never a silent down-clamp.synthesize_cqf_longlinkserves the cycle-dominates regime (T_c > every link), self-certifies against the exact bound, and returnsLongLinkDeadlineTooTightrather than an unsound config when a deadline would need sub-link cycles.Falsification statement
This is the anti-optimism gate that the three algebraic oracles (degeneracy, discrimination, inversion-guard) cannot provide on their own — they all re-apply the same
kᵢformula, so a sign/floor/off-by-one error would pass every one of them. A clean-room re-derivation (delay = T_c·Σk + (ρ−φ) < T_c·(1+Σk)) plus a 200k-config × 97-phase sweep independently confirmed 0 violations.D_min is not a universal lower bound (disclosed)
D_minis the draft's nominal figure, not a guaranteed floor: a frame released just before a boundary is delivered a fraction ofT_csooner than it returns (sim reaches 49 µs whereD_min= 50 µs). This is safe becauseD_minhas no buffer-sizing or minimum-latency consumer (verified by workspace grep — only thelib.rsre-export for jitter reporting); cyclic buffers key off per-hopk.Verification
cargo test -p spar-network --lib cqf→ 25 passed; clippy clean; fmt clean.min_by_keydiagnostic id-selection (419×4 — cosmetic, only names which flow appears in aDeadlineTooTightmessage) and the whole-bodyself_checkreplacement (461 — equivalent, a defensive guard unreachable on an already-filtered schedule). Documented inline.Displaycoverage for everyCqfSynthErrorvariant + an exact-csizeadmission-boundary test that kills the oversubscription>→>=/==mutants in bothsynthesize_cqfandself_check.Scope
Sound baseline only. The sub-link multi-cycle-per-hop regime and wiring the AADL bridge (
cqf_synth.rs) to read per-hopSpar_Network::Latencyare documented follow-ups (the bound + synthesizer are library-complete). Not the heterogeneous-cycle ambition (REQ-TSN-SYNTH-CQF-001).🤖 Generated with Claude Code