next up previous contents
Next: C. TRUMP Protocol Headers Up: Warrens Ph.D Thesis Previous: A. Glossary   Contents

Subsections


B. Verifying TRUMP with Spin

The TRUMP transport protocol was designed primarily as a rate-based protocol which would fit into the rate-based congestion control framework described in this thesis. Other functionality apart from a rate-based flow control are secondary to the thesis. However, in the author's opinion, it is still essential that TRUMP be proved to be a correct and logically consistent protocol.

This appendix describes the validation of the TRUMP transport protocol using the Spin protocol verifier [Holzmann 91] [Holzmann 97] and its associated verification language, Promela. The Spin verifier is introduced, followed the Promela language and the verification capabilities of Spin. The implementation of TRUMP in Promela is then described, and the verification of this implementation using Spin is finally considered.

1 Introduction to Spin

The abstract from the `Basic Spin Manual', part of the Spin software distribution, gives this description of Spin:

Spin is a tool for analyzing the logical consistency of concurrent systems, specifically of data communication protocols. The system is described in a modeling language called Promela. The language allows for the dynamic creation of concurrent processes. Communication via message channels can be defined to be synchronous (i.e., rendezvous), or asynchronous (i.e., buffered).

Given a model system specified in Promela, Spin can either perform random simulations of the system's execution or it can generate a C program that performs an efficient online verification of the system's correctness properties. During simulation and verification Spin checks for the absence of deadlocks, unspecified receptions, and unexecutable code. The verifier can also be used to verify the correctness of system invariants, it can find non-progress execution cycles, and it can verify correctness properties expressed in next-time free linear temporal logic formulae.

The verifier is setup to be efficient and to use a minimal amount of memory. An exhaustive verification performed by Spin can establish with mathematical certainty whether or not a given behavior is error-free. Very large verification problems, that can ordinarily not be solved within the constraints of a given computer system, can be attacked with a frugal ``bit state storage'' technique, also known as supertrace. With this method the state space can be collapsed to a small number of bits per reachable system state, with minimal side-effects.

2 The Promela Language

In order to be able to read and understand the implementation of TRUMP in the Promela language, given later in this appendix, an brief introduction to the language must first be given. The following is abstracted from the `Basic Spin Manual', with additional text relating the discussion to the TRUMP code.


Promela is a verification modeling language. It provides a vehicle for making abstractions of protocols (or distributed systems in general) that suppress details that are unrelated to process interaction. The intended use of Spin is to verify fractions of process behavior, that for one reason or another are considered suspect. The relevant behavior is modeled in Promela and verified. A complete verification is therefore typically performed in a series of steps, with the construction of increasingly detailed Promela models. Each model can be verified with Spin under different types of assumptions about the environment (e.g., message loss, message duplications etc). Once the correctness of a model has been established with Spin, that fact can be used in the construction and verification of all subsequent models.

Promela programs consist of processes, message channels, and variables. Processes are global objects. Message channels and variables can be declared either globally or locally within a process. Processes specify behavior, channels and global variables define the environment in which the processes run.

1 Executability

In Promela, there is no difference between conditions and statements: even isolated boolean conditions can be used as statements. The execution of every statement is conditional on its executability. Statements are either executable or blocked. The executability is the basic means of synchronization. A process can wait for an event to happen by waiting for a statement to become executable. A condition can only be executed (passed) when it holds. If the condition does not hold, execution blocks until it does.

2 Data Types

The primitive data types in Promela are bool, byte, short, int and mtype. A bool is a single bit of information. A byte is an unsigned quantity that can store a value between 0 and 255. shorts and ints are signed quantities that differ only in the range of values they can hold (typically 16-bits and 32-bits in size, respectively).

An mtype variable can be assigned symbolic values that are declared in an mtype={...} statement. This is the preferred way of specifying message types since it abstracts from the specific values to be used, and it makes the names of the constants available to an implementation, which can improve error reporting.

Variables can be also declared as arrays, using a C style syntax. An array of size N has elements numbered 0 to N-1. Element references outside of this range cause run-time errors in Spin. C style structures can be created with the typedef operator: the TRUMP implementation uses a structure for the messages passed between the Sender and Receiver process. Fields within structures are accessed using the usual C style syntax.

3 Processes

The state of a variable or of a message channel can only be changed or inspected by a process. The behavior of a process is defined in a proctype declaration. The declaration body (enclosed in curly braces) consists of a list of zero or more declarations of local variables and/or statements. Promela accepts two different statement separators: an arrow `->'and the semicolon `;'. The two statement separators are equivalent. The arrow is used as an informal way to indicate a causal relation between two statements.

A proctype definition only declares process behavior, it does not execute it. When simulated with Spin, the init process is always instantiated. Statements in init can be used to instantiate other processes. In the TRUMP implementation, the Sender, Receiver and two link processes are instantiated via init.

4 Atomic Sequences

Unless blocked on a condition which is not yet true, a process can execute its statements. During verification, Spin will simulate all possible interleaving of the statements from the running processes. By prefixing a sequence of statements enclosed in curly braces with the keyword d_step, the user can indicate that the sequence is to be executed as one indivisible unit, non-interleaved with any other processes. It causes a run-time error if any statement in the sequence can block. d_step sequences in the TRUMP implementation are used to atomicise the complex manipulation of local variables.

5 Message Channels

Message channels are used to model the transfer of data from one process to another. They are declared either locally or globally, for instance as follows:

     chan hold = [4] of { trumphdr };

This declares a channel that can store up to 4 messages of type trumphdr (a structure). Channel names can be passed from one process to another via parameters in process instantiations.

The statement hold!expr sends the value of variable expr to the channel just created: that is, it appends the value to the tail of the channel. hold?msg receives the message: it retrieves it from the head of the channel, and stores it in a variable msg. The channels pass messages in first-in-first-out order.

