Certified Closed-Loop Control for Packet Networks: A Compositional Certification Framework

Technische Samenvatting: Gecertificeerde Closed-Loop Controle voor Pakketnetwerken

1. Probleemstelling

Pakketnetwerken functioneren als gecontroleerde dynamische systemen die worden gekenmerkt door discontinuïteiten, vertraagde observaties en gedeeltelijke staat-informatie. Hoewel adaptieve of leergestuurde controllers (proposers) de prestaties kunnen verbeteren, missen zij inherente garanties; een onveilige voorstel kan leiden tot wachtrij-uithongering (queue starvation), extreme vertragingspieken (tail-delay spikes) of instabiliteit. Bestaande veiligheidsmechanismen analyseren vaak de bedoelde actie van een controller of vertrouwen op offline aannames die niet standhouden onder runtime-stress, vertraagde telemetrie of adversariële verkeersverschuivingen.

Het kernprobleem dat wordt aangepakt, is hoe men adaptief voorstellen kan combineren met strikte, online controleerbare garanties voor pakketwachtrijen op een manier die componeert over een netwerk. Specifiek streeft het artikel ernaar om te waarborgen dat de actie die daadwerkelijk wordt uitgevoerd aan de dataplane voldoet aan veiligheids- en stabiliteitsbeperkingen, ongeacht de kwaliteit of aard van de proposer (die heuristisch, geleerd of agentisch kan zijn).

2. Methodologie

Het artikel stelt een Certified Operator-architectuur voor die tussen elke proposer en de dataplane staat. Deze operator fungeert als een runtime-veiligheidsfilter die bij elke control-tick een gecompileerde configuratie-certificering afdwingt.

Kernmechanisme:

• Input: Bij elke tick $t$ geeft een proposer een kandidaat-actie $\tilde{u}(t)$ af op basis van vertraagde telemetrie.
• Certificering: De operator projecteert $\tilde{u}(t)$ op een gecertificeerde haalbare verzameling $U_{cert}(t)$ die is afgeleid van een verenigd certificaat.
• Output: De operator geeft een uitgevoerde actie $u(t)$, een geëxporteerde envelop $\bar{z}(t)$ voor downstream compositie, en een statusvlag ($\sigma(t)$) terug.
  • CERTIFIED: De actie voldoet aan alle beperkingen.
  • INFEASIBLE: Beperkingen kunnen niet worden nagekomen; de operator voert een "slack-minimaliserend fallback-beleid" uit (emergency policy) en rapporteert de omvang van de overtreding.
  • MISSING: Vereiste inputs (envelops of staat-grenzen) ontbreken.

Certificaatcomponenten:
Het framework verenigt drie typen beperkingen in één per-tick optimalisatieprobleem:

1. Type B (Barrier/Safety): Handhaaft backlog-limieten ($q_i(t) \le Q_{max}$) om overflow te voorkomen. Dit omvat lineaire beperkingen voor service-vloeren (voor beschermde klassen) en mitigatie-caps.
2. Type A (Drift/Stability): Handhaaft Foster–Lyapunov drift-condities. Als een wachtrij een hoge drempel overschrijdt ($q_i(t) \ge Q_{hi}$), moet de service-rate groter zijn dan de aankomst-envelop plus een marge ($\epsilon$), wat stabiliteit garandeert.
3. Type C (Composition): Exporteert een envelop $\bar{z}(t)$ die de bovengrens van de uitstroom vertegenwoordigt. Downstream modules gebruiken deze geëxporteerde grenzen als hun aankomst-aannames, wat modulaire redenering mogelijk maakt.

Omgaan met real-world beperkingen:

• Vertraagde Telemetrie & Actuatie: De operator construeert conservatieve backlog-grenzen met behulp van vertraagde tellers en verklaarde aankomst-envelops. Het houdt rekening met de "actuatie-vertraging" ($\tau_u$) door de beperkingen te projecteren naar de toekomstige tijd waarop de actie daadwerkelijk zal plaatsvinden.
• Service Tracking: In het besef dat echte schedulers (bijv. WFQ, DRR) de beoogde rates mogelijk niet perfect realiseren vanwege packetisatie of batching, introduceert het model een service-tracking factor $\kappa \in [\kappa_{min}, 1]$. Garanties zijn gekoppeld aan de gerealiseerde verwijdering, begrensd door deze factor.
• Semantiek van Onhaalbaarheid: In plaats van stilzwijgend te falen, lost de operator een relaxatie-projectie op die de slack minimaliseert wanneer beperkingen structureel onmogelijk zijn (bijv. onder zware overbelasting). Dit biedt een controleerbaar signaal van de overtreding.

3. Belangrijkste Bijdragen

