Scalable Verification of Multi-ACK Properties in Loss-Based Congestion Control Implementations

Congestion control algorithms, such as RENO and CUBIC, are vital for the Internet. However, numerous bugs have been discovered and reported in the Congestion Control Algorithm Implementations (CCAIs), even in those that have been extensively tested and used on the Internet for years, such as Linux RENO and Linux CUBIC. Some of these bugs have potentially severe impacts on the performance and stability of the Internet. Unfortunately, current CCAI testing and verification methods are inadequate for proving the absence of bugs, require substantial verification expertise, or are not scalable to a large number of acknowledgment packets (ACKs) that trigger CCAI actions. To address all these shortcomings, we propose an ACK Scalable Method, called ASM. Our experiments with two representative loss-based CCAIs, Linux RENO and CUBIC, demonstrate the promising performance of the proposed ASM even with tens of thousands of ACKs.