Toward Efficient Verification of Distributed In-Network Computing Programs
Authors: Mingyuan Song, Huan Shen, Jinghui Jiang, Qiang Su (Xiamen University); Ziheng Zhang, Qingyu Song, Yuchao Zhang, Wanjian Feng, Fei Yuan, Yitao Xing, Wenjia Wei (Beijing University of Posts and Telecommunications); Qiao Xiang, Jiwu Shu (Xiamen University)
Introduction
This paper studies how to efficiently verify distributed in-network computing programs implemented across multiple programmable switches. As in-network computing evolves from single-device deployments to distributed pipelines, interactions such as recirculation, mirroring, and cross-switch message passing become essential to program semantics. However, existing verification tools mainly model a single switch and represent repeated processing with local while loops. They therefore cannot accurately capture distributed interactions and may miss bugs or report false positives. At the same time, explicitly exploring all possible interleavings creates a prohibitively large execution space.
Key Idea and Contribution
The authors build Procurator, an end-to-end verification framework for distributed in-network computing programs. Its central idea is to replace while-loop-based modeling with an event-driven model that treats interactions across processing passes and switches as asynchronous message-passing events. Each P4 pipeline instance is modeled as an actor, while recirculation, mirroring, and related mechanisms are represented uniformly as messages.
Procurator includes an intent specification language through which users declare the topology, assumptions, and assertions needed for verification. It also introduces an intermediate-representation pruner that uses cross-node and cross-pass dependency analysis to retain only the statements that can affect the target assertions. For bugs involving recirculation and other long execution paths, Procurator uses a three-stage scheduling and replay process to avoid explicitly exploring every step in the full trace. Together, these techniques reduce the verification search space while preserving the semantics of distributed interactions.
Evaluation
The authors evaluate Procurator on 12 real distributed systems and discover 28 previously undetected bugs, including implementation errors, functional defects, interleaving races, and recirculation failures. These bugs all depend on cross-switch interactions that cannot be triggered by single-device models. Intent-driven IR pruning achieves up to 25.06 times end-to-end acceleration and enables two tasks that previously timed out to complete successfully. Compared with the state-of-the-art single-switch verifier p4tv, Procurator achieves up to 9.1 times speedup and completes all tasks, while p4tv times out or crashes on some cases. Procurator also avoids false bug reports caused by p4tv’s incorrect modeling of recirculation semantics. This result is significant because distributed interactions are becoming central to in-network computing, and failing to verify them leaves a major reliability gap between tested programs and production deployments.
Q1: Many distributed P4 programs also include a component running on an end host. How does Procurator model the interaction between that host component and the P4 switches?
A1: Procurator models the host component as an environment actor. The intent specification declares which pipeline receives the host input, and the verifier infers the injected packet fields and constraints before sending the request into the corresponding pipeline actor. The interaction between the host environment and the network pipelines is therefore explicit in the model.
Q2: Besides the wraparound optimization, what scalability challenges remain open?
A2: Stateful P4 pipelines continuously receive input from the environment, so their event and state space can grow explosively and may even contain non-terminating behavior. The current mitigations are to prove only statements relevant to the verification intent, apply domain-specific optimizations such as the three short checks for deep traces, and explore parameterized verification for unbounded programs. These directions help, but scalable verification of such systems remains an open problem.
Personal Thoughts
This paper addresses an increasingly important verification problem as in-network computing becomes distributed. The most impressive aspect is Procurator’s precise modeling of P4 interaction semantics: recirculation and mirroring are treated as asynchronous events across processing passes rather than as simple iterations inside a local loop. This directly addresses why existing single-switch tools fail.
The IR-pruning design is also effective because it reduces the search space through dependency analysis without sacrificing the relevant verification semantics. Finding 28 real bugs and achieving up to 9.1 times acceleration provides strong evidence of practical value. Future work could extend the framework to heterogeneous hardware behavior, parameterized topologies, and larger classes of distributed invariants.