docs: v0.7.0 Track A commit-2 design (hierarchical IRQ-aware RTA)#146
Merged
docs: v0.7.0 Track A commit-2 design (hierarchical IRQ-aware RTA)#146
Conversation
Codecov Report✅ All modified and coverable lines are covered by tests. 📢 Thoughts on this report? Let us know! |
Captures the design for the next Track A commit after PR #145 lands. Two-tier analysis: ISR layer preempts all tasks, residual capacity feeds classical task-priority RTA; Tindell-Clark jitter terms fold into the fixed-point recurrence; Compute_Execution_Time's Time_Range consumed as (BCET, WCET) with a new ResponseBand diagnostic. Includes: current rta.rs walkthrough with line refs, gap analysis, algorithm pseudocode, new diagnostics table, file-by-file change scope with LOC estimates, 10-unit-test plan + 3 fixture tests, out-of-scope list (PIP/PCP, multi-processor ISR migration), commit message template, and an executable agent brief ready to hand off when #145 merges. Non-regression is the critical gate: models with no Spar_Timing::* properties must produce byte-identical RTA output. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
avrabe
force-pushed
the
docs/v0.7.0-hierarchical-rta-design
branch
from
fab221c to
5067481
Compare
Merged
6 tasks
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.
Summary
Design doc for the next v0.7.0 Track A commit. Ready to hand off to an agent when PR #145 merges.
What's in
rta.rswalkthrough with line refs (line 34RtaAnalysis, line 121 the fixed-point call, property accessors at 195/214/240)rta.rs,property_accessors.rs,scheduling_verified.rs,diagnostics.rs)Why this exists
v0.7.0 Track A commit 2 is the big one — the actual algorithm change. Landing the design doc first means:
Non-regression is the critical gate
Any model without
Spar_Timing::*properties must produce byte-identical RTA output to today. This is explicitly called out as the first test to run.Not yet
proofs/Proofs/Scheduling/RTAJittered.lean)Test plan
🤖 Generated with Claude Code