A Performance Verification Methodology for Resource Allocation Heuristics

TL;DR

This paper introduces Virelay, a versatile framework for verifying the performance of resource allocation heuristics, demonstrating its utility through diverse case studies and uncovering practical insights and bugs.

Contribution

The paper presents Virelay, a new framework that simplifies performance verification of heuristics and applies it to multiple scenarios, revealing bounds, behaviors, and bugs.

Findings

Bounds on classical algorithms' performance under practical assumptions

Virelay captures models for congestion control and scheduling

Identified bugs in Linux CFS load balancer

Abstract

Performance verification is a nascent but promising tool for understanding the performance and limitations of heuristics under realistic assumptions. Bespoke performance verification tools have already demonstrated their value in settings like congestion control and packet scheduling. In this paper, we aim to emphasize the broad applicability and utility of performance verification. To that end, we highlight the design principles of performance verification. Then, we leverage that understanding to develop a set of easy-to-follow guidelines that are applicable to a wide range of resource allocation heuristics. In particular, we introduce Virelay, a framework that enables heuristic designers to express the behavior of their algorithms and their assumptions about the system in an environment that resembles a discrete-event simulator. We demonstrate the utility and ease-of-use of Virelay by applying it to six diverse case studies. We produce bounds on the performance of classical algorithms, work stealing and SRPT scheduling, under practical assumptions. We demonstrate Virelay's expressiveness by capturing existing models for congestion control and packet scheduling, and we verify the observation that TCP unfairness can cause some ML training workloads to spontaneously converge to a state of high network utilization. Finally, we use Virelay to identify two bugs in the Linux CFS load balancer.