diff options
Diffstat (limited to 'web/noweb/examples/breakmodel.nw')
-rw-r--r-- | web/noweb/examples/breakmodel.nw | 459 |
1 files changed, 459 insertions, 0 deletions
diff --git a/web/noweb/examples/breakmodel.nw b/web/noweb/examples/breakmodel.nw new file mode 100644 index 0000000000..284ad01719 --- /dev/null +++ b/web/noweb/examples/breakmodel.nw @@ -0,0 +1,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 |