From c02e7c721e14c0fd3f0c6e0ae11bf0769770b953 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Sun, 26 Apr 2026 01:32:02 +0200 Subject: [PATCH] feat(rta): PIP/PCP blocking term in hierarchical RTA (v0.7.1) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Extends the v0.7.0 hierarchical IRQ-aware RTA with a configurable blocking term B_i for tasks holding shared resources under PIP or PCP. Reads AS5506 Thread_Properties::Locking_Protocol and a new Spar_Timing::Critical_Section_Blocking time value. Joseph-Pandya / Buttazzo: R_i(n+1) = C_i + J_i + B_i + Σ⌈...⌉·C_j + ISR. Non-regression: models without Locking_Protocol produce byte-identical output to main (verified by no_locking_matches_v070 test). Closes the v0.7.1 follow-up explicitly carved out by #147 / #149. New requirement: REQ-TIMING-PIP-001. Co-Authored-By: Claude Opus 4.7 (1M context) --- artifacts/requirements.yaml | 22 + artifacts/verification.yaml | 26 ++ .../spar-analysis/src/property_accessors.rs | 160 +++++++ crates/spar-analysis/src/rta.rs | 406 +++++++++++++++++- .../spar-analysis/src/scheduling_verified.rs | 103 +++++ .../spar-hir-def/src/standard_properties.rs | 30 +- 6 files changed, 722 insertions(+), 25 deletions(-) diff --git a/artifacts/requirements.yaml b/artifacts/requirements.yaml index 6e58593..b78efd4 100644 --- a/artifacts/requirements.yaml +++ b/artifacts/requirements.yaml @@ -1204,4 +1204,26 @@ artifacts: status: planned tags: [variants, track-b, v07x] + # ── PIP/PCP blocking term in hierarchical RTA (v0.7.1) ───────────── + + - id: REQ-TIMING-PIP-001 + type: requirement + title: PCP/PIP blocking analysis in hierarchical RTA + description: > + System shall support PCP/PIP blocking analysis. Threads declaring + Thread_Properties::Locking_Protocol => Priority_Inheritance_Protocol + or Priority_Ceiling_Protocol contribute a blocking term B_i to the + v0.7.0 hierarchical IRQ-aware RTA recurrence (Joseph & Pandya 1986; + Buttazzo, *Hard Real-Time Computing Systems*). The blocking-term + magnitude is read from the new Spar_Timing::Critical_Section_Blocking + property (Time, picoseconds) and represents the user's bound on how + long a higher-priority task can be blocked by lower-priority tasks + holding shared resources. Stop_For_Lock and None values opt out of + blocking analysis (B_i = 0). Scope is the simple-ceiling case; + per-resource blocking analysis with shared-resource declarations is + deferred to v0.8.0+. Discharges the v0.7.1 follow-up explicitly + carved out of #147 / #149. + status: implemented + tags: [timing, rta, pip, pcp, blocking, v071] + # Research findings tracked separately in research/findings.yaml diff --git a/artifacts/verification.yaml b/artifacts/verification.yaml index 689c144..9794dcb 100644 --- a/artifacts/verification.yaml +++ b/artifacts/verification.yaml @@ -1532,3 +1532,29 @@ artifacts: links: - type: satisfies target: REQ-VARIANT-001 + + - id: TEST-RTA-BLOCKING + type: feature + title: PIP/PCP blocking-term unit tests + description: > + Unit tests in crates/spar-analysis/src/rta.rs and + crates/spar-analysis/src/scheduling_verified.rs covering the + v0.7.1 blocking-term extension to the hierarchical IRQ-aware RTA. + Coverage includes: the no_locking_matches_v070 byte-for-byte + non-regression gate; PIP and PCP blocking inflating response + times by exactly the configured Spar_Timing::Critical_Section_Blocking + magnitude; the BlockingInflated Info diagnostic emitted only when + blocking > 0; ISR + blocking and jitter + blocking compositions; + blocking-induced deadline misses; and the Stop_For_Lock / None + Locking_Protocol values opting out of blocking analysis (B_i = 0). + Backed by scheduling_verified tests for the new + compute_response_time_jittered_blocking fixed-point function. + fields: + method: automated-test + steps: + - run: cargo test -p spar-analysis --lib -- rta::tests scheduling_verified property_accessors + status: passing + tags: [v0.7.1, timing, irq, rta, pip, pcp, blocking] + links: + - type: satisfies + target: REQ-TIMING-PIP-001 diff --git a/crates/spar-analysis/src/property_accessors.rs b/crates/spar-analysis/src/property_accessors.rs index 2a9be0a..dbf98a6 100644 --- a/crates/spar-analysis/src/property_accessors.rs +++ b/crates/spar-analysis/src/property_accessors.rs @@ -450,6 +450,73 @@ pub fn get_dispatch_jitter(props: &PropertyMap) -> Option { get_timing_property(props, "Dispatch_Jitter") } +/// AS5506D §5.4.4 `Thread_Properties::Locking_Protocol` enumeration. +/// +/// Drives the PIP/PCP blocking-term selection in the v0.7.1 +/// hierarchical RTA. `StopForLock` and `None` opt out of blocking +/// analysis (treated as no blocking term). +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub enum LockingProtocol { + /// `Priority_Inheritance_Protocol` — Sha-Rajkumar-Lehoczky 1990. + Pip, + /// `Priority_Ceiling_Protocol` — Sha-Rajkumar-Lehoczky 1990. + Pcp, + /// `Stop_For_Lock` — coarse stop-the-world lock; no inheritance. + StopForLock, + /// `None` — no shared resources / no blocking term. + None, +} + +/// Get `Thread_Properties::Locking_Protocol`. +/// +/// Returns `None` when the property is not set; otherwise returns +/// `Some(LockingProtocol)` parsed from the enum value (case-insensitive). +/// An unrecognised string returns `None`. +pub fn get_locking_protocol(props: &PropertyMap) -> Option { + // Typed path + let typed_str = get_typed_qualified(props, "Thread_Properties", "Locking_Protocol") + .and_then(extract_string); + let raw_str = typed_str.or_else(|| { + props + .get("Thread_Properties", "Locking_Protocol") + .or_else(|| props.get("", "Locking_Protocol")) + .map(|s| s.trim().to_string()) + })?; + parse_locking_protocol(&raw_str) +} + +/// Parse a `Locking_Protocol` enum string (case-insensitive). +fn parse_locking_protocol(s: &str) -> Option { + match s.trim().to_ascii_lowercase().as_str() { + "priority_inheritance_protocol" => Some(LockingProtocol::Pip), + "priority_ceiling_protocol" => Some(LockingProtocol::Pcp), + "stop_for_lock" => Some(LockingProtocol::StopForLock), + "none" => Some(LockingProtocol::None), + _ => None, + } +} + +/// Get `Spar_Timing::Critical_Section_Blocking` in picoseconds. +/// +/// User-supplied bound on how long a higher-priority task can be +/// blocked by lower-priority tasks holding shared resources, under +/// the configured `Thread_Properties::Locking_Protocol` (PIP/PCP). +/// When absent, the v0.7.1 RTA treats the blocking term as 0. +pub fn get_critical_section_blocking(props: &PropertyMap) -> Option { + // Typed path + if let Some(expr) = get_typed_qualified(props, SPAR_TIMING, "Critical_Section_Blocking") + && let Some(ps) = extract_time_ps(expr) + { + return Some(ps); + } + + // String fallback + let raw = props + .get(SPAR_TIMING, "Critical_Section_Blocking") + .or_else(|| props.get("", "Critical_Section_Blocking"))?; + parse_time_value(raw) +} + /// Get `Thread_Properties::Dispatch_Protocol` as a string (e.g. "Sporadic", "Periodic"). /// /// Falls back to `Timing_Properties::Dispatch_Protocol` for legacy models. @@ -1203,4 +1270,97 @@ mod tests { let expr = PropertyExpr::UnitValue(Box::new(inner), Name::new("ms")); assert_eq!(extract_time_ps(&expr), Some(2_500_000_000)); } + + // ── Locking_Protocol / Critical_Section_Blocking (v0.7.1) ─── + + #[test] + fn locking_protocol_pip_string() { + let props = make_props(&[( + "Thread_Properties", + "Locking_Protocol", + "Priority_Inheritance_Protocol", + )]); + assert_eq!(get_locking_protocol(&props), Some(LockingProtocol::Pip)); + } + + #[test] + fn locking_protocol_pcp_string() { + let props = make_props(&[( + "Thread_Properties", + "Locking_Protocol", + "Priority_Ceiling_Protocol", + )]); + assert_eq!(get_locking_protocol(&props), Some(LockingProtocol::Pcp)); + } + + #[test] + fn locking_protocol_stop_for_lock() { + let props = make_props(&[("Thread_Properties", "Locking_Protocol", "Stop_For_Lock")]); + assert_eq!( + get_locking_protocol(&props), + Some(LockingProtocol::StopForLock) + ); + } + + #[test] + fn locking_protocol_none_string() { + let props = make_props(&[("Thread_Properties", "Locking_Protocol", "None")]); + assert_eq!(get_locking_protocol(&props), Some(LockingProtocol::None)); + } + + #[test] + fn locking_protocol_case_insensitive() { + let props = make_props(&[( + "Thread_Properties", + "Locking_Protocol", + "priority_ceiling_protocol", + )]); + assert_eq!(get_locking_protocol(&props), Some(LockingProtocol::Pcp)); + } + + #[test] + fn locking_protocol_typed_enum() { + let props = make_typed_props( + "Thread_Properties", + "Locking_Protocol", + "Priority_Inheritance_Protocol", + PropertyExpr::Enum(Name::new("Priority_Inheritance_Protocol")), + ); + assert_eq!(get_locking_protocol(&props), Some(LockingProtocol::Pip)); + } + + #[test] + fn locking_protocol_unrecognised_returns_none() { + let props = make_props(&[("Thread_Properties", "Locking_Protocol", "Spinlock")]); + assert_eq!(get_locking_protocol(&props), None); + } + + #[test] + fn locking_protocol_missing_returns_none() { + let props = PropertyMap::new(); + assert_eq!(get_locking_protocol(&props), None); + } + + #[test] + fn critical_section_blocking_parses_us() { + let props = make_props(&[("Spar_Timing", "Critical_Section_Blocking", "100 us")]); + assert_eq!(get_critical_section_blocking(&props), Some(100_000_000)); + } + + #[test] + fn critical_section_blocking_typed() { + let props = make_typed_props( + "Spar_Timing", + "Critical_Section_Blocking", + "100 us", + PropertyExpr::Integer(100, Some(Name::new("us"))), + ); + assert_eq!(get_critical_section_blocking(&props), Some(100_000_000)); + } + + #[test] + fn critical_section_blocking_missing_returns_none() { + let props = PropertyMap::new(); + assert_eq!(get_critical_section_blocking(&props), None); + } } diff --git a/crates/spar-analysis/src/rta.rs b/crates/spar-analysis/src/rta.rs index 7512b84..a2287a6 100644 --- a/crates/spar-analysis/src/rta.rs +++ b/crates/spar-analysis/src/rta.rs @@ -7,18 +7,25 @@ //! unconditionally. Their CPU utilization is computed first; if the //! sum per CPU exceeds a configurable threshold (default 30%), an //! [`IsrOverloadedCpu`]-style error diagnostic fires. -//! * **Tier 2 — Task RTA with Tindell-Clark jitter and ISR -//! interference.** For each thread the worst-case response time is -//! computed via the jittered fixed-point +//! * **Tier 2 — Task RTA with Tindell-Clark jitter, ISR interference, +//! and PIP/PCP blocking.** For each thread the worst-case response +//! time is computed via the jittered, blocked fixed-point //! //! ```text -//! R(0) = C_i + J_i -//! R(n+1) = C_i + J_i +//! R(0) = C_i + J_i + B_i +//! R(n+1) = C_i + J_i + B_i //! + Σ_j ⌈(R(n) + J_j) / T_j⌉ × C_j (hp tasks) //! + Σ_k ⌈R(n) / T_k⌉ × C_k (ISRs on same CPU) //! ``` //! -//! implemented by [`scheduling_verified::compute_response_time_jittered`]. +//! implemented by +//! [`scheduling_verified::compute_response_time_jittered_blocking`]. +//! `B_i` comes from `Spar_Timing::Critical_Section_Blocking` and is +//! only applied when `Thread_Properties::Locking_Protocol` is set to +//! `Priority_Inheritance_Protocol` or `Priority_Ceiling_Protocol` +//! (see Joseph & Pandya 1986; Buttazzo, *Hard Real-Time Computing +//! Systems*). Other locking-protocol values (`Stop_For_Lock`, `None`) +//! degrade to the no-blocking recurrence. //! //! For Sporadic-dispatched threads reachable from an ISR (either by //! name via the device's `Bottom_Half_Server` property, or by being @@ -31,11 +38,13 @@ //! //! # Non-regression //! -//! Models without any `Spar_Timing::*` property produce diagnostics +//! Models without any `Spar_Timing::*` property and no +//! `Thread_Properties::Locking_Protocol` produce diagnostics //! byte-identical to the prior (classical) implementation. The -//! jittered recurrence with all jitters zero and no ISR interference -//! reduces to the classical recurrence, and no Spar_Timing-driven -//! diagnostic fires. See the `no_isrs_matches_classical_rta` test. +//! jittered, blocked recurrence with all jitters zero, no ISR +//! interference, and `B_i = 0` reduces to the classical recurrence, +//! and no Spar_Timing- or PIP/PCP-driven diagnostic fires. See the +//! `no_isrs_matches_classical_rta` and `no_locking_matches_v070` tests. use rustc_hash::FxHashMap; @@ -43,9 +52,10 @@ use spar_hir_def::instance::{ComponentInstanceIdx, SystemInstance}; use spar_hir_def::item_tree::ComponentCategory; use crate::property_accessors::{ - get_bottom_half_server, get_dispatch_jitter, get_dispatch_protocol, get_execution_time, - get_execution_time_range, get_interrupt_latency_bound, get_isr_execution_time_range, - get_isr_priority, get_processor_binding, get_timing_property, + LockingProtocol, get_bottom_half_server, get_critical_section_blocking, get_dispatch_jitter, + get_dispatch_protocol, get_execution_time, get_execution_time_range, + get_interrupt_latency_bound, get_isr_execution_time_range, get_isr_priority, + get_locking_protocol, get_processor_binding, get_timing_property, }; use crate::scheduling_verified::{self, RtaResult}; use crate::{Analysis, AnalysisDiagnostic, Severity, component_path}; @@ -206,6 +216,20 @@ impl Analysis for RtaAnalysis { let exec_range = get_execution_time_range(props); let dispatch_protocol = get_dispatch_protocol(props); + // ── PIP/PCP blocking term (v0.7.1). ────────────────────── + // + // Only PIP and PCP contribute a blocking term in the + // recurrence. `Stop_For_Lock` and `None` degrade to the + // no-blocking recurrence (Buttazzo, §7). Threads with no + // Locking_Protocol are non-regression: blocking_ps = 0. + let locking_protocol = get_locking_protocol(props); + let blocking_ps = match locking_protocol { + Some(LockingProtocol::Pip) | Some(LockingProtocol::Pcp) => { + get_critical_section_blocking(props).unwrap_or(0) + } + _ => 0, + }; + processor_threads .entry(binding) .or_default() @@ -219,6 +243,8 @@ impl Analysis for RtaAnalysis { jitter_ps, comp_idx: idx, dispatch_protocol, + locking_protocol, + blocking_ps, }); } @@ -299,10 +325,34 @@ impl Analysis for RtaAnalysis { let thread_path = component_path(instance, thread.comp_idx); - let result = scheduling_verified::compute_response_time_jittered( + // ── BlockingInflated (Info) — emitted before RTA so + // it appears in deterministic order for the thread. ─ + if thread.locking_protocol.is_some() && thread.blocking_ps > 0 { + let proto_name = match thread.locking_protocol { + Some(LockingProtocol::Pip) => "Priority_Inheritance_Protocol", + Some(LockingProtocol::Pcp) => "Priority_Ceiling_Protocol", + Some(LockingProtocol::StopForLock) => "Stop_For_Lock", + Some(LockingProtocol::None) => "None", + None => unreachable!(), + }; + diags.push(AnalysisDiagnostic { + severity: Severity::Info, + message: format!( + "thread '{}' blocking inflated by {} under {}", + thread.name, + format_time(thread.blocking_ps), + proto_name, + ), + path: thread_path.clone(), + analysis: self.name().to_string(), + }); + } + + let result = scheduling_verified::compute_response_time_jittered_blocking( thread.exec_ps, thread.deadline_ps, thread.jitter_ps, + thread.blocking_ps, &higher_priority_jittered, &isr_interference, ); @@ -345,13 +395,15 @@ impl Analysis for RtaAnalysis { if let Some(bcet_ps) = thread.exec_bcet_ps && bcet_ps != thread.exec_ps { - let r_bcet = scheduling_verified::compute_response_time_jittered( - bcet_ps, - thread.deadline_ps, - thread.jitter_ps, - &higher_priority_jittered, - &isr_interference, - ); + let r_bcet = + scheduling_verified::compute_response_time_jittered_blocking( + bcet_ps, + thread.deadline_ps, + thread.jitter_ps, + thread.blocking_ps, + &higher_priority_jittered, + &isr_interference, + ); if let RtaResult::Converged(r_b) = r_bcet { diags.push(AnalysisDiagnostic { severity: Severity::Info, @@ -452,6 +504,14 @@ struct RtaThreadInfo { comp_idx: ComponentInstanceIdx, /// `Thread_Properties::Dispatch_Protocol` string, if set. dispatch_protocol: Option, + /// `Thread_Properties::Locking_Protocol`, if set. Only PIP and PCP + /// produce a blocking term in the v0.7.1 RTA recurrence. + locking_protocol: Option, + /// Effective blocking term `B_i` in picoseconds. Zero when no + /// `Locking_Protocol` is set, when the protocol does not request + /// blocking analysis (`Stop_For_Lock`, `None`), or when + /// `Spar_Timing::Critical_Section_Blocking` is absent. + blocking_ps: u64, } /// Per-CPU ISR record for Tier 1 utilization. @@ -1373,6 +1433,310 @@ mod tests { assert_eq!(make(false), make(true)); } + // ╔══════════════════════════════════════════════════════════════╗ + // ║ v0.7.1 PIP/PCP blocking-term tests ║ + // ╚══════════════════════════════════════════════════════════════╝ + + /// Helper: set Locking_Protocol + Critical_Section_Blocking on a thread. + fn set_blocking(b: &mut TestBuilder, idx: ComponentInstanceIdx, proto: &str, blocking: &str) { + b.set_property(idx, "Thread_Properties", "Locking_Protocol", proto); + b.set_property(idx, "Spar_Timing", "Critical_Section_Blocking", blocking); + } + + /// Helper: build the basic_convergence_two_threads model and analyze. + fn make_two_thread_model_diags( + with_proto: Option<&str>, + with_blocking: Option<&str>, + ) -> Vec { + let (mut b, root, proc) = make_base(); + let t1 = b.add_component("t1", ComponentCategory::Thread, Some(proc)); + let t2 = b.add_component("t2", ComponentCategory::Thread, Some(proc)); + + b.set_children( + root, + vec![ + ComponentInstanceIdx::from_raw(la_arena::RawIdx::from_u32(1)), + proc, + ], + ); + b.set_children(proc, vec![t1, t2]); + + bind_thread(&mut b, t1, "10 ms", "1 ms", None); + bind_thread(&mut b, t2, "20 ms", "2 ms", None); + + if let Some(proto) = with_proto { + b.set_property(t2, "Thread_Properties", "Locking_Protocol", proto); + } + if let Some(blk) = with_blocking { + b.set_property(t2, "Spar_Timing", "Critical_Section_Blocking", blk); + } + + let inst = b.build(root); + RtaAnalysis.analyze(&inst) + } + + // ── B1: non-regression — no Locking_Protocol must match v0.7.0 byte-for-byte ─ + #[test] + fn no_locking_matches_v070() { + // No Locking_Protocol on any thread: diagnostics must be + // identical to the v0.7.0 baseline (the same test set that + // `no_isrs_matches_classical_rta` checks against). + let diags = make_two_thread_model_diags(None, None); + + // No BlockingInflated diagnostic of any kind. + for d in &diags { + assert!( + !d.message.contains("blocking inflated"), + "no Locking_Protocol must not emit BlockingInflated, got: {}", + d.message, + ); + } + + // Golden snapshot identical to the v0.7.0 classical-RTA snapshot. + let mut msgs: Vec = diags.iter().map(|d| d.message.clone()).collect(); + msgs.sort(); + let expected: Vec = vec![ + "thread 't1' on processor 'cpu1': response time 1.00 ms <= deadline 10.00 ms" + .to_string(), + "thread 't2' on processor 'cpu1': response time 3.00 ms <= deadline 20.00 ms" + .to_string(), + ]; + assert_eq!(msgs, expected, "v0.7.0 byte-for-byte non-regression"); + } + + // ── B2: PIP blocking inflates response by exactly the configured amount ─ + #[test] + fn pip_blocking_inflates_response() { + // Baseline (no blocking): t2 response = 3.00 ms. + // With PIP + 100us blocking: response = 3.10 ms (additive). + let diags = + make_two_thread_model_diags(Some("Priority_Inheritance_Protocol"), Some("100 us")); + + let info = diags + .iter() + .find(|d| { + d.severity == Severity::Info + && d.message.contains("thread 't2'") + && d.message.contains("response time") + }) + .unwrap_or_else(|| panic!("no t2 response diagnostic: {:#?}", diags)); + assert!( + info.message.contains("3.10 ms"), + "PIP +100us must inflate to 3.10 ms, got: {}", + info.message, + ); + + // BlockingInflated Info diagnostic emitted with magnitude. + let blk = diags + .iter() + .find(|d| d.message.contains("blocking inflated")) + .unwrap_or_else(|| panic!("no BlockingInflated diagnostic: {:#?}", diags)); + assert_eq!(blk.severity, Severity::Info); + assert!(blk.message.contains("Priority_Inheritance_Protocol")); + assert!(blk.message.contains("100.00 us")); + } + + // ── B3: PCP blocking inflates response by exactly the configured amount ─ + #[test] + fn pcp_blocking_inflates_response() { + let diags = make_two_thread_model_diags(Some("Priority_Ceiling_Protocol"), Some("100 us")); + + let info = diags + .iter() + .find(|d| { + d.severity == Severity::Info + && d.message.contains("thread 't2'") + && d.message.contains("response time") + }) + .unwrap_or_else(|| panic!("no t2 response diagnostic: {:#?}", diags)); + assert!( + info.message.contains("3.10 ms"), + "PCP +100us must inflate to 3.10 ms, got: {}", + info.message, + ); + + let blk = diags + .iter() + .find(|d| d.message.contains("blocking inflated")) + .unwrap_or_else(|| panic!("no BlockingInflated diagnostic: {:#?}", diags)); + assert!(blk.message.contains("Priority_Ceiling_Protocol")); + } + + // ── B4: zero blocking value emits no BlockingInflated diagnostic ─ + #[test] + fn zero_blocking_no_diagnostic() { + // PIP set but Critical_Section_Blocking = 0 → no diagnostic. + let diags = + make_two_thread_model_diags(Some("Priority_Inheritance_Protocol"), Some("0 us")); + assert!( + !diags + .iter() + .any(|d| d.message.contains("blocking inflated")), + "zero blocking must not emit BlockingInflated: {:#?}", + diags, + ); + } + + // ── B5: ISR + blocking compose additively ────────────────────── + #[test] + fn blocking_plus_isr_compose() { + // CPU1: one ISR (T=2ms, C=100us) + one task (C=8ms, T=10ms, + // D=10ms). Without blocking and with the 5% ISR: + // R0 = 8ms; R1 = 8 + ⌈8/2⌉*100us = 8.4ms; R2 = 8 + ⌈8.4/2⌉*100us = 8.5ms; + // R3 = 8 + ⌈8.5/2⌉*100us = 8.5ms (fixed). + // With PCP + 200us blocking, every iterate adds +200us: + // R0 = 8.2ms; R1 = 8.2 + ⌈8.2/2⌉*100us = 8.7ms (was 8.4ms); + // R2 = 8.2 + ⌈8.7/2⌉*100us = 8.7ms (fixed). + let (mut b, root, proc) = make_base(); + let dev = add_isr_device(&mut b, root, "irq_src", "2 ms", "100 us", 99); + let t1 = b.add_component("t1", ComponentCategory::Thread, Some(proc)); + + b.set_children( + root, + vec![ + ComponentInstanceIdx::from_raw(la_arena::RawIdx::from_u32(1)), + proc, + dev, + ], + ); + b.set_children(proc, vec![t1]); + + bind_thread(&mut b, t1, "10 ms", "8 ms", Some("10 ms")); + set_blocking(&mut b, t1, "Priority_Ceiling_Protocol", "200 us"); + + let inst = b.build(root); + let diags = RtaAnalysis.analyze(&inst); + + let info = diags + .iter() + .find(|d| { + d.severity == Severity::Info + && d.message.contains("thread 't1'") + && d.message.contains("response time") + }) + .unwrap_or_else(|| panic!("no t1 response diag: {:#?}", diags)); + // ISR (8.5ms) + 200us blocking = 8.70 ms. Both terms applied. + assert!( + info.message.contains("8.70 ms"), + "ISR (8.50ms) + blocking (200us) must compose to 8.70 ms: {}", + info.message, + ); + + // BlockingInflated is also present. + assert!( + diags + .iter() + .any(|d| d.message.contains("blocking inflated")), + "expected BlockingInflated diagnostic: {:#?}", + diags, + ); + } + + // ── B6: jitter + blocking compose ────────────────────────────── + #[test] + fn blocking_plus_jitter_compose() { + // Single task with own Dispatch_Jitter = 50us and PIP blocking + // 75us: R = C + J + B = 1.000ms + 50us + 75us = 1.125 ms. + let (mut b, root, proc) = make_base(); + let t1 = b.add_component("t1", ComponentCategory::Thread, Some(proc)); + b.set_children( + root, + vec![ + ComponentInstanceIdx::from_raw(la_arena::RawIdx::from_u32(1)), + proc, + ], + ); + b.set_children(proc, vec![t1]); + + bind_thread(&mut b, t1, "10 ms", "1 ms", Some("10 ms")); + b.set_property(t1, "Timing_Properties", "Dispatch_Jitter", "50 us"); + set_blocking(&mut b, t1, "Priority_Inheritance_Protocol", "75 us"); + + let inst = b.build(root); + let diags = RtaAnalysis.analyze(&inst); + + let info = diags + .iter() + .find(|d| { + d.severity == Severity::Info + && d.message.contains("thread 't1'") + && d.message.contains("response time") + }) + .unwrap_or_else(|| panic!("no t1 response diag: {:#?}", diags)); + assert!( + info.message.contains("1.13 ms") || info.message.contains("1.12 ms"), + "jitter + blocking must compose to ~1.125 ms: {}", + info.message, + ); + } + + // ── B7: blocking forces a deadline miss ──────────────────────── + #[test] + fn pip_deadline_miss_with_blocking() { + // Single task: C=8ms, T=10ms, D=10ms, no HP, no ISR. + // Without blocking: R = 8ms, slack 2ms. + // With PIP + 3ms blocking: R = 11ms > D=10ms → Error. + let (mut b, root, proc) = make_base(); + let t1 = b.add_component("t1", ComponentCategory::Thread, Some(proc)); + b.set_children( + root, + vec![ + ComponentInstanceIdx::from_raw(la_arena::RawIdx::from_u32(1)), + proc, + ], + ); + b.set_children(proc, vec![t1]); + + bind_thread(&mut b, t1, "10 ms", "8 ms", Some("10 ms")); + set_blocking(&mut b, t1, "Priority_Inheritance_Protocol", "3 ms"); + + let inst = b.build(root); + let diags = RtaAnalysis.analyze(&inst); + + let err = diags + .iter() + .find(|d| { + d.severity == Severity::Error + && d.message.contains("thread 't1'") + && d.message.contains("misses deadline") + }) + .unwrap_or_else(|| panic!("expected deadline miss: {:#?}", diags)); + let _ = err; + } + + // ── B8: Stop_For_Lock and None opt out of blocking ───────────── + #[test] + fn stop_for_lock_treated_as_no_blocking() { + // Stop_For_Lock with a non-zero Critical_Section_Blocking must + // be ignored — blocking term is 0, no BlockingInflated, and + // response time is the no-blocking baseline (3.00 ms). + for proto in &["Stop_For_Lock", "None"] { + let diags = make_two_thread_model_diags(Some(proto), Some("100 us")); + assert!( + !diags + .iter() + .any(|d| d.message.contains("blocking inflated")), + "{} must not emit BlockingInflated: {:#?}", + proto, + diags, + ); + let info = diags + .iter() + .find(|d| { + d.severity == Severity::Info + && d.message.contains("thread 't2'") + && d.message.contains("response time") + }) + .unwrap(); + assert!( + info.message.contains("3.00 ms"), + "{} must NOT inflate response time, got: {}", + proto, + info.message, + ); + } + } + // ── T10: ISR priority preempts regardless of task priority ───── #[test] fn isr_priority_above_all_tasks() { diff --git a/crates/spar-analysis/src/scheduling_verified.rs b/crates/spar-analysis/src/scheduling_verified.rs index ced52e8..d2c1b88 100644 --- a/crates/spar-analysis/src/scheduling_verified.rs +++ b/crates/spar-analysis/src/scheduling_verified.rs @@ -187,6 +187,75 @@ pub fn compute_response_time_jittered( RtaResult::Diverged } +/// Jittered RTA recurrence with ISR interference and a PIP/PCP blocking term. +/// +/// Joseph & Pandya 1986 / Buttazzo: the blocking term `B_i` is the +/// maximum time the task can be blocked by lower-priority tasks +/// holding shared resources under the configured Locking_Protocol. +/// Modelled here as a constant added per step: +/// +/// ```text +/// R_{n+1} = exec + jitter + blocking +/// + Σ_{hp j} ⌈(R_n + J_j)/T_j⌉ × C_j +/// + Σ_{ISR k} ⌈R_n / T_k⌉ × C_k +/// ``` +/// +/// Convergence: `blocking` is a constant, so the recurrence remains +/// monotone non-decreasing in `r` and bounded above by `deadline + 1`, +/// preserving the proven termination argument. +#[inline] +pub fn rta_step_jittered_blocking( + exec: u64, + jitter: u64, + blocking: u64, + higher_priority_jittered: &[(u64, u64, u64)], + isr_interference: &[(u64, u64)], + r: u64, +) -> u64 { + rta_step_jittered(exec, jitter, higher_priority_jittered, isr_interference, r) + .saturating_add(blocking) +} + +/// Compute worst-case response time with jitter, ISR interference, and +/// a PIP/PCP blocking term `B_i`. +/// +/// When `blocking == 0` this reduces to +/// [`compute_response_time_jittered`] exactly (every iterate is identical). +/// +/// Max iterations bounded by `deadline + 1` (monotone convergence). +pub fn compute_response_time_jittered_blocking( + exec: u64, + deadline: u64, + jitter: u64, + blocking: u64, + higher_priority_jittered: &[(u64, u64, u64)], + isr_interference: &[(u64, u64)], +) -> RtaResult { + // Initial value: exec + own jitter + blocking (the minimum response window). + let mut r = exec.saturating_add(jitter).saturating_add(blocking); + if r > deadline { + return RtaResult::Diverged; + } + for _ in 0..=deadline { + let new_r = rta_step_jittered_blocking( + exec, + jitter, + blocking, + higher_priority_jittered, + isr_interference, + r, + ); + if new_r == r { + return RtaResult::Converged(r); + } + if new_r > deadline { + return RtaResult::Diverged; + } + r = new_r; + } + RtaResult::Diverged +} + #[cfg(test)] mod tests { use super::*; @@ -311,4 +380,38 @@ mod tests { let r = compute_response_time_jittered(8, 10, 0, &[(10, 5, 0)], &[]); assert_eq!(r, RtaResult::Diverged); } + + // ── Blocking-term recurrence tests (v0.7.1) ──────────────────── + + #[test] + fn blocking_zero_matches_jittered() { + // Identical to compute_response_time_jittered when blocking=0. + let hp = [(10, 2, 0)]; + let r_b = compute_response_time_jittered_blocking(3, 100, 0, 0, &hp, &[]); + let r_j = compute_response_time_jittered(3, 100, 0, &hp, &[]); + assert_eq!(r_b, r_j); + } + + #[test] + fn blocking_inflates_by_constant() { + // Single task, no HP, no ISR, B=2: R = C + B = 3 + 2 = 5. + let r = compute_response_time_jittered_blocking(3, 10, 0, 2, &[], &[]); + assert_eq!(r, RtaResult::Converged(5)); + } + + #[test] + fn blocking_plus_isr_compose() { + // C=3, D=100, B=5, ISR T=10 C=1. + // Without blocking: jittered → R0=3, R1=3+ceil(3/10)*1=4, R2=3+ceil(4/10)*1=4. R=4. + // With B=5: every iterate adds +5 → R=9. + let r = compute_response_time_jittered_blocking(3, 100, 0, 5, &[], &[(10, 1)]); + assert_eq!(r, RtaResult::Converged(9)); + } + + #[test] + fn blocking_diverges_on_overflow_of_deadline() { + // C=8, D=10, B=5: even before any HP/ISR work, exec+B=13 > D=10. + let r = compute_response_time_jittered_blocking(8, 10, 0, 5, &[], &[]); + assert_eq!(r, RtaResult::Diverged); + } } diff --git a/crates/spar-hir-def/src/standard_properties.rs b/crates/spar-hir-def/src/standard_properties.rs index ab05d4e..9fa61e7 100644 --- a/crates/spar-hir-def/src/standard_properties.rs +++ b/crates/spar-hir-def/src/standard_properties.rs @@ -177,6 +177,14 @@ const THREAD_PROPERTIES: &[(&str, &str)] = &[ "Active_Thread_Queue_Handling_Protocol", "enumeration (flush, hold)", ), + // AS5506D §5.4.4: concurrency control protocol used for shared + // resources accessed by this thread. `Priority_Inheritance_Protocol` + // and `Priority_Ceiling_Protocol` enable PIP/PCP blocking analysis + // in the v0.7.1 hierarchical RTA; `Stop_For_Lock` and `None` opt out. + ( + "Locking_Protocol", + "enumeration (Priority_Ceiling_Protocol, Priority_Inheritance_Protocol, Stop_For_Lock, None)", + ), ]; // ── Programming_Properties ────────────────────────────────────────── @@ -313,6 +321,12 @@ const SPAR_TIMING: &[(&str, &str)] = &[ // 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)"), + // User-supplied bound on how long a higher-priority task can be + // blocked by lower-priority tasks holding shared resources, under + // the configured Thread_Properties::Locking_Protocol (PIP/PCP). + // Drives the B_i term in the v0.7.1 hierarchical RTA recurrence. + // Applies to thread. + ("Critical_Section_Blocking", "Time"), ]; // ── Spar_Trace ────────────────────────────────────────────────────── @@ -619,7 +633,7 @@ mod tests { #[test] fn test_standard_properties_in_thread() { let props = standard_properties_in_set("Thread_Properties"); - assert_eq!(props.len(), 7); + assert_eq!(props.len(), 8); assert!(props.contains(&"Dispatch_Protocol")); assert!(props.contains(&"Dispatch_Trigger")); assert!(props.contains(&"Priority")); @@ -627,6 +641,7 @@ mod tests { assert!(props.contains(&"POSIX_Scheduling_Policy")); assert!(props.contains(&"Active_Thread_Handling_Protocol")); assert!(props.contains(&"Active_Thread_Queue_Handling_Protocol")); + assert!(props.contains(&"Locking_Protocol")); } #[test] @@ -695,11 +710,12 @@ mod tests { assert!(is_standard_property_set("Spar_Timing")); let props = standard_properties_in_set("Spar_Timing"); - assert_eq!(props.len(), 4); + assert_eq!(props.len(), 5); assert!(props.contains(&"ISR_Priority")); assert!(props.contains(&"ISR_Execution_Time")); assert!(props.contains(&"Interrupt_Latency_Bound")); assert!(props.contains(&"Bottom_Half_Server")); + assert!(props.contains(&"Critical_Section_Blocking")); // Each property resolves to its expected type. assert_eq!( @@ -718,6 +734,10 @@ mod tests { standard_property_type("Spar_Timing", "Bottom_Half_Server"), Some("reference (thread)") ); + assert_eq!( + standard_property_type("Spar_Timing", "Critical_Section_Blocking"), + Some("Time") + ); // Deliberately-wrong name returns None. assert_eq!(standard_property_type("Spar_Timing", "Nonexistent"), None); @@ -981,11 +1001,13 @@ mod tests { #[test] fn test_all_standard_properties_total_count() { let all = all_standard_properties(); - // 12 + 13 + 14 + 14 + 7 + 25 + 4 + 13 + 4 + 4 + 4 + 4 = 118 + // 12 + 13 + 14 + 14 + 8 + 25 + 4 + 13 + 5 + 4 + 4 + 4 = 120 // (Timing + Communication + Memory + Deployment + Thread + Programming // + Modeling + AADL_Project + Spar_Timing + Spar_Trace + Spar_Network // + Spar_Migration) - assert_eq!(all.len(), 118); + // Thread_Properties: +1 for Locking_Protocol (v0.7.1 PIP/PCP). + // Spar_Timing: +1 for Critical_Section_Blocking (v0.7.1 PIP/PCP). + assert_eq!(all.len(), 120); } #[test]