checkin small edits

.gitignore

@@ -1,3 +1,8 @@
 *~
 *.swp
 *.un~
+
+
+
+.DS_Store
+

doc/distributed-data-plane-verification/coral.md

@@ -3,21 +3,20 @@
 #### Rev 0.1
 
 # Table of Contents
-todo
+TBD in Markdown with links
 
 # Revision
 
 | Rev   | Date  | Author | Change Description |
-| :---: | :---: | :----- | :----------------- |
-|       |       |        |                    |
+| ---- | ---------- | -----------| ------------------|
+| v0.1 | 02/24/2022 | Qiao Xiang, Chenyang Huang, Ridi Wen, Jiwu Shu| Initial version |
 
-# About this Manual
-This document describes the design details of distributed data plane verification feature.
-
-TODO
 
 # Scope
-This document describes the high level design details about how distributed data plane verification works.
+This document describes the high-level design of the distributed data plane verification feature.
+
+
+
 
 # Definitions/Abbreviations
 ###### Table 1: Abbreviations
@@ -28,21 +27,24 @@ This document describes the high level design details about how distributed data
 | LEC          | Local Equivalence Class     |
 | DPV          | Data plane verification     |
 
-# 1 Motivation
+# Overview
 
 Network errors such as forwarding loops, undesired blackholes and waypoint violations are the outcome of various
 issues (e.g., software bugs, faulty hardware, protocol misconfigurations, and oversight negligence). They can happen in
 all types of networks (e.g., enterprise networks, wide area networks and data center networks), and have both disastrous
 financial and social consequences. Data plane verification (DPV) is important for finding such network errors. 
 Current DPV tools employ a centralized architecture, where a server collects the data planes of all devices and verifies them. 
-Despite substantial efforts on accelerating DPV, this centralized architecture is inherently unscalable. 
+Despite substantial efforts on accelerating DPV, this centralized architecture is inherently unscalable because (1) it requires a highly available management network, which is hard build itself; and (2) the server becomes the performance bottleneck and a single point of failure. 
+
+In this HLD, to tackle the scalability challenge of DPV, we propose a distributed
+data plane verification framework, which circumvents the scalability bottleneck
+of centralized design and performs data plane checking on commodity network
+devices.  Our key insight is that DPV can be transformed into a counting problem
+on a directed acyclic graph, which can be naturally decomposed into lightweight
+tasks executed at network devices, enabling scalability.
 
-In order to tackle the scalability challenge of DPV, distributed data plane verification is designed, a generic, distributed,
-on-device DPV framework, which circumvents the scalability bottleneck of centralized design. The key insight is as follows. A
-directed acyclic graph (DAG), which represents all valid paths in
-the network, is called DVNet. The problem of DPV can be transformed into a counting problem in DVNet; the latter can then be decomposed into small tasks at nodes on the DVNet, which can be distributively executed at corresponding network devices, enabling scalability.
 
-The picture below demonstrates the architechture and workflow of distributed data plane verification.
+The picture below demonstrates the architecture and workflow of distributed data plane verification.
 ![architecture](img/architecture.png)
 
 Firstly, DVNet is generated based on specified verification requirement and actual network topology. Then, the counting problem is distributed to individual switches. On each switch, counting result is computed depending on received verification messages and delivered to corresponding upstream node on DVNet. Finally, the source switch would be able to determine whether there is an error on data plane according to received verification messages.
@@ -173,4 +175,4 @@ to allow distributed data plane verification planners on the device to verify th
 Ashish Bhargava, Paul-Andre C Bissonnette, Shane Foster, Andrew
 Helwer, Mark Kasten, Ivan Lee, et al. 2019. Validating Datacenters
 at Scale. In Proceedings of the ACM Special Interest Group on Data
-Communication. 200–213.
+Communication. 200–213.