Control algorithms are ubiquitous in networked systems—from congestion control and load balancing to scheduling and caching. Despite their performance-critical nature, these algorithms are designed using human intuition and heuristics, and they frequently exhibit poor or unpredictable performance. This thesis envisions a methodology for designing controllers with formally verified performance guarantees. We focus on congestion control algorithms (CCAs)–a domain that continues to experience repeated failures despite decades of research.

Two main reasons make congestion control hard. First, CCAs operate in diverse environments with noisy feedback (e.g., cellular links, policers, token-bucket filters, operating system jitter, etc.). Second, the problem itself is computationally hard because CCAs operate under uncertainty–they lack direct visibility into the state of the network or the flows they compete with. To address the first challenge, we adopt the approach proposed by recent work that models networks as non-deterministic, non-stochastic automata. These models can capture a wide range of real-world phenomena and enable computer verification of controller performance on such networks. We seek to design CCAs that pass such verification checks. However, this approach does not scale out of the box.

We find that the key to making it tractable is to formally reason about uncertainty in the state of the network and other flows. This thesis contributes two abstractions–beliefs and contracts–that enable such reasoning and reveal new structure in CCAs that simplifies their design and analysis. Beliefs formalize what a CCA can infer about latent network state from its observations. Contracts formalize how flows coordinate with each other to share the network. Since flows cannot directly communicate, they implicitly encode information in observable congestion signals (e.g., delay or loss). Contracts formalize these communications mechanisms. Building on these abstractions, we develop CCmatic, a tool that automatically synthesizes CCAs withverified performance guarantees. Our abstractions and tools allowed us to discover previously unknown tradeoffs and design new CCAs that are on the Pareto-frontier and provably guarantee performance even under challenging network conditions.

We believe that the methodology developed in this thesis generalizes beyond congestion control and we outline steps towards this vision.

197 pages

Thesis Committee:
Srinivasan Seshan (Chair)
Vyas Sekar
Justine Sherry
Philip Brighten Godfrey (University of Illinois Urbana-Champaign)
Venkat Arun (University of Texas at Austin)

Jignesh Patel, Interim Head, Computer Science Department
Martial Hebert, Dean, School of Computer Science

Creative Commons: CC-BY (Attribution)

Return to: SCS Technical Report Collection
School of Computer Science

This page maintained by reports@cs.cmu.edu