The send operation is executable only when the channel addressed is not full. The receive operation, similarly, is only executable when the channel is non empty. Nothing bad will happen if a statement happens to be non-executable. The process trying to execute it will be delayed until the statement, or, more likely, an alternative statement, becomes executable.

Several additional functions on channels are predefined, which allow a process to inspect the size of a channel's queue without blocking: len(q), empty(q), nempty(q), full(q) and nfull(q), where q is the name of the channel. The latter four functions return true if the channel is empty, not empty, full, or not full, respectively.

6 Control Flow

Between the lines, we have already introduced three ways of defining control flow: concatenation of statements within a process, parallel execution of processes, and atomic sequences. There are three other control flow constructs in Promela to be discussed. They are case selection, repetition, and unconditional jumps.


The simplest construct is the selection structure. Using the relative values of two variables a and b to choose between two options, for instance, we can write:

    if
    :: (a != b) -> option1;
    :: (a == b) -> option2;
    fi;

The selection structure contains two execution sequences, each preceded by a double colon. Only one sequence from the list will be executed. A sequence can be selected only if its first statement is executable. The first statement is therefore called a guard.

In the above example the guards are mutually exclusive, but they need not be. If more than one guard is executable, one of the corresponding sequences is selected nondeterministically. If all guards are unexecutable the process will block until at least one of them can be selected. There is no restriction on the type of statements that can be used as a guard.


A logical extension of the selection structure is the repetition structure. As above, only one option can be selected for execution at a time. After the option completes, the execution of the structure is repeated.

    do
    :: (a != b) -> option1;
    :: (a == b) -> option2;
    od;

The normal way to terminate the repetition structure is with a break statement placed in one of the options. Note that to ensure the repetition is terminated, the guards on all the other options must be false, and hence not executable. Another way to break the repetition is with an unconditional jump: the infamous goto statement. The goto label statement is always executable, and takes execution to the named label elsewhere in the process.

One Promela statement commonly used with selection and repetition is the skip statement which is always executable and performs no action. A typical selection statement with no `else' clause can be written as

    if
    :: (a == b) -> option2;
    :: (a != b) -> skip;
    fi;

Without the skip option, the selection would block the process until the guard (a == b) was indeed true. Promela also provides an else guard, which is only true if all other guard statements are false.

7 Promela Verification Support

An important language construct in Promela that needs little explanation is the assert statement. Statements of the form assert(any_boolean_condition) are always executable. If the boolean condition specified holds, the statement has no effect. If, however, the condition does not necessarily hold, the statement will produce an error report during verifications with Spin.


When Promela is used as a verification language the user must be able to make very specific assertions about the behavior that is being modeled. In particular, if a Promela is checked for the presence of deadlocks, the verifier must be able to distinguish a normal end state from an abnormal one.

A normal end state could be a state in which every Promela process that was instantiated has properly reached the end of the defining program body, and all message channels are empty. But, not all Promela process are, of course, meant to reach the end of their program body. Some may very well linger in an idle state, or they may sit patiently in a loop ready to spring into action when new input arrives.

To make it clear to the verifier that these alternate end states are legal, and do not constitute a deadlock, a Promela model can use end state labels. There may be more than one end state label per verification model. If so, all labels that occur within the same process body must be unique. The rule is that every label name that starts with the three character sequence ``end'' is an endstate label.


In the same spirit as the end state labels, the user can also define progress state labels. In this case, a progress state label will mark a state that must be executed for the protocol to make progress. Any infinite cycle in the protocol execution that does not pass through at least one of these progress states is a potential starvation loop. Again, all progress labels that occur within the same process body must be unique. The rule is that every label name that starts with the character sequence ``progress'' is an progress state label.

3 Spin Verification Capabilities

The verification capabilities of Spin are described in detail in  [Holzmann 91] and in the `Basic Spin Manual'. Again, the following brief description is abstracted from the latter.

Given a model system specified in Promela, Spin can either perform random simulations of the system's execution or it can generate a C program that performs a fast exhaustive verification of the system state space. The verifier can check, for instance, if user specified system invariants may be violated during a protocol's execution.

If invoked as

    $ spin -a protocol.spin
Spin generates a protocol analyzer for the protocol described in the Promela language in the protocol.spin file. The output analyser is written into a set of C files that can be compiled to produce the analyzer (which is then executed to perform the analysis). To guarantee an exhaustive exploration of the state space, the program is compiled simply as

    $ cc -o run pan.c

The executable program run can now be executed to perform the verification. The verification is truly exhaustive: it tests all possible event sequences in all possible orders. Exhaustive search works up to system state spaces of roughly 100,000 states. For larger systems this may, however, exhaust the available memory on the machine used.

The coverage of a conventional analysis goes down rapidly when the memory limit is hit, i.e. if there are twice as many states in the full state space than we can store, the effective coverage of the search is only 50% and so on. Spin does substantially better in those cases by using the bit state space storage method [Holzmann 90]. Large to very large systems can still be analyzed by using a memory efficient bit state space method by compiling the analyser as

    $ cc -o run -DBITSTATE pan.c

An indication of the coverage of such a search can be derived from the hash factor given in the analyser's output. The hash factor is roughly equal to the maximum number of states divided by the actual number of states. A large hash factor (larger than 100) means, with high reliability, a coverage of 99% or 100%. As the hash factor approaches 1, the coverage approaches 0%.

Note carefully that the analyzer realizes a partial coverage only in cases where traditional verifiers are either unable to perform a search, or realize a far smaller coverage. In no case will Spin produce an answer that is less reliable than that produced by other automated verification systems (quite on the contrary).


4 Implementing TRUMP in Promela

