The PROMELA code in this appendix models ldb's implementation of breakpoints. Although ldb does not work with multithreaded programs, the model uses multiple threads because a procedure call from 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.[*]
<declarations>= (U->) [D->] #define NTHREADS 2 #define threadid bit
The [<-] in <declarations [<-]> is the page number on which the definition appears.
The three sets are modeled by the following constants.
Break
the breakpoint itself, Follow
the instruction(s) following the breakpoint, Outside
outside the breakpoint.
<declarations>+= (U->) [<-D->] #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>+= (U->) [<-D->] 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>+= (U->) [<-D->] 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 */
[0]
indicates that the channels are synchronous;
senders block until a receiver is ready and vice versa.
The communication structure is:
[picture]
* The CPU repeats the following steps.
pc
.
pc
is unchanged.
pc
.
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>+= (U->) [<-D->] 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>= (U->) [D->] proctype CPU(byte count) { threadid id = 0; do :: execute[id]?x -> if :: trapped[pc[id]] -> trap!id ; resume?x :: !trapped[pc[id]] -> <advancepc[id]
> fi; cont[id]!x; <possible context switch (change ofid
)> od }
Context switching is discussed below.
*
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]
>= (<-U)
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
The second if
statement has no guards, so an alternative is
chosen nondeterministically.
All threads begin execution outside the breakpoint.
<declarations>+= (U->) [<-D->] byte pc[NTHREADS];
<initialize data for thread id
>= (U->) [D->]
pc[id] = Outside;
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>+= (U->) [<-D->] byte threadcount[NTHREADS]; byte actioncount[NTHREADS];
<initialize data for thread id
>+= (U->) [<-D->]
threadcount[id] = 0;
actioncount[id] = 0;
* Here is the model of a thread, including the assertion that the thread and debugger counts are the same:
<proctypes>+= (U->) [<-D->] proctype thread(threadid id) { do :: if :: pc[id] == Break -> execute[id]!x; cont[id]?x; <if successfully executedBreak
, incrementthreadcount[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>+= (U->) [<-D->]
proctype debugger() {
threadid id;
do
:: atomic { breakaction?id -> <increment actioncount[id]
> }
od
}
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 executedBreak
, incrementthreadcount[id]
>= (<-U) if :: pc[id] != Break -> <incrementthreadcount[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]
>= (U->)
threadcount[id] = (threadcount[id] + 1) % 4
<increment actioncount[id]
>= (<-U)
actioncount[id] = (actioncount[id] + 1) % 4
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.
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.
breakstate == Break && trapped[Break] = 1 && trapped[Follow] = 0 || breakstate == Follow && trapped[Break] = 0 && trapped[Follow] = 1
<declarations>+= (U->) [<-D->] byte breakstate = Break;
<initialization>= (U->) trapped[Break] = 1;
Changing the state preserves the invariant.[*]
<move traps to Break
>= (U-> U->)
atomic { breakstate = Break; trapped[Break] = 1; trapped[Follow] = 0 }
<move traps to Follow
>= (U-> U->)
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>+= (U->) [<-D->] bit inbreak[NTHREADS];
<initialize data for thread id
>+= (U->) [<-D]
inbreak[id] = 0;
* 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 toFollow
> :: breakstate == Follow -> if :: inbreak[id] -> inbreak[id] = 0 :: !inbreak[id] -> skip fi; <move traps toBreak
> 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 *):
In this execution sequence, thread 1 goes through the breakpoint without triggering a breakpoint action. In an earlier version of 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.
breakpoint (debugger) CPU thread 0 thread 1 Outside
Break
*<take breakpoint action> <move traps to Follow
[<-]>resume context switch Outside
Break
Follow
*<take no action> <move traps to Break
[<-]>resume Outside
context switch Follow
Outside
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>+= (U->) [<-D] 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 toFollow
> :: breakstate == Follow -> if :: inbreak[id] -> inbreak[id] = 0 :: !inbreak[id] -> assert(0) fi; noswitch = noswitch - 1; <move traps toBreak
> fi; resume!x od }
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>+= (U->) [<-D] byte noswitch = 0;
* The CPU code to do the context switching correctly is:
<possible context switch (change ofid
)>= (<-U) if :: noswitch == 0 -> <setid
randomly> :: noswitch > 0 -> skip fi
<set id
randomly>= (<-U)
atomic {
if
:: id = 0
:: id = 1
fi
}
<*>=
<declarations>
<proctypes>
init {
threadid id;
atomic {
<initialization>
<for 0 <=id < NTHREADS, initialize data for thread id
>;
run thread(0);
run thread(1);
run debugger();
run breakpoint();
run CPU (2)
}
}
<for 0 <=id < NTHREADS, initialize data for threadid
>= (<-U) id = 0; do :: id < NTHREADS -> <initialize data for threadid
> if :: id == NTHREADS - 1 -> break :: id < NTHREADS - 1 -> id = id + 1 fi od
pc[id]
>: U1, D2
id
>: U1, D2
Break
, increment threadcount[id]
>: U1, D2
actioncount[id]
>: U1, D2
threadcount[id]
>: U1, D2
id
>: D1, D2, D3, U4
Break
>: D1, U2, U3
Follow
>: D1, U2, U3
id
)>: U1, D2
id
randomly>: U1, D2