ddNF: An Efficient Data Structure for Header Spaces

Nikolaj Bjorner, Garvit Juniwal, Sanjit A. Seshia, George Varghese, and Ratul Mahajan. ddNF: An Efficient Data Structure for Header Spaces. In Proceedings of the Haifa Verification Conference (HVC), pp. 49–64, November 2016.
Best Paper Award.

Download

[pdf] 

Abstract

Network Verification is emerging as a critical enabler to manage large complex networks. In order to scale to data-center networks found in Microsoft Azure we developed a new data structure called ddNF, disjoint difference Normal Form, that serves as an efficient container for a small set of equivalence classes over header spaces. Our experiments show that ddNFs outperform representations proposed in previous work, in particular representations based on BDDs, and is especially suited for incremental verification. The advantage is observed empirically; in the worst case ddNFs are exponentially inferior than using BDDs to represent equivalence classes. We analyze main characteristics of ddNFs to explain the advantages we are observing.

BibTeX

@InProceedings{bjorner-hvc16,
  author = 	 {Nikolaj Bjorner and Garvit Juniwal and Sanjit A. Seshia and George Varghese and Ratul Mahajan},
  title = 	 {{ddNF}: An Efficient Data Structure for Header Spaces},
  booktitle = {Proceedings of the Haifa Verification Conference (HVC)},
  month = {November},
  year = 	 {2016},
  pages = "49--64",
  abstract = {Network Verification is emerging as a critical enabler to manage large 
complex networks. In order to scale to data-center networks found in Microsoft Azure we developed a new data structure called ddNF,  
disjoint difference Normal Form, that serves as an efficient  
container for a small set of equivalence classes over header spaces.  
Our experiments show that 
ddNFs outperform representations proposed in previous work, in particular 
representations based on BDDs, and is especially suited for incremental 
verification. The advantage is observed empirically;  
in the worst case ddNFs are  
exponentially inferior than using BDDs to represent equivalence classes.  
We analyze main characteristics of ddNFs to explain the advantages 
we are observing.},
  wwwnote = {<b>Best Paper Award</b>.}
}