TRUMP is implemented in Promela as several intercommunicating processes. The Sender process attempts to deliver data packets successfully to the Receiver, following the protocol rules for connection setup, data transmission and connection teardown. The Receiver process receives data packets from the Sender, and returns acknowledgment packets. The Sender and Receiver are connected via two unidirectional links, whose operations are performed by two instantiations of the Badlinksrc process.

As the goal here is to verify the corrctness of the TRUMP protocol, features of TRUMP which do not affect its protocol operation are not implemented. This includes the protocol's rate-based flow control, the security features of TRUMP, and the use of connection identifiers. These features have no impact on the logical correctness and consistency of the protocol.

Protocol features of TRUMP which have not been implemented are the qualities of service and packet fragmentation/reassembly. The reason for these omissions is the limit on the time available to complete this thesis. However, despite this, the majority of the TRUMP protocol has been implemented in Promela and verified by the Spin program.


Although TRUMP is not as large as a `heavyweight' protocol such as TCP, it is still a complex protocol, and cannot be exhaustively verified using the platforms available to the author, mainly due to memory size considerations. To prove that TRUMP is indeed correct where only some of the features are available, the implementation of TRUMP in Promela is controlled by macro processor[*]`define's which enable or disable certain features:

REORD:
Allow packet reordering on the two links betwen the Sender and the Receiver. The maximum number of reordering operations per link is given by the value
MAXREORD in a constants file. The maximum number of packets `buffered' by the link for reordering is given by the value MAXPKTS in the constants file.
LOSE:
Allow packet loss on the two links betwen the Sender and the Receiver. The maximum number of packet losses per link is given by the value MAXLOSSES in the constants file.
SELACK:
Allow selective acknowledgments to be used between the Sender and the Receiver. The number of packets acknowledged in each selective acknowledgment is given by the value SELACKSIZE in the constants file.
RECVERRS:
Allow the Receiver to send errors in Special Acknowledgment at any time.
IMPLICIT:
Allow implicit connection setups and teardowns as well as the default explicit connection setups and teardowns.
ASSERT:
Install many Promela assert() statements into the TRUMP implementation.

The ASSERT option adds assertions to TRUMP and does not increase its complexity. The RECVERRS and IMPLICIT options add many extra states to both the Sender and Receiver processes, and increase the size of the state space to be exhaustively searched and verified. The same is true for the SELACK option, but this also increases the size of the inter-process messages and the number of local variables, which again increases the state space. The REORD and LOSE options do not affect the Sender or Receiver, but the packet reorderings and losses greatly add to the size of the state space to be searched.

1 TRUMP's Promela Implementation

TRUMP's implementation in Promela is divided into two files: the actual implementation is contained in trump.spin, and the constants used by TRUMP are contained in the constants file. This file is short and is given below.

/******************************/
/** Easily-changed constants **/
/******************************/
#define DATAPKTS        1       /* Send this many data packets */

#ifdef REORD
# define MAXPKTS        4       /* Max packets buffered by reordering */
# define MAXREORD       20      /* Max number of reorders permitted */
#endif

#ifdef LOSE
# define MAXLOSSES      20      /* Maximum number of losses permitted */
#endif
#ifdef SELACK
# define SELACKSIZE     8       /* Number of acks in selack packet */
# define EMPTY          255     /* Ack pkt is empty if seq_base==EMPTY */
#endif

/* The Sender keeps a linked list of
 * the in-transit packets. Each element
 *  has one of the following values.
 */
#define NOTSENT         253     /* Packet has not been transmitted yet */
#define RECEIVED        254     /* Packet was sucessfully received */
#define NULL            255     /* Null pointer */


The implementation of TRUMP in trump.spin is so heavily affected by macro processor directives as to be virtually unreadable. The version of the file below gives the values of the macro processor options, the code after macro processing, and with line numbers.

Some notes should be first given on the TRUMP implementation. In order to determine which packet to transmit next (and hence its sequence number), the TRUMP Sender needs to keep a linked list of in-transit packets and not-yet-transmitted packets. Promela does not have the capability of representing arbitrarily-sized linked lists. To overcome this deficiency, the Sender declares an array of bytes, data_status, to store the list of in-transit packets.

Two byte variables, head and tail, point at the head and tail nodes of the list. An arbitrary value of 255 is chosen to represent the NULL pointer. Elements in the array hold the index number of the next element in the array. The tail node has the value NULL.

There will obviously be some array elements which are not in transit to the Receiver. These have either the value NOTSENT (253) if they have not been transmitted yet, or the value RECEIVED (254) if they were sucessfully received by the Receiver.

As values in the data_status array above 252 have special meanings, there cannot be elements in the array with index 252 or above. Therefore, the TRUMP implementation in Promela is limited to around 250 data packets.

Here, finally, is the implementation of TRUMP in trump.spin.

  1  /**
  2   ** TRUMP verification in Promela
  3   **
  4   ** Copyright (c) 1997 Warren Toomey
  5   ** Revision: 1.32
  6   ** Date: 1997/04/17
  7   **/
  8  
  9  
 10  /*************************/
 11  /** Source-code defines **/
 12  /*************************/
 13  
 14  #define REORD                           /* Allow packet reordering on links */
 15  #define LOSE                            /* Allow packet loss on links */
 16  #define SELACK                          /* Allow selective acknowledgments */
 17  #define RECVERRS                        /* Allow receiver to send errors */
 18  #define IMPLICIT                        /* Allow implicit setups/teardowns */
 19  #define ASSERT                          /* Install lots of assertions */
 20  
 21  #include "constants"                    /* Get constants used below */
 22  
 23  
 24  /*******************/
 25  /** TRUMP Headers **/
 26  /*******************/
 27  
 28  /* Each packet must be one of these types */
 29  mtype = { setup, sack, data, ack, teardown, datasyn }
 30  
 31  
 32  /* A TRUMP packet has the following headers */
 33  typedef trumphdr {
 34      mtype pkt_type;                     /* Type of packet this is */
 35      byte  seq_no;                       /* Sequence number of data segment */
 36                                          /* in selack[0] */
 37      byte  seq_top;                      /* Top seq# in selack bitmap */
 38      bool  selack[SELACKSIZE];           /* Selack bitmap */
 39      bool  explicit_down;                /* If true, do explicit teardowns */
 40      bool  error_val;                    /* Error value of reply */
 41  }
 42  
 43  /***********************/
 44  /* Channel Definitions */
 45  /***********************/
 46  
 47  chan sendtolink = [1] of { trumphdr }   /* Channel from src to badlink  */
 48  chan recvtolink = [1] of { trumphdr }   /* Channel from dest to badlink */
 49  chan linktorecv = [1] of { trumphdr }   /* Channel from badlink to dest */
 50  chan linktosend = [1] of { trumphdr }   /* Channel from badlink to src  */
 51  
 52  
 53  /*********************/
 54  /** Network Section **/
 55  /*********************/
 56  
 57  proctype Badnetwork(chan in, out)
 58  {
 59    trumphdr packet;                      /* Packet received on link */
 60  
 61    chan hold = [MAXPKTS] of { trumphdr }; /* Pkt buffer for reordering */
 62    xr hold; xs hold;
 63    byte reordcnt;                        /* Count of # of reorderings done */
 64  
 65  
 66    byte losecnt;                         /* Count of # of losses done */
 67    losecnt=0;                            /* Initialise loss count */
 68    reordcnt=0;                           /* Initialise reordering count */
 69  
 70  end_bad0: /* Forerver, do */
 71          do
 72          :: in?packet ->         /* Receive a packet from in channel */
 73                  if
 74                  :: out!packet   /* Retransmit it immediately, */
 75  
 76                  :: ((reordcnt<MAXREORD) && nfull(hold)) ->
 77                      hold!packet; reordcnt++; /* save it for later transmit, */
 78  
 79                  :: (losecnt<MAXLOSSES) -> losecnt++; /* or lose it entirely */
 80                  fi;
 81  
 82          :: hold?packet ->
 83                  out!packet      /* Reinsert old data if no link pkt */
 84          od;
 85  }
 86  
 87  
 88  /******************/
 89  /** TRUMP Sender **/
 90  /******************/
 91  
 92  /* The sender has the following main states:
 93   *
 94   *  transmitting setup packets (optional)
 95   *  transmitting data packets
 96   *  transmitting teardown packets
 97   *  finished!
 98   */
 99  
100  proctype Sender(chan send_in, send_out)
101  {
102   trumphdr a;                    /* Packet received from destination */
103   byte data_status[DATAPKTS];    /* List of in-transit seq nums */
104   byte head;                     /* Head of list */
105   byte tail;                     /* Tail of list */
106   byte prev;                     /* Previous node pointer */
107   byte lost;                     /* Highest known lost packet */
108   byte notsent;                  /* Lowest not-yet sent packet */
109   byte i;                        /* Loop counter */
110   byte S;                        /* Next sequence number to send */
111   bool explicit_conn;            /* Should we do an explicit connection? */
112   bool explicit_down;            /* Should we do an explicit teardown? */
113  
114  
115   /* Initialise the data_status array to all NOTSENT */
116   d_step {
117     i=0; S=0; head=NULL; tail=NULL; lost=NULL; notsent=0;
118     do
119     :: (i==DATAPKTS) -> break;
120     :: (i!=DATAPKTS) -> data_status[i]= NOTSENT; i++;
121     od;
122   }
123  
124   /* Choose to do an implicit or explicit connection */
125   if
126   :: (1) -> explicit_conn=0;                     /* Implicit connection */
127             if
128             :: (1) -> explicit_down=0;           /* And implicit teardown, or */
129             :: (1) -> explicit_down=1;           /* Explicit teardown */
130             fi;
131  
132             /* Send off the implicit conn packet, which is also 1st data */
133             d_step {
134              a.pkt_type=datasyn; a.error_val=0; a.seq_no=0;
135              a.explicit_down=explicit_down; head=0; tail=0; lost=NULL;
136              data_status[0]=NULL; notsent=1;
137             };
138  
139             send_out!a; goto progress_send0;     /* Move to state 2, data tx */
140   :: (1) -> explicit_conn=1; explicit_down=1;    /* Explicit connection */
141   fi;
142  
143  
144   /* State 1: sending setup packets */
145   do
146   :: send_in?a -> /* Receive a packet from the receiver */
147           if /* it's a sack with no error, move to state 2 */
148           :: (a.pkt_type==sack && a.error_val==0) -> break;
149  
150              /* it's a sack with an error, terminate now */
151           :: (a.pkt_type==sack && a.error_val!=0) -> goto end_exit_state;
152  
153              /* some other packet, ignore it! */
154           :: else ->
155                  assert(0);      /* Should not get any other type of packet */
156           fi;
157  
158          /* If we can't receive a packet from the receiver */
159          /* then send it a setup packet */
160   :: (empty(send_in) && nfull(send_out)) ->
161            d_step { a.pkt_type=setup; a.seq_no=0; a.error_val=0; }
162            send_out!a;
163   od;
164  
165  progress_send0:
166  
167  
168   /* State 2: sending data packets */
169   do
170   :: send_in?a; /* Receive a packet from the receiver */
171           if /* it's a sack with no error, ignore it */
172           :: (a.pkt_type==sack && a.error_val==0) -> skip;
173  
174              /* it's a sack with an error, terminate now */
175           :: (a.pkt_type==sack && a.error_val!=0) -> goto end_exit_state;
176  
177              /* it's an ack packet, update the data_status array */
178           :: (a.pkt_type == ack) ->
179                  d_step {
180                    printf("Sender got SELACK %d/%d \n",a.seq_no,a.seq_top);
181                    i=a.seq_no; S=0; printf("\t");
182                    do
183                    :: (i>a.seq_top) -> break;
184                    :: else -> printf("%d ", a.selack[S]); i++; S++;
185                    od; printf("\n");
186                  }
187  
188                  /* Assert that  seq_no <= seq_top < seq_no+SELACKSIZE */
189                  /* We could assert that no ack bits above seq_top are on, */
190                  /* but the sender ignores them anyway */
191                  assert(a.seq_no<=a.seq_top);
192                  assert(a.seq_top<(a.seq_no+SELACKSIZE));
193  
194                  /* If it's an ack for the datasyn, check the explicit_down */
195                  d_step {
196                    if
197                    :: ((explicit_conn==0)&&(a.seq_no==0)) ->
198                      if
199                      :: ((explicit_down==0)&&(a.explicit_down==0)) -> skip;
200                      :: ((explicit_down==0)&&(a.explicit_down==1)) -> 
201                          explicit_down=1; /* Recvr asked for explicit teardown */
202  
203                      :: ((explicit_down==1)&&(a.explicit_down==0)) ->
204  
205                          /* Receiver asked for implicit teardown, but we've */
206                          /* already chosen explicit teardown, error! */
207                          assert(0);
208                      :: ((explicit_down==1)&&(a.explicit_down==1)) -> skip;
209                      fi;
210                    :: else -> skip;
211                    fi;
212                  }
213  
214                  /* Deal with each sequence number in turn */
215                  d_step {
216                     S=0;         /* S points at 0th bit in bitmap */
217                     /* For the selack code, loop a.seq_no up to a.seq_top */
218                     do
219                     :: (a.seq_no > a.seq_top) -> break;
220                     :: else ->
221  
222                          /* Assert that we did in fact transmit this one */
223                          assert(data_status[a.seq_no]!=NOTSENT);
224  
225                          if
226                          :: (a.selack[S]==0) ->  skip; /* Ignore lost pkts */
227                          :: (a.selack[S]!=0) ->  /* it was received! */
228  
229                          /* Assert that we did in fact transmit this one */
230                                  assert(data_status[a.seq_no]!=NOTSENT);
231  
232                                  if
233                                  :: (head==NULL) -> skip; /* Already got it */
234                                  :: (data_status[a.seq_no]==RECEIVED) -> skip;
235  
236                                  :: (head==a.seq_no) -> /* it's head packet */
237                                      /* Move the head up */
238                                      head= data_status[a.seq_no];
239  
240                                      if /* Null lost ptr if we received it */
241                                      :: (lost==a.seq_no) -> lost=NULL;
242                                      :: else -> skip;
243                                      fi;
244  
245                                      if /* list now empty? */
246                                      :: (head==NULL) -> tail=NULL;
247                                      :: else -> skip;
248                                      fi;
249                                  :: else ->
250                                      /* Not the head! Find previous node */
251                                      prev=head;
252  
253                                      do  /* prev can't point at NULL! */
254                                      :: (data_status[prev]==NULL) -> assert(0);
255                                      :: (data_status[prev]==a.seq_no) -> break;
256                                      :: else -> prev= data_status[prev];
257                                      od;
258  
259                                      if /* Null lost ptr if we received it */
260                                      :: (lost==a.seq_no) -> lost=prev;
261                                      :: else -> skip;
262                                      fi;
263  
264                                      /* Point lost at prev if prev's */
265                                      /* seq_no < a.seq_no */
266                                      if
267                                      :: (prev<a.seq_no) -> lost=prev;
268                                      :: else -> skip;
269                                      fi;
270                                      /* Now, remove seq_no from list */
271                                      data_status[prev]=data_status[a.seq_no];
272                                  fi;
273                                  if /* seq_no was the tail, point tail at prev */
274                                  :: (a.seq_no==tail) -> tail=prev;
275                                  :: else -> skip;
276                                  fi;
277                                      
278                                  /* Mark the sequence number as RECEIVED */
279                                  data_status[a.seq_no]=RECEIVED;
280                          fi;
281                          a.seq_no++; S++;        /* Move up to the next seq_no */
282                     od;
283                  };
284              /* some other packet, error! */
285           :: else -> assert(0);
286           fi;
287  
288          /* If we can't receive a packet from the receiver */
289          /* then send it a data packet */
290   :: (empty(send_in) && nfull(send_out)) ->
291  
292            /* Complicated bit. To obtain the next sequence number: */
293            /*   If lost!=NULL, choose head of intransit list, else */
294            /*   Use lowest notsent packet */
295            d_step {
296              S= NULL;            /* Assume no packets left to send */
297            
298              if /* Lost can't point to anything is list is empty! */
299              :: ((head==NULL) && (lost!=NULL)) -> assert(0);
300              :: else -> skip;
301              fi;
302  
303              if  /* no packets left to send */
304              :: ((lost==NULL)&&(head==NULL)&&(notsent==DATAPKTS)) -> skip;
305  
306              :: ((lost==NULL)&&(notsent<DATAPKTS)) -> /* choose new seq# */
307                  S= notsent;             /* Notsent has lowest notsent seq# */
308  
309                  if                      /* Append notsent to tail */
310                  :: (tail==NULL) -> head=notsent;
311                  :: (tail!=NULL) -> data_status[tail]=notsent;
312                  fi;
313                  tail=notsent; data_status[tail]=NULL; notsent++; /* Link ops */
314  
315              :: else ->          /* Something must be left in intransit list */
316  
317                  S= head;
318  
319                  if              /* Remove head node */
320                  :: (head==tail) -> head=NULL; tail=NULL;
321  
322                  :: (head!=tail) ->
323                          assert(head!=NULL); assert(tail!=NULL);
324                          head= data_status[head];
325                  fi;
326  
327                  if                      /* Append S to tail */
328                  :: (tail==NULL) -> head=S; tail=S;
329  
330                  :: (tail!=NULL) -> data_status[tail]=S; tail=S;
331                  fi;
332  
333                  data_status[tail]=NULL; 
334  
335                  if /* we're retxing the highest lost packet */
336                  :: (lost==S) -> lost=NULL;      /* No lost pkts left now */
337                  :: else -> skip;
338                  fi;
339              fi;
340            } /* End of the d_step many lines ago! */
341  
342            /* If S is still NULL here, no pkts to tx, then move to next state */
343            if
344            :: (S==NULL) -> break;
345            :: else -> skip;
346            fi;
347  
348            d_step { /* otherwise build and transmit the data packet */
349              a.pkt_type=data; a.error_val=0; a.seq_no=S;
350            }
351            send_out!a;
352   od;
353  
354  progress_send1:
355    /* Assert that all packets marked as RECEIVED */
356    i=0;
357    do
358    :: (i==DATAPKTS) -> break;
359    :: (i!=DATAPKTS) -> assert(data_status[i]==RECEIVED); i++;
360    od;
361  
362    if /* we don't need to do an explicit teardown, skip the teardown state */
363    :: (explicit_down==0) -> goto end_exit_state2;
364    :: else -> skip;      /* we do, so go straight into it */
365    fi;
366  
367  
368   /* State N: sending teardown packets */
369   do
370   :: send_in?a -> /* we can receive a packet from the receiver */
371           if /* it's a teardown, move to exit state */
372           :: (a.pkt_type==teardown) -> break;
373  
374              /* some other packet, ignore it! */
375           :: (a.pkt_type != teardown) -> skip;
376           fi;
377  
378        /* If we can't receive a packet from the receiver */
379        /* then send it a teardown packet */
380   :: (empty(send_in) && nfull(send_out)) ->
381           d_step { a.pkt_type=teardown; a.seq_no=0; a.error_val=0; }
382  
383           send_out!a;
384   od;
385  
386  end_exit_state:
387   printf("Sender exiting\n");
388  
389  /* Sit here mopping up any packets */
390  end_exit_state2:
391   do
392   :: send_in?a;
393   od;
394  }
395  
396  
397  /********************/
398  /** TRUMP Receiver **/
399  /********************/
400  
401  proctype Receiver(chan recv_in, recv_out)
402  {
403   trumphdr b;                    /* Received packet */
404   byte i;                        /* Loop counter */
405   trumphdr a;                    /* Acknowledgment packet */
406   bool alreadygot;               /* True if already marked in selack packet */
407   bool explicit_down;            /* Expect an explicit teardown */
408   bool gotit[DATAPKTS];          /* True if we've got this seq# */
409   byte got_thismany;             /* Count of seq#s we've got (excl. dups) */
410  
411                                  /* Initialise the empty acknowledgment packet */
412   d_step {
413      a.seq_no= EMPTY;
414      a.pkt_type=ack;
415  
416      i=0;                        /* Initialise the gotit array */
417      got_thismany=0;
418      do
419      :: (i==DATAPKTS) -> break;
420      :: (i!=DATAPKTS) -> gotit[i]=0; i++;
421      od;
422   };
423  
424                  /* State 1: receiving setup packets */
425   do
426   :: recv_in?b;
427      if
428      :: (b.pkt_type==setup) -> /* If pkt is a setup pkt, return sack pkt */
429          d_step { b.pkt_type=sack; b.seq_no=0; b.error_val=0; explicit_down=1; }
430  
431          recv_out!b; break;
432  
433      :: (b.pkt_type==setup) -> /* If pkt is a setup pkt, return ERROR sack pkt */
434          d_step { b.pkt_type=sack; b.seq_no=0; b.error_val=1; }
435  
436          recv_out!b;
437          goto end_recv_tosspkts; /* and just sink remaining packets */
438  
439      :: (b.pkt_type==datasyn) -> /* Implicit conn pkt */
440          explicit_down=b.explicit_down; /* Keep explicit teardown flag */
441  
442          /* Choose for explicit or implicit teardown */
443          if
444          :: (b.explicit_down==1) -> skip;
445          :: (b.explicit_down==0) -> explicit_down=0;     /* Implicit */
446          :: (b.explicit_down==0) -> explicit_down=1;     /* Explicit */
447          fi;
448          goto recv_gotdata; /* Skip to the data receive state */
449  
450      :: else -> skip;    /* If not a setup packet, ignore it */
451      fi;
452    od;
453  
454  progress_recv0:
455                  /* State 2: receiving data packets */
456   do
457  
458   :: (got_thismany==DATAPKTS) ->
459  
460  end_recvimplicit:
461      recv_in?b; goto process_data;       /* End state if got all seq#s */
462   :: (got_thismany!=DATAPKTS) ->         /* otherwise it isn't */
463  
464      recv_in?b;
465  
466  process_data:
467      if
468      :: (b.pkt_type==setup) -> /* If pkt is a setup pkt, return sack pkt */
469          d_step { b.pkt_type=sack; b.seq_no=0; b.error_val=0; }
470          recv_out!b;
471  
472      :: (b.pkt_type==setup) -> /* If pkt is a setup pkt, return ERROR pkt */
473          d_step { b.pkt_type=sack; b.seq_no=0; b.error_val=1; }
474          recv_out!b;
475          goto end_recv_tosspkts; /* go and sink remaining packets */
476  
477      :: (b.pkt_type==data) -> /* Received a data packet */
478  recv_gotdata:
479                                  /* Mark seq# as seen */
480          if
481          :: (gotit[b.seq_no]==1) -> skip;
482                                  /* & count the # unique seq#s we've received */
483          :: (gotit[b.seq_no]==0) -> gotit[b.seq_no]=1; got_thismany++;
484          fi;
485  
486          /* First thing is to see if we can fit this seq_no */
487          /* into the existing acknowledgment packet */
488          if
489          :: ((a.seq_no!=EMPTY) && ((b.seq_no<a.seq_no)
490              || (b.seq_no>=a.seq_no+SELACKSIZE))) ->
491                  /* Seq_no doesn't fit, so transmit existing ack packet */
492                  recv_out!a;
493  
494                  /* Reinitialise the ack packet */
495                  d_step { a.seq_no= EMPTY; }
496          :: else -> skip;
497          fi;
498  
499          /* At this point, either the ack packet is EMPTY or we can */
500          /* fit the seq_no in */
501          d_step {
502            if
503            :: (a.seq_no==EMPTY) ->
504                  a.seq_no= b.seq_no; a.seq_top= b.seq_no;
505                  a.selack[0]=1; alreadygot=0;
506                  a.explicit_down=explicit_down;
507  
508            :: (a.seq_no!=EMPTY) ->
509                  i = b.seq_no - a.seq_no;
510                  alreadygot=a.selack[i]; a.selack[i]=1;
511                  if
512                  :: (b.seq_no>a.seq_top) -> a.seq_top=b.seq_no;
513                  :: else -> skip;
514                  fi;
515            fi;
516          }
517  
518          /* If data pkt duplicates one we already have, send ack pkt back NOW */
519          if
520          :: (alreadygot==1) ->
521                  recv_out!a; a.seq_no=EMPTY;
522          :: else -> skip;
523          fi;
524  
525      :: (b.pkt_type==teardown) -> /* Received a teardown packet */
526  
527          /* It's an error if implicit teardowns selected */
528          assert(explicit_down==1);
529  
530          /* Reflect the teardown packet */
531          d_step { b.pkt_type=teardown; b.seq_no=0; b.error_val=0; }
532          recv_out!b; break;
533  
534      :: (b.pkt_type==data) -> /* If pkt is a data pkt, return ERROR sack pkt */
535          d_step { b.pkt_type=sack; b.error_val=1; } /* (to be perverse) */
536  
537          recv_out!b; goto end_recv_tosspkts;
538  
539      :: else -> skip;    /* Not a setup, data or teardown packet, ignore it */
540      fi;
541    od;
542  
543  
544                  /* State 3: Got a teardown, mopping up */
545  end_recv0:
546   do
547   :: recv_in?b;
548      if
549      :: (b.pkt_type==teardown) -> /* Reflect teardowns to source */
550          d_step { b.pkt_type=teardown; b.seq_no=0; b.error_val=0; }
551          recv_out!b;
552  
553      :: else -> skip;    /* If not a setup or teardown packet, ignore it */
554      fi;
555   od;
556  
557                  /* State for collecting remaining packets */
558  end_recv_tosspkts:
559    do
560    :: recv_in?b; d_step { b.pkt_type=sack; b.error_val=1; } recv_out!b;
561    od;
562  }
563  
564  
565  /***************************/
566  /** System Initialisation **/
567  /***************************/
568  
569  init
570  {
571    printf("TRUMP verification in Promela\n");
572    run Sender(linktosend, sendtolink);
573    run Badnetwork(sendtolink, linktorecv);
574    run Badnetwork(recvtolink, linktosend);
575    run Receiver(linktorecv, recvtolink);
576  }


5 TRUMP State Diagrams


Much of the Promela code for TRUMP deals with the manipulation of internal variables to detect packet loss and duplication, and to ensure packet retransmission when required. This tends to obscure the operation of TRUMP as a protocol, i.e as a communications language between two peers. To expose the operation of the protocol itself, state diagrams for the TRUMP sender and receiver are presented: these emphasise the communication operations in TRUMP. States and transitions dealing with the `internal' functionality of TRUMP (e.g working on the linked list of in-transit packets) have been omitted to improve clarity.