1. Formeel Model: Een vertraagd closed-loop model voor pakketwachtrijen en een certified-operator interface die configuratie compileert naar per-tick beperkingen.
2. Verenigde Beperkingen: Een framework dat backlog-caps, service-vloeren/caps, expliciete drift-gebaseerde stabiliteit en compositionele contracten via geëxporteerde envelopes ondersteunt.
3. Theoretische Garanties:
   • Operator-niveau Veiligheid: Er is bewezen dat als de operator CERTIFIED rapporteert en de inputs geldig zijn, de backlog binnen veilige grenzen blijft.
   • Compositionele Veiligheid & Stabiliteit: Bewezen voor feed-forward DAG-netwerken met gebruik van enkel geëxporteerde envelopes.
   • Cyclische Sluiting: Een resultaat dat aantoont dat cyclische netwerken een unieke fixed-point envelope oplossing bereiken onder een "small-gain" conditie (spectrale radius van de routing/export gain matrix $< 1$).
4. Semantiek van Falen: Expliciete definities voor breuk (envelope schending), onhaalbaarheid (beperkingsschending) en ontbrekende informatie, waardoor het systeem gedefinieerd en controleerbaar blijft, zelfs onder stress.

4. Resultaten en Evaluatie

De evaluatie werd uitgevoerd in een byte-level closed-loop Python backend, waarbij de focus lag op de certificeringsgrens in plaats van op de lage-niveau Linux scheduler implementatie-details.

• Prestaties: De certificeringsstap (het oplossen van de projectie) is computationeel efficiënt en duurt ongeveer 37–52 µs voor 128 wachtrijen, wat milliseconde-schaal controle-intervallen mogelijk maakt.
• Robuustheid tegenover Proposers:
  • Voor welwillende proposers (backlog-proportioneel of random) werkt de operator neutraal en laat hij acties door met minimale correctie.
  • Voor adversariële proposers (ontworpen om uithongering te veroorzaken) vermindert de operator de p99/p99.9 vertragingsstaarten aanzienlijk en herstelt de throughput door barrier en drift restricties af te dwingen.
• Omgaan met Vertragingen: Onder vertraagde telemetrie en actuatie voorkomt de operator de "threshold excursions" (drempeloverschrijdingen) die optreden bij directe uitvoering of naïeve clipping, door de beperkingen over de worst-case delay window te compileren.
• Envelope Mismatch: Het systeem identificeert en rapporteert correct breuken wanneer verklaarde envelopes te optimistisch zijn (overtreden door werkelijk verkeer), waardoor wordt voorkomen dat downstream modules vertrouwen op ongeldige contracten.
• Overbelasting: Onder overbelasting gaat het systeem over naar de "emergency mode", waarbij het INFEASIBLE rapporteert en de slack kwantificeert, in plaats van stilzwijgend de veiligheidsbeperkingen te schenden.
• Priority Inversion: Het framework voorkomt succesvol priority inversion (waarbij bulkverkeer latency-gevoelig verkeer uithongert) door expliciete service-vloeren als first-class constraints af te dwingen, onafhankelijk van de logica van de proposer.

5. Betekenis en Omvang

Het artikel stelt dat pakketnetwerkcontrole gecertificeerd moet worden op het punt van uitvoering, en niet alleen tijdens de fase van het voorstel. De betekenis ligt in het ontkoppelen van de intentie van een adaptieve controller van de veiligheid van de uitgevoerde actie.

• Bescheiden Claims: De auteurs stellen expliciet dat dit werk geen mechanische verificatie claimt van de certificaat-compiler, de solver of de onderliggende dataplane backend (bijv. Linux kernel of NIC hardware). De garanties zijn voorwaardelijk op de geldigheid van de verklaarde envelopes, staat-grenzen en de service-tracking factor ($\kappa_{min}$).
• Positionering: Het framework is ontworpen om samen te werken met klassieke network calculus (gebruikmakend van token-bucket contracten als inputs), maar verschuift de handhaving naar runtime. Het behandelt de "envelope" niet alleen als een offline aanname voor statische grenzen, maar als een dynamische input voor een per-tick certificeringsinterface.
• Toekomstig Werk: Het artikel identificeert de noodzaak om de service-tracking factor te implementeren op echte hardware (Linux HTB, DRR, programmeerbare switches) en om de trusted computing base te versterken door middel van translation validation of machine-checked bewijzen.

Samenvattend biedt het artikel een rigoureus, compositioneel framework voor runtime assurance in pakketnetwerken, waarbij wordt gegarandeerd dat zelfs als een proposer gebrekkig is of het netwerk onder stress staat, de uitgevoerde acties binnen controleerbare veiligheids- en stabiliteitsgrenzen blijven.