/* $Header: /home/stufs1/vicdu/ra/635/project/spin/RCS/proti.spin,v 3.1 1998/10/03 17:58:28 vicdu Exp $ */ /* * PROMELA Validation Model * Taylor's I-Protocol, as implemented in the GNU UUCP package */ #define true 1 #define false 0 #define QSZ 0 /* queue size -- we are only interested in rendez-vous communication since we are trying to model this as we did in VPL. In general we should have large queue sizes and verify that protocol is correct also in these cases. */ #define WIN 2 /* range sequence numbers */ #define HWIN (WIN/2) /* window size: WIN/2 */ #define QWIN (WIN/4) /* half window size: WIN/4 */ #define diff(x, y) ((x+WIN-y)%WIN) #define inc(x) x=(x+1)%WIN byte sndr_u_seq; byte rcvr_u_seq; #define sndr_1 (sndr_u_seq == 1) #define rcvr_1 (rcvr_u_seq == 1) #define error assert (false) mtype = { ack, nak, data } /* we do not model opening, closing, syncing of connections at this level of abstraction */ /* * the medium can drop a packet, corrupt its data, its header (or both) or deliver it intact; * it buffers at most 1 packet, a la the VPL code -- to make it buffer more, simply increase the * QSZ parameter appropriately */ */ proctype medium(chan in, out){ byte pty; /* packet type */ byte seq; /* sequence number field */ byte ak; /* acknowledgement field */ do :: in? pty(seq, ak) -> if :: out! pty(seq, ak, true, true) /* good transmission */ :: true -> /* put "true" here in order to add the label */ progress_m3 : skip /* packet silently dropped */ :: true -> progress_m0 : out! pty(seq, ak, true, false) :: true -> progress_m1 : out! pty(seq, ak, false, true) :: true -> progress_m2 : out! pty(seq, ak, false, false) fi od } /* * the sender half of the i-protocol. */ /* sender's updaterack routine */ #define s_updaterack if \ :: (!( (ak==sendseq) || diff(ak, rack)>WIN/2 || \ diff(sendseq, ak)>WIN/2)) -> rack = ak \ :: else -> skip \ fi /* sender's getdata "routine" */ #define s_getdata if \ :: hck -> \ /* good header */ \ if \ :: atomic { (pty==ack) -> s_updaterack } \ /* if it's an ack, update rack */ \ :: atomic {(pty==nak) -> \ /* if it's a nak, update rack & resend nakd packet if in send window */ \ s_updaterack \ }; \ if \ :: (!((seq==sendseq) || diff(seq, rack)>WIN/2 || diff(sendseq, seq)>WIN/2)) -> \ out! data(seq, 0) \ :: atomic {else -> skip} \ fi \ :: atomic { \ else -> printf("illegal packet type: s_getdata\n") \ } \ fi \ :: atomic {else -> skip} \ fi /* sender timeout "routine" */ #define s_timeout if \ :: in? pty(seq, ak, hck, dck); s_getdata \ /* receive a packet from remote, while timing out */ \ :: out! nak(1, 0); \ /* send "the" nak */ \ if \ :: (sendseq!=(rack+1)%WIN) ->out! data((rack+1)%WIN,0)\ :: atomic {else -> skip } \ fi \ fi /* sender's local initializations */ #define s_init atomic {sendseq = 1; rack = 0 } proctype sender(chan in, out, user) { byte sendseq; /* next sequence number to use when sending */ byte rack; /* last sequence number acked by remote */ byte pty; /* packet type */ byte seq; /* packet sequence number */ byte ak; /* ack field in packet */ bool hck; /* hck field in packet */ bool dck; /* dck field in packet */ byte tmp; /* scratch variable */ s_init; do :: atomic {user? tmp; assert(tmp==sendseq);} do /* try to send a new data packet */ :: ((diff(sendseq, rack)>WIN/2) || (sendseq == rack)) -> /* no opening in remote window */ if :: in? pty(seq, ak, hck, dck); s_getdata /* receive a packet from remote */ :: true-> s_timeout /* non-deterministic time out,can be done if nothing to receive */ fi :: atomic {else -> break } /* opening in remote window */ od; out! data(sendseq, 0); /* send data packet */ inc(sendseq); /* update sendseq */ :: in? pty(seq, ak, hck, dck); s_getdata /* receive a packet from remote */ :: true -> progress_t1: s_timeout /* can always timeout */ od /* sender */ } /* receiver's local initializations */ #define r_init atomic { \ recseq = 0; lack = 0; seq = 0; \ do \ :: (seq recbuf[seq] =false; nakd[seq] =false; seq++ \ :: (seq==WIN) -> break \ od } /* receiver's sennak routine */ #define r_sendnak(x) out! nak(x, recseq); atomic{lack = recseq; nakd[x] = true} /* receiver's getdata "routine" */ #define r_getdata \ Lab_getdata: if \ :: hck -> \ /* good header */ \ if \ :: (pty==data) -> \ if \ :: (!((diff(seq, lack)>WIN/2) || (seq==lack))) -> \ /* in my receive window */ \ if \ :: atomic{dck -> \ nakd[seq]=false;} \ if \ :: (!(seq==(recseq+1)%WIN)) -> \ /* unexpected sequwnce number */ \ if \ :: atomic{((seq!=recseq) && (! recbuf[seq])) -> \ recbuf[seq] = true; \ tmp = (recseq+1)%WIN;} \ do \ :: (tmp \ if \ :: (!(nakd[tmp] || recbuf[tmp])) -> r_sendnak(tmp) \ :: atomic {else -> skip } \ fi; \ inc(tmp) \ :: atomic{(tmp==seq) -> break} \ od \ :: atomic {else -> skip} \ fi; \ /* bug fix follows */ \ /* r_sendnak((recseq+1)%WIN) */ \ :: atomic{(seq==(recseq+1)%WIN) -> \ /* expected sequwnce number */ \ recseq = seq;} \ user! recseq; \ /* deliver to user */ \ tmp=(seq+1)%WIN; \ do \ :: atomic{recbuf[tmp] -> recseq=tmp;} \ user! recseq;\ atomic{ \ recbuf[tmp]=false; \ inc(tmp)} \ :: atomic{(! recbuf[tmp]) -> break} \ od; \ if \ :: (!(diff(seq, lack) \ out! ack(seq, seq); lack=recseq \ :: atomic{else -> skip} \ fi \ fi \ :: else -> /* dck is false */ \ if \ /* :: (!((seq==recseq)&& (!recbuf[seq]&&!nakd[seq]))) -> */ \ :: ((seq!=recseq)&& !recbuf[seq]&& (diff(seq, recseq)<= WIN/2)) -> \ r_sendnak(seq) \ :: atomic{else -> skip} \ fi \ fi /* of if dck-> */ \ /* :: r_sendnak((recseq+1)%WIN) */ \ /* bug fix */ \ :: atomic{else -> skip} \ fi /* of if (!(diff(seq, lack).. */ \ :: atomic{else -> assert(pty==nak);} \ /* my bug fix */ \ /* out!ack(recseq, recseq); \ lack=recseq */ \ fi /* if (pty == data) */ \ :: atomic{else -> skip} \ fi /* if hck -> */ /* receiver's timeout routine */ /* this following atomic cuts the state space by half */ #define r_timeout atomic { \ seq = 0; \ do \ :: (seq nakd[seq]=false; seq++ \ :: (seq==WIN) -> break \ od; \ } \ if \ :: in? pty(seq, ak, hck, dck); \ /* receive a packet from remote, while timing out */\ goto Lab_getdata \ /* r_sendnak((recseq+1)%WIN) */ \ /* proposed fix to stark livelock above */ \ :: r_sendnak((recseq+1)%WIN) \ /* send a nak if nothing to receive */ \ fi /* receiver's protocol */ proctype recver(chan in, out, user){ byte recseq; /* last sequence number returned to user */ byte lack; /* last seqnumber acked to remote */ bool recbuf[WIN]; /* array of out-of-order data packets rcvd from remote*/ bool nakd[WIN]; /* record of naks sent recently */ byte pty; /* packet type */ byte seq; /* packet seq no */ byte ak; /* piggyback ack */ bool hck; /* header checksum */ bool dck; /* data checksum */ byte tmp; /* local scratch variable */ r_init; do :: in? pty(seq, ak, hck, dck); r_getdata /* process a packet received */ :: true -> progress_t2: r_timeout /* can always timeout */ od } /* sender tester unit */ proctype sndr_u(chan out){ sndr_u_seq = 1; do :: atomic {out! sndr_u_seq; inc(sndr_u_seq)} od } /* receiver tester unit */ proctype rcvr_u(chan in){ byte tmp; /* sequence number */ rcvr_u_seq = 1; do :: atomic {in? tmp; assert(tmp == rcvr_u_seq);} progress_r : inc(rcvr_u_seq) od } init { /* the channels: s = sender, m = medium, r = receiver */ chan s2m = [QSZ] of { mtype, byte, byte }; /* type, sequence number, ack number (piggyback) */ chan m2s = [QSZ] of { mtype, byte, byte, bool, bool }; /* type, sequence number, ack number (piggyback), header checksum, data checksum */ chan r2m = [QSZ] of { mtype, byte, byte }; /* type, sequence number, ack number (piggyback) */ chan m2r = [QSZ] of { mtype, byte, byte, bool, bool }; /* type, sequence number, ack number (piggyback) */ chan usr_s = [QSZ] of { byte }; /* sequence number only */ chan usr_r = [QSZ] of { byte }; /* sequence number only */ atomic { run sndr_u(usr_s); run sender(m2s, s2m, usr_s); run medium(s2m, m2r); run medium(r2m, m2s); run recver(m2r, r2m, usr_r); run rcvr_u(usr_r); } }