Keeping P4 Switches Fast and Fault-free through Automatic Verification
Abstract
The networking dataplane is going through a paradigm shift as softwarization of switches sees an increased pull from the market. Yet, software tooling to support development with these new technologies is still in its infancy.
In this work, we introduce a framework for verifying performance requirement conformance of data plane protocols defined in the P4 language . We present a framework that transforms a P4 program in a versatile symbolic formula which can be utilized to answer various performance queries. We represented the system using denotational semantics and it can be easily extended with low-level target-dependent information. We demonstrate the operation of this system on a toy specification.
Downloads
References
P4C reference compiler for the P416 programming language. https://github.com/p4lang/p4c, 2017. [Online; accessed 30-September-2018].
7-Zip LZMA Benchmarks. https://www.7-cpu.com/cpu/Skylake_X.html, 2018. [Online; accessed 30-September-2018].
Sapio, A, Baldi, M., Pongrácz, G. Cross-Platform Estimation of Network Function Performance. In 2015 Fourth European Workshop on Software Defined Networks, pages 73-78, Sept 2015. DOI: 10.1109/EWSDN.2015.64.
Agner Fog. Lists of instruction latencies, throughputs and micro-operation breakdowns for Intel, AMD and VIA CPUs. https://www.agner.org/optimize/instruction_tables.pdf, 2018.09.15. [Online; accessed 30-September-2018].
Albert, Elvira, Arenas, Puri, Genaim, Samir, and Puebla, Germán. Cost relation systems: A language-independent target language for cost analysis. Electron. Notes Theor. Comput. Sci., 248:31--46, August 2009. DOI: 10.1016/j.entcs.2009.07.057.
Graf, Albert. The Pure Programming Language and Library Documentation. https://agraef.github.io/pure-docs/, 2018. [Online; accessed 30-September-2018].
Bosshart, et. al. P4: Programming protocol-independent packet processors. SIGCOMM Comput. Commun. Rev., 44(3):87--95, July 2014.
DOI: 10.1145/2656877.2656890.
Dobrescu, Mihai and Argyraki, Katerina. Software dataplane verification. In Proceedings of the 11th USENIX Conference on Networked Systems Design and Implementation, NSDI'14, pages 101--114, Berkeley, CA, USA, 2014. USENIX Association.
Flanagan, Cormac, Sabry, Amr, Duba, Bruce F., and Felleisen, Matthias. The essence of compiling with continuations. In Proceedings of the ACM SIGPLAN 1993 Conference on Programming Language Design and Implementation, PLDI '93, pages 237--247, New York, NY, USA, 1993. ACM. DOI: 10.1145/155090.155113.
Kheradmand, Ali and Rosu, Grigore. P4K: A formal semantics of P4 and applications. CoRR, abs/1804.01468, 2018.
Laki, Sándor, Horpácsi, Dániel, Vörös, Péter, Kitlei, Róbert, Leskó, Dániel, and Tejfel, Máté. High speed packet forwarding compiled from protocol independent data plane specifications. In Proceedings of the 2016 ACM SIGCOMM Conference, SIGCOMM '16, pages 629--630, New York, NY, USA, 2016. ACM. DOI: 10.1145/2934872.2959080.
Liu, et al. P4V: Practical Verification for Programmable Data Planes. In Proceedings of the 2018 Conference of the ACM Special Interest Group on
Data Communication, SIGCOMM '18, pages 490--503, New York, NY, USA, 2018. ACM. DOI: 10.1145/3230543.3230582.
Sivaraman, Anirudh, Kim, Changhoon, Krishnamoorthy, Ramkumar, Dixit, Advait, and Budiu, Mihai. Dc.p4: Programming the forwarding plane of a data-center switch. In Proceedings of the 1st ACM SIGCOMM Symposium on Software Defined Networking Research, SOSR '15, pages 2:1--2:8, New York, NY, USA, 2015. ACM. DOI: 10.1145/2774993.2775007.
Stoenescu, et. al. Debugging p4 programs with vera. In Proceedings of the 2018 Conference of the ACM Special Interest Group on Data Communication, SIGCOMM '18, pages 518--532, New York, NY, USA, 2018. ACM. DOI: 10.1145/3230543.3230548.
The P4 Language Consortium. P416 Language Specification. https://p4.org/specs/, 2017. [Online; accessed 30-September-2018].
Wegbreit, Ben. Mechanical program analysis. Commun. ACM, 18(9):528--539, September 1975. DOI: 10.1145/361002.361016.
