Argo: An efficient verification framework for distributed in-network computing

TL;DR

Procurator is a verification framework that models distributed in-network programs to detect bugs caused by interactive behaviors, significantly improving scalability and bug detection accuracy.

Contribution

It introduces a formal model combining actor paradigm and CSP, a unified intent language, and a semantic-aware state pruner for scalable verification of distributed in-network programs.

Findings

Uncovered 10 bugs in real-world systems

Reduced verification time by up to 913.2x

Lowered memory usage by up to 1.9x

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 detect bugs for programs running on a single switch, they overlook the common interactive behaviors in distributed settings, thereby missing related bugs that can cause state inconsistencies and system failures. This paper presents Procurator, a verification framework that efficiently captures interactive behaviors in distributed in-network programs. Procurator introduces a formal model combining the actor paradigm with Communicating Sequential Processes (CSP), translating pipeline execution into reactive, event-driven actors and unifying their interactions as message passing. To support flexible specification of distributed properties, it provides a unified intent language. Additionally, it incorporates a semantic-aware state pruner to reduce verification complexity, thus ensuring system scalability. Evaluation results show that Procurator efficiently uncovers 10 distinct bugs caused by interactive behaviors across five real-world in-network systems. It also reduces verification time by up to 913.2x and memory consumption by up to 1.9x compared to the state-of-the-art verifier.