Distributed network verification

Abstract

Some embodiments provide a method for evaluating a network. The method identifies multiple network correctness requirements configured for the network. The method instantiates a separate respective evaluation program instance for each respective identified network correctness requirement to evaluate the respective network correctness requirement. At least two evaluation program instances are instantiated on different machines. Each respective evaluation program instance stores in a respective memory a respective set of network device data to evaluate the respective network correctness requirement. Each set of network device data requires less memory than storing network device data for the entire network.

1 . A method for evaluating a network, the method comprising:
 identifying a plurality of network correctness requirements configured for the network; and   instantiating a separate respective evaluation program instance for each respective identified network correctness requirement to evaluate the respective network correctness requirement, at least two evaluation program instances instantiated on different machines,   wherein each respective evaluation program instance stores in a respective memory a respective set of network device data to evaluate the respective network correctness requirement, each set of network device data requiring less memory than storing network device data for the entire network.   
     
     
         2 . The method of  claim 1 , wherein first and second evaluation program instances are instantiated on a same particular machine. 
     
     
         3 . The method of  claim 2 , wherein the first and second evaluation program instances store respective first and second sets of network device data in memory of the particular machine to use in evaluating respective first and second network correctness requirements. 
     
     
         4 . The method of  claim 1 , wherein a particular evaluation program instance is assigned to evaluate two different network correctness requirements. 
     
     
         5 . The method of  claim 4 , wherein the particular evaluation program instance stores in its respective memory network device data to evaluate each of the two different network correctness requirements. 
     
     
         6 . The method of  claim 5 , wherein evaluation of the two network correctness requirements uses overlapping sets of network device data, the overlapping network device data only stored once in the memory for the particular evaluation program instance. 
     
     
         7 . The method of  claim 1  further comprising instantiating, for each respective network device in the network, a respective device data generation program instance to generate a respective network device data file for the respective network device. 
     
     
         8 . The method of  claim 7 , wherein:
 each respective device data generation program instance stores the respective network device data file in a distributed file system; and   evaluation program instances that require network device data for a particular network device retrieve the network device data file for the particular network device from the distributed file system and store in memory at least a portion of the network device data for the particular network device from the retrieved network device data file.   
     
     
         9 . The method of  claim 7 , wherein the evaluation program instances and the device data generation program instances are instantiated on a cluster of machines. 
     
     
         10 . The method of  claim 9 , wherein the cluster of machines is a cluster of virtual machines executing on a plurality of computing devices. 
     
     
         11 . The method of  claim 1 , wherein each respective evaluation program instance evaluates the respective network correctness requirement for which the respective evaluation program instance is instantiated when one or more network devices relevant to the respective network correctness requirement is updated. 
     
     
         12 . The method of  claim 11 , wherein a particular evaluation program instance evaluates its network correctness requirement by simulating processing within the network of a data message having a particular set of properties to ensure that data messages having the particular set of properties are processed correctly by the network. 
     
     
         13 . A non-transitory machine-readable medium storing a program which when executed by at least one processing unit evaluates a network, the program comprising sets of instructions for:
 identifying a plurality of network correctness requirements configured for the network; and   instantiating a separate respective evaluation program instance for each respective identified network correctness requirement to evaluate the respective network correctness requirement, at least two evaluation program instances instantiated on different machines,   wherein each respective evaluation program instance stores in a respective memory a respective set of network device data to evaluate the respective network correctness requirement, each set of network device data requiring less memory than storing network device data for the entire network.   
     
     
         14 . The non-transitory machine-readable medium of  claim 13 , wherein:
 first and second evaluation program instances are instantiated on a same particular machine; and   the first and second evaluation program instances store respective first and second sets of network device data in memory of the particular machine to use in evaluating respective first and second network correctness requirements.   
     
     
         15 . The non-transitory machine-readable medium of  claim 13 , wherein:
 a particular evaluation program instance is assigned to evaluate two different network correctness requirements; and   the particular evaluation program instance stores in its respective memory network device data to evaluate each of the two different network correctness requirements.   
     
     
         16 . The non-transitory machine-readable medium of  claim 15 , wherein evaluation of the two network correctness requirements uses overlapping sets of network device data, the overlapping network device data only stored once in the memory for the particular evaluation program instance. 
     
     
         17 . The non-transitory machine-readable medium of  claim 13 , wherein the program further comprises a set of instructions for instantiating, for each respective network device in the network, a respective device data generation program instance to generate a respective network device data file for the respective network device. 
     
     
         18 . The non-transitory machine-readable medium of  claim 17 , wherein:
 each respective device data generation program instance stores the respective network device data file in a distributed file system; and   evaluation program instances that require network device data for a particular network device retrieve the network device data file for the particular network device from the distributed file system and store in memory at least a portion of the network device data for the particular network device from the retrieved network device data file.   
     
     
         19 . The non-transitory machine-readable medium of  claim 17 , wherein the evaluation program instances and the device data generation program instances are instantiated on a cluster of machines. 
     
     
         20 . The non-transitory machine-readable medium of  claim 13 , wherein each respective evaluation program instance evaluates the respective network correctness requirement for which the respective evaluation program instance is instantiated when one or more network devices relevant to the respective network correctness requirement is updated. 
     
     
         21 . The non-transitory machine-readable medium of  claim 21 , wherein a particular evaluation program instance evaluates its network correctness requirement by simulating processing within the network of a data message having a particular set of properties to ensure that data messages having the particular set of properties are processed correctly by the network.