Skip to content

Commit 9ff68a0

Browse files
avrabeclaude
andauthored
feat(tsn): Spar_TSN::Hi_Credit + Lo_Credit user-tunable CBS (v0.9.2) (#195)
Reviewer Tier A #8 — v0.8.1 hardcoded `hi_credit_bytes` and `lo_credit_bytes` to `Spar_TSN::Max_Frame_Size` (default 1518 B) when constructing CbsReservation. Real Qcc/YANG configs (`ieee802-dot1q-bridge`, `tsn-stream`) carry these per traffic class — making the CBS recovery term `loCredit/|sendSlope|` constant + load-bearing on the bound for any tight AVB design. Add two properties to Spar_TSN: - `Hi_Credit` (aadlinteger units Size_Units; port, connection) - `Lo_Credit` (aadlinteger units Size_Units; port, connection) Property count: 129 → 131. Spar_TSN per-set count: 7 → 9. Accessors `get_hi_credit_bytes` and `get_lo_credit_bytes` follow the typed-first / string-fallback pattern of `get_max_frame_size_bytes`. The wctt CBS arm reads them from bus_props; when unset, falls back to `max_competing_frame_bytes` (preserves v0.8.1/v0.9.1 byte-identical output). New `WcttCbsCredit` Info diagnostic fires when at least one credit is explicit. REQ-TSN-005 + TEST-TSN-CBS-CREDITS. Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
1 parent 503b310 commit 9ff68a0

6 files changed

Lines changed: 122 additions & 8 deletions

File tree

artifacts/requirements.yaml

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1598,6 +1598,24 @@ artifacts:
15981598
status: implemented
15991599
tags: [analysis, arinc653, safety, v092]
16001600

1601+
- id: REQ-TSN-005
1602+
type: requirement
1603+
title: Spar_TSN::Hi_Credit + Lo_Credit user-tunable CBS credits
1604+
description: >
1605+
Spar_TSN::Hi_Credit and Spar_TSN::Lo_Credit (both
1606+
`aadlinteger units Size_Units`, applied to port and connection)
1607+
let users override the v0.8.1-default CBS credit bounds (which
1608+
were hardcoded to `max_competing_frame_bytes` for both, making
1609+
the CBS recovery term `loCredit/|sendSlope|` constant and
1610+
load-bearing on the bound for any tight AVB design). Real
1611+
Qcc/YANG configs (`ieee802-dot1q-bridge`, `tsn-stream`) carry
1612+
these per traffic class. v0.9.2 adds the property surface plus
1613+
the `WcttCbsCredit` Info diagnostic that fires when at least
1614+
one credit is explicit. Default unset → byte-identical to
1615+
v0.8.1/v0.9.1. Per the post-v0.9.0 reviewer's Tier A #8.
1616+
status: implemented
1617+
tags: [network, tsn, cbs, wctt, v092]
1618+
16011619
# ── Track G: spar-insight discrepancy assistant (v0.9.0) ──────────
16021620

16031621
- id: REQ-INSIGHT-001

artifacts/verification.yaml

Lines changed: 25 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2107,6 +2107,31 @@ artifacts:
21072107
- type: satisfies
21082108
target: REQ-ARINC-005
21092109

2110+
- id: TEST-TSN-CBS-CREDITS
2111+
type: feature
2112+
title: Spar_TSN::Hi_Credit + Lo_Credit user-tunable CBS credits
2113+
description: >
2114+
Verifies that `Spar_TSN::Hi_Credit` and `Spar_TSN::Lo_Credit`
2115+
register in the predeclared property tables (count 129 → 131,
2116+
Spar_TSN per-set 7 → 9), that `get_hi_credit_bytes` and
2117+
`get_lo_credit_bytes` accessors handle typed PropertyExpr +
2118+
string fallback paths and unit conversions, and that the wctt
2119+
CBS arm honours explicit credits in `CbsReservation::new` while
2120+
preserving v0.8.1 byte-identical output when both properties
2121+
are unset. The `WcttCbsCredit` Info diagnostic fires when at
2122+
least one of Hi_Credit / Lo_Credit is set on the bus.
2123+
fields:
2124+
method: automated-test
2125+
steps:
2126+
- run: cargo test -p spar-hir-def --lib -- standard_properties
2127+
- run: cargo test -p spar-network --lib -- tsn
2128+
- run: cargo test -p spar-analysis --lib -- wctt
2129+
status: passing
2130+
tags: [v0.9.2, network, tsn, cbs, wctt]
2131+
links:
2132+
- type: satisfies
2133+
target: REQ-TSN-005
2134+
21102135
- id: TEST-INSIGHT-DISCREPANCY
21112136
type: feature
21122137
title: spar-insight CTF parser + 5-kind discrepancy detection

crates/spar-analysis/src/wctt.rs

Lines changed: 32 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -58,8 +58,8 @@ use spar_network::extract::{
5858
use spar_network::tsn::{
5959
CbsReservation, ClassOfService, GateSchedule, cbs_residual_service, frame_quantization_ps,
6060
get_bandwidth_reservation_bps, get_class_of_service, get_frame_preemption, get_gate_schedule,
61-
get_max_frame_size_bytes, get_sync_error_ps, is_express_stream, preemption_blocking_term_ps,
62-
tas_residual_service_with_sync_error,
61+
get_hi_credit_bytes, get_lo_credit_bytes, get_max_frame_size_bytes, get_sync_error_ps,
62+
is_express_stream, preemption_blocking_term_ps, tas_residual_service_with_sync_error,
6363
};
6464
use spar_network::types::{NetworkGraph, NodeKind, SwitchType};
6565

@@ -356,11 +356,22 @@ impl WcttAnalysis {
356356
let link_rate_bps = read_output_rate_bps(bus_props).unwrap_or(0);
357357
let max_competing_frame_bytes = get_max_frame_size_bytes(bus_props)
358358
.unwrap_or(CBS_DEFAULT_COMPETING_FRAME_BYTES);
359+
// v0.9.2: explicit hi/loCredit override the v0.8.1
360+
// default (`max_competing_frame_bytes` for both),
361+
// letting users plug in real Qcc/YANG credit
362+
// numbers. Default unset = byte-identical to v0.8.1
363+
// / v0.9.1.
364+
let hi_credit_bytes =
365+
get_hi_credit_bytes(bus_props).unwrap_or(max_competing_frame_bytes);
366+
let lo_credit_bytes =
367+
get_lo_credit_bytes(bus_props).unwrap_or(max_competing_frame_bytes);
368+
let credits_explicit = get_hi_credit_bytes(bus_props).is_some()
369+
|| get_lo_credit_bytes(bus_props).is_some();
359370
let reservation = CbsReservation::new(
360371
idle_slope_bps,
361372
link_rate_bps,
362-
max_competing_frame_bytes,
363-
max_competing_frame_bytes,
373+
hi_credit_bytes,
374+
lo_credit_bytes,
364375
);
365376
if let Some(reservation) = reservation {
366377
let beta = cbs_residual_service(
@@ -392,6 +403,23 @@ impl WcttAnalysis {
392403
path: stream_path.clone(),
393404
analysis: self.name().to_string(),
394405
});
406+
if credits_explicit {
407+
diags.push(AnalysisDiagnostic {
408+
severity: Severity::Info,
409+
message: format!(
410+
"WcttCbsCredit: stream '{}' at hop {}: explicit \
411+
hi_credit={} B, lo_credit={} B (override default \
412+
max_competing_frame={} B)",
413+
stream_name,
414+
hop_idx,
415+
hi_credit_bytes,
416+
lo_credit_bytes,
417+
max_competing_frame_bytes,
418+
),
419+
path: stream_path.clone(),
420+
analysis: self.name().to_string(),
421+
});
422+
}
395423
beta
396424
} else if bus_preemption && stream.is_express {
397425
// CBS reservation invalid → fall back to

crates/spar-hir-def/src/standard_properties.rs

Lines changed: 15 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -517,6 +517,16 @@ const SPAR_TSN: &[(&str, &str)] = &[
517517
// accuracy. Default unset = 0 (legacy v0.8.1 behaviour).
518518
// Applies to bus and processor.
519519
("Sync_Error", "aadlinteger units Time_Units"),
520+
// CBS hi-credit / lo-credit (802.1Qav §34.5). Real Qcc/YANG configs
521+
// (`ieee802-dot1q-bridge`, `tsn-stream`) carry these explicitly per
522+
// traffic class. v0.8.1 hardcoded both to `Spar_TSN::Max_Frame_Size`
523+
// (default 1518 bytes) which made the CBS recovery term
524+
// `loCredit / |sendSlope|` constant and load-bearing on the bound
525+
// for any tight AVB design. v0.9.2 adds explicit overrides; when
526+
// unset the v0.8.1 default is preserved (byte-identical).
527+
// Applies to port and connection.
528+
("Hi_Credit", "aadlinteger units Size_Units"),
529+
("Lo_Credit", "aadlinteger units Size_Units"),
520530
];
521531

522532
/// Helper: collect properties from a table into the result vector.
@@ -1098,14 +1108,16 @@ mod tests {
10981108
assert!(is_standard_property_set("Spar_TSN"));
10991109

11001110
let props = standard_properties_in_set("Spar_TSN");
1101-
assert_eq!(props.len(), 7);
1111+
assert_eq!(props.len(), 9);
11021112
assert!(props.contains(&"Stream_ID"));
11031113
assert!(props.contains(&"Class_of_Service"));
11041114
assert!(props.contains(&"Gate_Control_List"));
11051115
assert!(props.contains(&"Max_Frame_Size"));
11061116
assert!(props.contains(&"Frame_Preemption"));
11071117
assert!(props.contains(&"Bandwidth_Reservation"));
11081118
assert!(props.contains(&"Sync_Error"));
1119+
assert!(props.contains(&"Hi_Credit"));
1120+
assert!(props.contains(&"Lo_Credit"));
11091121

11101122
// Each property resolves to its expected type.
11111123
assert_eq!(
@@ -1210,7 +1222,7 @@ mod tests {
12101222
#[test]
12111223
fn test_all_standard_properties_total_count() {
12121224
let all = all_standard_properties();
1213-
// 12 + 13 + 14 + 14 + 8 + 25 + 4 + 13 + 5 + 4 + 5 + 4 + 1 + 7 = 129
1225+
// 12 + 13 + 14 + 14 + 8 + 25 + 4 + 13 + 5 + 4 + 5 + 4 + 1 + 9 = 131
12141226
// (Timing + Communication + Memory + Deployment + Thread + Programming
12151227
// + Modeling + AADL_Project + Spar_Timing + Spar_Trace + Spar_Network
12161228
// + Spar_Migration + Spar_Power + Spar_TSN)
@@ -1222,7 +1234,7 @@ mod tests {
12221234
// Max_Frame_Size, Frame_Preemption (Track D Phase 2 v0.8.1 c1)
12231235
// +1 for Bandwidth_Reservation (Track D Phase 2 v0.8.1 c3, CBS).
12241236
// +1 for Sync_Error (v0.9.1 NC soundness, gPTP ε budget).
1225-
assert_eq!(all.len(), 129);
1237+
assert_eq!(all.len(), 131);
12261238
}
12271239

12281240
#[test]

crates/spar-network/src/lib.rs

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -57,6 +57,7 @@ pub use tsn::{
5757
CbsReservation, ClassOfService, CreditPool, GateSchedule, GateScheduleError, GateWindow,
5858
MIN_FRAGMENT_BYTES, PREEMPTION_HEADER_BYTES, cbs_residual_service,
5959
get_bandwidth_reservation_bps, get_class_of_service, get_frame_preemption, get_gate_schedule,
60-
is_express_stream, preemption_blocking_term_ps, tas_residual_service,
60+
get_hi_credit_bytes, get_lo_credit_bytes, is_express_stream, preemption_blocking_term_ps,
61+
tas_residual_service,
6162
};
6263
pub use types::{NetworkGraph, NetworkLink, NetworkNode, NodeKind, SwitchType};

crates/spar-network/src/tsn.rs

Lines changed: 30 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -313,6 +313,36 @@ pub fn get_max_frame_size_bytes(props: &PropertyMap) -> Option<u64> {
313313
parse_size_bytes(raw)
314314
}
315315

316+
/// Read [`Spar_TSN::Hi_Credit`] as the CBS hiCredit upper bound in
317+
/// bytes. Per IEEE 802.1Qav §34.5, hiCredit is the maximum positive
318+
/// credit a class can accumulate before sending; it bounds the
319+
/// burst-out tolerance. AADL declares the property as `aadlinteger
320+
/// units Size_Units` so it lowers via the same machinery as
321+
/// `Max_Frame_Size`. Returns `None` when unset (callers default to
322+
/// the pre-v0.9.2 behaviour of `Max_Frame_Size`).
323+
pub fn get_hi_credit_bytes(props: &PropertyMap) -> Option<u64> {
324+
if let Some(expr) = get_typed(props, "Hi_Credit") {
325+
return extract_size_bytes(expr);
326+
}
327+
let raw = get_raw(props, "Hi_Credit")?;
328+
parse_size_bytes(raw)
329+
}
330+
331+
/// Read [`Spar_TSN::Lo_Credit`] as the CBS loCredit lower bound in
332+
/// bytes (declared as a positive magnitude — the AVB spec uses a
333+
/// negative value but spar stores the absolute byte count). Per
334+
/// IEEE 802.1Qav §34.5, loCredit gives the worst-case credit
335+
/// drain, which combined with `|sendSlope|` yields the recovery
336+
/// time `T_recovery = loCredit / |sendSlope|` that lands in the
337+
/// CBS rate-latency service curve. Returns `None` when unset.
338+
pub fn get_lo_credit_bytes(props: &PropertyMap) -> Option<u64> {
339+
if let Some(expr) = get_typed(props, "Lo_Credit") {
340+
return extract_size_bytes(expr);
341+
}
342+
let raw = get_raw(props, "Lo_Credit")?;
343+
parse_size_bytes(raw)
344+
}
345+
316346
/// Read [`Spar_TSN::Frame_Preemption`] — whether frames in this
317347
/// class can be pre-empted by Express traffic (802.1Qbu).
318348
pub fn get_frame_preemption(props: &PropertyMap) -> Option<bool> {

0 commit comments

Comments
 (0)