-
Notifications
You must be signed in to change notification settings - Fork 0
/
index.html
324 lines (315 loc) · 13.2 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
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
<!DOCTYPE html>
<html lang="en">
<head>
<title></title>
<meta charset="UTF-8">
<meta name="viewport" content="width=device-width, initial-scale=1">
<script type="module" src="./src/deck.mjs"></script>
<style>
body { padding:0; margin:0;}
razzle-slide { opacity:0 }
</style>
</head>
<body>
<razzle-deck>
<razzle-slide>
<h1>TLA+</h1>
<blockquote>
<p> a high-level language for modeling programs and
systems—especially concurrent and distributed ones.</p>
<p>It's based on the idea that the best way to describe
things precisely is with simple mathematics. TLA+ and its
tools are useful for eliminating fundamental design errors,
which are hard to find and expensive to correct in code.</p>
</blockquote>
</razzle-slide>
<razzle-slide>
<h2>What is it?</h2>
</razzle-slide>
<razzle-slide>
<h2>Fundamental idea</h2>
<p> We can model specify <i>behaviors</i> of
systems, including computer processes, through descriptions of
<i>actions</i> that update <i>states</i>.</p>
</razzle-slide>
<razzle-slide>
Assume a fixed set of variables.
<dl>
<dt>States:</dt>
<dd>Assignments of values to variables</dd>
<dt>Behaviors:</dt>
<dd>Infinite discrete sequences of states, with a starting
point, like: s₁, s₂, s₃, …
</dd>
</dl>
Behaviors are naturally ordered by “tail of” relation, so
s₁, s₂, s₃, … is immediately followed by s₂, s₃, s₄ …
</razzle-slide>
<razzle-slide>
<dl>
<dt>Actions:</dt>
<dd>Boolean valued expression, expressing relation between the
values of variables in two states, intuitively the current and next state.
</dl>
</razzle-slide>
<razzle-slide>
<h4>Examples of actions:</h4>
<ul>
<li><code>x' = x + 1</code></li>
<li><code>x = x' + 1</code></li>
<li><code>x = y' ∧ y = x'</code></li>
</ul>
<p>NB: for some reason, “=” is a boolean operator and “≜” is
definitional equality. Assignment would correspond to an action.
</p>
</razzle-slide>
<razzle-slide>
<h4> The Temporal Logic of Actions</h3>
<p>TLA is a language that can be used to write statements that
could be true or false within (at the starting point of)
behaviors.
</p>
</razzle-slide>
<razzle-slide>
<p>Intuitively:</p>
<ol>
<li> “All (non-trivial) transitions conform to this action”:
</li>
<li> “This action could occur”</li>
<li> “If this action eventually always could occur, it eventually does”</li>
</ol>
</razzle-slide>
<razzle-slide>
<p>One nuance. TLA is designed to ensure that behaviors always are
allowed to “stutter”, i.e. fail to update anything. There seem to
be at least two reasons for this.
</p>
</razzle-slide>
<razzle-slide>
<p> Stuttering is supposed to be more realistic.
</p>
</razzle-slide>
<razzle-slide>
<p> If behaviors can stutter, then “implementation is implication”
</p>
<p> For example, a spec for a clock with an hour hand and
a minute hand will be implied by a spec for a clock with an
hour, minute, and second hand, in the sense that every behavior
satisfying the second spec satisfies the first.
</p>
<p> The idea is to ensure that you can leave out temporal detail
in higher-level specifications, and then add it in without
needing to backtrack.</p>
</razzle-slide>
<razzle-slide>
<p> Some formal results here, Lamport/Cohen reduction theorem. </p>
</razzle-slide>
<razzle-slide>
<pre>
Predicate ≜ Action with no primed variables
| ENABLED Action
Form ≜ Predicate | □[Action]ₜ | ¬Form
| Form ∧ Form | □Form
</pre>
<p>Where:</p>
<ul>
<li>□ means “always”, in every subsequent behavior</li>
<li><code>[Φ]ₜ</code> abbreviates <code>Φ ∨ t'=t</code></li>
</ul>
</razzle-slide>
<razzle-slide>
<p>TLA+ extends the above (simple TLA) by adding general
quantification, sets, and specific operators for use in
actions.
</p>
</razzle-slide>
<razzle-slide>
<h2>How do you use it?</h2>
</razzle-slide>
<razzle-slide>
<p>The main tool for using TLA+ is the <code>tlc</code> model checker.
<p>Given a sufficiently descriptive statement in TLA+,
<code>tlc</code> can attempt to generate a representation of
all possible behaviors that conform to that statement.</p>
<p> The representation (I think) is called a model</p>
</razzle-slide>
<razzle-slide>
<p>“Sufficiently descriptive” means basically that the
statement gives an initial assignment to each declared
variable, and gives an update relation that pins down how state
changes.
</p>
</razzle-slide>
<razzle-slide>
<h3>Example:</h3>
<pre>
Init ≜ V = 0 // Nat
∧ pc = "Plus" // program counter
Plus ≜ pc = "Plus" ∧ pc' = "Minus"
∧ V' = V + 1
Minus ≜ pc = "Minus" ∧ pc' = "Plus"
∧ V' = V - 1
Next ≜ Plus ∨ Minus
Spec ≜ Init ∧ □[Next]ₜ
</pre>
</razzle-slide>
<razzle-slide>
<img style="width:25em" src="./m1.svg"></img>
</razzle-slide>
<razzle-slide>
<p>
Models have a general graph structure; kind of like automata,
with behaviors corresponding to automata runs.
</p>
</razzle-slide>
<razzle-slide>
<code>tlc</code> can also do some extra checks on the model:
<ol>
<li> Invariants: make sure some predicate is true in every state</li>
<li> Liveness properties: statements that are true somewhere in any behavior.</li>
<li> More: e.g. “if φ is always true, then so is ψ.”</li>
</ol>
Basically check any TLA+ formula, abort if violation found.
</razzle-slide>
<razzle-slide>
<p>The TLA+ language is pretty simple.</p>
<p> But if you want to model algorithms, writing in pure TLA+
still introduces a layer of indirection.</p>
</razzle-slide>
<razzle-slide>
<p>One possible solution is to use a DSL for representing an
algorithm, and then automatically translate to TLA+.</p>
</razzle-slide>
<razzle-slide>
<h3>PlusCal:</h3>
<pre>
variable seq = <<1, 2, 3, 2>>;
index = 1;
seen = {};
is_unique = TRUE;
begin
TheMainLoop:
while index <= Len(seq) do
if seq[index] \notin seen then
seen := seen \union {seq[index]};
else
is_unique := FALSE;
end if;
index := index + 1;
end while;
end algorithm;
</pre>
</razzle-slide>
<razzle-slide>
<h3>PlusCal:</h3>
<pre>
variable seq = <<1, 2, 3, 2>>;
index = 1;
seen = {};
is_unique = TRUE;
begin
<span style="color:red">TheMainLoop:</span>
while index <= Len(seq) do
if seq[index] \notin seen then
seen := seen \union {seq[index]};
else
is_unique := FALSE;
end if;
index := index + 1;
end while;
end algorithm;
</pre>
</razzle-slide>
<razzle-slide>
<h2>Is it any good?</h2>
</razzle-slide>
<razzle-slide>
<h2>The Good:</h2>
<ol>
<li>Very expressive.</li>
<li>Learnable.</li>
<li>Some neat case studies of industrial applications: <a href="https://lamport.azurewebsites.net/tla/industrial-use.html">https://lamport.azurewebsites.net/tla/industrial-use.html</a>: Intel, Amazon, Microsoft, NASA, OpenComRTOS.</li>
<li>Use might be growing. In April 2023, AWS, Microsoft,
and Oracle became founding members of the TLA+
Foundation, launched by the Linux Foundation. The TLA+ Foundation
will “promote adoption, provide education and training
resources, fund research, develop tools, and build
a community of TLA+ practitioners.” Also functions as
a language committee</li>
</ol>
</razzle-slide>
<razzle-slide>
<h3>The Bad:</h3>
<ol>
<li>Only concrete models (symbolic model checker, apalache, seems immature). State explosion.</li>
<li><s>No spec ↔ implementation automation. A few academic
experiments (e.g. C2TLA+) translating PlusCal to and from
C.</s> Actually, there's PGo, which can translate PlusCal
to Go.
</li>
<li>No type system (by design), no pattern matching… Awkward recursion.</li>
</ol>
</razzle-slide>
<razzle-slide>
<h3>The Ugly:</h3>
<ol>
<li>TLA-toolbox (main TLA+ IDE) is not great.</li>
<li>Support for modern editors is limited. There's a VSCode
plugin, and syntax highlighting for other editors, but
that's about it.</li>
<li>TLAPs, proof system for TLA+, is not particularly well
documented (defunct "hyperbook", some video lectures).
I don't know if it's used.</li>
</ol>
</razzle-slide>
<razzle-slide>
<h2>What did <em>you</em> do with it?</h2>
</razzle-slide>
<razzle-slide>
<p>I tried out comparing two algorithms in TLA+.</p>
</razzle-slide>
<razzle-slide>
<p>Basic Method:</p>
<ol>
<li>Write both algorithms in pluscal</li>
<li>Translate to TLA+</li>
<li>Merge (by hand) the two resultant specifications, so
that the update relation updates state for both.</li>
</ol>
</razzle-slide>
<razzle-slide>
Problem: Stuttering.
</razzle-slide>
<razzle-slide>
<ol>
<li>Add some checkpoints, where one algorithm will pause and wait for the other to catch up</li>
<li>Write invariants that say certain parts of the state are the same, when the algorithms are in sync.</li>
</ol>
</razzle-slide>
<razzle-slide>
<p>Basically works, probably wasn't a great idea.</p>
<p>I think the main kind of algorithm comparison that TLA+ is
intended for is <i>refinement</i>.
</p>
</razzle-slide>
<razzle-slide>
<blockquote>
One develops a program through a series of refinements,
starting from a high-level algorithm and eventually reaching
a low-level program. Just as we went from Program 1 to the
finier-grained Program 2… the entire process from specification
to C code could in principle be carried out in TLA. “All” we
would need is a precise semantics of C, which would allow the
translation of any C program into a TLA formula.
</blockquote>
</razzle-slide>
<razzle-slide>
The ideal, I think, is refinement-driven-development, not
verification of existing software.
</razzle-slide>
</razzle-deck>
</body>
<script defer>
document.body.style.setProperty('--razzle-hide',1)
</script>
</html>