Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion COMPLIANCE.md
Original file line number Diff line number Diff line change
Expand Up @@ -216,7 +216,7 @@

## In progress / v0.7.0

- IRQ-aware RTA: property-set surface (`Spar_Timing::*`, `Spar_Trace::*`) landed; analysis wiring in follow-up commits.
- 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.

---

Expand Down
2 changes: 2 additions & 0 deletions Cargo.lock

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

51 changes: 51 additions & 0 deletions artifacts/verification.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -1205,3 +1205,54 @@ artifacts:
target: REQ-CODEGEN-WIT
- type: verifies
target: REQ-CODEGEN-RUST

- id: TEST-RTA-HIERARCHICAL
type: feature
title: Hierarchical IRQ-aware RTA unit tests
description: >
Unit tests in crates/spar-analysis/src/rta.rs covering the
two-tier (ISR layer + task RTA) analysis. Includes the
no_isrs_matches_classical_rta non-regression gate, ISR
utilization overload, Dispatch_Jitter inflation, BCET/WCET
response band, IRQ chain budget, Bottom_Half_Server warning,
multi-processor isolation, zero-jitter equivalence, and ISR
priority above all tasks. Also exercises the new verified
function compute_response_time_jittered.
fields:
method: automated-test
steps:
- run: cargo test -p spar-analysis --lib -- rta::tests scheduling_verified
status: passing
tags: [v0.7.0, timing, irq, rta]
links:
- type: satisfies
target: REQ-TIMING-IRQ-001
- type: satisfies
target: REQ-TIMING-IRQ-002
- type: satisfies
target: REQ-TIMING-IRQ-003

- id: TEST-RTA-FIXTURES
type: feature
title: Hierarchical IRQ-aware RTA fixture tests
description: >
Integration tests in crates/spar-analysis/tests/rta_fixtures.rs
that parse committed AADL fixtures in tests/fixtures/rta/ and
diff the sorted RTA diagnostic output against the committed
.expected.json snapshots. Fixtures cover: irq_brake_handler
(full chain with device ISR and sporadic handler),
multi_isr_same_cpu (ISR-overload detection), and jittered_chain
(Tindell-Clark Dispatch_Jitter extension).
fields:
method: automated-test
steps:
- run: cargo test -p spar-analysis --test rta_fixtures
status: passing
tags: [v0.7.0, timing, irq, rta, fixtures]
links:
- type: satisfies
target: REQ-TIMING-IRQ-001
- type: satisfies
target: REQ-TIMING-IRQ-002
- type: satisfies
target: REQ-TIMING-IRQ-003
4 changes: 4 additions & 0 deletions crates/spar-analysis/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -11,3 +11,7 @@ spar-hir-def.workspace = true
la-arena.workspace = true
rustc-hash = "2"
serde.workspace = true

[dev-dependencies]
spar-base-db.workspace = true
serde_json = "1"
110 changes: 110 additions & 0 deletions crates/spar-analysis/src/property_accessors.rs
Original file line number Diff line number Diff line change
Expand Up @@ -365,6 +365,116 @@ pub fn extract_reference_target(val: &str) -> Option<&str> {
None
}

// ── Spar_Timing property accessors (IRQ-aware RTA, v0.7.0) ──────────

const SPAR_TIMING: &str = "Spar_Timing";

/// Get `Spar_Timing::ISR_Priority` as an integer (higher = more important).
pub fn get_isr_priority(props: &PropertyMap) -> Option<u64> {
// Typed path
if let Some(expr) = get_typed_qualified(props, SPAR_TIMING, "ISR_Priority")
&& let Some(v) = extract_integer(expr)
{
return Some(v);
}

// String fallback
let raw = props
.get(SPAR_TIMING, "ISR_Priority")
.or_else(|| props.get("", "ISR_Priority"))?;
raw.trim().parse::<u64>().ok()
}

/// Get `Spar_Timing::ISR_Execution_Time` as a (BCET, WCET) range in picoseconds.
pub fn get_isr_execution_time_range(props: &PropertyMap) -> Option<(u64, u64)> {
// Typed path
if let Some(expr) = get_typed_qualified(props, SPAR_TIMING, "ISR_Execution_Time")
&& let Some(range) = extract_time_range_ps(expr)
{
return Some(range);
}

// String fallback
let raw = props
.get(SPAR_TIMING, "ISR_Execution_Time")
.or_else(|| props.get("", "ISR_Execution_Time"))?;

if let Some((min_str, max_str)) = raw.split_once("..") {
let min_ps = parse_time_value(min_str.trim())?;
let max_ps = parse_time_value(max_str.trim())?;
Some((min_ps, max_ps))
} else {
let val = parse_time_value(raw)?;
Some((val, val))
}
}

/// Get `Spar_Timing::Interrupt_Latency_Bound` in picoseconds.
///
/// This is a processor-level property bounding HW+kernel IRQ dispatch.
pub fn get_interrupt_latency_bound(props: &PropertyMap) -> Option<u64> {
// Typed path
if let Some(expr) = get_typed_qualified(props, SPAR_TIMING, "Interrupt_Latency_Bound")
&& let Some(ps) = extract_time_ps(expr)
{
return Some(ps);
}

// String fallback
let raw = props
.get(SPAR_TIMING, "Interrupt_Latency_Bound")
.or_else(|| props.get("", "Interrupt_Latency_Bound"))?;
parse_time_value(raw)
}

/// Get `Spar_Timing::Bottom_Half_Server` reference name.
pub fn get_bottom_half_server(props: &PropertyMap) -> Option<String> {
// Typed path
if let Some(expr) = get_typed_qualified(props, SPAR_TIMING, "Bottom_Half_Server")
&& let Some(target) = extract_typed_reference(expr)
{
return Some(target.to_string());
}

// String fallback
let raw = props
.get(SPAR_TIMING, "Bottom_Half_Server")
.or_else(|| props.get("", "Bottom_Half_Server"))?;
extract_reference_target(raw).map(|s| s.to_string())
}

/// Get `Timing_Properties::Dispatch_Jitter` in picoseconds.
///
/// Note: Dispatch_Jitter lives under `Timing_Properties`, not `Spar_Timing`.
pub fn get_dispatch_jitter(props: &PropertyMap) -> Option<u64> {
get_timing_property(props, "Dispatch_Jitter")
}

/// Get `Thread_Properties::Dispatch_Protocol` as a string (e.g. "Sporadic", "Periodic").
///
/// Falls back to `Timing_Properties::Dispatch_Protocol` for legacy models.
pub fn get_dispatch_protocol(props: &PropertyMap) -> Option<String> {
// Typed path: Thread_Properties first
if let Some(expr) = get_typed_qualified(props, "Thread_Properties", "Dispatch_Protocol")
&& let Some(s) = extract_string(expr)
{
return Some(s);
}
// Legacy typed path: Timing_Properties
if let Some(expr) = get_typed_qualified(props, "Timing_Properties", "Dispatch_Protocol")
&& let Some(s) = extract_string(expr)
{
return Some(s);
}

// String fallback
props
.get("Thread_Properties", "Dispatch_Protocol")
.or_else(|| props.get("Timing_Properties", "Dispatch_Protocol"))
.or_else(|| props.get("", "Dispatch_Protocol"))
.map(|s| s.trim().to_string())
}

// ── AI_ML property accessors ───────────────────────────────────────

const AI_ML: &str = "AI_ML";
Expand Down
Loading
Loading