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
22 changes: 22 additions & 0 deletions artifacts/requirements.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -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
26 changes: 26 additions & 0 deletions artifacts/verification.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -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
160 changes: 160 additions & 0 deletions crates/spar-analysis/src/property_accessors.rs
Original file line number Diff line number Diff line change
Expand Up @@ -450,6 +450,73 @@ pub fn get_dispatch_jitter(props: &PropertyMap) -> Option<u64> {
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<LockingProtocol> {
// 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<LockingProtocol> {
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<u64> {
// 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.
Expand Down Expand Up @@ -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);
}
}
Loading
Loading