A Layered Formal Methods Approach to Answering Queue-related Queries

on YouTube ↗16m

" summary

QuASI answers whether queue-related queries (e.g., whether a queue could exceed a threshold, burst occurrence, max buffer occupancy) are possible using only per-port minute packet counts by checking existence of a consistent packet trace. It uses a lossless enqueue-rate abstraction, a two-layer pipeline with a fast over-approximation layer that builds a cover-set and representative traces and reduces consistency to a 0/1 matrix (Gale–Ryser), and an SMT-based exact check for positives. Claims no false positives or false negatives, is up to 106X faster than prior work, and scales to hundreds of millions of time steps.

AI-written summary · about

" chapters (8)

1. 0:00Introduction
2. 1:47Latency SLOs with limited data
3. 3:57Queue length query problem
4. 6:46Quasi's layered formal methods
5. 9:37Quasi's over-approximate analysis
6. 12:29Quasi's exact analysis
7. 13:52Evaluation and comparison
8. 15:38Key takeaways

" related talks

• 16mManaging Congestion Control Heterogeneity on the Internet with Approximate Performance...Ayush Mishra, Archit Bhatnagar, Yixuan Zhang, Ben Leong, Ya Gao, Raj Joshi · NSDI '26
• 15mFormal Methods for Network Performance AnalysisRyan Beckett, Mina Tahmasbi Arashloo, Rachit Agarwal · NSDI 2023
• 16mGearbox: A Hierarchical Packet Scheduler for Approximate Weighted Fair QueuingPeixuan Gao, Anthony Dalleggio, Yang Xu, H. Jonathan Chao · 19th USENIX Symposium on Networked Systems Design and Implementation (NSDI '22)
• 25mApproximating Fair Queueing on Reconfigurable SwitchesMing Liu, Arvind Krishnamurthy, Naveen Kr. Sharma, Kishore Atreya · NSDI '18
• 12mTwenty Years After: Hierarchical Core-Stateless Fair QueueingIon Stoica, Xin Jin, Vladimir Braverman, Zhuolong Yu, Jingfeng Wu · NSDI ’21
• 20mHarmony: A Congestion-free Datacenter ArchitectureAmin Vahdat, Saksham Agarwal, Qizhe Cai, Rachit Agarwal, David Shmoys · 21st USENIX Symposium on Networked Systems Design and Implementation (NSDI '24)
• 22mProgrammable Calendar Queues for High-speed Packet SchedulingMing Liu, Changhoon Kim, Arvind Krishnamurthy, Anirudh Sivaraman, Chenxingyu Zhao, Pravein Govindan Kannan, Naveen Kr. Sharma · NSDI 2020
• 17mTowards provably performant congestion controlRuben Martins, Anup Agarwal, Srinivasan Seshan, Venkat Arun, Devdeep Ray · 21st USENIX Symposium on Networked Systems Design and Implementation (NSDI '24)