diff --git a/COMPLIANCE.md b/COMPLIANCE.md index b478066..4b1a243 100644 --- a/COMPLIANCE.md +++ b/COMPLIANCE.md @@ -1,8 +1,8 @@ # AS5506 AADL v2.2 Compliance Gap Analysis -**Updated**: 2026-04-05 (v0.6.0) +**Updated**: 2026-04-25 (v0.7.0 in progress) **Source**: 102 HTML files from OSATE2 (`org.osate.help/html/std/`) -**Toolchain**: spar (1200+ tests passing across 16 crates) +**Toolchain**: spar (1900+ tests passing across 17 crates) --- @@ -216,7 +216,36 @@ ## In progress / v0.7.0 -- IRQ-aware RTA: hierarchical two-tier analysis with `Dispatch_Jitter` and BCET/WCET split landed (Track A commit 2); PIP/PCP blocking deferred to v0.7.1. +**Track A — IRQ-aware RTA (4/4 commits delivered)** + +- Foundation (#145): `Spar_Timing::{ISR_Priority, ISR_Execution_Time, Interrupt_Latency_Bound, Bottom_Half_Server}` and `Spar_Trace::{Probe_Point, Expected_BCET, Expected_WCET, Expected_Mean}` property sets land as non-standard predefined sets, resolvable via the same idiom as AS5506 standard sets. +- Hierarchical RTA (#147): two-tier analysis — ISR layer steals CPU capacity first; residual feeds task RTA. `Dispatch_Jitter` woven into the Tindell-Clark recurrence. `Compute_Execution_Time`'s Time_Range consumed as `(BCET, WCET)`. Five new diagnostic kinds: `IrqResponseBudget`, `IrqBudgetViolated`, `IsrOverloadedCpu`, `MissingBottomHalfServer`, `ResponseBand`. Non-regression gate (`no_isrs_matches_classical_rta`) verifies models without `Spar_Timing::*` produce byte-identical RTA output. +- Lean convergence (#148): `proofs/Proofs/Scheduling/RTAJittered.lean` proves monotonicity, zero-jitter degeneration to classical `rtaStep`, and least-fixed-point convergence in `deadline + 1` iterations. Three core theorems plus two helper lemmas, no `sorry`. +- Close-out (this commit): COMPLIANCE wording, COMPLIANCE-side acknowledgement of out-of-scope items. + +**Out of scope for v0.7.0, deferred to v0.7.1+**: priority inheritance (PIP) / priority ceiling (PCP) blocking; multi-processor ISR migration; cache-aware interference inflation (research-grade, v1.0+). + +**Track B — Variants (foundation only)** + +- Variant binding contract v1 (#144): `docs/contracts/rivet-spar-variant-v1.md` — rivet owns the PLE truth (feature model, variant configs, bindings, SAT), spar consumes a JSON context blob and filters HIR. Implementation of the consumer crate (`spar-variants`) waits for rivet to emit its first context blob; tracked separately. + +**v0.7.x infrastructure landed alongside Track A** + +- Kani harnesses for spar-solver and spar-codegen invariants (#141, closes #136). +- cargo-fuzz scaffolding for parser, solver, codegen-roundtrip targets (#142, closes #138). +- Criterion benchmarks for scheduling solver and codegen (#143, closes #137). +- Lean / Bazel / proptest CI gates (#151, closes #135) — Lean proofs now machine-checked in CI for the first time. +- Track D and Track E research design docs landed (#152, #153) anchoring v0.8.0+ scope. + +--- + +## v0.8.0 planning + +Two parallel tracks scoped from the v0.7.0 research: + +**Track D — TSN/Ethernet WCTT analysis (#149)**: WCTT is a foundational primitive for honest end-to-end timing, not a TSN-specific feature. Phase 1 (v0.8.0) ships a Network Calculus engine for FIFO+priority networks (classical Ethernet, CAN, FlexRay) and replaces `latency.rs`'s scalar bus-latency lookup with per-stream NC-derived bounds. Phase 2 (v0.8.x) adds TSN-specific service curves (TAS, CBS, frame preemption). Roadmap: 7 weeks across 6 commits. + +**Track E — Frozen-platform / mobile-application split + hypothetical-rebinding oracle (#150)**: Adds `Spar_Migration::{Frozen, Mobile, Allowed_Targets, Pinned_Reason}` plus a verification mode (`spar moves verify`) and an enumeration mode (`spar moves enumerate`). The MCP tool surface (`spar.verify_move`, `spar.enumerate_moves`) ships in v0.9.0 — read-only / idempotent only, deterministic apply via CLI. LLM agents propose moves; spar deterministically verifies; certification chain stays in spar. Roadmap: 8 weeks across 8 commits for v0.8.0; another 8.5 weeks across the v0.9.0 MCP surface. --- diff --git a/crates/spar-cli/tests/track_a_close_out.rs b/crates/spar-cli/tests/track_a_close_out.rs new file mode 100644 index 0000000..df4c174 --- /dev/null +++ b/crates/spar-cli/tests/track_a_close_out.rs @@ -0,0 +1,111 @@ +//! Track A close-out: end-to-end CLI integration test for IRQ-aware RTA. +//! +//! Exercises the full pipeline (parse → instance → analyze) on a model +//! using the v0.7.0 `Spar_Timing::*` property surface. The unit/fixture +//! tests in `spar-analysis/tests/fixtures/rta/` cover the algorithm at +//! the analysis-crate level; this test is the CLI-level guard that the +//! property surface flows through `spar analyze` end-to-end. + +use std::env; +use std::fs; +use std::process::Command; + +fn spar() -> Command { + Command::new(env!("CARGO_BIN_EXE_spar")) +} + +const MODEL: &str = "\ +package Test_Track_A_IRQ +public + with Timing_Properties; + with Deployment_Properties; + with Spar_Timing; + + processor M4 + end M4; + + device Sensor_IRQ + end Sensor_IRQ; + + device implementation Sensor_IRQ.Impl + properties + Spar_Timing::ISR_Priority => 100; + Spar_Timing::ISR_Execution_Time => 20 us .. 30 us; + Spar_Timing::Interrupt_Latency_Bound => 10 us; + end Sensor_IRQ.Impl; + + thread Brake_Handler + end Brake_Handler; + + thread implementation Brake_Handler.Impl + properties + Dispatch_Protocol => Sporadic; + Period => 1 ms; + Compute_Execution_Time => 50 us .. 200 us; + Deadline => 1 ms; + end Brake_Handler.Impl; + + process P + end P; + + process implementation P.Impl + subcomponents + bh: thread Brake_Handler.Impl; + end P.Impl; + + system Top + end Top; + + system implementation Top.Impl + subcomponents + cpu: processor M4; + irq: device Sensor_IRQ.Impl; + app: process P.Impl; + properties + Actual_Processor_Binding => (reference (cpu)) applies to app.bh; + end Top.Impl; +end Test_Track_A_IRQ; +"; + +#[test] +fn track_a_irq_aware_rta_runs_through_cli() { + let path = env::temp_dir().join(format!("spar_track_a_irq_{}.aadl", std::process::id())); + fs::write(&path, MODEL).expect("write temp AADL"); + + let output = spar() + .arg("analyze") + .arg("--root") + .arg("Test_Track_A_IRQ::Top.Impl") + .arg(&path) + .output() + .expect("failed to run spar"); + + let combined = format!( + "{}\n{}", + String::from_utf8_lossy(&output.stdout), + String::from_utf8_lossy(&output.stderr), + ); + + // The pipeline must complete (non-zero exit only on hard parse errors, + // which this model doesn't have). Diagnostic content can vary as the + // analysis matures; we only guard the must-not-crash invariant + the + // presence of *some* RTA output, since the model is RTA-relevant. + assert!( + !combined.contains("panicked"), + "spar analyze panicked on Spar_Timing::* model:\n{combined}", + ); + assert!( + !combined.contains("internal compiler error"), + "spar analyze internal error:\n{combined}", + ); + + // Loose check: RTA must say *something* about the handler thread + // since it is bound to a CPU and has a deadline. + let mentions_handler = combined.contains("Brake_Handler") || combined.contains("bh"); + assert!( + mentions_handler, + "spar analyze did not surface any output mentioning the handler thread:\n{combined}", + ); + + let _ = fs::remove_file(&path); +}