The two diagrams show the states and state transitions for the TRUMP sender and receiver. States are represented as nodes with line numbers corresponding to the implementation of TRUMP given in the previous section: essentially, these correspond to the points where a choice is available, or where a implementation can be blocked on a receive or send operation. Receiving states are marked in blue, and sending states are marked in pink. Transitions are represented as directed edges, with labels describing the reason for the transition. Transitions marked with a `*' character must be taken.

1 TRUMP Sender State Diagram

The TRUMP Sender operation goes through three stages. Connection establishment negotiates connection parameters and determines if the receiver is willing to accept connection. Data transmission either transmits a data packet if no acknowledgment packet can be received, or deals with the ack packet. Connection termination occurs on receiver errors, or if all data packets have been received sucessfully.


\begin{pic}{Eps/sender2.eps}{sender2}{TRUMP Sender State Diagram}
\end{pic}

2 TRUMP Receiver State Diagram

The TRUMP Receiver operation also goes through three stages. Connection establishment negotiates connection parameters and determines if the receiver is willing to accept connection. Data reception is controlled by packets from the source (lines 456 and 464), and returns acknowledgment packets. Connection termination occurs when teardown packets are received, and returns teardown packets to the source. A fourth stage of operation, Abnormal Termination, is only used if the receiver wishes to abort the connection at any stage.


\begin{pic}{Eps/receiver2.eps}{receiver2}{TRUMP Receiver State Diagram}
\end{pic}

6 Verification of TRUMP

A TRUMP protocol, with certain of the available features enabled, is correct if:

for all possible interleavings of statements and events across all the processes in the implementation: this forms the state space to be verfied.

The state space must also incorporate the state of all local variables within each process, as state transitions may be chosen on the basis of these state variables. In the implementation of TRUMP in Promela, both the sender and receiver have several local variables, of which the largest are the arrays used to track the number of packets sucessfully transmitted.

In the verification of the TRUMP protocol with Spin, the number of possible states, combined with the size of each state, makes an exhaustive proof of the protocol impossible. The computing equipment available does not have enough real memory to hold the state space. Using the `supertrace' method of verification, the amount of memory required to hold each state is much reduced, but again the number of states is too large to fully prove the protocol. However, let us look at the areas in which the protocol can be proved.

