\begin{verbatim} 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 77 hold!packet; reordcnt++; /* save it for later transmit, */ 78 79 :: (losecnt 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 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 /* 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+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 } \end{verbatim}