A Formal Model of Breakpoints

[*] This appendix provides a formal model of 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 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 ids.[*]

<declarations>= (U->) [D->]
#define NTHREADS 2
#define threadid bit

The [<-] in <declarations [<-]> is the page number on which the definition appears.

Modeling the program counter and execution

To keep things simple, I partition the possible values of the program counter into three sets:
Breakthe breakpoint itself,
Followthe instruction(s) following the breakpoint,
Outsideoutside the breakpoint.
The three sets are modeled by the following constants.

<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.

  1. Wait for a thread to attempt to execute the instruction at pc.
  2. If the instruction is a trap, notify the debugger. When the debugger tells the CPU to resume, pc is unchanged.
  3. If the instruction is not a trap, advance pc.
  4. Ask the thread to continue executing.
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>+= (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]] -> <advance pc[id]>
       fi;
       cont[id]!x;
       <possible context switch (change of id)>
  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;

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>+= (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 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>+= (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 executed Break, increment threadcount[id]>= (<-U)
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]>= (U->)
threadcount[id] = (threadcount[id] + 1) % 4
<increment actioncount[id]>= (<-U)
actioncount[id] = (actioncount[id] + 1) % 4

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.

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 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 *):

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
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.

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 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
}

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 of id)>= (<-U)
if 
:: noswitch == 0 -> <set id randomly>
:: noswitch  > 0 -> skip
fi
<set id randomly>= (<-U)
atomic {
  if
  :: id = 0
  :: id = 1
  fi
}

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 <=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 thread id>= (<-U)
id = 0;
do
:: id < NTHREADS -> <initialize data for thread id> 
   if 
   :: id == NTHREADS - 1  -> break
   :: id <  NTHREADS - 1  -> id = id + 1
   fi
od

List of chunks