| Autor: |
William T. Hallahan, Calin Cascaval, Nick McKeown, Jeongkeun Lee, Jed Liu, Cole Schlesinger, Milad Sharif, Han Wang, Nate Foster, Robert Soulé |
| Rok vydání: |
2018 |
| Předmět: |
|
| Zdroj: |
SIGCOMM |
| DOI: |
10.1145/3230543.3230582 |
| Popis: |
We present the design and implementation of p4v, a practical tool for verifying data planes described using the P4 programming language. The design of p4v is based on classic verification techniques but adds several key innovations including a novel mechanism for incorporating assumptions about the control plane and domain-specific optimizations which are needed to scale to large programs. We present case studies showing that p4v verifies important properties and finds bugs in real-world programs. We conduct experiments to quantify the scalability of p4v on a wide range of additional examples. We show that with just a few hundred lines of control-plane annotations, p4v is able to verify critical safety properties for switch.p4, a program that implements the functionality of on a modern data center switch, in under three minutes. |
| Databáze: |
OpenAIRE |
| Externí odkaz: |
|
