Repository navigation
fix(latency): #455 items 2 and 3 — a flow's own budget, a real best case and its minimum; descent into a process's flow implementation - #488
Merged
Conversation
Rivet verification gate✅ 20/20 passed
Filter: Failed artifacts(none) Updated automatically by |
avrabe
force-pushed
the
fix/latency-flow-own-budget-455
branch
from
October 14, 2026 11:55
f287147 to
5a54939
Compare
avrabe
changed the title
avrabe
changed the title
Codecov Report❌ Patch coverage is
📢 Thoughts on this report? Let us know! |
…uts it #455 item (2), clause (b) of REQ-ANALYSIS-LATENCY-BUDGET-001. Stacked on the range/property-set/severity fix; this is the clause that makes #455's OWN declaration form work, since it wrote the budget in the flow's braces: e2e : end to end flow a.s -> h -> b.k { Latency => 300 ns .. 250 us; }; THE ITEM TREE WAS FINE AND INSTANTIATION DROPPED IT. A probe confirmed the lowering captures a flow-local block in both spellings, bare and `Communication_Properties::`. `EndToEndFlowInstance` simply had no field to carry them, so every analysis could see only the OWNER component — which is not where AADL puts a flow's latency budget. THE FIRST DESIGN WAS REJECTED ON MEASUREMENT. A side-table on `SystemInstance`, like `connection_property_maps`, looked cleaner. It meant editing ~70 exhaustive `SystemInstance` struct literals across a dozen crates and dragging all of them into the diff. A field on `EndToEndFlowInstance` touches 4 construction sites. Counted, not guessed. THE FLOW'S OWN BUDGET WINS, the owner's is the fallback — so models written against the old owner-only lookup keep working. Precedence is pinned in BOTH directions, because each alone passes a wrong precedence: flow met (100 ms), owner would breach (1 ms) -> silent flow breached (10 ms), owner would be met -> Error, "bound 10.000 ms" A flow with NO block must stay empty rather than inherit the owner's properties; otherwise owner-fallback and flow-own become indistinguishable. END TO END, through the CLI, published v0.45.0 against this change: { Latency => 300 ns .. 1 ms; } exit 0 -> exit 1 [ERROR] { Communication_Properties::Latency => 1 ms; } exit 0 -> exit 1 [ERROR] { Latency => 1 ms .. 500 ms; } (met) exit 0 -> exit 0 MUTANTS, each confirmed SURVIVING the suite before its case was written: flow props pushed into a throwaway map only the HIR instantiation test owner-only lookup (the pre-fix code) the 3 flow-budget tests owner takes precedence the precedence PAIR flow-only, owner fallback removed the 4 owner-budget tests `cargo mutants --in-diff` on this increment: spar-analysis 2 mutants (1 caught, 1 unviable), spar-hir-def 2 (1 caught, 1 unviable), 0 missed, end_time populated on both. CI's ratchet covers spar-analysis only. STILL NOT SHIPPED, so the requirement stays `implemented`: the below-minimum check, blocked on REQ-ANALYSIS-LATENCY-BEST-CASE-001 — `best_case_ps` is a sum of worst-case execution times, and a minimum check over it is unsound in exactly the direction it exists for. Verified: cargo test --workspace exit 0, 3242 passed across 102 result lines, zero failures; workspace builds all targets; clippy -D warnings clean on both crates; fmt clean; rivet validate PASS; stale-scope green. Refs #455 Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01BnBWxgVEUPdsBTLNKtrA6Z
… cases REQ-ANALYSIS-LATENCY-BEST-CASE-001, found while implementing #455's budget check, and the blocker for its below-minimum clause. `best_case_ps` was accumulated from `get_execution_time`, whose doc says "worst-case from range". So the LOWER end of every reported latency range was a sum of WCETs. End to end through the CLI, two `20 ms .. 40 ms` devices, published v0.45.0 against this change: [80.000 ms .. 80.000 ms] -> [40.000 ms .. 80.000 ms] The provenance defect class again: a printed figure labelled as something it is not, correct as an upper bound and wrong as a lower one, with nothing downstream able to tell which end was trustworthy. THE UPPER BOUND IS BIT-FOR-BIT UNCHANGED, and that is the change's safety property. Both accessors read the same property and parse the maximum the same way; the `[compute hop]` figure still reports the worst case; and a range whose MINIMUM fails to parse falls back to the old worst-case accessor, so no model loses an execution time it has today. Every upper-bound and budget comparison is therefore untouched. THE SUITE WAS BLIND TO BOTH ENDS. No test used a ranged execution time, so all 944 analysis tests passed on a mutant that made the WORST case take the minimum — an OPTIMISTIC bound on every model with a ranged execution time, the unsafe direction for a timing analysis. Separately, the `[compute hop]` millisecond value had never been asserted anywhere; its only test checked the hop COUNT, over scalar execution times where minimum and maximum coincide. FOUR MUTANTS, each confirmed SURVIVING before its case was written, each now killed by exactly one test: best case takes the max (the original bug) a_ranged_execution_time_gives_a_real_best_case worst case takes the min (OPTIMISTIC) the_worst_case_is_still_the_sum_of_maxima no fallback on an unparseable minimum a_malformed_minimum_does_not_lose_the_execution_time compute hop reports its minimum a_compute_hop_reports_its_worst_case_execution_time `cargo mutants --in-diff` on this increment: 2 mutants, 1 caught, 1 unviable, 0 missed, end_time populated. BEHAVIOUR CHANGE: every reported range with a ranged execution time gets a lower lower bound. Release notes. Verified: cargo test --workspace exit 0, 3246 passed across 102 result lines, zero failures; clippy -D warnings clean; fmt clean; rivet validate PASS. Refs #455 Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01BnBWxgVEUPdsBTLNKtrA6Z
…ase is real The last clause of REQ-ANALYSIS-LATENCY-BUDGET-001, and of #455 item (2). The requirement goes to `verified`: every clause has shipped and is tested. IT WAS WITHHELD ON PURPOSE, AND THE WITHHOLDING WAS TESTED. While `best_case_ps` summed WORST-case execution times, a minimum check over that inflated figure would have stayed silent on real violations — unsound in exactly the direction #455's kill-criterion needs. A test pinned that no below-minimum diagnostic shipped meanwhile. It FAILED the moment this check was added, which is what it existed to do; with the best case now real it is retired, not weakened. THE MESSAGE CLAIMS ONLY WHAT IS KNOWN. `best_case_ps` is a LOWER bound on any realised latency. So `best >= min` GUARANTEES the minimum is met, and `best < min` means the flow CAN complete faster than its budget allows — the diagnostic says "can", not "does". A scalar budget has no minimum and is never checked below. END TO END through the CLI, two 20..40 ms devices (best case 40 ms): { Latency => 50 ms .. 500 ms; } exit 0 -> exit 1 [ERROR] below the declared minimum 50.000 ms { Latency => 40 ms .. 500 ms; } exit 0 -> exit 0 exactly at the minimum meets it { Latency => 30 ms .. 500 ms; } exit 0 -> exit 0 FOUR MUTANTS of the new check, each SURVIVING the suite with the obsolete pin removed and before its own case existed, each now killed by exactly one test: check never fires a_flow_that_can_beat_its_declared_minimum_is_an_error `<` -> `<=` at the boundary a_flow_exactly_at_its_declared_minimum_meets_it scalar max used as a minimum a_scalar_budget_has_no_minimum_to_breach Error downgraded to Warning a_flow_that_can_beat_its_declared_minimum_is_an_error The third would have failed EVERY flow under a scalar budget against its own "minimum". `cargo mutants --in-diff` on this increment: 7 mutants, 4 caught, 3 unviable, 0 missed, end_time populated. Verified: cargo test --workspace exit 0, 3248 passed across 102 result lines, zero failures; clippy -D warnings clean on spar-analysis and spar-hir-def; fmt clean; rivet validate PASS; stale-scope green. Refs #455 Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01BnBWxgVEUPdsBTLNKtrA6Z
… as not AADL, not resolved to the enclosing component A PREREQUISITE of #455 item 3, not its delivery. Re-confirmed on the published v0.45.0 binary: A system-level end-to-end flow written `app.caller.lock_flow -> app.c_hand -> app.consumer.consumer_flow`, with both threads carrying Compute_Execution_Time, reported `components without timing properties: app, app` and `latency: not computed`. Every analysis that walks a flow kept only the FIRST dotted part of a segment, so both thread references resolved to the enclosing process; flow_check's unknown-connection warning exempted any segment containing a dot, so `app.c_hand` passed silently too. REJECT, NOT RESOLVE — decided from the grammar. osate2@87468992 Aadl2.xtext:2043-2048: a flow element is `[subcomponent '.'] flow`, one level, and a connection element is a bare identifier. Resolving the nested spelling would make spar accept models OSATE rejects. `EndToEndFlowInstance::nested_segment()` is the single legality predicate. flow_check reports the first offending segment as an ERROR naming the segment, its kind, its position and the one spelling measured to work; latency skips a rejected flow so it stops reporting on components the flow never named. flow_rules and latency's processor-crossing walk are left alone: on a rejected flow they emit nothing actionable, so a skip there would be code no test can observe. POSITIVE CONTROL, run on v0.45.0 before designing the fix: the same threads with the flow written inside App.impl derive [22.000 ms .. 22.000 ms], exit 0 — so the spelling the Error recommends works. ORACLE, a pair through the real parser (tests/flow_nested_segment.rs): NESTED must fail with the flow_check Error and contain neither `app, app` nor `not computed` (v0.45.0 fails all three); LEGAL must derive a `22.000 ms]` worst case and exit 0. Unit level: a grammar table for the predicate, flow AND connection rejection in flow_check, and a latency test that fails on exactly `app, app` + `not computed` when the skip is deleted by hand (cargo-mutants never generates that mutant). MUTATION: before any test, 15 of 21 in-diff mutants MISSED — including `nested_segment -> Some(0, ..)`, which rejects every flow, because cargo-mutants runs only the mutated crate's tests. After: 19 tested, 17 caught, 2 unviable, 0 missed. ITEM 3 IS NOT DELIVERED, measured after the first push of this commit. The LEGAL route — a flow path on the process, implemented in App.impl through both threads, used at system level as `s.src -> c1 -> app.proc_flow -> c2 -> k.snk` — still reports `not computed` and `components without timing properties: s, app, k`: latency never expands a subcomponent's flow specification into its implementation (instantiation drops flow implementations). The first push marked REQ-ANALYSIS-FLOW-THREAD-DESCENT-001 verified under a retitle to the reject branch, and its Error advised that very route. Corrected: - rejection is its own requirement, REQ-ANALYSIS-FLOW-SEGMENT-LEGALITY-001 (verified, traces-to DESCENT-001); - DESCENT-001 keeps the capability #455 asked for, stays proposed, and its oracle is that legal model deriving [12.000 ms .. 22.000 ms] — the figure the same threads give with the flow written inside App.impl; - the Error recommends only the in-implementation spelling and says the flow-specification route is not yet descended; - a PIN test asserts today's `not computed` on the legal model, so it fails the moment descent lands. NOT CLAIMED: that thread timing inside a process is reachable from system level by any spelling. The MCP `spar.check_chain` tool's tests use the nested spelling; they assert only tool-level success and still pass, but on such a model the tool now surfaces this Error. Refs #455 Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01BnBWxgVEUPdsBTLNKtrA6Z
…so thread timing inside a process reaches the end-to-end latency #455 item 3, the capability itself. REQ-ANALYSIS-FLOW-THREAD-DESCENT-001. The legal route from system level to thread timing: a flow path on process `App`, implemented in `App.impl` through both threads, used as `s.src -> c1 -> app.proc_flow -> c2 -> k.snk`. With 5..10 ms and 7..12 ms threads, the previous commit measured: [ERROR] latency: ... 'req_to_done' latency: not computed [WARNING] ... components without timing properties: s, app, k exit 1 Now: [INFO] latency: ... 'req_to_done' latency: [12.000 ms .. 22.000 ms] [WARNING] ... components without timing properties: s, k exit 0 That is exactly the figure the same threads give with the end-to-end flow written inside App.impl. INSTANTIATION DROPPED FLOW IMPLEMENTATIONS. The item tree kept them (FlowImplItem); the instance did not. `FlowInstance.impl_segments` now carries them, collected over the extends chain with an extension's own implementation overriding. The field was placed on FlowInstance by count: 3 construction sites, against 106 for ComponentInstance and 122 for SystemInstance. `expand_flow_steps` replaces `sub.flow` by its implementation's steps, resolving components AND connections in the child's scope, so `c_hand` is looked up in `app`, not in the flow's owner. Both the latency walk and the processor-crossing walk use it; a child with no implementation of the flow is a leaf, exactly as before. Depth is capped at 16. Descent only moves to a child, so there is no cycle to guard. BOUNDARY LEGS ARE NOT COUNTED TWICE. `c1 : s.o -> app.pin` and `c_in : pin -> caller.i` are two legs of one semantic connection. Counting `c_in` would reset the WCTT suppression a bound `c1` sets, re-adding the sampling period on top of the network bound. The rejection Error from the previous commit now advises BOTH legal routes, since both are measured to derive a figure. The pin asserting `not computed` on the legal model failed as designed and was converted into the oracle. ORACLE: tests/flow_nested_segment.rs `the_flow_specification_route_descends_into_the_process` asserts the figure, no flow_check finding, no `not computed`, `app` absent from missing timing, and exit 0. latency.rs adds 14 unit tests: descent, the leaf fallback, a latency-carrying connection inside the process proving child-scope lookup, the depth cap, and both directions of the crossing note. instance.rs covers attach, inherit, override and none. MUTATION, in-diff: 38 mutants. 20 MISSED after the implementation and before its tests; after, 31 caught, 7 unviable, 0 missed. Re-derived independently of the implementer's report. Implemented by a Sonnet subagent under supervision. Every figure above was re-run independently before this commit. NOT CLAIMED: a network-hop bound declared only on a boundary leg inside the process. It is dropped with the leg, and a binding belongs on the system-level connection. Modal flow implementations (`in modes`) are not filtered. Refs #455 Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01BnBWxgVEUPdsBTLNKtrA6Z
avrabe
force-pushed
the
fix/latency-flow-own-budget-455
branch
from
October 14, 2026 16:35
26bd696 to
e12bead
Compare
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.
Refs #455 — delivers items (2) and (3) (numbering as in the 2026-10-14 comment on the issue). #455 stays open until they ship in a published release.
Stacked on #487 (range budget, property set, severity), rebased onto main after it merged.
Item (2) — the budget a flow declares is read and enforced in both directions
fix(latency): read a budget declared on the flow itselfEndToEndFlowInstancecarries the flow's own{ Latency => … }block; it wins over the owner component's, which stays the fallbackfix(latency): a reported best case is a best casebest_case_pssummed worst-case execution times20 ms .. 40 msdevices:[80 .. 80]→[40 .. 80]; the upper bound is bit-for-bit unchangedfix(latency): enforce a declared latency MINIMUMbest < minis an Error ("can complete faster"),best == minmeets it, a scalar budget has no minimum50 ms .. 500 msexit 0 → exit 1;40 ms ..and30 ms ..stay exit 0REQ-ANALYSIS-LATENCY-BUDGET-001 and REQ-ANALYSIS-LATENCY-BEST-CASE-001 →
verified.Item (3) — thread timing inside a process now reaches the latency
There are two commits.
Rejecting the illegal spelling (
90db90c, REQ-ANALYSIS-FLOW-SEGMENT-LEGALITY-001 →verified).app.caller.lock_flow -> app.c_hand -> …at system level reaches two levels deep. OSATE's grammar (osate2@87468992Aadl2.xtext:2043-2048) allows only one, so spar rejected it wrongly before. It now raises an Error that names the segment and advises both legal routes.Descent (
e12bead, REQ-ANALYSIS-FLOW-THREAD-DESCENT-001 →verified).App.implthrough both threads, ass.src -> c1 -> app.proc_flow -> c2 -> k.snk.not computed, missing timings, app, k, exit 1. After:[12.000 ms .. 22.000 ms], missing timings, k, exit 0.FlowInstance.impl_segments, including inherited ones.sub.flowwith that implementation's steps, resolving them in the child's scope.c_in/c_out) aren't counted on top ofc1/c2, so the network bound and the sampling period aren't added twice.Oracles
crates/spar-cli/tests/flow_nested_segment.rs. v0.45.0's output fails NESTED and passes LEGAL.Not claimed
spar.check_chainstill tolerates the nested spelling. Its matcher (crates/spar-mcp/src/tools/check_chain.rs) and its tests use the nested spellingapp.producer.f1. The tests still pass, but the tool will now surface flow_check's Error on such a model. Aligning the tool is follow-up work.🤖 Generated with Claude Code
https://claude.ai/code/session_01BnBWxgVEUPdsBTLNKtrA6Z