Count-Based Abstractions for Performance Verification of Contention Points
summary
Develops a count+window abstraction that tracks small windows of per-class packet counts plus overflow barriers to bound reordering and trade precision for size. Arrays model memory per packet and fails beyond tens of packets while pure counts scale but allow pathological reordering; setting window size to buffer capacity yields the same verification results as prior array models on FRoof benchmarks and makes verification largely insensitive to buffer capacity up to realistic hundreds or thousands of packets. A modular tool decouples buffers from mediation logic so multiple buffer models plug in and scale benefits appear in evaluation.
AI-written summary · about
chapters (13)
- 0:00Introduction
- 1:22Contention points in networks
- 2:47Buffers for performance verification
- 4:52Limitations of count-only buffers
- 6:37Counts plus windows model
- 8:44Windowing enforces ordering
- 10:48Choosing window size
- 11:50Evaluating buffer model
- 13:15Case studies and results
- 14:20Array vs count-based models
- 15:00Decoupling buffer models
- 15:42Additional topics
- 16:03Key takeaways and concluding remarks
related talks
17mTowards provably performant congestion control
31mParameterized Verification of Systems with Precise (0,1)-Counter Abstraction
40mCentralized Counters in a Distributed World Event Based Realtime Statistics using eTally
25mVirtualizing Traffic Shapers for Practical Resource Allocation
15mEverything Matters in Programmable Packet Scheduling
16mA Layered Formal Methods Approach to Answering Queue-related Queries
16mPacket Order Matters! Improving Application Performance by Deliberately Delaying Packets
25mApproximating Fair Queueing on Reconfigurable Switches