forked from hopnets/valinor
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathindex.html
124 lines (111 loc) · 6.44 KB
/
index.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
---
layout: default
title: Valinor framework home
---
<h2>Motivation</h2>
<p>
♦ While existing network verification tools focus almost exclusively on different variants of reachability, can we verify <b>liveness properties</b> at scale? <br><br>
♦ Given a <b>combinational property</b>, i.e., a property that falls under both safety and liveness criteria, can we decompose it to <b>safety-only</b> and <b>liveness-only</b> properties? <br><br>
♦ Can we verify the <b>latency</b> of modern large-scale networks with <b>packet-level granularity</b>?
</p>
<p>
Below, we highlight the <a href="http://soudeh.net/#research">research</a> conducted by <a href="http://soudeh.net/#bio">our team</a> to answer these questions.
</p>
<hr/>
<h2>Scalable liveness verification</h2>
<p>
We argue that the goal of verifying liveness properties is achievable using a <b>top-down function-oriented strategy</b> that rethinks network abstractions with the efficiency of verification in mind.
<br><br>
Contributions:
<ul class="val-list-parent">
<li class="val-list"><b>Abstraction:</b> We provide network programmers with a simple, familiar abstraction of one big switch to express their intent. This abstraction enforces the logical separation of different network functions.</li>
<li class="val-list"><b>Packet-less model:</b> We model the program as a compact packet-less data structure that abstracts away the explicit notion of packets and focuses instead on the entities responsible for implementing functions (packet handling rules).</li>
<li class="val-list"><b>P4 compiler:</b> We provide a compiler that translates the programs written using our abstraction to P4 programs.</li>
</ul>
</p>
<h3>Our abstraction is expressive.</h3>
<p>
Our one big switch abstraction is designed to be capable of performing similar computations and is therefore
expressive enough to program a wide range of network functions. Table below lists the
functions of a few common control planes and recent network
abstractions that we re-wrote on top of our abstraction <br><br>
<img src="verified_list.png" class="design-figure" alt="Verified properties">
</p>
<h3>Our model is fast.</h3>
<p>
Below, Figure (a) and (b) show examples for a UDP flood mitigation function which deploys a per-source IP counter that is incremented for every UDP
packet and starts dropping packets when the counter exceeds a threshold. Figure (c) and (d) show examples for an “absence” property
(host A is never reachable) and “universality” (A is always reachable), respectively. The results demonstrate that packet-less verification
significantly reduces the verification time of different properties for a flood mitigation function.
<br><br>
<img src="liveness_result.png" class="design-figure" alt="Packet-less verification time">
</p>
<p>
More details can be found in our paper: <a href="https://www.usenix.org/conference/nsdi20/presentation/yousefi">Liveness Verification of Stateful Network Functions
</a>. <br><br>
</p>
<hr/>
<h2>Property decomposition</h2>
<hr/>
<h2>Packet-level latency verification</h2>
<p>
Albeit faster than their current simulation-based counterparts, the state-of-the-art verifiers today
have major limitations such as not modeling failures or latency that prevent
them from reliably verifying latency. We bridge this gap by proposing a scalable latency verification
method that refines advanced abstract network models to enable fast latency verification.
<br><br>
Contributions:
<ul class="val-list-parent">
<li class="val-list"><b>Temporal verification:</b> We decompose the latency verification task
into two phases: (i) functional verification, in which we
compute the probability of two nodes being reachable under various network states, and (ii) temporal verification, in
which we calculate the probability of reaching a node
from another one below the user-specified latency bound.</li>
<li class="val-list"><b>Optimization:</b> We propose novel caching mechanisms that speed up the verification process.</li>
<li class="val-list"><b>Implementation:</b> We implement our verifier, i.e., Tempus, in Julia and evaluate it under various scales of datacenter and wide area networks..</li>
</ul>
<br>
The architecture of Tempus:
<br><br>
<img src="tempus_arch.png" class="design-figure" alt="Tempus's architecture">
</p>
<h3>Tempus is fast.</h3>
<p>
We run Tempus on various scales of k-ary fat-tree topology with 100 Gbps links under 25%
load and compare the verification time with the time taken for simulating all failure scenarios using the state-of-the-art
network simulators. For this purpose, we use OMNeT++ (a non-parallel packet-level network simulator), Parsimon (a parallel flow-level simulator), and DONS
(a parallel packet-level simulator). We observe that tempus is orders of magnitude faster than all these simulators:<br><br>
<img src="tempus_fast.png" class="design-figure" alt="Tempus is fast">
''αy βmo γd δh ηmin κs’’ represents α years, β months, γ days, δ hours, η minutes, and κ seconds.
</p>
<h3>Tempus is accurate.</h3>
<p>
To evaluate the accuracy of Tempus, we simulate the
no-failure scenario and various degrees of load in a two-tier leaf-spine topology using
OMNeT++ and measure the tail (99th percentile) packet-level delay. We repeat the
simulations ten times to capture various randomnesses caused
by the simulator. For Tempus, we input the network topology
and the empirical queueing time measurements from our
simulations and record the tail latency estimated
by Tempus for the no-failure scenario. We observe that,
irrespective of the load, Tempus accurately captures the upper
limit for the tail delay:<br><br>
<img src="tempus_accurate.png" class="design-figure" alt="Tempus is accurate">
The box and whisker plots represent distinct tail latencies
recorded as we repeat the simulations multiple times.
</p>
<p>
More details can be found in our paper: <a href="">Tempus: Probabilistic Network Latency Verification</a>.
<br>
For the codebase, please refer to the <a href="https://github.com/hopnets/Tempus">Github page of Tempus</a>.
<br><br>
</p>
<div class="listing">
{% for post in paginator.posts %}
<div class="post other link">
<h2></span> <a href="{{site.url}}{{post.url}}">{{ post.title }}</a></h2>
<p class="post-date">{{ post.date | date_to_string }}</p>
{{ post.excerpt }}
</div>
{% endfor %}
</div>