| 1 | /* |
| 2 | * PROMELA Validation Model |
| 3 | * FLOW CONTROL LAYER VALIDATION |
| 4 | */ |
| 5 | |
| 6 | #define LOSS 1 /* message loss */ |
| 7 | #define DUPS 0 /* duplicate msgs */ |
| 8 | #define QSZ 2 /* queue size */ |
| 9 | |
| 10 | mtype = { |
| 11 | red, white, blue, |
| 12 | abort, accept, ack, sync_ack, close, connect, |
| 13 | create, data, eof, open, reject, sync, transfer, |
| 14 | FATAL, NON_FATAL, COMPLETE |
| 15 | } |
| 16 | |
| 17 | chan ses_to_flow[2] = [QSZ] of { byte, byte }; |
| 18 | chan flow_to_ses[2] = [QSZ] of { byte, byte }; |
| 19 | chan dll_to_flow[2] = [QSZ] of { byte, byte }; |
| 20 | |
| 21 | /* |
| 22 | * Flow Control Layer Validation Model |
| 23 | */ |
| 24 | |
| 25 | #define true 1 |
| 26 | #define false 0 |
| 27 | |
| 28 | #define M 4 /* range sequence numbers */ |
| 29 | #define W 2 /* window size: M/2 */ |
| 30 | |
| 31 | proctype fc(chan s2f, f2d, f2s, d2f) |
| 32 | { bool busy[M]; /* outstanding messages */ |
| 33 | byte q; /* seq# oldest unacked msg */ |
| 34 | byte m; /* seq# last msg received */ |
| 35 | byte s; /* seq# next msg to send */ |
| 36 | byte window; /* nr of outstanding msgs */ |
| 37 | byte type; /* msg type */ |
| 38 | bit received[M]; /* receiver housekeeping */ |
| 39 | bit x; /* scratch variable */ |
| 40 | byte p; /* seq# of last msg acked */ |
| 41 | byte I_buf[M], O_buf[M]; /* message buffers */ |
| 42 | |
| 43 | xr s2f; |
| 44 | xs f2d; |
| 45 | xs f2s; |
| 46 | xr d2f; |
| 47 | |
| 48 | /* sender part */ |
| 49 | end: do |
| 50 | :: atomic { |
| 51 | (window < W && nempty(s2f) |
| 52 | && nfull(f2d)) -> |
| 53 | s2f?type,x; |
| 54 | window = window + 1; |
| 55 | busy[s] = true; |
| 56 | O_buf[s] = type; |
| 57 | f2d!type,s; |
| 58 | if |
| 59 | :: (type != sync) -> |
| 60 | s = (s+1)%M |
| 61 | :: (type == sync) -> |
| 62 | window = 0; |
| 63 | s = M; |
| 64 | do |
| 65 | :: (s > 0) -> |
| 66 | s = s-1; |
| 67 | busy[s] = false |
| 68 | :: (s == 0) -> |
| 69 | break |
| 70 | od |
| 71 | fi |
| 72 | } |
| 73 | :: atomic { |
| 74 | (window > 0 && busy[q] == false) -> |
| 75 | window = window - 1; |
| 76 | q = (q+1)%M |
| 77 | } |
| 78 | #if DUPS |
| 79 | :: atomic { |
| 80 | (nfull(f2d) && window > 0 && busy[q] == true) -> |
| 81 | f2d!O_buf[q],q |
| 82 | } |
| 83 | #endif |
| 84 | :: atomic { |
| 85 | (timeout && nfull(f2d) && window > 0 && busy[q] == true) -> |
| 86 | f2d!O_buf[q],q |
| 87 | } |
| 88 | /* receiver part */ |
| 89 | #if LOSS |
| 90 | :: d2f?type,m /* lose any message */ |
| 91 | #endif |
| 92 | :: d2f?type,m -> |
| 93 | if |
| 94 | :: atomic { |
| 95 | (type == ack) -> |
| 96 | busy[m] = false |
| 97 | } |
| 98 | :: atomic { |
| 99 | (type == sync) -> |
| 100 | m = 0; |
| 101 | do |
| 102 | :: (m < M) -> |
| 103 | received[m] = 0; |
| 104 | m = m+1 |
| 105 | :: (m == M) -> |
| 106 | break |
| 107 | od |
| 108 | }; f2d!sync_ack,0 |
| 109 | :: (type == sync_ack) -> |
| 110 | f2s!sync_ack,0 |
| 111 | :: (type != ack && type != sync && type != sync_ack)-> |
| 112 | if |
| 113 | :: atomic { |
| 114 | (received[m] == true) -> |
| 115 | x = ((0<p-m && p-m<=W) |
| 116 | || (0<p-m+M && p-m+M<=W)) }; |
| 117 | if |
| 118 | :: (x) -> f2d!ack,m |
| 119 | :: (!x) /* else skip */ |
| 120 | fi |
| 121 | :: atomic { |
| 122 | (received[m] == false) -> |
| 123 | I_buf[m] = type; |
| 124 | received[m] = true; |
| 125 | received[(m-W+M)%M] = false |
| 126 | } |
| 127 | fi |
| 128 | fi |
| 129 | :: /* atomic { */ |
| 130 | (received[p] == true && nfull(f2s) && nfull(f2d)) -> |
| 131 | f2s!I_buf[p],0; |
| 132 | f2d!ack,p; |
| 133 | p = (p+1)%M |
| 134 | /* } */ |
| 135 | od |
| 136 | } |
| 137 | |
| 138 | proctype upper_s(chan s2f, f2s0) |
| 139 | { byte s_state; |
| 140 | byte type, toggle; |
| 141 | |
| 142 | xs s2f; |
| 143 | xr f2s0; |
| 144 | |
| 145 | s2f!sync,toggle; |
| 146 | do |
| 147 | :: f2s0?sync_ack,type -> |
| 148 | if |
| 149 | :: (type != toggle) |
| 150 | :: (type == toggle) -> break |
| 151 | fi |
| 152 | :: timeout -> |
| 153 | s2f!sync,toggle |
| 154 | od; |
| 155 | toggle = 1 - toggle; |
| 156 | |
| 157 | end: do |
| 158 | :: s2f!white,0 |
| 159 | :: atomic { |
| 160 | (s_state == 0 && nfull(s2f)) -> |
| 161 | s2f!red,0 -> |
| 162 | s_state = 1 |
| 163 | } |
| 164 | :: atomic { |
| 165 | (s_state == 1 && nfull(s2f)) -> |
| 166 | s2f!blue,0 -> |
| 167 | s_state = 2 |
| 168 | } |
| 169 | od |
| 170 | } |
| 171 | |
| 172 | proctype upper_r(chan f2s1) |
| 173 | { byte r_state; |
| 174 | |
| 175 | xr f2s1; |
| 176 | |
| 177 | do |
| 178 | :: f2s1?white,0 |
| 179 | :: f2s1?red,0 -> break |
| 180 | :: f2s1?blue,0 -> assert(0) |
| 181 | od; |
| 182 | |
| 183 | do |
| 184 | :: f2s1?white,0 |
| 185 | :: f2s1?red,0 -> assert(0) |
| 186 | :: f2s1?blue,0 -> goto end |
| 187 | od; |
| 188 | end: |
| 189 | do |
| 190 | :: f2s1?white,0 |
| 191 | :: f2s1?red,0 -> assert(0) |
| 192 | :: f2s1?blue,0 -> assert(0) |
| 193 | od |
| 194 | } |
| 195 | |
| 196 | init |
| 197 | { |
| 198 | atomic { |
| 199 | run fc(ses_to_flow[0], dll_to_flow[1], flow_to_ses[0], dll_to_flow[0]); |
| 200 | run fc(ses_to_flow[1], dll_to_flow[0], flow_to_ses[1], dll_to_flow[1]); |
| 201 | run upper_s(ses_to_flow[0], flow_to_ses[0]); |
| 202 | run upper_r(flow_to_ses[1]) |
| 203 | } |
| 204 | } |