Towards Efficient Verification of Distributed In-Network Computing Programs
TL;DR
Procurator is a verification framework that efficiently captures interactive behaviors in distributed in-network programs and employs an intermediate representation (IR) pruner to reduce the execution space and a schedule-replay-based acceleration approach to avoid explicit exploration of long execution traces.
Abstract
Distributed in-network programs are increasingly deployed in data centers for their performance benefits, but shifting application logic to switches also enlarges the failure domain. Ensuring their correctness before deployment is thus critical for reliability. While prior verification frameworks can efficiently verify programs running on a single switch, they overlook the common interactive behaviors in distributed settings, thereby missing related bugs that can cause system failures. This paper presents Procurator, a verification framework that efficiently captures interactive behaviors in distributed in-network programs. Procurator models each P4 pipeline as a reactive actor and unifies their interactions as message passing to capture interactive behaviors under an event-driven paradigm. To improve the verification efficiency, Procurator employs an intermediate representation (IR) pruner to reduce the execution space and a schedule-replay-based acceleration approach to avoid explicit exploration of long execution traces. Evaluation shows that Procurator uncovers 28 distinct bugs in twelve real-world distributed in-network systems, and achieves up to a 9.1X speedup over the state-of-the-art framework.