SearcharxivSearch

arXiv subjects

Wanjian Feng

Publications and source records attributed to Wanjian Feng.

3 recordsLinked to original sources

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

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.

cs.NI

Janus: Leveraging Incremental Computation for Efficient DNS Verification

Existing DNS configuration verification tools face significant issues (e.g., inefficient and lacking support for incremental verification). Inspired by the advancements in recent work of distributed data plane verification and the resemblance be- tween the data plane and DNS configuration, we tackle the challenge of DNS misconfiguration by introducing Janus, a DNS verification tool. Our key insight is that the process of a nameserver handling queries can be transformed into a matching process on a match-action table. With this insight, Janus consists of (1) an efficient data structure for partition query space based on the behaviors, (2) a symbolic execution algorithm that specifies how a single nameserver can efficiently cover all possible queries and ensure the accuracy of verification, (3) a mechanism to support incremental verification with less computational effort. Extensive experiments on real-world datasets (with over 6 million resource records) show that Janus achieves significant speedups, with peak improvements of up to 255.7x and a maximum 6046x reduction in the number of LECs.

cs.NI

RepLLM: Toward Automatically Reproducing Network Research Results

Result reproduction of computer networking research is challenging as the scarcity of open-source implementations and the complexity of heterogeneous system architectures. Even though Large Language Models have demonstrated potential in code generation, existing code generation frameworks often fail to address the long-context constraints and intricate logical dependencies, which are vital in reproducing network systems from academic papers. Thus, we introduce RepLLM, an end-to-end multi-agent framework designed to automate code reproduction from paper content. RepLLM features a collaborative architecture comprising four specialized agents -- Content Parsing, Architecture Design, Code Generation, and Audit&Repair, which are coordinated through Shared Memory mechanism to ensure global context consistency. With the enhancement of Structured Chain-of-Thought LLM reasoning and a sandbox-isolated static-dynamic debugging methodology, our framework effectively resolves semantic discrepancies and runtime errors, thereby improving reliable reproductions. Extensive evaluations on representative papers in top conferences demonstrate that RepLLM outperforms state-of-the-art system-level LLM frameworks in generating compile-ready and logically correct systems. Our results show that, with the aid of RepLLM, we can reproduce 95% of the original benchmarks within approximately two hours while reducing token consumption by up to 10% compared with state-of-the-art baselines.

cs.NI