Data plane program verification
A method for verifying data plane programs is provided in some embodiments. Because the behavior of a data plane program (e.g., a program written in the P4 language) is determined in part by the control plane populating match-action tables with specific forwarding rules, in some embodiments, programmers are provided with a way to document assumptions about the control plane using annotations (e.g., in the form of “assertions” or “assumptions” about the state based on the unknown control plane contribution). In some embodiments, annotations are added automatically to verify common properties, including checking that every header read or written is valid, that every expression has a well-defined value, and that all standard metadata is manipulated correctly. The method in some embodiments translates programs from a first language (e.g., P4) to a second language (e.g., Guarded Command Language (GCL)) for verification by a satisfiability modulo theory (SMT) solver.
1. A non-transitory machine readable medium comprising instructions stored thereon, that if executed by one or more processors, cause the one or more processors to:
access a data-plane configuration program, wherein:
the data-plane configuration program is to configure one or more programmable stages of a packet processing pipeline and the data-plane configuration program comprises one or more annotations of one or more assumptions concerning data-plane execution by at least one of the one or more programmable stages of a packet processing pipeline;
verify correctness of the data-plane configuration program, including the one or more annotations of one or more assumptions concerning data-plane execution by at least one of the one or more programmable stages of a packet processing pipeline; and
based on a presence of an erroneous assumption associated with an annotation in the data-plane configuration program, provide an indication of error concerning the erroneous assumption in an annotation.
2. The machine readable medium of claim 1 , wherein the data-plane configuration program is consistent with P4 programming language.
3. The machine readable medium of claim 1 , wherein to verify correctness of the data-plane configuration program, including the one or more annotations of one or more assumptions concerning data-plane execution by at least one of the one or more programmable stages of a packet processing pipeline, the one or more processors are to:
translate the data-plane configuration program from a first programming language to a second programming language.
4. The machine readable medium of claim 1 , wherein the first programming language is consistent with P4 programming language and the second programming language is consistent with Guarded Command Language (GCL).
5. The machine readable medium of claim 1 , wherein to verify correctness of the data-plane configuration program, including the one or more annotations of one or more assumptions concerning data-plane execution by at least one of the one or more programmable stages of a packet processing pipeline, the one or more processors are to:
translate the data-plane configuration program from a first programming language to a second programming language, wherein the second programming language includes a non-deterministic choice based on at least one of the one or more annotations of one or more assumptions concerning data-plane execution by at least one of the one or more programmable stages of a packet processing pipeline.
6. The machine readable medium of claim 1 , wherein the at least one of the one or more annotations of one or more assumptions concerning data-plane execution by at least one of the one or more programmable stages of a packet processing pipeline comprises a match-action table configuration.
7. The machine readable medium of claim 1 , wherein the at least one of the one or more annotations of one or more assumptions concerning data-plane execution by at least one of the one or more programmable stages of a packet processing pipeline comprises a forwarding rule configured in a match-action table by a control-plane.
8. A method comprising:
receiving a source code of a program comprising a domain-specific language for programming a data plane circuit, wherein the program includes one or more annotations of one or more assumptions concerning data-plane execution by the data plane circuit and providing feedback of one or more invalid assumptions in a user interface (UI).
9. The method of claim 8 , wherein the domain-specific language for programming a data plane circuit comprises P4 programming language.
10. The method of claim 8 , comprising:
verifying correctness of the domain-specific language.
11. The method of claim 10 , wherein:
verifying correctness of the domain-specific language comprises translating the program from a first programming language to a second programming language.
12. The method of claim 11 , wherein the first programming language is consistent with P4 programming language and the second programming language is consistent with Guarded Command Language (GCL).
13. The method of claim 10 , wherein:
verifying correctness of the domain-specific language comprises translating the program from a first programming language to a second programming language, wherein the second programming language includes a non-deterministic choice based on at least one of the one or more annotations of one or more assumptions concerning data-plane execution by at least one of the one or more programmable stages of a packet processing pipeline.
14. The method of claim 8 , wherein the one or more annotations of one or more assumptions concerning data-plane execution by the data plane circuit comprises an assumption that a match-action operation was performed.
15. The method of claim 8 , wherein the one or more annotations of one or more assumptions concerning data-plane execution comprises a forwarding rule configured in a match-action table by a control-plane.