1 No Features Enabled

In Section B.4, it was mentioned that certain TRUMP features could be enabled or disabled via preprocessor macros. Each feature adds extra complexity and state size to TRUMP, and for some of the combinations of features, the TRUMP protocol can be verified.

With no features enabled, the protocol provides reliable data transmission of $N$ data packets across an error-free link with no selective acknowledgments (i.e one acknowledgment per data packet) using explicit connection setup and teardown. For values of $N$ up to 28, the protocol can be exhaustively proved correct: there are 177,614 states (of size 128 bytes) and 222,136 state transitions for $N=$28.

Above $N=$28, we must use the `supertrace' method of verification in Spin. Here, the verifier can estimate the fraction of all states verified by consulting the number of unused hash entries and the number of hash collisions for a hash table that is used to represent the state space. Using the supertrace method, a protocol can be proved correct for the fraction of possible states covered by the verifier. In the case of Spin, a verification shows that a protocol is correct after covering either '$\ge$ 99.9% of states', `$\ge$ 98% of states' or `$<$ 98% of states'.

Using supertrace, TRUMP with no features enabled is provably correct after covering
$\ge$ 98% of states for $N$ up to 250 data packets.

2 Selective Acknowledgments

With the enabling of selective acknowledgments of size 8 (that is, one acknowledgment for 8 data packets), the state vector is 60 bytes larger then for the equivalent `no features' state, and the number of states is approximately 4 times that of the equivalent `no features' protocol. The supertrace method was used for all values of $N$, showing that TRUMP with selective acknowlegments of size 8 is provably correct after covering $\ge$ 98% of states for $N$ up to 250 data packets.

