Model Checking-Based Performance Prediction for P4

Next-generation networks focus on scale and scope at the price of increasing complexity, leading to difficulties in network design and planning. As a result, anticipating all hardware- and software-related factors of network performance requires time-consuming and expensive benchmarking. This work presents a framework and software tool for automatically inferring the performance of P4 programmable network switches based on the P4 source code and probabilistic models of the execution environment with the hope of eliminating the requirement of the costly set-up of networked hardware and conducting benchmarks. We designed the framework using a top-down approach. First, we transform high-level P4 programs into a representation that can be refined incrementally by adding probabilistic environment models of increasing levels of complexity in order to improve the estimation precision. Then, we use the PRISM probabilistic model checker to perform the heavy weight calculations involved in static performance prediction. We present a formalization of the performance estimation problem, detail our solution, and illustrate its usage and validation through a case study conducted using a small P4 program and the P4C-BM reference switch. We show that the framework is already capable of performing estimation, and it can be extended with more concrete information to yield better estimates.