summaryrefslogtreecommitdiff
path: root/web/noweb/examples/breakmodel.nw
blob: 284ad01719d35d3ebc1d7aad6fc958f9f4ac6d8f (plain)
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
% \global\def\begindocs#1{\relax}
% \global\let\enddocs=\relax

{\def\semifilbreak#1{\vskip0pt plus #1\penalty-200\vskip0pt plus -#1}
\def\single{\def\baselinestretch{1.0}\small\normalsize}

% l2h ignore semifilbreak {
% l2h ignore single 

% l2h substitution LA <
% l2h substitution RA >

\section{A Formal Model of Breakpoints}
\label{appendix:breakpoint-model}
This appendix provides a formal model of {\tt ldb}'s follow-set breakpoints.
The model takes the form of a PROMELA program~\cite{holzmann:design}. 
PROMELA programs define several threads of control that communicate by
passing messages.  
Each thread of control runs a program written in a guarded-command
language with a C-like syntax.
Programs may be nondeterministic.
PROMELA can simulate the execution of a program and
search its state space for states violating assertions embedded in the
program.
The simulator also searches for states with no successors, i.e.,
deadlocks.

The PROMELA code in this appendix models {\tt ldb}'s implementation of
breakpoints.
Although {\tt ldb} does not work with multithreaded programs, the
model uses multiple threads because a procedure call from {\tt ldb} to
a target process effectively creates a new thread.
The assertions embedded in the model specify that the debugger
takes a breakpoint action just before any thread's
successful execution of the instruction at the breakpoint.
Breakpoints may be implemented either in the operating system or in
the debugger itself; the choice does not affect the model used here.
The model assumes it can plant trap instructions in
the instruction stream of the target program, and that 
it will be notified when the target program encounters a trap.
The model also suits a machine with a ``trace mode''
 that causes a trap after the execution of every instruction.


The model has a single
breakpoint. 
To keep the state space small, the model has only two threads, so that
 a single bit can represent thread [[id]]s.\label{noweb-sample-page-number}
<<declarations>>=
#define NTHREADS 2
#define threadid bit
@ \noindent
The {\footnotesize\pageref{noweb-sample-page-number}} in
\LA{}declarations~\footnotesize\pageref{noweb-sample-page-number}\RA{}
is the page number on which the definition appears.

\section{Modeling the program counter and execution}
To keep things simple, I partition the possible values of the program
counter into three sets:
\begin{quote}
\begin{tabular}{ll}
  [[Break]]&the breakpoint itself,\\
  [[Follow]]&the instruction(s) following the breakpoint,\\
  [[Outside]]&outside the breakpoint.\\
\end{tabular}
\end{quote}
\semifilbreak{2\baselineskip}
\noindent The three sets are modeled by the following constants.
<<declarations>>=
#define NPCS 3
#define Break   0	/* pc at the breakpoint */
#define Follow  1	/* pc in breakpoint's follow set */
#define Outside 2	/* all other pc's */
@ 

The ability to plant traps is modeled by the array [[trapped]], which
records whether a trap instruction has been 
stored at a particular location:
<<declarations>>=
bool trapped[NPCS];
@

The model has five active components: two threads, a CPU that
executes one thread at a time, the breakpoint, and the rest of the debugger.
Here are the channels that are used for communication between the
threads, the CPU, the breakpoint, and the debugger.
Taking a breakpoint action is modeled by sending a message on the channel 
[[breakaction]].
<<declarations>>=
chan execute[NTHREADS] = [0] of {bit};	  /* try to execute instruction */
chan cont[NTHREADS]    = [0] of {bit};	  /* instruction executed */
chan trap              = [0] of {byte};	  /* CPU trapped on id! */
chan resume            = [0] of {bit};	  /* debugger resumed after trap */
chan breakaction       = [0] of {byte};	  /* deliver breakpoint to debugger */
@ \noindent [[[0]]] indicates that the channels are synchronous;
 senders block until a receiver is ready and vice~versa.{\hfuzz=0.9pt\par}

The communication structure is:
\begin{center}
\setlength{\unitlength}{0.01in}%
\footnotesize
\begin{picture}(580,180)( 50,-90)
\thicklines
\put(585,  0){\oval(90,60)}
\put(402,  0){\oval(90,62)}
\put(252,  0){\oval(90,60)}
\put( 95, 60){\oval(90,60)}
\put( 95,-60){\oval(90,60)}
\put(295, 10){\vector( 1, 0){ 60}}
\put(355,-10){\vector(-1, 0){ 60}}
\put(450,  0){\vector( 1, 0){ 90}}
\put(140, 55){\vector( 2,-1){ 70}}
\put(205, 10){\vector(-2, 1){ 70}}
\put(135,-45){\vector( 2, 1){ 70}}
\put(210,-20){\vector(-2,-1){ 70}}
\put(585,  0){\makebox(0,0){{\tt debugger()}}}
\put(402,  0){\makebox(0,0){{\tt breakpoint()}}}
\put(255,  0){\makebox(0,0){{\tt CPU()}}}
\put( 95,-65){\makebox(0,0)[b]{{\tt thread(1)}}}
\put( 95, 55){\makebox(0,0)[b]{{\tt thread(0)}}}
\put(165,-21){\makebox(0,0)[rb]{{\tt execute[1]}}}
\put(165, 16){\makebox(0,0)[rb]{{\tt cont[0]}}}
\put(170,-50){\makebox(0,0)[lb]{{\tt cont[1]}}}
\put(165, 50){\makebox(0,0)[lb]{{\tt execute[0]}}}
\put(330,-20){\makebox(0,0)[b]{{\tt resume}}}
\put(330, 15){\makebox(0,0)[b]{{\tt trap!id}}}
\put(493,  5){\makebox(0,0)[b]{{\tt breakaction!id}}}
\end{picture}
\end{center}
@

\noindent The CPU repeats the following steps.
\begin{enumerate}\single
\item
Wait for a thread to attempt to execute the instruction at [[pc]].
\item
If the instruction is a trap, notify the debugger.
When the debugger tells the CPU to resume, [[pc]] is unchanged.
\item
If the instruction is not a trap, advance [[pc]].
\item
Ask the thread to continue executing.
\end{enumerate} 
There is only one debugger, but there are multiple threads, and each
one has its own [[pc]] and its own communication with the CPU.
When the CPU notifies the debugger of a trap, it identifies the
trapping thread.
Other messages are used only for synchronization, so they send and
receive the nonsense variable [[x]].
<<declarations>>=
bit x;			/* junk variable for sending messages */
@
A [[proctype]] is a procedure that a thread can execute; this one
models the CPU.
 [[c?x]] receives the value [[x]] on channel [[c]]; [[c!x]] sends.
Arrows ([[->]]) separate guards from commands.
<<proctypes>>=
proctype CPU(byte count) {
  threadid id = 0;
  do
  :: execute[id]?x ->
       if
       ::  trapped[pc[id]] -> trap!id ; resume?x
       :: !trapped[pc[id]] -> <<advance [[pc[id]]]>>
       fi;
       cont[id]!x;
       <<possible context switch (change of [[id]])>>
  od
}
@ Context switching is discussed below.
@
\semifilbreak{1in} % page tuning
@ 
Since the program counter is an abstraction, advancing it does not
mean incrementing it.  A successful execution at [[Break]] is
guaranteed to be followed by an attempt to execute [[Follow]];
aside from that, any instruction can follow any other.
<<advance [[pc[id]]]>>=
if
:: pc[id] == Break -> pc[id] = Follow
:: pc[id] != Break -> /* any instruction can be next */
     if 
     :: pc[id] = Outside
     :: pc[id] = Break
     :: pc[id] = Follow
     fi
fi
@ \noindent
The second [[if]] statement has no guards, so an alternative is
chosen nondeterministically. 

All threads begin execution outside the breakpoint.
<<declarations>>=
byte pc[NTHREADS];
<<initialize data for thread [[id]]>>=
pc[id] = Outside;

@
\section{Counting events}
The correctness criterion for the breakpoint implementation is that
one breakpoint action must be taken for every
successful execution of an instruction at [[Break]].
[[threadcount[id]]] counts how many times thread~[[id]]
has executed the breakpoint, and [[actioncount[id]]] counts how many
breakpoint actions  have been taken on behalf of thread~[[id]]. 
<<declarations>>=
byte threadcount[NTHREADS];
byte actioncount[NTHREADS];
<<initialize data for thread [[id]]>>=
threadcount[id] = 0;
actioncount[id] = 0;
@
\semifilbreak{0.75in} % page tuning
@
Here is the model of a thread, including the assertion that the thread
and debugger counts are the same:
<<proctypes>>=
proctype thread(threadid id) {
  do
  :: if
     :: pc[id] == Break -> execute[id]!x; cont[id]?x;
          <<if successfully executed [[Break]], increment [[threadcount[id]]]>>
     :: pc[id] != Break -> execute[id]!x; cont[id]?x
     fi;
     assert(pc[id] != Outside || threadcount[id] == actioncount[id])
  od
}
@ 
The corresponding model of the debugger is
<<proctypes>>=
proctype debugger() {
  threadid id;
  do 
  :: atomic { breakaction?id -> <<increment [[actioncount[id]]]>> }
  od
}
@ \noindent
[[atomic]] groups statements into a single atomic action.
When the debugger takes a breakpoint action, it atomically increments 
[[actioncount[id]]].
Without [[atomic]], it might delay incrementing the counter and
invalidate the assertion above.

A thread knows it has successfully executed [[Break]] if the [[pc]]
has changed:
<<if successfully executed [[Break]], increment [[threadcount[id]]]>>=
if
:: pc[id] != Break -> <<increment [[threadcount[id]]]>>
:: pc[id] == Break -> skip
fi
@
 To keep the state space small, I restrict the values of the
counters to be in the range [[0..3]].
<<increment [[threadcount[id]]]>>=
threadcount[id] = (threadcount[id] + 1) % 4
<<increment [[actioncount[id]]]>>=
actioncount[id] = (actioncount[id] + 1) % 4
@
\section{Implementing the breakpoint}
There is a long tradition of implementing breakpoints using traps
and single stepping.  To set a breakpoint at $I$, plant a trap
at $I$.  When the target program hits the trap, that's a breakpoint
event.
To resume execution after the breakpoint, 
 restore the original instruction to $I$,
 single step the machine to execute just the instruction at $I$,
and once again plant a trap at $I$ and continue execution.
Not all machines have a single-step mode in hardware, but
single stepping can be simulated in software by using more trap
instructions. 
In my model, I eliminate single stepping entirely, working directly
with trap instructions and  a follow set
(modeled by [[Follow]]).

The simpler model does not preclude the use of hardware single stepping.
One of the operations in the model is planting traps at the locations
in the follow set of an instruction.
This operation can be implemented either by computing the follow set
and planting actual traps, or by setting a trace bit on a machine with
hardware single stepping.

\semifilbreak{3\baselineskip}

An active breakpoint is trapped either on the instruction of the
breakpoint itself or on that instruction's follow set.
The breakpoint keeps track of which state it is in, with the following 
invariant.
\begin{verbatim}
   breakstate == Break  && trapped[Break] = 1 && trapped[Follow] = 0
|| breakstate == Follow && trapped[Break] = 0 && trapped[Follow] = 1
\end{verbatim}
<<declarations>>=
byte breakstate = Break;
<<initialization>>=
trapped[Break] = 1;
@ Changing the state preserves the invariant.\label{move-traps-page}
<<move traps to [[Break]]>>=
atomic { breakstate = Break;  trapped[Break] = 1; trapped[Follow] = 0 }
<<move traps to [[Follow]]>>=
atomic { breakstate = Follow; trapped[Break] = 0; trapped[Follow] = 1 }
@

It's necessary to keep track of the state of each thread with respect
to the breakpoint.  A thread is ``in the breakpoint'' if it has
trapped at [[Break]], and it does not ``leave the breakpoint'' until
it traps at [[Follow]].  Threads are initially outside the breakpoint.
<<declarations>>=
bit  inbreak[NTHREADS];
<<initialize data for thread [[id]]>>=
inbreak[id] = 0;
@
\semifilbreak{2in} % page tuning
@
One possible implementation just keeps track of the various states and
delivers a breakpoint event at the right time:
<<candidate breakpoint implementation>>=
proctype breakpoint() {
  threadid id;

  do
  :: trap?id ->
       if
       :: breakstate == Break ->
            if 
            :: !inbreak[id] -> breakaction!id ; inbreak[id] = 1
            ::  inbreak[id] -> skip /* no event */
            fi;
            <<move traps to [[Follow]]>>
       :: breakstate == Follow ->
            if 
            ::  inbreak[id] -> inbreak[id] = 0
            :: !inbreak[id] -> skip
            fi;
            <<move traps to [[Break]]>>
       fi;  
       resume!x
  od
}
@ 
This implementation works fine for a single thread.
With two threads, the PROMELA state-space search finds the
following erroneous execution sequence
(attempted executions that trap are marked with a {*}):
\begin{quote}\single
\begin{tabular}{llcc}
breakpoint (debugger)& CPU       & thread 0     &   thread 1\\
&       &   [[Outside]]\\
&       &   [[Break]]\rlap{*}\\
%\multicolumn{3}{l}
{\LA{}take breakpoint action\RA{}}\\
{\LA{}move traps to [[Follow]]~\footnotesize\pageref{move-traps-page}\RA{}}\\
resume\\
&context switch\\
        &&&                  [[Outside]]\\
        &&&                  [[Break]]\\
        &&& [[Follow]]\rlap{*}\\
%\multicolumn{3}{l}
{\LA{}take no action\RA{}}\\
{\LA{}move traps to [[Break]]~\footnotesize\pageref{move-traps-page}\RA{}}\\
resume\\
           &&&              [[Outside]]\\
&context switch\\
         && [[Follow]]\\
         && [[Outside]]\\
\end{tabular} 
\end{quote} 
In this execution sequence, thread~1 goes through the breakpoint
without triggering a breakpoint action. 
In an earlier version of {\tt ldb}, this sequence could be provoked by
executing a procedure call after the user's program hit a breakpoint;
the user's program was thread~0, and the procedure call was thread~1.

%%%% \semifilbreak{3in} % page tuning
To prevent such an occurrence, the CPU must not be permitted to change
contexts when a thread is in the middle of a breakpoint.
If the CPU can change contexts only when [[noswitch == 0]], then the
following breakpoint implementation works correctly.
<<proctypes>>=
proctype breakpoint() {
  threadid id;

  do
  :: trap?id ->
       if
       :: breakstate == Break ->
            if 
            :: !inbreak[id] -> breakaction!id ; inbreak[id] = 1
            ::  inbreak[id] -> assert(0)
            fi;
	    noswitch = noswitch + 1;
            <<move traps to [[Follow]]>>
       :: breakstate == Follow ->
            if 
            ::  inbreak[id] -> inbreak[id] = 0
            :: !inbreak[id] -> assert(0)
            fi;
            noswitch = noswitch - 1;
            <<move traps to [[Break]]>>
       fi;  
       resume!x
  od
}
@ \noindent The ban on context switching makes it possible to strengthen
 [[skip]] to [[assert(0)]].

[[noswitch]] is declared to be a counter, not a bit, because that
implementation  generalizes to multiple breakpoints.
<<declarations>>=
byte noswitch = 0;
@
\semifilbreak{1.6in} % page tuning
@
The CPU code to do the context switching correctly is:
<<possible context switch (change of [[id]])>>=
if 
:: noswitch == 0 -> <<set [[id]] randomly>>
:: noswitch  > 0 -> skip
fi
<<set [[id]] randomly>>=
atomic {
  if
  :: id = 0
  :: id = 1
  fi
}
@
\section{Completing the model}
The boilerplate needed to turn the model into
a complete PROMELA specification is:
<<*>>=
<<declarations>>
<<proctypes>>
init {
  threadid id;
  atomic { 
    <<initialization>> 
    <<for $0 \le \tt id < NTHREADS$, initialize data for thread [[id]]>>;
    run thread(0);
    run thread(1);
    run debugger();
    run breakpoint();
    run CPU (2) 
  }
}
@ \semifilbreak{1in}
<<for $0 \le \tt id < NTHREADS$, initialize data for thread [[id]]>>=
id = 0;
do
:: id < NTHREADS -> <<initialize data for thread [[id]]>> 
   if 
   :: id == NTHREADS - 1  -> break
   :: id <  NTHREADS - 1  -> id = id + 1
   fi
od
@
}
@
\section{List of chunks}
\nowebchunks