3 Receiver Errors

One optional feature of the TRUMP implementation in Promela is to allow the receiver to return a special `error' acknowledgment at any time during the course of the connection setup, data transmission and connection teardown. Upon receipt of this acknowledgment, the sender must immediately desist transmission of all packets. This arbitrary return of an `error' acknowledgment increases the size of the state space to approximately 2.6 times that of the equivalent `no features' protocol; the state size is unchanged. The supertrace method was used for all values of $N$, showing that TRUMP with arbitrary receiver errors is provably correct after covering $\ge$ 98% of states for $N$ up to 250 data packets.

4 Implicit Connection Setup

Enabling implicit connection setups and teardown (with the latter selectable by both sender and receiver), the size of each state is approximately twice that with implicit connections disabled. The state space for implicit connections is also approximately 3.5 times that of the equivalent `no features' protocol. The supertrace method was used for all values of $N$, showing that TRUMP with implicit connections is provably correct after covering $\ge$ 98% of states for $N$ up to 250 data packets.

5 Packet Losses

Two of the selectable `features' in the TRUMP implementation are the enabling of packet reordering on the two links between the sender and receiver, and the enabling of packet loss on these two links. These features do not affect the sender's or receiver's code, but they do affect the protocol's operation. Both options have a tremendous effect on the possible interleavings of the sender, receiver and link states, and so significantly affect the size of the total state space to be verified. With either enabled, TRUMP cannot be verified for large values of $N$.

