US 11,720,373 B2
Data plane program verification
Jeongkeun Lee, Los Altos, CA (US); Cole Nathan Schlesinger, Mountain View, CA (US); John Nathan Foster, Ithaca, NY (US); Han Wang, San Jose, CA (US); Robert Soule, Hamden, CT (US); William Hallahan, Nashua, NH (US); Steffen Julif Smolka, Ithaca, NY (US); and Mon Jed Liu, Santa Clara, CA (US)
Assigned to Barefoot Networks, Inc., Santa Clara, CA (US)
Filed by Barefoot Networks, Inc., Santa Clara, CA (US)
Filed on Nov. 29, 2021, as Appl. No. 17/537,301.
Application 17/537,301 is a continuation of application No. 16/022,601, filed on Jun. 28, 2018, granted, now 11,188,355.
Claims priority of provisional application 62/663,141, filed on Apr. 26, 2018.
Claims priority of provisional application 62/571,121, filed on Oct. 11, 2017.
Prior Publication US 2022/0083352 A1, Mar. 17, 2022
Int. Cl. G06F 9/445 (2018.01); G06F 11/36 (2006.01); G06F 8/51 (2018.01); H04L 45/745 (2022.01)
CPC G06F 9/44589 (2013.01) [G06F 8/51 (2013.01); G06F 11/3604 (2013.01); G06F 11/3608 (2013.01); G06F 11/3636 (2013.01); H04L 45/745 (2013.01)] 18 Claims
OG exemplary drawing
 
1. A non-transitory machine-readable medium storing a verification program for execution by a set of processing units, the verification program for verifying the correctness of a forwarding-element program to be executed by a control-plane circuit to configure a data-plane circuit of a forwarding element to forward data messages, the forwarding-element program specifying at least one element that is populated during execution by a control plane circuit, the verification program comprising a set of instructions that when executed by the set of processing units results in performance of operations comprising:
receiving the forwarding-element program;
annotating the forwarding-element program to reflect assumptions regarding control-plane behavior;
translating the forwarding-element program and annotations into a different programming language that incorporates non-deterministic choice based on the assumptions regarding control plane behavior; and
using the translated program to verify the correctness of the forwarding-element program and assumptions regarding the control plane behavior;
wherein:
the data-plane circuit comprises a plurality of programmable packet processing stages that comprise match-action tables that are to be configured by the control-plane circuit for use in forwarding the data messages; and
the using the translated program to verify the correctness of the forwarding-element program and the assumptions regarding the control-plane behavior comprises verifying whether entries in the match-action tables depend on each other.