-
Notifications
You must be signed in to change notification settings - Fork 1
/
high-level-view13c2.html
626 lines (480 loc) · 22.8 KB
/
high-level-view13c2.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
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
<!DOCTYPE html>
<HTML>
<!-- Mirrored from lamport.azurewebsites.net/tla/high-level-view.html?unhideBut=hide-pluscal&unhideDiv=pluscal&back-link=hyperbook.html by HTTrack Website Copier/3.x [XR&CO'2014], Thu, 26 Mar 2020 22:42:07 GMT -->
<HEAD>
<META HTTP-EQUIV="Content-Type" CONTENT="text/html; charset=iso-8859-1">
<META NAME="GENERATOR" CONTENT="Mozilla/4.05 [en] (X11; I; OSF1 V4.0 alpha)
[Netscape]">
<!--
%&b&<b>#</b>&
%&c& <b>#</b> &
-->
<!-- The following loads the style sheet for the html files of
the tla web site -->
<link rel="stylesheet" type="text/css" href="tlaweb.css">
<!-- style>
UL {margin-top:5px}
.smallpar {margin-top:7px}
DT {margin-top:10px}
</style -->
<script src="tlaweb.js"> </script>
<!-- The following causes the name of this page in the left-hand column
not to have a link -->
<SCRIPT>
noLinkName = "High-Level View" ;
</SCRIPT>
</HEAD>
<BODY onload="initialize()">
<title>A High-Level View of TLA+</title>
<table id="main">
<tr>
<td id="main_leftcolumn" >
</td>
<td id="main_contentcolumn">
<table>
<tr >
<td style="vertical-alight:top">
<div id = "showleftcol" > </div>
<H1>A High-Level View of TLA+</H1>
<p style="margin-top:-8px; margin-bottom:-18px">
Leslie Lamport<p>
<font size=-1><I> Last modified on 4 September 2018</I></font>
</td>
<td style="vertical-alight:top;width:auto">
</td>
</tr>
</table>
<HR style="margin-bottom:-5px;margin-top:-11px">
<P style="margin-top:0px"> </P>
<DIV class="hidden-div" style="color:red;margin-bottom:-22px"><b>
You'll miss a lot on this web site unless you enable Javascript
in your browser. </b></DIV>
<H2 id ="h2intro"
class="show-hide" onclick="showHide('hide-intro','intro')">Introduction
<font
id="hide-intro" >
[show]</font>
</H2>
<DIV id="intro" class="hidden-div"> <!-- style="display:none"-->
TLA+ is a language for modeling software above the code level and
hardware above the circuit level. It has an IDE (Integrated
Development Environment) for writing models and running tools to check
them. The tool most commonly used by engineers is the TLC model
checker, but there is also a proof checker. TLA+ is based on
mathematics and does not resemble any programming language.
Most engineers will find PlusCal, described below, to be the easiest way to
start using TLA+.
<p>
TLA+ models are usually called <em>specifications</em>. They are called
<font id = "model-popup"
class = "popup-blue"
color = "blue"
onclick = "popup('model-popup.html',175)">
<b>models</b></font>
in this introduction.
</DIV>
<H2 id="h2pluscal" class="show-hide" onclick="showHide('hide-pluscal','pluscal')"><a name="pluscal">PlusCal</a>
<font
id="hide-pluscal"> [show]</font>
</H2>
<DIV class = "hidden-div" id="pluscal"> <!-- style="display:block"-->
<!-- style="display:none"-->
PlusCal is a language for writing algorithms—especially
concurrent and distributed ones. It is meant to replace
pseudocode with precise, testable code. PlusCal looks like a
simple toy programming language, but with constructs for describing
concurrency and nondeterminacy. It is infinitely more expressive
than any programming language because any mathematical formula can be
used as a PlusCal expression.
A PlusCal algorithm is translated into a
TLA+ model that can be checked with the TLA+ tools.
Because it looks like a programming language, most engineers find PlusCal
easier to learn than TLA+. But because it looks like a
programming language, PlusCal cannot structure complex models as well as
TLA+ can.
<p>
<a href="petersona83c.html?back-link=high-level-view.html#pluscal?unhideBut@EQhide-pluscal@AMPunhideDiv@EQpluscal">Click here</a> for an example of
an algorithm written in PlusCal.
</DIV>
<H2 id="h2models" class="show-hide" onclick="showHide('hide-models','models')">Models
<font
id="hide-models" >
[show]</font>
</H2>
<DIV id="models" class="hidden-div"> <!-- style="display:none"-->
Computers and computer networks are physical objects whose behaviors
are described by continuous physical laws. They differ from most
other kinds of physical objects in that their behaviors are naturally
modeled as sets of discrete events. Programming, software
engineering, and most of computer science is concerned with models in
which a behavior of a system is described as a set of discrete events.
No model is a completely accurate description of a real system.
A model is a description of some aspect of the system, written for
some purpose.
<!--
We all use one or more ways of modeling the behavior of a computer
systems as a set of discrete events. Often, people think their
model is the actual system, not just a model of it. When
presented with a different model, they may think it's wrong or perhaps
just incomplete because it doesn't describe things that are in their
model. No model is a completely accurate description of a real
system. A model should be judged not by how accurate it is, but
by how useful it is; and that depends on what you're using it for.
-->
<p>
TLA+ is state-based, meaning that it models an execution of a system
as a sequence of states, where an event is represented by a pair of
consecutive states. We call a sequence of states a
<em>behavior</em>; and we call a pair of consecutive states a
<em>step</em> rather than an event.
A system is modeled as the set of behaviors describing all of its
possible executions.
</DIV>
<h2 id="h2above" class="show-hide" onclick="showHide('hide-above-code','above-code')">
Modeling Above the Code Level
<font
id="hide-above-code" >
[show]</font>
</H2>
<DIV id="above-code" class="hidden-div"> <!-- style="display:bloxk"-->
TLA+ is used to model systems above the code level.
To see what this, means consider Euclid's algorithm for computing
<nobr> <code>GCD(M,N)</code> ,</nobr> the greatest
common divisor of two positive integers  <code>M</code> 
and  <code>N</code> . Here is the algorithm:
<UL>
<LI>
Let  <code>x</code>  equal
 <code>M</code>  and  <code>y</code> 
equal  <code>N</code> .
</LI>
<LI style="margin-top:7px">
Repeated subtract the smaller of  <code>x</code>  and
 <code>y</code>  from the larger.
</LI>
<LI style="margin-top:7px">
Stop when  <code>x</code>  and
 <code>y</code>  have the same value. That value is the
GCD of  <code>M</code>  and
 <code>N</code> .
</LI>
</UL>
This description is above the code level.
Code to compute <nobr> <code>GCD(M,N)</code> </nobr>
would have to specify additional details such as the type of
 <code>M</code>  and  <code>N</code>  (is
it  <code>int</code>?
 <code>long</code>?
 <code>BigInteger</code>?) and what to do if
 <code>M</code>  or  <code>N</code>  is
not positive (throw an exception? return an error value?). <p>
A programmer who didn't know Euclid's algorithm might decide to compute
<nobr> <code>GCD(M,N)</code> </nobr>
by a naive algorithm that sets  <code>x</code>  to the
minimum of  <code>M</code>  and
 <code>N</code>  and keeps decreasing
 <code>x</code>  until it divides both
 <code>M</code>  and
 <code>N</code> . The best coder in the world will
not produce a good GCD program by coding the naive algorithm.
Moreover, thinking in terms of code makes it harder for a programmer
to find a better algorithm. Finding a good algorithm requires
thinking above the code level.
<p>
No one writes a piece of code without first having a high-level model
of what the code should do and how it should do it. A programmer
never starts by deciding to declare some variables, adding a
 <b>while</b>  statement, then adding an
 <b>if</b>  statement, and so on—only discovering
when finished that she's written a sorting program. But
programmers rarely start with a <em>precise</em> model of the code.
Having only a vague, incomplete model leads to basic design errors
that the best coding won't correct. <p>
<p>
TLA+ is a language for writing precise high-level models of what
code does and how it does it.
<!--
It looks nothing like a programming language because programming
languages are designed for writing code, not for thinking above the
code level. Instead, TLA+ is based on mathematics, the universal
language of science and engineering.
-->
Most programmers believe that precise models are good only for
tiny well-defined problems like computing the GCD, but are useless for
implementing complex systems. They're wrong. The more
complex a system is, the more important it is to make it as simple as
possible. In complex systems, simplicity isn't achieved by coding
tricks. It's achieved by rigorous thinking above the code level.
<p>
In
<a href="industrial-use2903.html?unhideBut=hide-rtos&unhideDiv=rtos&back-link=high-level-view.html#language?unhideBut@EQhide-above-code@AMPunhideDiv@EQabove-code">
one industrial project</a>,
starting with a TLA+ model reduced the size of a real-time
operating system's code by a factor of ten.
Such a reduction in
code size isn't obtained by better coding; it comes from thinking
rigorously above the code level.
<p>
Writing a model above the code level doesn't prevent coding
errors. Many methods and tools have been developed for finding
coding errors, and they should be used. But they are not good
for finding errors in the high-level model from which the code is
derived. And it's impossible to test that a high-level model is
implemented correctly if the model is just a vague idea in the
programmer's mind, with no precise description.
<p>
Testing the code is not an effective way to find fundamental design
errors—especially in concurrent and distributed systems.
Moreover, a design error found after the code has been written is
usually fixed with an <em>ad hoc</em> patch that is unlikely to
eliminate all instances of the problem and is likely to introduce new
errors. Design errors should be caught by writing a precise
high-level model, before the code is written.
</DIV>
<h2 id="h2concurrent" class="show-hide"
onclick="showHide('hide-concurrent','concurrent')">
Modeling Concurrent Systems
<font
id="hide-concurrent" >
[show]</font>
</h2>
<DIV id="concurrent" class="hidden-div">
A concurrent system is one that we think of as composed of multiple
concurrently operating components called
<font id = "process-popup"
class = "popup-blue"
class="show-hide" onclick = "popup('process-popup.html',220)">
<b><font color="blue">processes</font></b>
</font>.
<!--
(Contrary to popular belief, being composed of multiple processes is
not an inherent property of a system, but rather a result of how we
view it.)
-->
A distributed system is a concurrent system in which we
think of the processes as being spatially separated, usually communicating
with one other by sending messages.
<p>
In a state-based model, a state represents the entire physical state
of a system. Some people find it hard to believe that one can or
should model a distributed system in terms of a single global
state. Over 40 years of experience has taught me that this is
the most generally useful way to model distributed algorithms and
systems.
</DIV>
<h2 id="h2machines" class="show-hide"
onclick="showHide('hide-state-machines','state-machines')">State Machines
<font
id="hide-state-machines" >
[show]</font>
</H2>
<DIV id="state-machines" class="hidden-div"> <!-- style="display:none"-->
Like many state-based methods, TLA+ describes a set of
behaviors with two things:
<ol > <li> An <em>initial condition</em> that specifies the
possible starting states.</li>
<li style="margin-top:7px">A <em>next-state relation</em> that
specifies the possible steps (pairs of successive states). </li>
</ol>
They specify the set of behaviors whose first state satisfies the
initial condition and whose every step
satisfies the next-state relation.
<p>
This kind of model is often called a <em>state machine</em>. (A
finite-state machine is a state machine with a finite set of possible
states. Finite-state machines are not nearly as useful as
general state machines.) A Turing machine is an example of a
state machine. In a deterministic Turing machine, the next-state
relation allows at most one next state for any state, and it allows no
next state for a terminating state.
<p>
The simplest and most practical method of precisely describing the
semantics of a programming language, called operational semantics,
essentially consists of showing how to <q>compile</q> a program in the
language to a state machine. Given an operational semantics, any
program in the language can be viewed as a state machine. I
suspect that most programmers intuitively think of a program in that
way.
<p> The next-state action specifies what steps <em>may</em> happen; it
doesn't specify what steps, if any, <em>must</em> happen. That
requires an additional condition, called a <em>fairness</em>
property. A state machine that models a sequential program
usually includes the fairness property that some step must be taken
(the behavior must not stop) if the next-state relation allows a step
to be taken. Models of concurrent and distributed programs often
have more complicated fairness properties.
<!--
Most people find it natural to consider an initial condition and
next-state relation to describe only behaviors that cannot end in a
state in which there exists a possible next state. This is fine
for modeling sequential systems, but not concurrent ones. For
example, it's not a natural way of modeling a client-server system in
which clients can stop sending requests. TLA+ considers the
next-state relation to describe what steps are allowed to happen, but
to say nothing about what steps must happen. For example, it
never rules out a behavior that stops in its initial state. What
steps must happen are described by an additional
condition—usually what is called a <em>fairness</em>
condition. That a behavior doesn't stop in a state from which
the next-state relation allows a step is a fairness condition.
-->
<p>
A state-machine model without a fairness condition can be used to
catch errors of <q>commision</q>, in which the system does something
wrong. It can't be used to catch errors of <q>omission</q>, in
which the system fails to do something. In practice, errors of
commission are more numerous and harder to find than errors of
omission. Often, engineers don't bother adding fairness
conditions. Therefore, you should first learn to write the
initial condition and next-state relation in your TLA+ models.
Later, you can learn to write fairness conditions.
</DIV>
<h2 id="h2checking"
class="show-hide"
onclick="showHide('hide-checking','checking')"><a
name="checking">Checking Properties</a>
<font
id="hide-checking" >
[show]</font>
</H2>
<DIV id="checking" class="hidden-div"> <!-- style="display:none"-->
One reason for modeling a system is to check if it does what we want
it to. We do that by checking if the model satisfies properties
that we believe assert that the system does what it should. TLA+
can assert, and its tools can check, only that some property of an
individual behavior is true of every possible behavior of the
model. Thus, TLA+ cannot assert that 99% of all possible
behaviors terminate in a correct state. However, it can assert
(and its tools can check) that every possible behavior terminates in a
correct state if its initial state belongs to a particular set
containing 99% of all possible initial states.
<p>
The most useful type of property to check is an invariance property,
which asserts that something is true of every state of every possible
behavior. Often, an engineer will check only invariance
properties of a model.
<p>
For a model containing a fairness condition, you should also check
simple properties asserting that something eventually happens—for
example, that every execution eventually halts. Those properties,
called <em>liveness properties</em>, are easily expressed in TLA+.
<p>
The rich variety of properties that we want to check for concurrent
systems can't all be expressed as invariance and simple liveness
properties. They can be expressed as state machines (possibly with
fairness conditions).
A state machine can be viewed as the property that is satisfied by the
possible behaviors of the state machine. We can check whether
another state machine satisfies this property. If it does, we
say that the other state machine <em>implements</em> the state
machine.
<p>
In TLA+ there is no formal distinction between a state machine and a
property. Both are described by mathematical formulas.
A state machine is a formula having a particular <q>shape</q>,
different from the shape of an invariance or liveness property.
Both <em>satisfying a property</em> and <em>implementing a state
machine</em> mean that one formula implies another.
<p>
Today, most engineers check only invariance properties and simple
liveness properties.
However, even if you never do it, knowing how it is done explains
what it means for a program to implement a model, which can help you
avoid making errors in your code.
</DIV>
<H2 id="h2language" class="show-hide"
onclick="showHide('hide-language','language')">
<a name="language">The TLA+ Language</a>
<font
id="hide-language" >
[show]</font>
</H2>
<DIV id="language" class="hidden-div"> <!-- style="display:none"-->
TLA+ is based on mathematics and does not resemble a programming
language. Most engineers are familiar with programming
languages, but not with precise mathematical notation. We
naturally find what we're familiar with to be simpler than anything
else. It's hard for me to believe that English is not inherently
simpler than German. Upon first seeing a TLA+ model, some
engineers find TLA+ intimidating. Read the
<a href="industrial-usea83c.html?back-link=high-level-view.html#language?unhideBut@EQhide-language@AMPunhideDiv@EQlanguage">
Industrial Use of TLA+</a>
page to see that TLA+ is not very hard to learn.
<p>
Using TLA+ teaches you that math is inherently more expressive than
programming languages because it can describe a value without having
to describe how the value is computed. For example, it can
describe the greatest common divisor (GCD) of two numbers as the
largest positive integer that divides both numbers. This makes
it possible to write a model for a specific purpose, abstracting away
irrelevant details such as how to calculate the GCD. (Putting
code in a procedure doesn't abstract it away; it just makes you
go elsewhere to read the code, requiring that you understand the
semantics of procedure call as well as the code.)
<p>
Starting with PlusCal provides a gentle entry to TLA+. Even if you
know TLA+, it's easier to write some models in PlusCal rather
than directly in TLA+. But to get the full benefit of thinking
mathematically above the code level, you should learn TLA+.
</DIV>
</td>
</tr>
<!-- Bottom Back button -->
<tr>
<td>
<a class="back-link" style="display:none" href="#">
<p style="margin-top:-50px"><b>Back</b>
</p>
</a>
</td>
</tr>
</table>
</BODY>
<!-- Mirrored from lamport.azurewebsites.net/tla/high-level-view.html?unhideBut=hide-pluscal&unhideDiv=pluscal&back-link=hyperbook.html by HTTrack Website Copier/3.x [XR&CO'2014], Thu, 26 Mar 2020 22:42:07 GMT -->
</HTML>
<!--
<p>
Since the work of Floyd and Hoare in the late 1960s, it has been
generally agreed that the behavior of a sequential programs is best
thought of as a sequence of states, and we should think of a step of a
program as a state-changing event. I have found this to be true of
concurrent and distributed systems as well. States are important
because what a system does in the future is controlled by its current
state, not by what happened in the past.
<p>
<hr>
Some methods, including TLA+, have a way of hiding part of the state.
They can describe a system as behaving <em>as if</em> that hidden
state exists, but it needn't actually exist. There is little
practical benefit in doing this. Understanding the system requires
understanding the complete state, including its hidden part. In
practice, it suffices to simply say in a comment that a certain part
of the state need not actually be implemented.
-->
<!--
Some other methods model a behavior as a sequence of actions.
The ones that are comparable to TLA+ in terms of their utility employ
a sequence of states to control the order in which actions can occur,
the current state determining which actions are possible and the
action determining the next state. Adding named actions to the
state changes would add nothing to the usefulness of TLA+. <p>
-->
<!--
Rarely can we say that one model is better than
another. We can at most say that one is more useful than another
for a certain purpose.
-->
<!--
I've found that for most engineering uses, the behavior of a system
can be modeled as a sequence of events. If two events represent
concurrent operations in different processes, the model will allow
behaviors in which the events occur in either order.
-->