-
Notifications
You must be signed in to change notification settings - Fork 1
/
advancedee39.html
292 lines (207 loc) · 8.92 KB
/
advancedee39.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
<!DOCTYPE html>
<HTML>
<!-- Mirrored from lamport.azurewebsites.net/tla/advanced.html?unhideBut=hide-stuttering&unhideDiv=stuttering&back-link=practical-tla.html by HTTrack Website Copier/3.x [XR&CO'2014], Thu, 26 Mar 2020 22:42:03 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">
<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 = "Advanced Topics" ;
</SCRIPT>
<title>Advanced Topics</title>
</HEAD>
<BODY onload="initialize()">
<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>Advanced Topics</H1>
<p style="margin-top:-8px; margin-bottom:-18px">
Leslie Lamport<p>
<font size=-1><I> Last modified on 27 June 2019</I></font>
</td>
<!-- td style="vertical-alight:top;width:auto" -->
<!-- img src="tla-logo.png" style="width:170px;margin-top:14px"> </img -->
<!-- /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">
This page assumes you are familiar enough with TLA+ to be able to
understand a simple TLA+ spec (not just a PlusCal spec).
It contains links to documents explaining topics that go beyond what
most engineers need to know about TLA+.
These topics may be useful to engineers who want to push the boundary
of what they can do with TLA+, and they will be of interest to
those who want a deeper understanding of the principles underlying
TLA+.
</DIV>
<H2 id="h2stuttering" class="show-hide"
onclick="showHide('hide-stuttering','stuttering')">Stuttering Steps
<font id="hide-stuttering" >
[show]</font>
</H2>
<DIV id="stuttering" class = "hidden-div">
It seems obvious to me that in any sensible definition of
<i>implementation</i>, a clock that displays hours, minutes, and
seconds should implement the specification of a clock that displays
hours and minutes.
I realized in 1983 that the simplest way to ensure that this is true
is to require that all specifications allow <q>stuttering
steps</q>—steps in which the state of the system does not
change. Steps of an hour/minute/second clock in which only the
seconds change implement stuttering steps of the hour/minute clock's
specification. In the decades since then, I have continued to explain
this to people. To my knowledge, no state-based specification
formalism other than TLA has adopted the idea.
I suspect that even many TLA+ users think it's weird to require that
specifications allow stuttering steps. Here is a link to a short
note explaining why not requiring it is weird:
<A href =
"stuttering1505.html?back-link=advanced.html#stuttering?unhideBut@EQhide-stuttering@AMPunhideDiv@EQstuttering"
> [a link]</A>.
I don't understand why many people write such weird specs.
</DIV>
<H2 id="h2liveness" class="show-hide"
onclick="showHide('hide-liveness','liveness')">Safety, Liveness,
and Fairness
<font id="hide-liveness" >
[show]</font>
</H2>
<DIV id="liveness" class = "hidden-div">
The terms <i>safety</i>, <i>liveness</i>, and
<i>fairness</i> are used informally throughout the TLA+
documentation—including in the
<A href="http://lamport.azurewebsites.net/video/videos.html">
TLA+ Video Course</A>. They are defined precisely
<A href="safety-liveness.pdf">in this note</A>, which also describes
their significance. Although it requires little knowledge of TLA+,
you might find the note to be tough going if you're not used to
reading mathematics. But it's worth the effort if you want a more
complete understanding of TLA+.
</DIV>
<H2 id="h2proving-safety" class="show-hide"
onclick="showHide('hide-proving-safety','proving-safety')">Proving Safety Properties
<font id="hide-proving-safety" >
[show]</font>
</H2>
<DIV id="proving-safety" class = "hidden-div">
I have been writing correctness proofs of concurrent algorithms for
about 45 years.
I developed what I find to be a natural way of writing these proofs.
However, writing rigorous proofs has remained a black art that few
people have mastered.
Learning to write these proofs starts with learning to write proofs
of safety properties.
I believe that TLA+ and its tools can help you learn to write
these proofs.
The document <a href="proving-safety.pdf">Proving Safety Properties</a>
shows you how.
It explains the art of writing rigorous proofs, but not completely
formal machine-checked proofs.
Writing machine-checked proofs requires a lot of additional effort, as
well as practice using the TLAPS proof system.
</DIV>
<H2 id="h2hiding" class="show-hide"
onclick="showHide('hide-hiding','hiding')">Hiding,
Refinement, and Auxiliary Variables
<font id="hide-hiding" >
[show]</font>
</H2>
<DIV id="hiding" class = "hidden-div">
I started thinking about writing specifications around 1980. I
quickly realized that it was important to understand what it meant for
a program to satisfy a spec. I knew that, in principle, a spec
and an executable program are both specifications of a physical
system, written at two different levels of abstractions. So, I
needed to understand what it meant for one specification to implement
or refine another. This ultimately led me to TLA, the temporal
logic underlying the TLA+ language, and to using the temporal
existential quantification operator (written <code>\EE</code> in TLA+)
to write specifications. This operator served to distinguish
variables that represent externally observable parts of the system
from ones that represent unobservable parts that need not appear in an
implementation. Temporal existential quantification hid those
<q>unobservable</q> variabled.
<p>
With the development of the TLA+ tools and seeing how TLA+ is used in
practice, I came to realize that engineers and computer scientists
didn't need the <code>\EE</code> operator. So, I generally don't
talk about it; and I explain refinement without it. For example,
<code>\EE</code> is not mentioned in the
<a href="http://lamport.azurewebsites.net/video/videos.html">TLA+ Video
Course</a>.
<p>
While engineers don't need to use variable hiding and the
<code>\EE</code> operator, knowing why I used them to write specs
provides a deeper understanding of refinement and
auxiliary variables. So, I have explained this background in the note
<A href="hiding-and-refinement.pdf">Hiding, Refinement, and
Auxiliary Variables</A>.
You should read it before attempting to read the complete guide to
auxiliary variables in the paper
<a href="http://lamport.azurewebsites.net/pubs/pubs.html#auxiliary">Auxiliary
Variables in TLA+</a>.
</DIV>
<!--
<H2 id="h2xxxx" class="show-hide"
onclick="showHide('hide-xxxx','xxxx')">A Section
<font id="hide-xxxx" >
[show]</font>
</H2>
<DIV id="xxxx" class = "hidden-div">
</DIV>
-->
<!-- **************** ENDING BOILERPLATE *************** -->
</td>
</tr>
<!-- Bottom Back button -->
<tr>
<td>
<a class="back-link" style="display:none" href="#">
<p style="margin-top:-27px"><b>Back</b>
</p>
</a>
<!-- For a long page, add more back buttons higher on the page
by add one or more items like this, adjusting the margin-top
parameter as desired.
<a class="back-link" style="display:none" href="">
<p style="margin-top:-1100px"><b>Back</b> </p> </a>
-->
</td>
</tr>
</table>
</BODY>
<!-- Mirrored from lamport.azurewebsites.net/tla/advanced.html?unhideBut=hide-stuttering&unhideDiv=stuttering&back-link=practical-tla.html by HTTrack Website Copier/3.x [XR&CO'2014], Thu, 26 Mar 2020 22:42:03 GMT -->
</HTML>