Doctoral Thesis Oral Defense - Anup Agarwal
— 3:00pm
Location:
In Person and Virtual - ET
-
Reddy Conference Room, Gates Hillman 4405 and Zoom
Speaker:
ANUP AGARWAL
,
Ph.D. Candidate
Computer Science Department
Carnegie Mellon University
https://www.cs.cmu.edu/~anupa/
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 and noisy environments (e.g., cellular links, policers, token-bucket filters, operating system jitter). Second, they operate under uncertainty—they lack direct visibility into the state of the network or the flows they compete with. Recent work showed that we can model networks as non-deterministic, non-stochastic automatons to capture a wide range of real-world phenomena and formally verify controller performance on such environments. We seek to design CCAs that pass such verification checks. However, this 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 with verified performance guarantees. Our abstractions and tools allow us to discover previously unknown tradeoffs, design new CCAs that are on the Pareto-frontier, and provably guarantee performance even under challenging network conditions.
Thesis Committee
Srinivasan Seshan (Chair)
Vyas Sekar
Justine Sherry
Philip Brighten Godfrey (University of Illinois Urbana-Champaign)
Venkat Arun (University of Texas at Austin)
In Person and Zoom Participation. See announcement.
For More Information:
matthewstewart@cmu.edu