Using headerspace analysis to identify flow entry reachability

A method comprising:

• receiving a plurality of flow entries for distribution to a forwarding element in a network, wherein each flow entry comprises a set of conditions to be matched by a packet header and a set of actions to perform on a packet that matches the set of conditions, wherein the flow entries are arranged in stages;
• modeling each of the flow entries as a function that operates on a representation of a packet header;
• determining a set of packet headers of packets to be received by the forwarding element;
• determining a set of the plurality of flow entries that are not matched by a packet header of any packet to be received by the forwarding element by applying the functions to representations of the determined set of packet headers,
• wherein applying the functions to representations of the determined set of packet headers comprises, for a particular representation of a particular packet header:
• for each particular stage:
• identifying a set of transfer functions for flow entries of the particular stage matched by a current packet header representation, wherein the current packet header representation is the particular packet header representation for the first stage;
• selecting one of the identified set of transfer functions for the flow entries of the particular stage and applying the selected transfer function to the current packet header representation to generate a modified packet header representation;
• when the selected transfer function does not include an action that serves as an endpoint for the current packet header representation, advancing to a next stage;
• when the selected transfer function includes an action that serves as an endpoint for the current packet header representation and the identified set of transfer functions for the current stage includes unselected transfer functions, selecting and applying another of the selected transfer functions to the modified packet header representation to generate a new modified packet header representation;
• and
• when the selected transfer function includes an action that serves as an endpoint for the current packet header representation and all of the transfer functions of the identified set of transfer functions for the current stage have been selected, returning to a previous stage with additional unselected transfer functions to apply the unselected transfer functions to a current packet header representation from the previous stage.

A non-transitory machine readable medium storing a program for execution by at least one processing unit, the program comprising sets of instructions for:

• receiving a plurality of flow entries for distribution to a forwarding element in a network, wherein each flow entry comprises a set of conditions to be matched by a packet header and a set of actions to perform on a packet that matches the set of conditions, wherein the flow entries are arranged in stages;
• modeling each of the flow entries as a function that operates on a representation of a packet header;
• determining sets of packet headers representing all possible packets to be received by the forwarding element from a particular set of sources, each set of packet headers represented by a plurality of packet header field values with at least one packet header field wildcarded;
• and
• determining, of the plurality of flow entries, a set of flow entries that are not matched by a packet header of any of the possible packets to be received by the forwarding element, by processing the representations of the sets of packet headers through the stages of functions that model the flow entries and marking each of the flow entries the corresponding function of which is applied to at least one packet header representation.