Seminars

View all Seminars  |  Download ICal for this event

Reasoning about congestion control behavior

Series: Department Seminar

Speaker: Venkat Arun, MIT, USA

Date/Time: Aug 18 14:30:00

Location: CSA Class (Room No. 252, First Floor)

Faculty Advisor:

Abstract:
The diversity of paths on the Internet makes it difficult for designers and operators to confidently deploy new congestion control algorithms (CCAs) without extensive real-world experiments, but such capabilities are not available to most of the networking community. And even when they are available, understanding why a CCA under-performs by trawling through massive amounts of statistical data from network connections is challenging. The history of congestion control is replete with many examples of surprising and unanticipated behaviors unseen in simulation but observed on real-world paths. In this talk I will present a simple mathematical approach to enable us to reason about congestion control behavior under such complex network phenomena. We use this approach in two ways. First, we develop CCAC (Congestion Control Anxiety Controller), a tool that uses formal verification to establish certain properties of CCAs. It is able to prove hypotheses about CCAs or generate counterexamples for invalid hypotheses. With CCAC, a designer can not only gain greater confidence prior to deployment to avoid unpleasant surprises, but can also use the counterexamples to iteratively improve their algorithm. We have modeled additive-increase/multiplicative-decrease (AIMD), Copa, and BBR with CCAC, and describe some surprising results from the exercise. Second, we tried designing a CCA that works under our network model. To our surprise, CCAC showed that all CCAs we tried suffer from starvation, an extreme form of unfairness. Further, starvation occurred under network conditions that are common on the internet. Motivated by this, we proved an impossibility result: current methods to develop delay-bounding CCAs cannot always avoid starvation. We identify a key property that makes current CCAs susceptible to starvation: when run on a path with a fixed bottleneck rate, these CCAs converge to a small delay range in equilibrium. Starvation may occur when such a CCA runs on paths that have non-congestive network delay variations due to real-world factors such as ACK aggregation and end-host scheduling. These can cause the CCA to misestimate capacity and starve. Finally I will talk about how these techniques may be used understand the performance of other heuristics used in computer systems in a mathematically precise and practically relevant way.

Speaker Bio:
Venkat Arun is a sixth year PhD student at CSAIL, MIT working with Hari and Mohammad. He has worked on congestion control. His CCA, Copa (NSDI'18), is being used in production at Facebook. His work on formally verifying congestion control is the subject of this talk (SIGCOMM'21, SIGCOMM'22). He also worked on RFocus (NSDI'20), a radio system that makes it practical to have single communication links use thousands of antennas by moving beamforming functions from the endpoints to the environment. Each

Host Faculty: R Govindarajan