From 73a774b338fef0f3c1f2d4553de1eb9a152e8921 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Thu, 23 Apr 2026 21:15:40 +0200 Subject: [PATCH] feat(timing): Spar_Timing + Spar_Trace property sets (Track A foundation) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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) --- COMPLIANCE.md | 6 + artifacts/requirements.yaml | 63 +++++++ artifacts/verification.yaml | 44 +++++ .../spar-hir-def/src/standard_properties.rs | 177 +++++++++++++++++- 4 files changed, 288 insertions(+), 2 deletions(-) diff --git a/COMPLIANCE.md b/COMPLIANCE.md index 2eafa4c..f87a5cd 100644 --- a/COMPLIANCE.md +++ b/COMPLIANCE.md @@ -214,6 +214,12 @@ --- +## In progress / v0.7.0 + +- IRQ-aware RTA: property-set surface (`Spar_Timing::*`, `Spar_Trace::*`) landed; analysis wiring in follow-up commits. + +--- + ## What's Working Well - **Parser coverage is excellent** (~95%). All major AADL constructs parse correctly. diff --git a/artifacts/requirements.yaml b/artifacts/requirements.yaml index 6d517f4..026d29d 100644 --- a/artifacts/requirements.yaml +++ b/artifacts/requirements.yaml @@ -1008,4 +1008,67 @@ artifacts: status: planned tags: [interop, autosar, bridge, v050] + # ── IRQ-aware RTA (Track A, v0.7.0) ──────────────────────────────── + + - id: REQ-TIMING-IRQ-001 + type: requirement + title: ISR execution time distinct from handler thread WCET + description: > + System shall support modeling of ISR execution time separate from + handler thread WCET. Exposed via the non-standard Spar_Timing + property set as ISR_Execution_Time (Time_Range). This commit lands + the property-set surface only; hierarchical RTA consumption ships + in subsequent Track A commits. + status: planned + tags: [timing, irq, rta, v070] + + - id: REQ-TIMING-IRQ-002 + type: requirement + title: Hardware IRQ-to-ISR latency bound + description: > + System shall support modeling of hardware IRQ-assertion-to-ISR-entry + latency bound (platform-given upper bound covering hardware dispatch + plus kernel vectoring). Exposed via Spar_Timing::Interrupt_Latency_Bound + (Time). Drives the "from wire to handler" latency chain in hierarchical + RTA. + status: planned + tags: [timing, irq, rta, v070] + + - id: REQ-TIMING-IRQ-003 + type: requirement + title: Top-half/bottom-half thread decomposition + description: > + System shall support top-half/bottom-half thread decomposition via + the Spar_Timing::Bottom_Half_Server property (reference to thread). + Allows ISR bodies to declare the handler thread responsible for + deferred work, so hierarchical RTA can chain the two layers. + status: planned + tags: [timing, irq, rta, v070] + + # ── Closed-loop trace verification (v0.8.0 precursor) ────────────── + + - id: REQ-TRACE-001 + type: requirement + title: Probe-point annotation for runtime trace emission + description: > + System shall support probe-point annotation on components for + runtime trace emission. Exposed via Spar_Trace::Probe_Point + (aadlboolean). Flags components whose entry/exit codegen should + emit a trace event (Zephyr CTF k_*-primitive style in v0.8.0). + status: planned + tags: [trace, verification, v080] + + - id: REQ-TRACE-002 + type: requirement + title: Per-component expected-timing properties for runtime comparison + description: > + System shall support per-component expected-timing properties + (BCET/WCET/Mean) for runtime comparison. Exposed via + Spar_Trace::Expected_BCET, Expected_WCET, Expected_Mean (all Time). + Distinct from Compute_Execution_Time because these are design-time + predictions intended for runtime comparison by `spar verify-trace`, + not the declared WCET the scheduler uses. + status: planned + tags: [trace, verification, v080] + # Research findings tracked separately in research/findings.yaml diff --git a/artifacts/verification.yaml b/artifacts/verification.yaml index 903659b..df0d744 100644 --- a/artifacts/verification.yaml +++ b/artifacts/verification.yaml @@ -992,3 +992,47 @@ artifacts: target: REQ-PROP-002 - type: satisfies target: COVERAGE-CH11 + + - id: TEST-SPAR-TIMING-PROPS + type: feature + title: Spar_Timing property set surface tests + description: > + Unit tests in spar-hir-def/src/standard_properties.rs verifying + that Spar_Timing is a known predefined property set, that each of + ISR_Priority, ISR_Execution_Time, Interrupt_Latency_Bound, and + Bottom_Half_Server resolves to the expected AADL type, and that + unknown names in the set return None / ResolvedProperty::Unresolved. + fields: + method: automated-test + steps: + - run: cargo test -p spar-hir-def -- test_standard_properties_in_spar_timing test_spar_property_sets_resolved_via_global_scope + status: passing + tags: [v0.7.0, timing, irq, properties] + links: + - type: satisfies + target: REQ-TIMING-IRQ-001 + - type: satisfies + target: REQ-TIMING-IRQ-002 + - type: satisfies + target: REQ-TIMING-IRQ-003 + + - id: TEST-SPAR-TRACE-PROPS + type: feature + title: Spar_Trace property set surface tests + description: > + Unit tests in spar-hir-def/src/standard_properties.rs verifying + that Spar_Trace is a known predefined property set, that each of + Probe_Point, Expected_BCET, Expected_WCET, and Expected_Mean + resolves to the expected AADL type, and that unknown names return + None / ResolvedProperty::Unresolved. + fields: + method: automated-test + steps: + - run: cargo test -p spar-hir-def -- test_standard_properties_in_spar_trace test_spar_property_sets_resolved_via_global_scope + status: passing + tags: [v0.8.0, trace, verification, properties] + links: + - type: satisfies + target: REQ-TRACE-001 + - type: satisfies + target: REQ-TRACE-002 diff --git a/crates/spar-hir-def/src/standard_properties.rs b/crates/spar-hir-def/src/standard_properties.rs index 79d559e..cb13995 100644 --- a/crates/spar-hir-def/src/standard_properties.rs +++ b/crates/spar-hir-def/src/standard_properties.rs @@ -18,6 +18,12 @@ pub struct StandardProperty { } /// All standard predefined property set names. +/// +/// Includes the AS5506 Appendix A predeclared sets plus two non-standard +/// spar-defined sets (`Spar_Timing`, `Spar_Trace`) that support +/// IRQ-aware RTA (Track A, v0.7.0) and closed-loop trace verification +/// (v0.8.0 precursor). The spar-defined sets are treated like predefined +/// sets so they resolve without explicit `with` imports. pub const STANDARD_PROPERTY_SET_NAMES: &[&str] = &[ "Timing_Properties", "Communication_Properties", @@ -27,6 +33,8 @@ pub const STANDARD_PROPERTY_SET_NAMES: &[&str] = &[ "Programming_Properties", "Modeling_Properties", "AADL_Project", + "Spar_Timing", + "Spar_Trace", ]; // ── Timing_Properties ─────────────────────────────────────────────── @@ -279,6 +287,53 @@ const AADL_PROJECT: &[(&str, &str)] = &[ ), ]; +// ── Spar_Timing ───────────────────────────────────────────────────── +// +// Non-standard property set defined by spar itself (not AS5506); used +// for IRQ-aware RTA (Track A, v0.7.0). Models the interrupt layer so +// hierarchical RTA can reason about ISR priority, the ISR body's own +// BCET..WCET, the hardware-dispatch latency bound, and the top-half / +// bottom-half deferred-work split. + +const SPAR_TIMING: &[(&str, &str)] = &[ + // Priority at which the ISR executes (higher than any task). + // Drives hierarchical RTA layer ordering. Applies to thread + // (handler thread) and virtual processor (ISR layer). + ("ISR_Priority", "aadlinteger"), + // BCET..WCET of the ISR body itself, separately from the handler + // thread. Applies to thread and device. + ("ISR_Execution_Time", "Time_Range"), + // Platform-given upper bound on IRQ-assertion → ISR-entry + // (hardware + kernel dispatch). Drives the "from wire to handler" + // latency chain. Applies to processor and device. + ("Interrupt_Latency_Bound", "Time"), + // Reference to the thread that handles deferred ISR work (classic + // top-half / bottom-half split). Applies to thread and device. + ("Bottom_Half_Server", "reference (thread)"), +]; + +// ── Spar_Trace ────────────────────────────────────────────────────── +// +// Non-standard property set defined by spar itself (not AS5506); used +// for closed-loop trace verification (v0.8.0 precursor). Annotates +// components whose entry/exit codegen should emit a runtime trace +// event and carries design-time predictions against which the observed +// traces are compared by `spar verify-trace`. + +const SPAR_TRACE: &[(&str, &str)] = &[ + // Flags a component whose entry/exit codegen should emit a trace + // event (Zephyr CTF k_*-primitive style in v0.8.0). + ("Probe_Point", "aadlboolean"), + // Design-time best-case prediction, separate from + // Compute_Execution_Time because these are predictions for runtime + // comparison, not the declared WCET the scheduler uses. + ("Expected_BCET", "Time"), + // Design-time worst-case prediction (runtime-comparison only). + ("Expected_WCET", "Time"), + // Design-time mean/expected prediction (runtime-comparison only). + ("Expected_Mean", "Time"), +]; + /// Helper: collect properties from a table into the result vector. fn collect_properties( table: &[(&'static str, &'static str)], @@ -314,6 +369,8 @@ pub fn all_standard_properties() -> Vec { ); collect_properties(MODELING_PROPERTIES, "Modeling_Properties", &mut result); collect_properties(AADL_PROJECT, "AADL_Project", &mut result); + collect_properties(SPAR_TIMING, "Spar_Timing", &mut result); + collect_properties(SPAR_TRACE, "Spar_Trace", &mut result); result } @@ -339,6 +396,8 @@ fn lookup_table(set_lower: &str) -> Option<&'static [(&'static str, &'static str "programming_properties" => Some(PROGRAMMING_PROPERTIES), "modeling_properties" => Some(MODELING_PROPERTIES), "aadl_project" => Some(AADL_PROJECT), + "spar_timing" => Some(SPAR_TIMING), + "spar_trace" => Some(SPAR_TRACE), _ => None, } } @@ -383,6 +442,8 @@ mod tests { assert!(is_standard_property_set("Programming_Properties")); assert!(is_standard_property_set("Modeling_Properties")); assert!(is_standard_property_set("AADL_Project")); + assert!(is_standard_property_set("Spar_Timing")); + assert!(is_standard_property_set("Spar_Trace")); // Case-insensitive assert!(is_standard_property_set("timing_properties")); @@ -547,6 +608,118 @@ mod tests { assert!(props.contains(&"Supported_Active_Thread_Handling_Protocols")); } + #[test] + fn test_standard_properties_in_spar_timing() { + // Spar_Timing is a known property set. + assert!(is_standard_property_set("Spar_Timing")); + + let props = standard_properties_in_set("Spar_Timing"); + assert_eq!(props.len(), 4); + assert!(props.contains(&"ISR_Priority")); + assert!(props.contains(&"ISR_Execution_Time")); + assert!(props.contains(&"Interrupt_Latency_Bound")); + assert!(props.contains(&"Bottom_Half_Server")); + + // Each property resolves to its expected type. + assert_eq!( + standard_property_type("Spar_Timing", "ISR_Priority"), + Some("aadlinteger") + ); + assert_eq!( + standard_property_type("Spar_Timing", "ISR_Execution_Time"), + Some("Time_Range") + ); + assert_eq!( + standard_property_type("Spar_Timing", "Interrupt_Latency_Bound"), + Some("Time") + ); + assert_eq!( + standard_property_type("Spar_Timing", "Bottom_Half_Server"), + Some("reference (thread)") + ); + + // Deliberately-wrong name returns None. + assert_eq!(standard_property_type("Spar_Timing", "Nonexistent"), None); + + // Case-insensitive. + assert_eq!( + standard_property_type("spar_timing", "isr_priority"), + Some("aadlinteger") + ); + } + + #[test] + fn test_standard_properties_in_spar_trace() { + // Spar_Trace is a known property set. + assert!(is_standard_property_set("Spar_Trace")); + + let props = standard_properties_in_set("Spar_Trace"); + assert_eq!(props.len(), 4); + assert!(props.contains(&"Probe_Point")); + assert!(props.contains(&"Expected_BCET")); + assert!(props.contains(&"Expected_WCET")); + assert!(props.contains(&"Expected_Mean")); + + // Each property resolves to its expected type. + assert_eq!( + standard_property_type("Spar_Trace", "Probe_Point"), + Some("aadlboolean") + ); + assert_eq!( + standard_property_type("Spar_Trace", "Expected_BCET"), + Some("Time") + ); + assert_eq!( + standard_property_type("Spar_Trace", "Expected_WCET"), + Some("Time") + ); + assert_eq!( + standard_property_type("Spar_Trace", "Expected_Mean"), + Some("Time") + ); + + // Deliberately-wrong name returns None. + assert_eq!(standard_property_type("Spar_Trace", "Nonexistent"), None); + + // Case-insensitive. + assert_eq!( + standard_property_type("spar_trace", "probe_point"), + Some("aadlboolean") + ); + } + + #[test] + fn test_spar_property_sets_resolved_via_global_scope() { + use crate::name::Name; + use crate::resolver::{GlobalScope, ResolvedProperty}; + + let scope = GlobalScope::from_trees(vec![]); + + // Spar_Timing::ISR_Priority is resolvable without explicit `with`. + let result = scope.resolve_property(&Name::new("Spar_Timing"), &Name::new("ISR_Priority")); + assert!( + matches!(result, ResolvedProperty::PropertyDef { .. }), + "expected PropertyDef for Spar_Timing::ISR_Priority, got {:?}", + result + ); + + // Spar_Trace::Probe_Point is resolvable without explicit `with`. + let result = scope.resolve_property(&Name::new("Spar_Trace"), &Name::new("Probe_Point")); + assert!( + matches!(result, ResolvedProperty::PropertyDef { .. }), + "expected PropertyDef for Spar_Trace::Probe_Point, got {:?}", + result + ); + + // Deliberately-wrong name inside a known spar set is Unresolved. + let result = scope.resolve_property(&Name::new("Spar_Timing"), &Name::new("Nonexistent")); + assert!( + matches!(result, ResolvedProperty::Unresolved), + "expected Unresolved for Spar_Timing::Nonexistent, got {:?}", + result + ); + } + #[test] fn test_standard_properties_unknown_set() { let props = standard_properties_in_set("Nonexistent_Properties"); @@ -563,8 +736,8 @@ mod tests { #[test] fn test_all_standard_properties_total_count() { let all = all_standard_properties(); - // 12 + 13 + 14 + 14 + 7 + 25 + 4 + 13 = 102 - assert_eq!(all.len(), 102); + // 12 + 13 + 14 + 14 + 7 + 25 + 4 + 13 + 4 + 4 = 110 + assert_eq!(all.len(), 110); } #[test]