Skip to content

feat(network): PLP on converging sink-trees via topological relabel (REQ-NC-PLP-CONVERGE-001) #285

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
avrabe merged 1 commit into from
Jun 14, 2026
Merged

feat(network): PLP on converging sink-trees via topological relabel (REQ-NC-PLP-CONVERGE-001) #285

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
103 changes: 86 additions & 17 deletions artifacts/requirements.yaml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2688,13 +2688,19 @@ artifacts:
server — e.g. a converging tree handed in first-appearance order) is
likewise rejected (PlpError::NonTopologicalSinkTree) rather than
panicking inside the sink-tree projection; reordering such trees so
PLP can fire is REQ-NC-PLP-002. This ports
panco's PURE polynomial PLP LP (no TFA/SFA strengthening):
bounds are always ≤ TFA and strictly inside the soundness sandwich
EXACT ≤ plp ≤ TFA, matching panco's polynomial-PLP reference to
solver precision — exact on 2 of 3 validation fixtures, within
5.6% of EXACT on the 3-hop line (72.22 vs 68.4 µs, still ≪ the
134.7 µs TFA). PLP works beyond the tandem-only LUDB/PMOO: 72.22
PLP can fire is the follow-on REQ-NC-PLP-CONVERGE-001 (which
repurposes that same guard as a post-relabel invariant). This ports
panco's PURE polynomial PLP LP (no TFA/SFA strengthening): bounds are
SOUND (≥ EXACT) and, on the validation fixtures, also ≤ TFA. But pure
PLP and TFA are INCOMPARABLE over-approximations — neither dominates;
under extreme cross-burst pure PLP can exceed TFA (panco's own
reference does so on the converging-bridge net: PLP 1148 > TFA 1048 ≥
EXACT 1035 µs — the network_wide_tfa_index_aligns_on_converging_tree
counterexample). The authoritative per-flow bound is therefore
min(PLP, TFA) (tracked as REQ-NC-PLP-MIN-001). On the validation
fixtures PLP matches panco's polynomial-PLP reference to solver
precision — exact on 2 of 3, within 5.6% of EXACT on the 3-hop line
(72.22 vs 68.4 µs, still ≪ the 134.7 µs TFA). PLP works beyond the tandem-only LUDB/PMOO: 72.22
≪ 134.7 on a 3-server LINE is the dominance the existing tools
cannot show. NOTE: this is PORT-FIDELITY against panco, not
independent method-soundness (the LP is transcribed from panco and
Expand All @@ -2719,14 +2725,12 @@ artifacts:
spar-network shall extend PLP (REQ-NC-PLP-001) from feed-forward
sink-trees to GENERIC topology — including CYCLIC service
dependencies — via panco's forest decomposition (edges_forest) and
the LP fixpoint over the decomposed trees. Includes the smaller
precursor of topologically REORDERING a single-successor converging
sink-tree whose indices arrive non-topological (today rejected by
REQ-NC-PLP-001 as PlpError::NonTopologicalSinkTree) so PLP fires on
the common many-talkers→one-listener TSN shape — a relabelling, sound
because TFA/PLP are invariant under server renumbering, but gated on
the same converging-tree panco fixtures below before emitting numbers.
This carries the
the LP fixpoint over the decomposed trees. The smaller single-
successor precursor (topologically RELABELLING a converging sink-tree
whose indices arrive non-topological so PLP fires on the common
many-talkers→one-listener TSN shape) is split out as the now-shipped
REQ-NC-PLP-CONVERGE-001; this requirement is the GENERIC/CYCLIC core
that remains. This carries the
headline claim REQ-NC-PLP-001 cannot test: PLP CONVERGES where TFA
diverges at high utilization. That divergence is a cyclic-
dependency phenomenon (TFA's fixpoint terminates on any feed-
Expand All @@ -2739,6 +2743,43 @@ artifacts:
arXiv:2010.09263; Tabatabaee/Bouillard/Le Boudec arXiv:2208.11400]
status: proposed
tags: [network-calculus, plp, cyclic, substrate, tier1]
fields:
release: v0.20.0

- id: REQ-NC-PLP-CONVERGE-001
type: requirement
title: "PLP on converging sink-trees via topological relabel"
description: >
spar-network shall fire PLP (REQ-NC-PLP-001) on single-successor
CONVERGING sink-trees whose server indices arrive in NON-topological
order — the common many-talkers→one-listener TSN shape handed in
first-appearance order, which REQ-NC-PLP-001 shipped REJECTING
(PlpError::NonTopologicalSinkTree) rather than panicking inside the
sink-tree projection. plp_bound computes a topological relabelling of
servers and applies it as a pure permutation BEFORE projection, so the
sink lands at the highest index — the invariant the per-flow sub-network
solve assumes (sink == num_servers-1). This is SOUND with no change to
the bound because TFA/PLP are invariant under server renumbering, and a
graph already validated single-successor + acyclic is a rooted in-forest
that ALWAYS admits a topological order. The former NonTopologicalSinkTree
guard is not deleted but REPURPOSED as a post-relabel invariant check
(after relabel no edge may point to a lower-numbered server; a violation
means the topo sort is buggy → Err, never the .expect panic this guard
was added to prevent). GATE: per-flow bounds (a) match panco's pinned
converging-tree reference to solver precision, sound (≥ EXACT) and —
on these benign converging nets — below TFA (PLP ≤ TFA holds per-
fixture here; it is NOT universal, see REQ-NC-PLP-001's incomparability
note and counterexample), and (b) equal — exactly — the bounds of the SAME
physical network presented already-topologically (permutation
invariance, the primary property). Pinned converging fixtures from
panco: converge_2to1 (PLP 48.89 ≪ TFA 60.39 µs), converge_2to1_tail2
(60.0 ≪ 106.44, the 1.77× wedge), converge_3to1 (70.0 ≪ 74.59). This is
the single-successor precursor split out of REQ-NC-PLP-002; the
GENERIC/CYCLIC core and the "PLP converges where TFA diverges" headline
remain in REQ-NC-PLP-002 (gated on not-yet-generated cyclic fixtures).
[SOLID — Bouillard arXiv:2010.09263]
status: implemented
tags: [network-calculus, plp, converging, substrate, tier1]
fields:
release: v0.19.0

Expand All @@ -2764,6 +2805,31 @@ artifacts:
fields:
release: v0.19.0

- id: REQ-NC-PLP-MIN-001
type: requirement
title: "Authoritative per-flow NC bound = min(PLP, TFA)"
description: >
The network-wide NC bridge (REQ-NC-BRIDGE-001) shall report, per flow,
the TIGHTER of its PLP and TFA bounds as the authoritative end-to-end
delay. MOTIVATION: pure polynomial PLP (REQ-NC-PLP-001) and TFA are
INCOMPARABLE over-approximations — both sound (≥ exact), but neither
dominates. PLP is usually tighter, yet under extreme cross-burst it can
exceed TFA (the live counterexample
network_wide_tfa_index_aligns_on_converging_tree: panco's own PLP 1148
> TFA 1048 ≥ EXACT 1035 µs, reproduced to the decimal by spar). Taking
min(PLP, TFA) makes the reported bound never worse than TFA while
keeping the PLP win wherever it helps — so "PLP > TFA sometimes" is a
non-issue, not a regression. SCOPE: pure presentation/selection over the
two already-computed bounds; does NOT change either engine. This is
DISTINCT from REQ-NC-PLP-003 (which tightens the LP itself via TFA-
strengthening so PLP ≤ TFA holds by construction) — MIN-001 is the
cheap, always-correct selection that holds even for the pure LP.
GATE: on the converging-bridge fixture the bridge's authoritative bound
equals TFA (1048 µs) for the cross-burst flow, not the looser PLP.
[SOLID — Bouillard arXiv:2010.09263]
status: proposed
tags: [network-calculus, plp, bridge, substrate, tier1]

- id: REQ-NC-BRIDGE-001
type: requirement
title: "AADL instance -> network-wide NC solver inputs (TfaFlow/PlpFlow)"
Expand Down Expand Up @@ -2796,8 +2862,11 @@ artifacts:
tagged tandem): TFA/PLP take ALL flows + ALL services at once. Use
pmoo_or_sfa as the pattern for HOW to bridge (Stream -> solver input,
fall back on failure), not WHAT to compute. Output: the network-wide
TFA and PLP end-to-end delay bound, where PLP <= TFA is the
demonstrable competitor wedge on a real model.
TFA and PLP end-to-end delay bound. PLP is usually the tighter bound
(the demonstrable competitor wedge on a real model), but PLP and TFA
are incomparable in general (REQ-NC-PLP-001) — the authoritative
per-flow bound is min(PLP, TFA) (REQ-NC-PLP-MIN-001); the bridge emits
both.

