Search papers, labs, and topics across Lattice.
This paper introduces a fast analyzer for quantitative network properties using weighted NetKAT (wNetKAT), enabling engineers to assess trade-offs in network design effectively. The core innovation lies in the creation of weighted symbolic packet programs (wSPPs), which allow for the compact representation and symbolic computation of weighted policies, significantly improving efficiency over existing methods. The authors demonstrate that their implementation not only competes with established tools like KATch but also outperforms others like McNetKAT and Storm, showcasing its utility in multi-objective design-time analysis through a case study on data-center topologies.
Achieving orders of magnitude speedup in quantitative network analysis, this tool enables engineers to efficiently navigate complex design trade-offs.
When designing a network, engineers must navigate trade-offs (e.g., one topology offers more aggregate bandwidth, another lower latency or better resilience) that demand reasoning about quantitative properties. We present a fast analyzer for quantitative network properties based on weighted NetKAT (wNetKAT), a domain-specific language that provides a semantic foundation for quantitative reasoning by modeling network behavior using weights drawn from a semiring. At the core of our development is the design of a symbolic data structure -- weighted symbolic packet programs (wSPPs) -- that compactly represent the semantics of weighted policies, for which a direct implementation would be intractable. We show how to compute all policy constructs symbolically; unsurprisingly, the crux is Kleene star, for which we design a tailored algorithm. We further develop trace-carrying Pareto semirings, which compute multi-objective frontiers together with the network paths that realize them. We formalize the development in Lean and provide an optimized Rust implementation. Being parametric on a semiring, our implementation covers both classical and quantitative analyses: we show that it is competitive with KATch, a heavily optimized Boolean-reachability verifier, and orders of magnitude faster than McNetKAT and Storm on probabilistic analyses. A case study comparing Fat-tree and Jellyfish data-center topologies shows the framework supports multi-objective design-time analysis.
