feat(rta): PIP/PCP blocking term in hierarchical RTA (v0.7.1)

[avrabe]

Summary

Extends the v0.7.0 hierarchical IRQ-aware RTA (#147) with a configurable
blocking term B_i for tasks holding shared resources under
Priority_Inheritance_Protocol (PIP) or Priority_Ceiling_Protocol
(PCP), per Joseph & Pandya 1986 / Buttazzo, Hard Real-Time Computing
Systems. Discharges the v0.7.1 follow-up explicitly carved out by #147
/ #149.

The recurrence becomes:

R_i(0)   = C_i + J_i + B_i
R_i(n+1) = C_i + J_i + B_i
         + Σ_{j ∈ HP} ⌈(R_i(n) + J_j) / T_j⌉ × C_j
         + IsrInterference(p, R_i(n))

What's in this PR

• Property surface

  • Thread_Properties::Locking_Protocol (AS5506D §5.4.4 enum:
    Priority_Inheritance_Protocol, Priority_Ceiling_Protocol,
    Stop_For_Lock, None).
  • Spar_Timing::Critical_Section_Blocking (Time, picoseconds) — the
    user's bound on B_i.
  • Standard-property total count: 118 → 120.

• Typed accessors (property_accessors.rs)

  • LockingProtocol enum + get_locking_protocol(&PropertyMap).
  • get_critical_section_blocking(&PropertyMap) -> Option<u64>.

• Verified RTA (scheduling_verified.rs)

  • New compute_response_time_jittered_blocking(...) and
    rta_step_jittered_blocking(...). Convergence preserved (blocking
    is a constant; recurrence remains monotone non-decreasing in r).
  • Existing compute_response_time_jittered unchanged (no breaking API).

• RTA pass (rta.rs)

  • Reads Locking_Protocol + Critical_Section_Blocking per thread;
    only PIP/PCP contribute a blocking term (Stop_For_Lock/None
    degrade to B_i = 0).
  • Emits a per-thread BlockingInflated Info diagnostic when blocking

    0, naming the protocol and the magnitude.

  • BCET response-band re-run also threads the blocking term.

• Tests (8 new RTA tests + 4 scheduling-verified tests)

  • no_locking_matches_v070 (non-regression byte-for-byte gate)
  • pip_blocking_inflates_response, pcp_blocking_inflates_response
  • zero_blocking_no_diagnostic
  • blocking_plus_isr_compose, blocking_plus_jitter_compose
  • pip_deadline_miss_with_blocking
  • stop_for_lock_treated_as_no_blocking

• Rivet artifacts (append-only)

  • REQ-TIMING-PIP-001 requirement.
  • TEST-RTA-BLOCKING verification entry.

Non-regression

Models without Locking_Protocol produce byte-identical output to main:
compute_response_time_jittered_blocking(..., blocking=0, ...) reduces
to compute_response_time_jittered(...) term-by-term, and no
BlockingInflated diagnostic fires. The no_locking_matches_v070 test
asserts the golden snapshot of the prior basic_convergence_two_threads
model.

Deferred (out of scope for v0.7.1)

• Per-resource blocking analysis (computing B_i from declared shared
  resources rather than reading the user's bound directly) — v0.8.0+.
• Lean proof of compute_response_time_jittered_blocking convergence —
  Mathlib RTABlocking.lean is a v0.8.0 follow-up tracked separately.
• Other Track D / Track E surfaces and the v0.7.1 close-out
  COMPLIANCE.md update — separate commits.

Test plan

• cargo build --workspace clean
• cargo test -p spar-analysis green (814 lib + 3 fixture)
• cargo test -p spar-hir-def green (438 tests)
• cargo clippy --workspace --all-targets -- -D warnings clean
• cargo fmt --all -- --check clean
• rivet validate PASS

🤖 Generated with Claude Code

[codecov]

Codecov Report

❌ Patch coverage is 98.94459% with 4 lines in your changes missing coverage. Please review.

Files with missing lines	Patch %	Lines
crates/spar-analysis/src/rta.rs	98.63%	3 Missing ⚠️
crates/spar-analysis/src/scheduling_verified.rs	98.27%	1 Missing ⚠️

📢 Thoughts on this report? Let us know!