-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathindex.html
127 lines (110 loc) · 3.96 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
125
126
127
<!DOCTYPE html>
<html>
<head>
<meta charset="UTF-8">
<title>Distributed Components</title>
<link rel='stylesheet' type='text/css' href='css/disco.css'>
</head>
<body>
<div id='header'>
<div class='floatL'>
<h1 id='header-title'>Distributed Components</h1>
</div>
<div class='floatR'>
<img id='header-logo' src='img/disco.png'>
</div>
<div class='clearB'></div>
</div>
<p>
Building reliable distributed systems is challenging for many reasons.
Such systems must tolerate faults gracefully: machines may crash, new
nodes may suddenly join or leave the system, and the network may drop,
reorder, or duplicate packets. Distributed systems are also highly
concurrent; engineers must ensure that for any schedule of events, the
system's key correctness guarantees are maintained and that the service
remains available. Furthermore, large-scale applications are often built by
composing services from multiple distributed systems, requiring
developers to reason about interactions between different systems.
</p><p>
To help address these challenges, the
<!-- -->
<a href='https://github.com/DistributedComponents'>Distributed Components</a>
<!-- -->
(or "DisCo" for short) project provides reusable infrastructure for
formally verifying distributed systems using the <a href=''>Coq</a> proof
assistant.
<h2>News</h2>
<p>
<span class='post-date'>Jan 2018</span> James Wilcox will give a talk on
Distributed Separation Logic (Disel) at POPL 2018.
</p><p>
<span class='post-date'>Jan 2017</span> Ryan Doenges will give a talk on
Verdi extensions to support churn at CoqPL 2017.
</p><p>
<span class='post-date'>Jan 2016</span> James Wilcox will give a talk on
our experiences verifying Raft in Verdi at CPP 2016.
</p><p>
<span class='post-date'>Jun 2015</span> Doug Woos will give a talk on
the design of the Verdi framework at PLDI 2015.
</p>
<h2>Publications</h2>
<p>
Ilya Sergey, James R. Wilcox, and Zachary Tatlock. <br>
<a href="files/disel.pdf">Programming and Proving with Distributed Protocols.</a> <br>
POPL 2018, Los Angeles, CA, January 2018. <br>
<a href="files/disel-slides.key">Slides (Keynote)</a>. <a href="files/disel-slides.pdf">Slides (PDF)</a>.
</p><p>
Doug Woos, James R. Wilcox, Steve Anton, Zachary Tatlock, Michael D. Ernst, and Thomas Anderson. <br>
<a href="https://verdi.uwplse.org/raft-proof.pdf">Planning for Change in a Formal Verification of the Raft Consensus Protocol.</a> <br>
CPP 2016, St. Petersburg, FL, January 2016.
</p><p>
James R. Wilcox, Doug Woos, Pavel Panchekha, Zachary Tatlock, Xi Wang, Michael D. Ernst, and Thomas Anderson. <br>
<a href="https://verdi.uwplse.org/verdi.pdf">Verdi: A Framework for Implementing and Verifying Distributed Systems.</a> <br>
PLDI 2015, Portland, OR, June 2015.
</p>
<!--
<h2>Posts</h2>
<p>
<span class='post-date'>TODO</span> Network Semantics for verifying
distributed systems.
</p><p>
<span class='post-date'>TODO</span> How to build a simple system in
Verdi.
</p>
-->
<h2>Projects</h2>
<p>
Currently, DisCo projects include:
</p><ul>
<li>Disel</li>
<li>Verdi</li>
<ul>
<li>LockServ</li>
<li>Raft</li>
<li>Aggregation</li>
<li>Chord</li>
<li>Runtime</li>
<li>Cheerios</li>
</ul>
<li>InfSeqExt</li>
</ul>
<h2>Contributors</h2>
<p>
DisCo is an international collaboration between researchers at the
Unviersity of Washington, University College London, and the University
of Illinois. Many volunteers have helped out on DisCo projects; we're
very grateful for their contributions! Folks currently working on DisCo
include:
</p><ul>
<li>Tom Anderson</li>
<li>Ryan Doenges</li>
<li>Michael Ernst</li>
<li>Karl Palmskog</li>
<li>Ilya Sergey</li>
<li>Keith Simmons</li>
<li>Zach Tatlock</li>
<li>James Wilcox</li>
<li>Doug Woos</li>
</ul>
</body>
</html>