1#define NBUFS 2 2#define READMAX 2 3#define BUFSIZ 2*READMAX 4#define EOF 255 5#define TIMEOUT 254 6#define FILEMAXLEN 20 7 8byte n[NBUFS]; 9byte ntotal[NBUFS]; 10byte putnext[NBUFS]; 11byte getnext[NBUFS]; 12bool eof[NBUFS]; 13bool roomwait[NBUFS]; 14bool datawait[NBUFS]; 15byte rwant; 16 17/* use one big data array to simulate 2-d array */ 18#define bufstart(slot) (slot*BUFSIZ) 19#define bufend(slot) ((slot+1)*BUFSIZ) 20/* bit data[BUFSIZ*NBUFS]; */ 21 22bool selwait; 23/* bool hastimeout; */ 24 25#define get 0 26#define release 1 27 28chan lock = [0] of { bit }; 29chan lockkill = [0] of { bit }; 30chan sel = [0] of { byte }; 31chan selcall = [0] of { byte }; 32chan selans = [0] of { byte, byte }; 33chan selkill = [0] of { bit }; 34chan readcall = [0] of { byte, byte }; 35chan readans = [0] of { byte }; 36chan readkill = [0] of { bit }; 37chan croom[NBUFS] = [0] of { bit }; 38chan cdata[NBUFS] = [0] of { bit }; 39 40proctype Lockrendez() 41{ 42 do 43 :: lock!get -> lock?release 44 :: lockkill?release -> break 45 od 46} 47 48proctype Copy(byte fd) 49{ 50 byte num; 51 bit b; 52 53 do :: 1 -> 54 /* make sure there's room */ 55 lock?get; 56 if 57 :: (BUFSIZ-putnext[fd]) < READMAX -> 58 if 59 :: getnext[fd] == putnext[fd] -> 60 getnext[fd] = 0; 61 putnext[fd] = 0; 62 lock!release 63 :: getnext[fd] != putnext[fd] -> 64 roomwait[fd] = 1; 65 lock!release; 66 croom[fd]?b 67 fi 68 :: (BUFSIZ-putnext[fd]) >= READMAX -> 69 lock!release 70 fi; 71 /* simulate read into data buf at putnext */ 72 if 73 :: ntotal[fd] > FILEMAXLEN -> 74 num = EOF 75 :: ntotal[fd] <= FILEMAXLEN -> 76 if 77 :: num = 1 78 :: num = READMAX 79 :: num = EOF 80 fi 81 fi; 82 /* here is where data transfer would happen */ 83 lock?get; 84 if 85 :: num == EOF -> 86 eof[fd] = 1; 87/* printf("Copy %d got eof\n", fd);/**/ 88 if 89 :: datawait[fd] -> 90 datawait[fd] = 0; 91 lock!release; 92 cdata[fd]!1 93 :: !datawait[fd] && (rwant & (1<<fd)) && selwait -> 94 selwait = 0; 95 lock!release; 96 sel!fd 97 :: !datawait[fd] && !((rwant & (1<<fd)) && selwait) -> 98 lock!release 99 fi; 100 break 101 :: num != EOF -> 102/* printf("Copy %d putting %d in; old putnext=%d, old n=%d\n", fd, num, putnext[fd], n[fd]); /* */ 103 putnext[fd] = putnext[fd] + num; 104 n[fd] = n[fd] + num; 105 ntotal[fd] = ntotal[fd] + num; 106 assert(n[fd] > 0); 107 if 108 :: datawait[fd] -> 109 datawait[fd] = 0; 110 lock!release; 111 cdata[fd]!1 112 :: !datawait[fd] && (rwant & (1<<fd)) && selwait -> 113 selwait = 0; 114 lock!release; 115 sel!fd 116 :: !datawait[fd] && !((rwant & (1<<fd)) && selwait) -> 117 lock!release 118 fi 119 fi; 120 od 121} 122 123proctype Read() 124{ 125 byte ngot; 126 byte fd; 127 byte nwant; 128 bit b; 129 130 do 131 :: readcall?fd,nwant -> 132 if 133 :: eof[fd] && n[fd] == 0 -> 134 readans!EOF 135 :: !(eof[fd] && n[fd] == 0) -> 136 lock?get; 137 ngot = putnext[fd] - getnext[fd]; 138/* printf("Reading %d, want %d: ngot = %d - %d, n = %d\n", fd, nwant, putnext[fd], getnext[fd], n[fd]); /* */ 139 if 140 :: ngot == 0 -> 141 if 142 :: eof[fd] -> 143 skip 144 :: !eof[fd] -> 145 /* sleep until there's data */ 146 datawait[fd] = 1; 147/* printf("Read sleeping\n"); /* */ 148 lock!release; 149 cdata[fd]?b; 150 lock?get; 151 ngot = putnext[fd] - getnext[fd]; 152/* printf("Read awoke, ngot = %d\n", ngot); /**/ 153 fi 154 :: ngot != 0 -> skip 155 fi; 156 if 157 :: ngot > nwant -> ngot = nwant 158 :: ngot <= nwant -> skip 159 fi; 160 /* here would take ngot elements from data, from getnext[fd] ... */ 161 getnext[fd] = getnext[fd] + ngot; 162 assert(n[fd] >= ngot); 163 n[fd] = n[fd] - ngot; 164 if 165 :: ngot == 0 -> 166 assert(eof[fd]); 167 ngot = EOF 168 :: ngot != 0 -> skip 169 fi; 170 if 171 :: getnext[fd] == putnext[fd] && roomwait[fd] -> 172 getnext[fd] = 0; 173 putnext[fd] = 0; 174 roomwait[fd] = 0; 175 lock!release; 176 croom[fd]!0 177 :: getnext[fd] != putnext[fd] || !roomwait[fd] -> 178 lock!release 179 fi; 180 readans!ngot 181 fi 182 :: readkill?b -> break 183 od 184} 185 186proctype Select() 187{ 188 byte num; 189 byte i; 190 byte fd; 191 byte r; 192 bit b; 193 194 do 195 :: selcall?r -> 196/* printf("Select called, r=%d\n", r); /**/ 197 i = 0; 198 do 199 :: i < NBUFS -> 200 if 201 :: r & (1<<i) -> 202 if 203 :: eof[i] && n[i] == 0 -> 204/* printf("Select got eof on %d\n", i);/**/ 205 num = EOF; 206 r = i; 207 goto donesel 208 :: !eof[i] || n[i] != 0 -> skip 209 fi 210 :: !(r & (1<<i)) -> skip 211 fi; 212 i = i+1 213 :: i >= NBUFS -> break 214 od; 215 num = 0; 216 lock?get; 217 rwant = 0; 218 i = 0; 219 do 220 :: i < NBUFS -> 221 if 222 :: r & (1<<i) -> 223 if 224 :: n[i] > 0 || eof[i] -> 225/* printf("Select found %d has n==%d\n", i, n[i]); /**/ 226 num = num+1 227 :: n[i] == 0 && !eof[i] -> 228/* printf("Select asks to wait for %d\n", i); /**/ 229 r = r &(~(1<<i)); 230 rwant = rwant | (1<<i) 231 fi 232 :: !(r & (1<<i)) -> skip 233 fi; 234 i = i+1 235 :: i >= NBUFS -> break 236 od; 237 if 238 :: num > 0 || rwant == 0 -> 239 rwant = 0; 240 lock!release; 241 :: num == 0 && rwant != 0 -> 242 selwait = 1; 243 lock!release; 244/* printf("Select sleeps\n"); /**/ 245 sel?fd; 246/* printf("Select wakes up, fd=%d\n", fd); /**/ 247 if 248 :: fd != TIMEOUT -> 249 if 250 :: (rwant & (1<<fd)) && (n[fd] > 0) -> 251 r = r | (1<<fd); 252 num = 1 253 :: !(rwant & (1<<fd)) || (n[fd] == 0) -> 254 num = 0 255 fi 256 :: fd == TIMEOUT -> skip 257 fi; 258 rwant = 0 259 fi; 260 donesel: 261 selans!num,r 262 :: selkill?b -> break 263 od 264} 265 266/* This routine is written knowing NBUFS == 2 in several places */ 267proctype User() 268{ 269 byte ndone; 270 byte i; 271 byte rw; 272 byte num; 273 byte nwant; 274 byte fd; 275 bool goteof[NBUFS]; 276 277 ndone = 0; 278 do 279 :: ndone == NBUFS -> break 280 :: ndone < NBUFS -> 281 if 282 :: 1-> 283 /* maybe use Read */ 284/* printf("User trying to read. Current goteofs: %d %d\n", goteof[0], goteof[1]); /**/ 285 /* randomly pick fd 0 or 1 from non-eof ones */ 286 if 287 :: !goteof[0] -> fd = 0 288 :: !goteof[1] -> fd = 1 289 fi; 290 if 291 :: nwant = 1 292 :: nwant = READMAX 293 fi; 294 readcall!fd,nwant; 295 readans?num; 296 if 297 :: num == EOF -> 298 goteof[fd] = 1; 299 ndone = ndone + 1 300 :: num != EOF -> assert(num != 0) 301 fi 302 :: 1-> 303/* printf("User trying to select. Current goteofs: %d %d\n", goteof[0], goteof[1]); /**/ 304 /* maybe use Select, then Read */ 305 /* randomly set the "i want" bit for non-eof fds */ 306 if 307 :: !goteof[0] && !goteof[1] -> rw = (1<<0) | (1<<1) 308 :: !goteof[0] -> rw = (1<<0) 309 :: !goteof[1] -> rw = (1<<1) 310 fi; 311 selcall!rw; 312 selans?i,rw; 313 if 314 :: i == EOF -> 315 goteof[rw] = 1; 316 ndone = ndone + 1 317 :: i != EOF -> 318 /* this next statement knows NBUFS == 2 ! */ 319 if 320 :: rw & (1<<0) -> fd = 0 321 :: rw & (1<<1) -> fd = 1 322 :: rw == 0 -> fd = EOF 323 fi; 324 if 325 :: nwant = 1 326 :: nwant = READMAX 327 fi; 328 if 329 :: fd != EOF -> 330 readcall!fd,nwant; 331 readans?num; 332 assert(num != 0) 333 :: fd == EOF -> skip 334 fi 335 fi 336 fi 337 od; 338 lockkill!release; 339 selkill!release; 340 readkill!release 341} 342 343init 344{ 345 byte i; 346 347 atomic { 348 run Lockrendez(); 349 i = 0; 350 do 351 :: i < NBUFS -> 352 run Copy(i); 353 i = i+1 354 :: i >= NBUFS -> break 355 od; 356 run Select(); 357 run Read(); 358 run User() 359 } 360} 361