Canopy: Property-Driven Learning for Congestion Control

TL;DR

Canopy addresses the risk of suboptimal or unsafe behavior in learning-based congestion controllers by embedding Quantitative Certificates (QCs) into the training loop through abstract interpretation, enabling in-loop worst-case guarantees and runtime monitoring. The framework blends the base LCC (Orca) with a verifier-guided reward that balances average-case performance and worst-case property satisfaction, producing controllers with formal regional proofs of property adherence. At run time, QC_sat provides a monitorable measure and a fallback mechanism to TCP Cubic when guarantees are not met, improving safety without sacrificing efficiency. Across synthetic, real-world, and in-the-wild deployments, Canopy delivers up to 1.4x improvements in worst-case satisfaction and substantial delay reductions while maintaining comparable bandwidth utilization, demonstrating the practical viability of certifiable learning in networked systems.

Abstract

Learning-based congestion controllers offer better adaptability compared to traditional heuristics. However, the unreliability of learning techniques can cause learning-based controllers to behave poorly, creating a need for formal guarantees. While methods for formally verifying learned congestion controllers exist, these methods offer binary feedback that cannot optimize the controller toward better behavior. We improve this state-of-the-art via Canopy, a new property-driven framework that integrates learning with formal reasoning in the learning loop. Canopy uses novel quantitative certification with an abstract interpreter to guide the training process, rewarding models, and evaluating robust and safe model performance on worst-case inputs. Our evaluation demonstrates that unlike state-of-the-art learned controllers, Canopy-trained controllers provide both adaptability and worst-case reliability across a range of network conditions.

Figures (17)

• Figure 1: Orca under noises -- (a) Sending Rate of Orca and Canopy with and without noise. Canopy is much more robust. (b) invRTT observed by Orca (including the noise) and its cwnd, during the region within the dashed lines in (a). After the dashed vertical line, Orca under noise continues to use a small cwnd while Orca, with a similar input, uses a higher cwnd.
• Figure 2: Orca entering critically bad states. (a) Orca's sending rate drops and remains low for a prolonged period while Canopy maintains its sending rate. (b) Orca's states for the region within the dashed lines in (a). Despite high invRTT (i.e., low queueing delays), TCP increases the cwnd (>100) but Orca repeatedly reduces it (<50).
• Figure 3: Canopy Overview. Raw feedback is the training reward used by the base LCC, and verifier feedback is the additional signal provided in Canopy used to construct the Quantitative Certificate. $[a_i, b_i]$ denotes one component of the input region $[a,b]$.
• Figure 4: Abstract Interpretation lifts a concrete set of inputs to the abstract hyper-interval domain, and propagates the abstract state through the lifted$f^{\#}$ function.
• Figure 5: [Shallow Buffer & Deep Buffer Properties] Mean and std of QC$_\text{sat}$ on different categories of traces -- with trained buffer sizes ($0.5BDP$ for shallow buffer, $5BDP$ for deep buffer).