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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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).
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![[*]](footnote.gif)
`define's which enable or disable certain features:
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.
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 }
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.
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.
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.
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.
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 
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 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 
28.
Above 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 '
99.9% of states',
` 98% of states' or `
98% of states'.
Using supertrace, TRUMP with no features enabled is provably correct
after covering 98% of states for up to 250 data packets.
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 , showing that TRUMP
with selective acknowlegments of size 8 is provably correct after covering
98% of states for up to 250 data packets.
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 , showing that TRUMP
with arbitrary receiver errors is provably correct after covering
98% of states for up to 250 data packets.
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
, showing that TRUMP with implicit connections is provably correct after
covering 98% of states for up to 250 data packets.
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 .
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
: for example, there are 
states for 5 packets. The size of
each state is unaffected. Figure 66 shows the range of vs.
packet loss values for which the TRUMP specification in Promela can be
verified correct.
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 vs.
packet loss values for which the TRUMP specification in Promela can be
verified correct.
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.