Skip to content

feat(timing): Spar_Timing + Spar_Trace property sets (Track A foundation) (v0.7.0)#145

Merged
avrabe merged 1 commit intomainfrom
feat/v0.7.0-timing-properties
Apr 23, 2026
Merged

feat(timing): Spar_Timing + Spar_Trace property sets (Track A foundation) (v0.7.0)#145
avrabe merged 1 commit intomainfrom
feat/v0.7.0-timing-properties

Conversation

@avrabe
Copy link
Copy Markdown
Contributor

@avrabe avrabe commented Apr 23, 2026

Summary

First commit of roughly four for Track A (IRQ-aware RTA, v0.7.0). Lands
only the property-set surface so the foundation is small and
reviewable. Analysis wiring ships in follow-up commits.

Two new non-standard property sets are registered in
spar-hir-def::standard_properties so they resolve without explicit
with imports, matching the treatment of the AS5506 Appendix A sets:

  • Spar_Timing — IRQ/interrupt-layer modeling for hierarchical RTA

    • ISR_Priority (aadlinteger)
    • ISR_Execution_Time (Time_Range)
    • Interrupt_Latency_Bound (Time)
    • Bottom_Half_Server (reference (thread))
  • Spar_Trace — probe points for closed-loop trace verification (v0.8.0 precursor)

    • Probe_Point (aadlboolean)
    • Expected_BCET, Expected_WCET, Expected_Mean (all Time)

What's explicitly NOT in this commit

  • No changes to spar-analysis/*.rs — RTA consumption is later.
  • No parser or lexer changes — these are standard-named property sets, no syntax extension needed.
  • No changes to docs/contracts/rivet-spar-variant-v1.md (separate track).
  • No claim in COMPLIANCE.md that IRQ-aware RTA "works" — only that the property surface landed.

Rivet traceability

New requirements in artifacts/requirements.yaml:

  • REQ-TIMING-IRQ-001 — ISR execution time distinct from handler thread WCET
  • REQ-TIMING-IRQ-002 — Hardware IRQ-to-ISR latency bound
  • REQ-TIMING-IRQ-003 — Top-half/bottom-half thread decomposition
  • REQ-TRACE-001 — Probe-point annotation for runtime trace emission
  • REQ-TRACE-002 — Per-component expected-timing properties for runtime comparison

Linked from two new features in artifacts/verification.yaml
(TEST-SPAR-TIMING-PROPS, TEST-SPAR-TRACE-PROPS) pointing at the
specific unit tests added to spar-hir-def/src/standard_properties.rs.

How reviewers can verify

  • cargo test -p spar-hir-def — 426 tests pass, including three new tests:
    • test_standard_properties_in_spar_timing
    • test_standard_properties_in_spar_trace
    • test_spar_property_sets_resolved_via_global_scope
  • cargo build --workspace — clean.
  • cargo clippy --workspace --all-targets -- -D warnings — clean.
  • cargo fmt --all -- --check — clean.
  • rivet validate — PASS (warnings only; same class of field not defined in schema notices that already exist for every other feature in the file).

Test plan

  • cargo build --workspace
  • cargo test -p spar-hir-def
  • cargo clippy --workspace --all-targets -- -D warnings
  • cargo fmt --all -- --check
  • rivet validate

🤖 Generated with Claude Code

…ion)

Adds two non-standard property sets that v0.7.0 IRQ-aware RTA and
v0.8.0 trace-based verification will consume. No analysis wiring in
this commit — surface only, to keep the foundation reviewable.

Spar_Timing::{ISR_Priority, ISR_Execution_Time, Interrupt_Latency_Bound,
              Bottom_Half_Server}
Spar_Trace::{Probe_Point, Expected_BCET, Expected_WCET, Expected_Mean}

New requirements: REQ-TIMING-IRQ-{001,002,003}, REQ-TRACE-{001,002}.
Analysis wiring ships in subsequent Track A commits (hierarchical RTA,
Dispatch_Jitter, BCET/WCET split).

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
@codecov
Copy link
Copy Markdown

codecov Bot commented Apr 23, 2026

Codecov Report

✅ All modified and coverable lines are covered by tests.

📢 Thoughts on this report? Let us know!

@avrabe avrabe merged commit fa109bb into main Apr 23, 2026
11 checks passed
@avrabe avrabe deleted the feat/v0.7.0-timing-properties branch April 23, 2026 21:04
avrabe added a commit that referenced this pull request Apr 24, 2026
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 added a commit that referenced this pull request Apr 24, 2026
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 added a commit that referenced this pull request Apr 25, 2026
…I integration (#154)

Closes the v0.7.0 Track A milestone:

- COMPLIANCE.md "In progress / v0.7.0" expanded into a full narrative
  covering all four Track A commits (foundation #145, hierarchical RTA
  #147, Lean convergence #148, this close-out), the Track B variant-
  contract foundation (#144), v0.7.x infrastructure landings (#141-143,
  #151), and v0.8.0 planning anchors (Track D #149/#152, Track E
  #150/#153).

- Updated header date to 2026-04-25 and crate count from "16 crates,
  1200+ tests" to "17 crates, 1900+ tests" reflecting the test growth
  through Track A and the v0.7.x infrastructure additions.

- New CLI integration test crates/spar-cli/tests/track_a_close_out.rs
  exercises the full parse → instance → analyze pipeline on a model
  using the Spar_Timing::ISR_* property surface plus a sporadic handler
  thread. The unit + fixture tests in spar-analysis cover the algorithm
  at the analysis-crate level; this test guards the property surface
  flowing through the CLI binary end-to-end.

Out-of-scope items explicitly recorded: PIP/PCP blocking deferred to
v0.7.1, multi-processor ISR migration deferred, cache-aware
interference inflation deferred to v1.0+.

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant