Mahjong: A Generic Framework for Network Data Plane Verification

Existing network data plane verification approaches check network correctness with various models and algorithms. With respect to a specific scenario, it is hard to judge which network model provides sufficient functionality and suitable performance, because existing verification approaches are implemented with different languages and evaluated against different datasets on different hardware platforms in their papers. A network operator usually has to try out a number of complex verification approaches to find the best one for her/his network and intents. Mahjong has a modular system architecture, a unified input format, and three classic verification tools built-in. Leveraging its well-defined partition interfaces and straight-forward configuration file, not only existing approaches can be refactored and merged into Mahjong, new approaches can also be introduced and evaluated with ease.