From b0692c6a693688e6ab436410ce28f073ece7ab1f Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Sat, 25 Apr 2026 16:13:31 +0200 Subject: [PATCH] feat(network): NetworkGraph types + extractor (Track D commit 2/6) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Adds the bridge between AADL ItemTree and WCTT analysis. crates/spar-network/src/types.rs — NetworkNode, NetworkLink, SwitchType, NetworkGraph. Switch types: FIFO/Priority (Phase 1) and TSN (opaque until Phase 2's service curves land). crates/spar-network/src/extract.rs — walks SystemInstance, reads Spar_Network::* properties, emits a typed NetworkGraph. No Network Calculus, no analysis pass, no latency.rs integration — those are Track D commits 3, 4, and 6 respectively. New requirement: REQ-NETWORK-004. Co-Authored-By: Claude Opus 4.7 (1M context) --- Cargo.lock | 4 + artifacts/requirements.yaml | 15 + artifacts/verification.yaml | 31 ++ crates/spar-network/Cargo.toml | 2 + crates/spar-network/src/extract.rs | 548 +++++++++++++++++++++ crates/spar-network/src/lib.rs | 61 +-- crates/spar-network/src/types.rs | 211 ++++++++ crates/spar-network/tests/extract_tests.rs | 314 ++++++++++++ 8 files changed, 1152 insertions(+), 34 deletions(-) create mode 100644 crates/spar-network/src/extract.rs create mode 100644 crates/spar-network/src/types.rs create mode 100644 crates/spar-network/tests/extract_tests.rs diff --git a/Cargo.lock b/Cargo.lock index f140fbc..ea7ffc5 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -1299,6 +1299,10 @@ dependencies = [ [[package]] name = "spar-network" version = "0.6.0" +dependencies = [ + "spar-base-db", + "spar-hir-def", +] [[package]] name = "spar-parser" diff --git a/artifacts/requirements.yaml b/artifacts/requirements.yaml index c17def7..7d13d90 100644 --- a/artifacts/requirements.yaml +++ b/artifacts/requirements.yaml @@ -1153,4 +1153,19 @@ artifacts: status: planned tags: [migration, track-e, v080, audit] + - id: REQ-NETWORK-004 + type: requirement + title: Typed network graph extraction from a SystemInstance + description: > + System shall extract a typed network graph (nodes + links) from + a SystemInstance for downstream WCTT analysis. Nodes classify as + switches (bus components carrying Spar_Network::Switch_Type) or + end stations (devices/processors connected to a switched bus); + links carry the per-hop bandwidth, forwarding-latency range, and + queue-depth annotations from Spar_Network::*. The graph is the + bridge between the AADL ItemTree and the Network Calculus + primitives that follow in subsequent Track D commits. + status: planned + tags: [network, wctt, v080] + # Research findings tracked separately in research/findings.yaml diff --git a/artifacts/verification.yaml b/artifacts/verification.yaml index 39f649b..8d8e0d0 100644 --- a/artifacts/verification.yaml +++ b/artifacts/verification.yaml @@ -1445,3 +1445,34 @@ artifacts: target: REQ-MIGRATION-001 - type: satisfies target: REQ-MIGRATION-002 + + - id: TEST-SPAR-NETWORK-GRAPH + type: feature + title: Network graph extraction tests + description: > + Integration tests in crates/spar-network/tests/extract_tests.rs + that drive small inline AADL fixtures through the spar-hir-def + pipeline and call extract_network_graph on the resulting + SystemInstance. Coverage includes a simple FIFO topology + (switch + two end stations), a Priority switch classification, + a TSN switch (classified but otherwise opaque per Phase 1), an + unannotated bus that must be skipped, and a Forwarding_Latency + range that must lower to a (BCET, WCET) tuple in picoseconds. + Backed by unit tests in spar-network's types and extract modules + that exercise the SwitchType enum parsing and the typed-first / + string-fallback property accessors. + fields: + method: automated-test + steps: + - run: cargo test -p spar-network + status: passing + tags: [v0.8.0, network, wctt, tsn, extract] + links: + - type: satisfies + target: REQ-NETWORK-001 + - type: satisfies + target: REQ-NETWORK-002 + - type: satisfies + target: REQ-NETWORK-003 + - type: satisfies + target: REQ-NETWORK-004 diff --git a/crates/spar-network/Cargo.toml b/crates/spar-network/Cargo.toml index 1bb9936..1e458bc 100644 --- a/crates/spar-network/Cargo.toml +++ b/crates/spar-network/Cargo.toml @@ -7,5 +7,7 @@ repository.workspace = true description = "Network Calculus primitives for AADL WCTT analysis (TSN/Ethernet, Track D)" [dependencies] +spar-hir-def.workspace = true [dev-dependencies] +spar-base-db.workspace = true diff --git a/crates/spar-network/src/extract.rs b/crates/spar-network/src/extract.rs new file mode 100644 index 0000000..38dc98c --- /dev/null +++ b/crates/spar-network/src/extract.rs @@ -0,0 +1,548 @@ +//! Extract a [`NetworkGraph`] from a [`SystemInstance`] by walking the +//! bus and device components and reading their `Spar_Network::*` +//! properties. +//! +//! This is the bridge between the AADL ItemTree and the WCTT analysis +//! that lands in later Track D commits. The algorithm is intentionally +//! lightweight: it walks the existing [`SystemInstance`] data, classifies +//! buses by `Switch_Type`, classifies devices/processors connected to +//! those buses as end stations, and emits one [`NetworkLink`] per AADL +//! connection that traverses a switched bus. +//! +//! We **complement** rather than duplicate `bus_bandwidth.rs` and +//! `connectivity.rs` in `spar-analysis`: those passes inspect the same +//! AADL data for different purposes (capacity check, dangling +//! connections), whereas this module distills the data into the typed +//! shape required by Network Calculus. + +use spar_hir_def::instance::{ComponentInstanceIdx, SystemInstance}; +use spar_hir_def::item_tree::{ComponentCategory, PropertyExpr}; +use spar_hir_def::name::Name; +use spar_hir_def::properties::PropertyMap; +use spar_hir_def::property_value::parse_time_value; + +use crate::types::{NetworkGraph, NetworkLink, NetworkNode, NodeKind, SwitchType}; + +const SPAR_NETWORK: &str = "Spar_Network"; + +// ── Property accessors ─────────────────────────────────────────────── +// +// Mirrors the typed-first / string-fallback idiom from +// `spar-analysis::property_accessors`. We re-implement the small set +// we need locally rather than introducing a `spar-analysis -> spar-network` +// dependency in the wrong direction. + +/// Get a typed [`PropertyExpr`] for a `Spar_Network::` property, +/// falling back to an unqualified lookup. +fn get_typed_spar_network<'a>(props: &'a PropertyMap, name: &str) -> Option<&'a PropertyExpr> { + props + .get_typed(SPAR_NETWORK, name) + .or_else(|| props.get_typed("", name)) +} + +/// Get the raw string value for a `Spar_Network::` property, +/// falling back to an unqualified lookup. +fn get_raw_spar_network<'a>(props: &'a PropertyMap, name: &str) -> Option<&'a str> { + props + .get(SPAR_NETWORK, name) + .or_else(|| props.get("", name)) +} + +/// Read `Spar_Network::Switch_Type` and return the matched [`SwitchType`]. +/// +/// Returns `None` if the property is unset, has a value not recognised +/// by [`SwitchType::from_aadl_enum`], or is a typed expression that is +/// neither a [`PropertyExpr::Enum`] nor a [`PropertyExpr::StringLit`]. +pub fn read_switch_type(props: &PropertyMap) -> Option { + if let Some(expr) = get_typed_spar_network(props, "Switch_Type") { + match expr { + PropertyExpr::Enum(name) => return SwitchType::from_aadl_enum(name.as_str()), + PropertyExpr::StringLit(s) => return SwitchType::from_aadl_enum(s), + _ => { /* fall through to string */ } + } + } + + let raw = get_raw_spar_network(props, "Switch_Type")?; + SwitchType::from_aadl_enum(raw.trim().trim_matches('"')) +} + +/// Read `Spar_Network::Queue_Depth` as a frame count. +pub fn read_queue_depth(props: &PropertyMap) -> Option { + if let Some(expr) = get_typed_spar_network(props, "Queue_Depth") + && let PropertyExpr::Integer(v, _) = expr + && *v >= 0 + { + return Some(*v as u64); + } + + let raw = get_raw_spar_network(props, "Queue_Depth")?; + raw.trim().parse::().ok() +} + +/// Read `Spar_Network::Forwarding_Latency` as a `(BCET, WCET)` range in +/// picoseconds. +pub fn read_forwarding_latency_ps(props: &PropertyMap) -> Option<(u64, u64)> { + if let Some(expr) = get_typed_spar_network(props, "Forwarding_Latency") { + if let PropertyExpr::Range { min, max, .. } = expr { + let min_ps = extract_time_ps(min)?; + let max_ps = extract_time_ps(max)?; + return Some((min_ps, max_ps)); + } + if let Some(v) = extract_time_ps(expr) { + return Some((v, v)); + } + } + + let raw = get_raw_spar_network(props, "Forwarding_Latency")?; + 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 v = parse_time_value(raw)?; + Some((v, v)) + } +} + +/// Read `Spar_Network::Output_Rate` as bandwidth in bits per second. +/// +/// AADL's `Data_Rate` is a unit-typed integer (`aadlinteger units +/// Data_Rate_Units`). We accept the common units shipped by the AADL +/// project (`bitsps`, `Bytesps`, `KBytesps`, `MBytesps`, `GBytesps`) +/// case-insensitively. A bare integer is interpreted as bits per second. +pub fn read_output_rate_bps(props: &PropertyMap) -> Option { + if let Some(expr) = get_typed_spar_network(props, "Output_Rate") + && let Some(bps) = extract_data_rate_bps(expr) + { + return Some(bps); + } + + let raw = get_raw_spar_network(props, "Output_Rate")?; + parse_data_rate_bps(raw) +} + +/// Convert a typed [`PropertyExpr`] for time into picoseconds. +fn extract_time_ps(expr: &PropertyExpr) -> Option { + match expr { + PropertyExpr::Integer(v, Some(unit)) => { + let factor = time_unit_factor(unit.as_str())?; + Some((*v as u64).checked_mul(factor)?) + } + PropertyExpr::Integer(v, None) => { + if *v >= 0 { + Some(*v as u64) + } else { + None + } + } + PropertyExpr::Real(s, Some(unit)) => { + let v: f64 = s.parse().ok()?; + let factor = time_unit_factor(unit.as_str())?; + Some((v * factor as f64) as u64) + } + PropertyExpr::UnitValue(inner, unit) => { + let factor = time_unit_factor(unit.as_str())?; + match inner.as_ref() { + PropertyExpr::Integer(v, _) => Some((*v as u64).checked_mul(factor)?), + PropertyExpr::Real(s, _) => { + let v: f64 = s.parse().ok()?; + Some((v * factor as f64) as u64) + } + _ => None, + } + } + _ => None, + } +} + +const TIME_UNIT_FACTORS_PS: &[(&str, u64)] = &[ + ("ps", 1), + ("ns", 1_000), + ("us", 1_000_000), + ("ms", 1_000_000_000), + ("sec", 1_000_000_000_000), + ("min", 60_000_000_000_000), + ("hr", 3_600_000_000_000_000), +]; + +fn time_unit_factor(unit: &str) -> Option { + TIME_UNIT_FACTORS_PS + .iter() + .find(|(name, _)| name.eq_ignore_ascii_case(unit)) + .map(|(_, f)| *f) +} + +const DATA_RATE_UNITS_BPS: &[(&str, u64)] = &[ + ("bitsps", 1), + ("Bytesps", 8), + ("KBytesps", 8 * 1024), + ("MBytesps", 8 * 1024 * 1024), + ("GBytesps", 8 * 1024 * 1024 * 1024), +]; + +fn data_rate_unit_factor(unit: &str) -> Option { + DATA_RATE_UNITS_BPS + .iter() + .find(|(name, _)| name.eq_ignore_ascii_case(unit)) + .map(|(_, f)| *f) +} + +fn extract_data_rate_bps(expr: &PropertyExpr) -> Option { + match expr { + PropertyExpr::Integer(v, Some(unit)) if *v >= 0 => { + let factor = data_rate_unit_factor(unit.as_str())?; + (*v as u64).checked_mul(factor) + } + PropertyExpr::Integer(v, None) if *v >= 0 => Some(*v as u64), + PropertyExpr::Real(s, Some(unit)) => { + let v: f64 = s.parse().ok()?; + if v < 0.0 { + return None; + } + let factor = data_rate_unit_factor(unit.as_str())?; + Some((v * factor as f64) as u64) + } + PropertyExpr::UnitValue(inner, unit) => { + let factor = data_rate_unit_factor(unit.as_str())?; + match inner.as_ref() { + PropertyExpr::Integer(v, _) if *v >= 0 => (*v as u64).checked_mul(factor), + PropertyExpr::Real(s, _) => { + let v: f64 = s.parse().ok()?; + if v < 0.0 { + return None; + } + Some((v * factor as f64) as u64) + } + _ => None, + } + } + _ => None, + } +} + +fn parse_data_rate_bps(s: &str) -> Option { + let s = s.trim(); + for &(unit, factor) in DATA_RATE_UNITS_BPS { + if let Some(num_str) = s.strip_suffix(unit).map(|s| s.trim()) { + if let Ok(v) = num_str.parse::() { + return v.checked_mul(factor); + } + if let Ok(v) = num_str.parse::() { + if v < 0.0 { + return None; + } + return Some((v * factor as f64) as u64); + } + } + } + s.parse::().ok() +} + +// ── Graph extraction ───────────────────────────────────────────────── + +/// Extract a [`NetworkGraph`] from an AADL [`SystemInstance`]. +/// +/// Algorithm: +/// 1. Walk all components. Buses (and virtual buses) carrying a +/// recognised `Spar_Network::Switch_Type` are classified as +/// [`NodeKind::Switch`]. Buses without `Switch_Type` are skipped — +/// they are classical (unswitched) AADL buses that other passes +/// such as `bus_bandwidth.rs` already handle. +/// 2. For each switch, walk the connections owned by its parent +/// component. A connection that touches the switch on one side and +/// a `device` or `processor` subcomponent on the other side +/// contributes a [`NetworkLink`] and registers the device/processor +/// as a [`NodeKind::EndStation`]. +/// 3. Each link copies the switch's `Output_Rate`, `Forwarding_Latency` +/// and `Queue_Depth` annotations. Missing annotations propagate as +/// `None` — diagnostic emission is the WCTT pass's job, not ours. +pub fn extract_network_graph(instance: &SystemInstance) -> NetworkGraph { + let mut graph = NetworkGraph::default(); + + // Pass 1: identify switches (buses carrying Switch_Type). + let mut switches: Vec<(ComponentInstanceIdx, SwitchType)> = Vec::new(); + for (idx, comp) in instance.all_components() { + if !is_bus_category(comp.category) { + continue; + } + let props = instance.properties_for(idx); + if let Some(switch_type) = read_switch_type(props) { + switches.push((idx, switch_type)); + graph.nodes.push(NetworkNode { + idx, + kind: NodeKind::Switch { switch_type }, + name: comp.name.as_str().to_string(), + }); + } + } + + // Pass 2: for each switch, gather links + end stations from + // connections in the parent component. We register each end station + // at most once even if it has multiple connections to the same + // switch. + let mut end_stations_seen: Vec = Vec::new(); + for (bus_idx, _switch_type) in &switches { + let bus_idx = *bus_idx; + let bus_props = instance.properties_for(bus_idx); + let bandwidth_bps = read_output_rate_bps(bus_props); + let forwarding_latency_ps = read_forwarding_latency_ps(bus_props); + let queue_depth = read_queue_depth(bus_props); + + // The parent of a bus subcomponent is the system that owns it; + // that system's connections are where we look for links to the + // bus. + let bus_comp = instance.component(bus_idx); + let parent_idx = match bus_comp.parent { + Some(p) => p, + None => continue, + }; + let parent_comp = instance.component(parent_idx); + let bus_name = bus_comp.name.as_str(); + + for &conn_idx in &parent_comp.connections { + let conn = &instance.connections[conn_idx]; + + let src_idx = conn + .src + .as_ref() + .and_then(|end| resolve_subcomponent(instance, parent_idx, &end.subcomponent)); + let dst_idx = conn + .dst + .as_ref() + .and_then(|end| resolve_subcomponent(instance, parent_idx, &end.subcomponent)); + + // Determine which endpoint touches the bus and which + // touches an end station. + let (other_idx, src_is_bus) = match (src_idx, dst_idx) { + (Some(s), Some(d)) if s == bus_idx => (d, true), + (Some(s), Some(d)) if d == bus_idx => (s, false), + _ => { + // Fall back to a name-based check for connections + // whose endpoint omits the subcomponent (i.e., + // references the owner's own feature). This is + // rare in switched topologies but cheap to handle. + if let Some(other) = name_other_endpoint(instance, parent_idx, conn, bus_name) { + // We don't know which side was the bus; + // assume src is the bus to keep direction + // stable. A later commit (the WCTT pass) can + // refine this when the connection is + // bidirectional. + (other, true) + } else { + continue; + } + } + }; + + if !is_end_station_category(instance.component(other_idx).category) { + continue; + } + + let (from, to) = if src_is_bus { + (bus_idx, other_idx) + } else { + (other_idx, bus_idx) + }; + + graph.links.push(NetworkLink { + from, + to, + bus_idx, + bandwidth_bps, + forwarding_latency_ps, + queue_depth, + }); + + if !end_stations_seen.contains(&other_idx) { + end_stations_seen.push(other_idx); + let other = instance.component(other_idx); + graph.nodes.push(NetworkNode { + idx: other_idx, + kind: NodeKind::EndStation, + name: other.name.as_str().to_string(), + }); + } + } + } + + graph +} + +fn is_bus_category(cat: ComponentCategory) -> bool { + matches!(cat, ComponentCategory::Bus | ComponentCategory::VirtualBus) +} + +fn is_end_station_category(cat: ComponentCategory) -> bool { + matches!( + cat, + ComponentCategory::Device | ComponentCategory::Processor + ) +} + +/// Resolve a connection endpoint subcomponent name to the corresponding +/// [`ComponentInstanceIdx`]. `None` subcomponent means the endpoint is +/// on the owner itself. +fn resolve_subcomponent( + instance: &SystemInstance, + owner: ComponentInstanceIdx, + subcomponent: &Option, +) -> Option { + match subcomponent { + Some(sub_name) => { + let owner_comp = instance.component(owner); + owner_comp + .children + .iter() + .find(|&&child_idx| { + instance.component(child_idx).name.as_str() == sub_name.as_str() + }) + .copied() + } + None => Some(owner), + } +} + +/// Fallback for connections that reference a feature on the owner +/// itself rather than a named subcomponent. Returns the *other* endpoint +/// of the connection if the bus name appears in either endpoint's +/// feature path. +fn name_other_endpoint( + instance: &SystemInstance, + owner: ComponentInstanceIdx, + conn: &spar_hir_def::instance::ConnectionInstance, + bus_name: &str, +) -> Option { + let src_sub = conn.src.as_ref().and_then(|e| e.subcomponent.as_ref()); + let dst_sub = conn.dst.as_ref().and_then(|e| e.subcomponent.as_ref()); + + let bus_lower = bus_name.to_ascii_lowercase(); + let src_is_bus = src_sub + .map(|n| n.as_str().eq_ignore_ascii_case(&bus_lower)) + .unwrap_or(false); + let dst_is_bus = dst_sub + .map(|n| n.as_str().eq_ignore_ascii_case(&bus_lower)) + .unwrap_or(false); + + let other_sub = if src_is_bus { + dst_sub + } else if dst_is_bus { + src_sub + } else { + return None; + }; + + let other_sub = other_sub?; + let owner_comp = instance.component(owner); + owner_comp + .children + .iter() + .find(|&&child_idx| instance.component(child_idx).name.as_str() == other_sub.as_str()) + .copied() +} + +#[cfg(test)] +mod tests { + use super::*; + use spar_hir_def::name::PropertyRef; + use spar_hir_def::properties::PropertyValue; + + fn make_props(set: &str, name: &str, value: &str, expr: Option) -> PropertyMap { + let mut props = PropertyMap::new(); + props.add(PropertyValue { + name: PropertyRef { + property_set: if set.is_empty() { + None + } else { + Some(Name::new(set)) + }, + property_name: Name::new(name), + }, + value: value.to_string(), + typed_expr: expr, + is_append: false, + }); + props + } + + #[test] + fn read_switch_type_typed_enum() { + let props = make_props( + SPAR_NETWORK, + "Switch_Type", + "FIFO", + Some(PropertyExpr::Enum(Name::new("FIFO"))), + ); + assert_eq!(read_switch_type(&props), Some(SwitchType::Fifo)); + } + + #[test] + fn read_switch_type_string_fallback() { + let props = make_props(SPAR_NETWORK, "Switch_Type", "Priority", None); + assert_eq!(read_switch_type(&props), Some(SwitchType::Priority)); + } + + #[test] + fn read_switch_type_missing_returns_none() { + let props = PropertyMap::new(); + assert_eq!(read_switch_type(&props), None); + } + + #[test] + fn read_queue_depth_typed_integer() { + let props = make_props( + SPAR_NETWORK, + "Queue_Depth", + "16", + Some(PropertyExpr::Integer(16, None)), + ); + assert_eq!(read_queue_depth(&props), Some(16)); + } + + #[test] + fn read_forwarding_latency_typed_range() { + let expr = PropertyExpr::Range { + min: Box::new(PropertyExpr::Integer(5, Some(Name::new("us")))), + max: Box::new(PropertyExpr::Integer(10, Some(Name::new("us")))), + delta: None, + }; + let props = make_props( + SPAR_NETWORK, + "Forwarding_Latency", + "5 us .. 10 us", + Some(expr), + ); + assert_eq!( + read_forwarding_latency_ps(&props), + Some((5_000_000, 10_000_000)) + ); + } + + #[test] + fn read_forwarding_latency_string_range() { + let props = make_props(SPAR_NETWORK, "Forwarding_Latency", "5 us .. 10 us", None); + assert_eq!( + read_forwarding_latency_ps(&props), + Some((5_000_000, 10_000_000)) + ); + } + + #[test] + fn read_output_rate_kbytesps() { + let props = make_props( + SPAR_NETWORK, + "Output_Rate", + "1000 KBytesps", + Some(PropertyExpr::Integer(1000, Some(Name::new("KBytesps")))), + ); + assert_eq!(read_output_rate_bps(&props), Some(1000 * 8 * 1024)); + } + + #[test] + fn parse_data_rate_bps_known_unit() { + assert_eq!( + parse_data_rate_bps("100 MBytesps"), + Some(100 * 8 * 1024 * 1024) + ); + assert_eq!(parse_data_rate_bps("1000"), Some(1000)); + } +} diff --git a/crates/spar-network/src/lib.rs b/crates/spar-network/src/lib.rs index 51b1c87..559235f 100644 --- a/crates/spar-network/src/lib.rs +++ b/crates/spar-network/src/lib.rs @@ -12,42 +12,35 @@ //! //! # Phasing //! -//! - **Phase 1 (this milestone, v0.8.0):** types only. The crate is a -//! skeleton placeholder. The Spar_Network property set surface -//! landed in `spar-hir-def::standard_properties` alongside this -//! crate. Subsequent commits in Track D add the algorithm pieces: -//! network-graph extraction (commit 2), Network Calculus primitives -//! (commit 3), the `wctt.rs` analysis pass (commit 4), and Lean -//! theorems (commit 5). -//! - **Phase 2 (v0.8.x or v0.9.0):** Network Calculus primitives — -//! arrival/service curves, min-plus convolution and deconvolution, -//! horizontal/vertical distance bounds. Exposed under -//! [`types`] and (later) `curve` modules. -//! - **Phase 3:** TSN-shaped service curves (TAS/Qbv, Qbu preemption, -//! Qcr ATS). These build on Phase 2's primitives. +//! - **Phase 1 (this milestone, v0.8.0):** +//! - **Commit 1 (#155):** `Spar_Network` property set surface in +//! `spar-hir-def::standard_properties`. +//! - **Commit 2 (this commit):** [`types`] — `NetworkNode`, +//! `NetworkLink`, `SwitchType`, `NetworkGraph`. [`extract`] — +//! extractor that walks a `SystemInstance` and emits a +//! `NetworkGraph` for downstream WCTT analysis. +//! - **Commit 3:** Network Calculus primitives (`ArrivalCurve`, +//! `ServiceCurve`, min-plus operators). +//! - **Commit 4:** `wctt.rs` analysis pass in `spar-analysis`. +//! - **Commit 5:** Lean theorems in `proofs/Proofs/Network/`. +//! - **Commit 6:** `latency.rs` integration + COMPLIANCE.md update. +//! - **Phase 2 (v0.8.x or v0.9.0):** TSN-shaped service curves +//! (TAS/Qbv, Qbu preemption, Qcr ATS) under a separate `Spar_TSN` +//! property set. //! -//! # What is intentionally NOT in this crate yet +//! # Crate boundary //! -//! - No `wctt.rs` — that lives in `spar-analysis` and lands later in -//! Track D. -//! - No Network Calculus algebra — Phase 2 will introduce -//! `ArrivalCurve`, `ServiceCurve`, and the min-plus operators. -//! - No TSN-specific service-curve generators — Phase 3. -//! - No AADL-specific knowledge: this crate stays free of -//! `spar-hir-def`/`spar-hir`/diagnostic dependencies. Adapters -//! between `SystemInstance` and the network graph live in -//! `spar-analysis`. -//! -//! See the design doc for the full scope and the rationale behind the -//! crate split. +//! Commit 2 introduces a dependency on `spar-hir-def` so the extractor +//! can read from `SystemInstance`. Future Network Calculus primitives +//! (commit 3) and the `wctt.rs` analysis pass (commit 4) keep this +//! direction: lower-level math types are AADL-aware only via the typed +//! `NetworkGraph` produced here. `spar-analysis` will pull from +//! `spar-network`, never the reverse. #![forbid(unsafe_code)] -/// Placeholder module for network-domain types. -/// -/// Phase 1 leaves this empty. Phase 2 will introduce -/// `ArrivalCurve`, `ServiceCurve`, server-graph node/edge types, and -/// the WCTT result record. The module is exposed today only to fix -/// the public path so that downstream crates can already write -/// `use spar_network::types::*;` without a future breaking change. -pub mod types {} +pub mod extract; +pub mod types; + +pub use extract::extract_network_graph; +pub use types::{NetworkGraph, NetworkLink, NetworkNode, NodeKind, SwitchType}; diff --git a/crates/spar-network/src/types.rs b/crates/spar-network/src/types.rs new file mode 100644 index 0000000..566b0a2 --- /dev/null +++ b/crates/spar-network/src/types.rs @@ -0,0 +1,211 @@ +//! Network graph types — the typed view of a network topology +//! extracted from an AADL ItemTree, ready for WCTT analysis. +//! +//! These types are the bridge between the AADL `SystemInstance` (in +//! `spar-hir-def`) and the Network Calculus analyses that follow in +//! later Track D commits. They are intentionally lightweight: a node +//! identifies a forwarding device or end station, a link captures the +//! per-hop properties consumed by the WCTT pass, and the [`NetworkGraph`] +//! collects both. No Network Calculus primitives live here — those land +//! in commit 3. + +use spar_hir_def::instance::ComponentInstanceIdx; + +/// One node in the network graph: either a switch (forwarding device) +/// or an end station (origin/destination of frames). +#[derive(Debug, Clone, PartialEq, Eq)] +pub struct NetworkNode { + /// Index of the underlying AADL `ComponentInstance`. + pub idx: ComponentInstanceIdx, + /// What role this node plays in the network. + pub kind: NodeKind, + /// Display name copied from the underlying `ComponentInstance` for + /// diagnostics. + pub name: String, +} + +/// Role of a [`NetworkNode`] in the network topology. +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub enum NodeKind { + /// A forwarding bus that carries `Spar_Network::Switch_Type`. + Switch { switch_type: SwitchType }, + /// A device or processor connected to one or more switches. + EndStation, +} + +/// Forwarding discipline of a switch, sourced from +/// `Spar_Network::Switch_Type`. +/// +/// Phase 1 (v0.8.0) covers `Fifo` and `Priority`. `Tsn` is accepted and +/// classified, but Phase 1 analyses treat it as opaque — full +/// TSN-shaped service curves land in Phase 2 alongside the `Spar_TSN` +/// property set. +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub enum SwitchType { + Fifo, + Priority, + /// Reserved for Phase 2 (TSN-shaped service curves). Phase 1 + /// analysis treats TSN-typed switches as opaque. + Tsn, +} + +impl SwitchType { + /// Parse the AADL enumeration literal for `Switch_Type`. + /// + /// Comparison is case-insensitive, matching AADL spec semantics. + /// Returns `None` for unrecognised values. + pub fn from_aadl_enum(s: &str) -> Option { + let lower = s.trim().to_ascii_lowercase(); + match lower.as_str() { + "fifo" => Some(Self::Fifo), + "priority" => Some(Self::Priority), + "tsn" => Some(Self::Tsn), + _ => None, + } + } +} + +/// One link (edge) in the network graph: a connection between two +/// [`NetworkNode`]s that traverses a specific switch (bus). +/// +/// All numeric fields are optional because the underlying AADL model +/// may omit `Spar_Network::*` annotations; the WCTT pass that consumes +/// the graph is responsible for diagnosing missing values. +#[derive(Debug, Clone, PartialEq, Eq)] +pub struct NetworkLink { + /// Source node (typically an end station or another switch). + pub from: ComponentInstanceIdx, + /// Destination node. + pub to: ComponentInstanceIdx, + /// The switch (bus) that carries this link. + pub bus_idx: ComponentInstanceIdx, + /// Egress bandwidth in bits per second, from + /// `Spar_Network::Output_Rate` on the bus. + pub bandwidth_bps: Option, + /// Per-hop store-and-forward latency in picoseconds as + /// `(BCET, WCET)`, from `Spar_Network::Forwarding_Latency`. + pub forwarding_latency_ps: Option<(u64, u64)>, + /// Per-port queue capacity in frames, from + /// `Spar_Network::Queue_Depth`. + pub queue_depth: Option, +} + +/// The full network graph extracted from a [`SystemInstance`]. +/// +/// [`SystemInstance`]: spar_hir_def::instance::SystemInstance +#[derive(Debug, Clone, Default, PartialEq, Eq)] +pub struct NetworkGraph { + pub nodes: Vec, + pub links: Vec, +} + +impl NetworkGraph { + /// All nodes in the graph (both switches and end stations). + pub fn nodes(&self) -> &[NetworkNode] { + &self.nodes + } + + /// All links in the graph. + pub fn links(&self) -> &[NetworkLink] { + &self.links + } + + /// Iterate over only the switch nodes. + pub fn switches(&self) -> impl Iterator { + self.nodes + .iter() + .filter(|n| matches!(n.kind, NodeKind::Switch { .. })) + } + + /// Iterate over only the end-station nodes. + pub fn end_stations(&self) -> impl Iterator { + self.nodes + .iter() + .filter(|n| matches!(n.kind, NodeKind::EndStation)) + } + + /// Look up a node by its underlying [`ComponentInstanceIdx`]. + pub fn node(&self, idx: ComponentInstanceIdx) -> Option<&NetworkNode> { + self.nodes.iter().find(|n| n.idx == idx) + } + + /// Returns the set of nodes reachable from `start` via `NetworkLink`s. + /// + /// Links are treated as undirected for reachability — a network + /// link between two stations on the same switch makes them mutually + /// reachable. The starting node itself is included in the result. + /// Returns an empty vec if `start` is not a node in the graph. + pub fn reachable_from(&self, start: ComponentInstanceIdx) -> Vec { + if self.node(start).is_none() { + return Vec::new(); + } + + let mut visited: Vec = Vec::new(); + let mut stack: Vec = vec![start]; + + while let Some(current) = stack.pop() { + if visited.contains(¤t) { + continue; + } + visited.push(current); + + for link in &self.links { + let next = if link.from == current { + Some(link.to) + } else if link.to == current { + Some(link.from) + } else { + None + }; + if let Some(next) = next + && !visited.contains(&next) + { + stack.push(next); + } + } + } + + visited + } +} + +#[cfg(test)] +mod tests { + use super::*; + + #[test] + fn switch_type_from_aadl_enum_recognises_canonical_values() { + assert_eq!(SwitchType::from_aadl_enum("FIFO"), Some(SwitchType::Fifo)); + assert_eq!( + SwitchType::from_aadl_enum("Priority"), + Some(SwitchType::Priority) + ); + assert_eq!(SwitchType::from_aadl_enum("TSN"), Some(SwitchType::Tsn)); + } + + #[test] + fn switch_type_from_aadl_enum_is_case_insensitive() { + assert_eq!(SwitchType::from_aadl_enum("fifo"), Some(SwitchType::Fifo)); + assert_eq!( + SwitchType::from_aadl_enum("priority"), + Some(SwitchType::Priority) + ); + assert_eq!(SwitchType::from_aadl_enum("tsn"), Some(SwitchType::Tsn)); + assert_eq!(SwitchType::from_aadl_enum("TsN"), Some(SwitchType::Tsn)); + } + + #[test] + fn switch_type_from_aadl_enum_rejects_unknown() { + assert_eq!(SwitchType::from_aadl_enum("Random"), None); + assert_eq!(SwitchType::from_aadl_enum(""), None); + } + + #[test] + fn empty_graph_has_no_nodes_or_links() { + let g = NetworkGraph::default(); + assert!(g.nodes().is_empty()); + assert!(g.links().is_empty()); + assert_eq!(g.switches().count(), 0); + assert_eq!(g.end_stations().count(), 0); + } +} diff --git a/crates/spar-network/tests/extract_tests.rs b/crates/spar-network/tests/extract_tests.rs new file mode 100644 index 0000000..5f2f41e --- /dev/null +++ b/crates/spar-network/tests/extract_tests.rs @@ -0,0 +1,314 @@ +//! Integration tests for `extract_network_graph`. +//! +//! Each test pipes a small inline AADL string through the spar-hir-def +//! pipeline (`file_item_tree` → `GlobalScope` → `SystemInstance::instantiate`) +//! and then asks `extract_network_graph` for the typed +//! [`spar_network::NetworkGraph`]. The fixtures are deliberately small +//! so the tests stay focused on the extractor's classification and link +//! emission logic rather than full AADL semantics. + +use spar_hir_def::instance::SystemInstance; +use spar_hir_def::{HirDefDatabase, Name, file_item_tree, resolver::GlobalScope}; +use spar_network::extract::extract_network_graph; +use spar_network::types::{NodeKind, SwitchType}; + +/// Parse an AADL source string and instantiate the named root system. +fn instantiate(aadl_src: &str, pkg: &str, sys: &str, sys_impl: &str) -> SystemInstance { + let db = HirDefDatabase::default(); + let file = spar_base_db::SourceFile::new(&db, "fixture.aadl".to_string(), aadl_src.to_string()); + let tree = file_item_tree(&db, file); + let scope = GlobalScope::from_trees(vec![tree]); + let inst = SystemInstance::instantiate( + &scope, + &Name::new(pkg), + &Name::new(sys), + &Name::new(sys_impl), + ); + assert!( + inst.component_count() > 0, + "instantiation failed; diagnostics: {:?}", + inst.diagnostics + ); + inst +} + +/// Common AADL source: one FIFO switch carrying two end stations +/// connected by a single bus-access connection on each side. +const SIMPLE_FIFO_TOPOLOGY: &str = r#" +package Net +public + + bus eth_switch + properties + Spar_Network::Switch_Type => FIFO; + Spar_Network::Queue_Depth => 32; + Spar_Network::Forwarding_Latency => 5 us .. 10 us; + Spar_Network::Output_Rate => 100 MBytesps; + end eth_switch; + + bus implementation eth_switch.impl + end eth_switch.impl; + + device sensor + features + net : requires bus access; + end sensor; + + device implementation sensor.impl + end sensor.impl; + + device actuator + features + net : requires bus access; + end actuator; + + device implementation actuator.impl + end actuator.impl; + + system Sys + end Sys; + + system implementation Sys.impl + subcomponents + sw : bus eth_switch.impl; + s : device sensor.impl; + a : device actuator.impl; + connections + c1 : bus access sw -> s.net; + c2 : bus access sw -> a.net; + end Sys.impl; + +end Net; +"#; + +#[test] +fn simple_switched_topology() { + let inst = instantiate(SIMPLE_FIFO_TOPOLOGY, "Net", "Sys", "impl"); + let graph = extract_network_graph(&inst); + + // 1 switch + 2 end stations. + assert_eq!( + graph.switches().count(), + 1, + "expected exactly one switch, got {}", + graph.switches().count() + ); + assert_eq!( + graph.end_stations().count(), + 2, + "expected exactly two end stations, got {}", + graph.end_stations().count() + ); + + // 2 links (one per bus-access connection). + assert_eq!(graph.links().len(), 2, "expected two links"); + + // The single switch should be classified as FIFO. + let sw = graph.switches().next().unwrap(); + assert_eq!( + sw.kind, + NodeKind::Switch { + switch_type: SwitchType::Fifo + } + ); + assert_eq!(sw.name, "sw"); +} + +#[test] +fn priority_switch_classified_correctly() { + let src = r#" +package Net +public + + bus prio_switch + properties + Spar_Network::Switch_Type => Priority; + end prio_switch; + + bus implementation prio_switch.impl + end prio_switch.impl; + + device d + features + net : requires bus access; + end d; + + device implementation d.impl + end d.impl; + + system Sys + end Sys; + + system implementation Sys.impl + subcomponents + sw : bus prio_switch.impl; + x : device d.impl; + connections + c1 : bus access sw -> x.net; + end Sys.impl; + +end Net; +"#; + let inst = instantiate(src, "Net", "Sys", "impl"); + let graph = extract_network_graph(&inst); + + let sw = graph + .switches() + .next() + .expect("priority switch should be present"); + assert_eq!( + sw.kind, + NodeKind::Switch { + switch_type: SwitchType::Priority + } + ); +} + +#[test] +fn tsn_switch_remains_opaque() { + let src = r#" +package Net +public + + bus tsn_switch + properties + Spar_Network::Switch_Type => TSN; + Spar_Network::Queue_Depth => 64; + Spar_Network::Forwarding_Latency => 1 us .. 2 us; + Spar_Network::Output_Rate => 1000 MBytesps; + end tsn_switch; + + bus implementation tsn_switch.impl + end tsn_switch.impl; + + device sensor + features + net : requires bus access; + end sensor; + + device implementation sensor.impl + end sensor.impl; + + system Sys + end Sys; + + system implementation Sys.impl + subcomponents + sw : bus tsn_switch.impl; + s : device sensor.impl; + connections + c1 : bus access sw -> s.net; + end Sys.impl; + +end Net; +"#; + let inst = instantiate(src, "Net", "Sys", "impl"); + let graph = extract_network_graph(&inst); + + let sw = graph + .switches() + .next() + .expect("TSN switch should be classified"); + assert_eq!( + sw.kind, + NodeKind::Switch { + switch_type: SwitchType::Tsn + }, + "TSN must be classified even though Phase 1 leaves analysis opaque" + ); + + // The link to the end station still populates bandwidth/latency/queue + // even though Phase 1 will not feed them through Network Calculus + // service curves yet. + let link = graph + .links() + .iter() + .next() + .expect("expected a link to the sensor"); + assert!(link.bandwidth_bps.is_some(), "Output_Rate should populate"); + assert!( + link.forwarding_latency_ps.is_some(), + "Forwarding_Latency should populate" + ); + assert_eq!(link.queue_depth, Some(64)); +} + +#[test] +fn unannotated_bus_skipped() { + // Same shape as the simple FIFO topology, except the bus carries no + // Spar_Network properties. The extractor must treat it as a + // classical (non-switched) AADL bus and skip it. + let src = r#" +package Net +public + + bus plain_bus + end plain_bus; + + bus implementation plain_bus.impl + end plain_bus.impl; + + device d + features + net : requires bus access; + end d; + + device implementation d.impl + end d.impl; + + system Sys + end Sys; + + system implementation Sys.impl + subcomponents + b : bus plain_bus.impl; + x : device d.impl; + connections + c1 : bus access b -> x.net; + end Sys.impl; + +end Net; +"#; + let inst = instantiate(src, "Net", "Sys", "impl"); + let graph = extract_network_graph(&inst); + + assert_eq!( + graph.switches().count(), + 0, + "unannotated bus must not appear as a switch" + ); + assert_eq!( + graph.end_stations().count(), + 0, + "without a switch there is no end station to register" + ); + assert!(graph.links().is_empty(), "no links without a switch"); +} + +#[test] +fn forwarding_latency_range_propagates() { + let inst = instantiate(SIMPLE_FIFO_TOPOLOGY, "Net", "Sys", "impl"); + let graph = extract_network_graph(&inst); + + let link = graph.links().first().expect("expected at least one link"); + assert_eq!( + link.forwarding_latency_ps, + Some((5_000_000, 10_000_000)), + "Forwarding_Latency => 5 us .. 10 us should lower to (5_000_000, 10_000_000) ps" + ); +} + +#[test] +fn reachable_from_traverses_links() { + let inst = instantiate(SIMPLE_FIFO_TOPOLOGY, "Net", "Sys", "impl"); + let graph = extract_network_graph(&inst); + + // From any node we should reach the full graph (1 switch + 2 stations). + let any_node = graph.nodes().first().unwrap().idx; + let reachable = graph.reachable_from(any_node); + assert_eq!( + reachable.len(), + 3, + "expected to reach all 3 nodes from the single switch" + ); +}