BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//project/author//NONSGML v1.0//EN
CALSCALE:GREGORIAN
BEGIN:VEVENT
DTEND:20220818T120000Z
UID:3223d6c911cef022bc0dfa879ab9ac9f-314
DTSTAMP:19700101T120014Z
DESCRIPTION:Reasoning about congestion control behavior
URL;VALUE=URI:https://www.csa.iisc.ac.in/newweb/event/314/reasoning-about-congestion-control-behavior/
SUMMARY: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.
DTSTART:20220818T120000Z
END:VEVENT
END:VCALENDAR