Date: February 23, 2021
Time: 3:30-4:30pm ET
Video coming soon.
Abstract
Like many industrial languages, the P4 programming language has developed without a formal foundation. The P4 Language Specification is a 160-page document with a mixture of informal prose, graphical diagrams, and pseudocode; it leaves many aspects of program behavior up to individual compilation targets and compiler backends. The P4 reference implementation is a complex system, running to over 40KLoC of C++ code, with support for only a few targets. This talk presents a new framework, called Petr4, that puts the P4 programming language on a more solid semantic foundation. Petr4 consists of a clean-slate definitional interpreter and a core calculus that models a fragment of P4. Its semantics have been validated against existing test suites and the core calculus has been proved type-safe and terminating. While developing Petr4, we reported dozens of bugs in the language specification and the reference implementation, many of which have been fixed.
Bio
Ryan is a Ph.D. student at Cornell University where he is advised by Nate Foster. His research applies programming language techniques to computer networking problems.