FABRIC: TSN-first and TSN-only. NC (FIFO/CBS) is the CORRECT model
for TSN/AVB and extract_network_graph already yields the NetworkGraph.
Expand Down
82 changes: 68 additions & 14 deletions artifacts/verification.yaml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1810,8 +1810,10 @@ artifacts:
(optimistic) bound, which a self-consistent hand-golden cannot. panco
is not vendored; the reference numbers are pinned in-test with
provenance + regen recipe in tests/oracles/panco/README.md (Python is
not in spar's CI path). Establishes the soundness floor that
REQ-NC-PLP-001 is gated against (sandwich EXACT <= plp <= TFA).
not in spar's CI path). Establishes the EXACT soundness floor that
REQ-NC-PLP-001 is gated against (plp >= EXACT). PLP <= TFA holds on
these fixtures but is NOT a universal law (PLP and TFA are
incomparable — see TEST-NC-PLP's incomparability note).
fields:
method: automated-test
steps:
Expand All @@ -1837,22 +1839,26 @@ artifacts:
the SOUNDNESS floor (plp >= panco EXACT ELP bound), PORT-FIDELITY
(spar's HiGHS solve reproduces panco's lp_solve pure-PLP optimum to
<= 0.05% — solver precision: 39.0/34.0, 27.0, and the discriminating
72.22/61.11/57.98 µs), and the SANDWICH ceiling (plp <= spar's own
TFA bound). Pure PLP equals EXACT on the tandems and is strictly
inside the sandwich on the 3-hop line (72.22 vs 68.4 µs EXACT,
<< 134.7 µs TFA) — the dominance LUDB/PMOO cannot show on a line.
72.22/61.11/57.98 µs), and a PER-FIXTURE pin plp <= spar's own TFA
bound. That ≤ TFA pin is NOT a universal law: pure polynomial PLP and
TFA are INCOMPARABLE over-approximations (both sound, neither
dominates) — under extreme cross-burst PLP can exceed TFA (panco's own
PLP 1148 > TFA 1048 ≥ EXACT 1035 µs on the converging-bridge net; see
network_wide_tfa_index_aligns_on_converging_tree). The authoritative
bound is min(PLP, TFA) (REQ-NC-PLP-MIN-001). On these benign fixtures
pure PLP equals EXACT on the tandems and is strictly below TFA on the
3-hop line (72.22 vs 68.4 µs EXACT, << 134.7 µs TFA) — the dominance
LUDB/PMOO cannot show on a line.
Because the LP is transcribed from panco and the floor is also
panco's, this is port-fidelity (a regression pin), NOT independent
method-soundness; the latter is the deferred simulation floor
REQ-NC-SIM-FLOOR-001. Cyclic / branching topology is rejected
(NotFeedForward, REQ-NC-PLP-002); the tfa=True tightening to EXACT is
REQ-NC-PLP-003. Two guard tests pin the soundness boundary of the
sink-tree projection: non_topological_sink_tree_rejected asserts a
valid converging tree whose sink is NOT the highest-numbered server
returns PlpError::NonTopologicalSinkTree (no panic in solve), and
topological_sink_tree_accepted asserts the same shape relabelled with
the sink last solves cleanly — proving the guard rejects the labelling,
not the topology (reordering is REQ-NC-PLP-002).
REQ-NC-PLP-003. As of REQ-NC-PLP-CONVERGE-001 a non-topological
single-successor converging tree is no longer rejected but topologically
RELABELLED and solved (see TEST-NC-PLP-CONVERGE); the former
NonTopologicalSinkTree guard is retained as a post-relabel invariant
that still prevents the .expect panic if the topo sort is buggy.
fields:
method: automated-test
steps:
Expand All @@ -1866,6 +1872,45 @@ artifacts:
- type: satisfies
target: REQ-NC-VALIDATION-001

- id: TEST-NC-PLP-CONVERGE
type: feature
title: PLP on converging sink-trees via topological relabel
description: >
Exercises the topological-relabel path added to plp_bound for
single-successor CONVERGING sink-trees handed in non-topological order
(many-talkers→one-listener). Two layers of oracle. (1) PERMUTATION
INVARIANCE — the primary property, needing no external numbers: the
plp.rs unit test non_topological_relabel_is_permutation_invariant builds
a converging tree whose sink is NOT the highest-numbered server, asserts plp_bound
now returns Ok (no PlpError::NonTopologicalSinkTree, no panic in solve),
and asserts its per-flow bound equals — exactly — the bound of the SAME
physical network presented already-topologically (sink last). This
proves the relabel is a sound pure permutation. topological_sink_tree_
accepted is retained unchanged as the already-ordered baseline. (2)
SOUNDNESS FLOOR — the plp_converge_xval module in nc_validation.rs
(feature milp-solver) runs the three pinned converging panco fixtures in
non-topological first-appearance order and asserts per-flow PLP matches
panco's pure-PLP reference to solver precision, sound (≥ EXACT) and —
on these benign converging nets — below TFA (PLP ≤ TFA holds per-fixture
here; it is NOT universal, see TEST-NC-PLP's incomparability note):
converge_2to1 PLP 48.89 ≪ TFA 60.39, converge_2to1_
tail2 60.0 ≪ 106.44 (the 1.77× wedge), converge_3to1 70.0 ≪ 74.59 µs.
Values regenerated fresh from the pinned panco venv (lp_solve backend).
The relabel closes the sink==num_servers-1 assumption the sub-network
solve depends on (lines that .expect a successor for every non-sink
server), so the converging shape — the dominant TSN topology — now
yields the PLP≪TFA dominance LUDB/PMOO cannot show on a tree.
fields:
method: automated-test
steps:
- run: "cargo test -p spar-network --lib plp::"
- run: "cargo test -p spar-network --test nc_validation plp_xval::panco_converge"
status: passing
tags: [v0.19.0, network, network-calculus, plp, converging, validation, oracle]
links:
- type: satisfies
target: REQ-NC-PLP-CONVERGE-001

- id: TEST-NC-BRIDGE
type: feature
title: AADL instance → network-wide NC solver bridge
Expand Down Expand Up @@ -1898,7 +1943,16 @@ artifacts:
Non-FIFO hops, unstable servers, and PLP
NotFeedForward skip the arm transparently, leaving the per-stream SFA
bounds authoritative. The production caller is the CLI --pmoo path
(run_all_analyses_with_pmoo, package spar).
(run_all_analyses_with_pmoo, package spar). A fourth test,
network_wide_tfa_index_aligns_on_converging_tree, guards the global
index on a CONVERGING (many-talkers→one-sink) shape; as of
REQ-NC-PLP-CONVERGE-001 the PLP arm fires there (topological relabel)
rather than skipping. That fixture is a deliberately pathological
10000-µs-slow-switch net and doubles as the live counterexample to a
universal PLP ≤ TFA: pure PLP exceeds TFA there (panco PLP 1148 > TFA
1048 ≥ EXACT 1035 µs, reproduced to the decimal), so the test asserts
only index alignment (slow-stream PLP dominates fast), not a sandwich.
The authoritative bound min(PLP, TFA) is REQ-NC-PLP-MIN-001.
fields:
method: automated-test
steps:
Expand Down
Loading
Loading