The P4 sandbox is powered by Petr4, developed at Cornell University in the Networking Lab, led by Nate Foster. Additional information about Petr4 and how it powers our sandbox is found at the bottom of this page.
You can explore P4 code evaluation with an input packet and observe the resulting output packet and port number. Experiment by replacing the P4 Program textbox and/or the Input Packet textbox with your own values. Click the Evaluate button and see the results! We will be adding more examples, so check back in the future as well.
This example is a subset of the demo shown in the video below. It provides a simple case of a packet routed through three ports. The input packet header (in hex: “01 02 00 03 00 04 01 AA BB”) specifies start (01), a hop out port 2 (02 00), a hop out port 3 (03 00), and a hop out port 4 (04 01, with 01 as the hop terminator). “AA BB” in the input header is allowed by the ACL table in the P4 program; see line 70 in the code box. The rest of the input packet is the data, “4f 48 20 4d 59 59 20 49 20 4b 4e 4f 57 20 57 48 59”. Don’t worry about formatting because Petr4 ignores whitespace.
Click the Evaluate! button, and the output packet (in hex) is displayed, followed by the port number (as a string). Notice that Petr4 removed the first hop (02 00) from the packet because it is complete.
Now copy the output packet, excluding the port number, and paste it in the input packet textbox, overwriting everything else in the input packet textbox.
Click the Evaluate! button again for the 2nd hop.
As you did previously, copy the output packet, excluding the port number, and overwrite the entire input packet textbox. Then click the Evaluate! button for the 3rd hop.
The process is complete, as indicated by 00 at the beginning of the packet.
You can experiment with the input packet and code by following along in the demo or by using your imagination.
Follow along with the demo
READ ACM PAPER
P4 is a domain-specific language for programming and specifying packet-processing systems with high-level abstractions efficiently compiled for software or hardware implementations. Petr4 is a formal framework that models the semantics of P4. It consists of a clean-slate definitional interpreter for P4 and a formal calculus that models the essential features of the language. Petr4 is not tied to any particular target.
Result: The Petr4 interpreter validated a suite of over 750 tests from the P4 reference implementation, exercising the interface for different targets. The core calculus was validated with a proof of type-preserving termination.
Benefit: Petr4 discovered dozens of bugs in the P4 language specification and reference implementation, many of which have been fixed.
Future: The Petr4 project plans to extend the calculus to model the full language and publish it as a valuable resource for designers, compiler writers, and application programmers in the P4 community.
Petr4 is equipped with two user interfaces.
Both user interfaces are useful in teaching P4. They eliminate much of the overhead and complexity associated with using p4c and bmv, such as setting up virtual machines, installing dependencies, hooking into the Linux networking stack, and coordinating behavior across multiple stand-alone binaries.
In the Petr4 web interface, the evaluation function takes an input packet (as a hex string) and a P4 program (as a string in P4 syntax) and returns the output packet (as a hex string) and the output port (e.g., “port 2”).
Petr4 source is found on GitHub. The project is part of the Cornell University Networking Lab, led by Nate Foster.