The implementation of TRUMP in Promela imposes a limit on the number of packet reorderings and packet losses on a single link. This is set in the `constants' file at 20 reorderings and 20 losses per link. Even with these small values, the state space is extremely large.


With only packet loss enabled, the state space to be explored is at least 330 times that of TRUMP with no packet loss, for equivalent values of $N$: for example, there are $2.8 * 10^7$ states for $N=$5 packets. The size of each state is unaffected. Figure 66 shows the range of $N$ vs. packet loss values for which the TRUMP specification in Promela can be verified correct.


\begin{pic}{Eps/spinloss.eps}{spinloss}
{Verification of TRUMP during Packet Loss}
\end{pic}

6 Packet Reordering

With only packet reorderings enabled, the state space to be explored is again very much larger than that of TRUMP with no packet loss. The size of each state is unaffected. Figure 67 shows the range of $N$ vs. packet loss values for which the TRUMP specification in Promela can be verified correct.


\begin{pic}{Eps/spinreord.eps}{spinreord}
{Verification of TRUMP during Packet Reordering}
\end{pic}

7 Summary

The correct operation of a complex transport protocol must be verified; otherwise, severe operational errors may come to light either after an implementation of the protocol, or after the implementation's deployment. In this appendix, we have reviewed the use of the Spin protocol verification tool to prove TRUMP correct where possible.

Due to CPU and memory constraints, Spin was unable to exhaustively prove TRUMP correct. The Promela implementation of the protocol was designed to allow certain TRUMP functionality to be enabled and disabled. With packet loss and packet reordering disabled, the TRUMP protocol was verified with the following features enabled, for up to 250 data packets per connection:

The complexity of the Promela implementation of TRUMP increases dramatically with packet losses or packet reordering enabled. With no features enabled, Spin was able to prove the correctness of the TRUMP protocol for a very small number of packet loss/data packet combinations, and similarly for a very small number of packet reordering/data packet combinations.

Although TRUMP has not been exhaustively verified, it appears to be a robust transport protocol, with no correctness flaws discovered.


next up previous contents
Next: C. TRUMP Protocol Headers Up: Warrens Ph.D Thesis Previous: A. Glossary   Contents
Warren Toomey 2011-12-04