Verifying the Performance of Network Control Algorithms

As networked systems become critical infrastructure, their design must reflect their new societal role. Today, we build systems with hundreds of heuristics but often do not understand their inherent and emergent behaviors. This dissertation presents, performance verification, a set of tools and techniques to prove performance properties of heuristics running in real-world conditions. It provides an alternative to queuing and control theory, which are typically too optimistic about performance because of their limited capacity to accurately model real-world phenomena. Overly optimistic analysis can lead to heuristic designs that fail in unexpected ways upon deployment. Rigorous proofs on the other hand, can not only inspire confidence in our designs, but also give counter-intuitive insights about their performance. A key theme in our approach is to model uncertainty in systems using non-random, non-deterministic objects that cover a wide range of possible behaviors under a single abstraction. Such models allow us to analyze complex system behaviors using automated reasoning techniques. We will present automated tools to analyze congestion control and process scheduling algorithms. These tools prove performance properties and find counter-examples where widely deployed heuristics fail. We will also prove that current end-to-end congestion control algorithms that bound delay cannot avoid starvation.

Name thesis:degree_name

Doctoral

Department dc:contributor.department

Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science

Grantor dc:publisher

Massachusetts Institute of Technology

Year dc:date.issued

2023

Author dc:creator

• Arun, Venkat

Advisors dc:contributor.advisor

• Balakrishnan, Hari
• Alizadeh, Mohammad

Statement dc:rights

• In Copyright - Educational Use Permitted
• Copyright retained by author(s)

Licence dc:rights.uri

• https://rightsstatements.org/page/InC-EDU/1.0/

Handle dc:identifier.uri

https://hdl.handle.net/1721.1/152861

OAI identifier oai:identifier

oai:dspace.mit.edu:1721.1/152861