Computing Precise Control Interface Specifications
summary
Algorithm computes precise control interface specs for data-plane programs by lifting GCL programs, applying quantifier elimination, and using a path-based analysis with modular instrumentation to produce CI-specs that are both safe and maximally permissive. Checking a fixed device configuration against a CI-spec runs in polynomial time; the implementation Capiche infers specs for real P4 pipelines (most in seconds–minutes), finds actual bugs in deployed code, and flags some cases that hit a 24‑hour timeout which often indicate interface defects.
AI-written summary · about
chapters (11)
- 0:00Precise control interface specs
- 1:26Unknown function implementations
- 3:13Limitations of interface specs
- 4:58Defining precise specs
- 6:21Computed specs in networking
- 7:46Control specs in robust networks
- 8:28Pipeline programs with GCL
- 10:34Compiling functions to logic
- 11:56Efficient monitoring
- 13:19Evaluation on P4 programs
- 14:43Summary and open questions
related talks
18mP4Cub: A Little Language for Big Routers
18mCCC: Re-architecting Delay-based Congestion Control in Datacenter Networks
16mCetus: Releasing P4 Programmers from the Chore of Trial and Error Compiling
21mConfig2Spec: Mining Network Specifications from Network Configurations
17mMitigating CPU Frontend for Complex Data Plane Applications
17mPerformance Interfaces for Network Functions
25mP4-SpecTec: A Language Mechanization Framework for P4
25mFormal Verification of a Software Defined Delay-Tolerant Network