123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360 |
- #define NBUFS 2
- #define READMAX 2
- #define BUFSIZ 2*READMAX
- #define EOF 255
- #define TIMEOUT 254
- #define FILEMAXLEN 20
- byte n[NBUFS];
- byte ntotal[NBUFS];
- byte putnext[NBUFS];
- byte getnext[NBUFS];
- bool eof[NBUFS];
- bool roomwait[NBUFS];
- bool datawait[NBUFS];
- byte rwant;
- /* use one big data array to simulate 2-d array */
- #define bufstart(slot) (slot*BUFSIZ)
- #define bufend(slot) ((slot+1)*BUFSIZ)
- /* bit data[BUFSIZ*NBUFS]; */
- bool selwait;
- /* bool hastimeout; */
- #define get 0
- #define release 1
- chan lock = [0] of { bit };
- chan lockkill = [0] of { bit };
- chan sel = [0] of { byte };
- chan selcall = [0] of { byte };
- chan selans = [0] of { byte, byte };
- chan selkill = [0] of { bit };
- chan readcall = [0] of { byte, byte };
- chan readans = [0] of { byte };
- chan readkill = [0] of { bit };
- chan croom[NBUFS] = [0] of { bit };
- chan cdata[NBUFS] = [0] of { bit };
- proctype Lockrendez()
- {
- do
- :: lock!get -> lock?release
- :: lockkill?release -> break
- od
- }
- proctype Copy(byte fd)
- {
- byte num;
- bit b;
- do :: 1 ->
- /* make sure there's room */
- lock?get;
- if
- :: (BUFSIZ-putnext[fd]) < READMAX ->
- if
- :: getnext[fd] == putnext[fd] ->
- getnext[fd] = 0;
- putnext[fd] = 0;
- lock!release
- :: getnext[fd] != putnext[fd] ->
- roomwait[fd] = 1;
- lock!release;
- croom[fd]?b
- fi
- :: (BUFSIZ-putnext[fd]) >= READMAX ->
- lock!release
- fi;
- /* simulate read into data buf at putnext */
- if
- :: ntotal[fd] > FILEMAXLEN ->
- num = EOF
- :: ntotal[fd] <= FILEMAXLEN ->
- if
- :: num = 1
- :: num = READMAX
- :: num = EOF
- fi
- fi;
- /* here is where data transfer would happen */
- lock?get;
- if
- :: num == EOF ->
- eof[fd] = 1;
- /* printf("Copy %d got eof\n", fd);/**/
- if
- :: datawait[fd] ->
- datawait[fd] = 0;
- lock!release;
- cdata[fd]!1
- :: !datawait[fd] && (rwant & (1<<fd)) && selwait ->
- selwait = 0;
- lock!release;
- sel!fd
- :: !datawait[fd] && !((rwant & (1<<fd)) && selwait) ->
- lock!release
- fi;
- break
- :: num != EOF ->
- /* printf("Copy %d putting %d in; old putnext=%d, old n=%d\n", fd, num, putnext[fd], n[fd]); /* */
- putnext[fd] = putnext[fd] + num;
- n[fd] = n[fd] + num;
- ntotal[fd] = ntotal[fd] + num;
- assert(n[fd] > 0);
- if
- :: datawait[fd] ->
- datawait[fd] = 0;
- lock!release;
- cdata[fd]!1
- :: !datawait[fd] && (rwant & (1<<fd)) && selwait ->
- selwait = 0;
- lock!release;
- sel!fd
- :: !datawait[fd] && !((rwant & (1<<fd)) && selwait) ->
- lock!release
- fi
- fi;
- od
- }
- proctype Read()
- {
- byte ngot;
- byte fd;
- byte nwant;
- bit b;
- do
- :: readcall?fd,nwant ->
- if
- :: eof[fd] && n[fd] == 0 ->
- readans!EOF
- :: !(eof[fd] && n[fd] == 0) ->
- lock?get;
- ngot = putnext[fd] - getnext[fd];
- /* printf("Reading %d, want %d: ngot = %d - %d, n = %d\n", fd, nwant, putnext[fd], getnext[fd], n[fd]); /* */
- if
- :: ngot == 0 ->
- if
- :: eof[fd] ->
- skip
- :: !eof[fd] ->
- /* sleep until there's data */
- datawait[fd] = 1;
- /* printf("Read sleeping\n"); /* */
- lock!release;
- cdata[fd]?b;
- lock?get;
- ngot = putnext[fd] - getnext[fd];
- /* printf("Read awoke, ngot = %d\n", ngot); /**/
- fi
- :: ngot != 0 -> skip
- fi;
- if
- :: ngot > nwant -> ngot = nwant
- :: ngot <= nwant -> skip
- fi;
- /* here would take ngot elements from data, from getnext[fd] ... */
- getnext[fd] = getnext[fd] + ngot;
- assert(n[fd] >= ngot);
- n[fd] = n[fd] - ngot;
- if
- :: ngot == 0 ->
- assert(eof[fd]);
- ngot = EOF
- :: ngot != 0 -> skip
- fi;
- if
- :: getnext[fd] == putnext[fd] && roomwait[fd] ->
- getnext[fd] = 0;
- putnext[fd] = 0;
- roomwait[fd] = 0;
- lock!release;
- croom[fd]!0
- :: getnext[fd] != putnext[fd] || !roomwait[fd] ->
- lock!release
- fi;
- readans!ngot
- fi
- :: readkill?b -> break
- od
- }
- proctype Select()
- {
- byte num;
- byte i;
- byte fd;
- byte r;
- bit b;
- do
- :: selcall?r ->
- /* printf("Select called, r=%d\n", r); /**/
- i = 0;
- do
- :: i < NBUFS ->
- if
- :: r & (1<<i) ->
- if
- :: eof[i] && n[i] == 0 ->
- /* printf("Select got eof on %d\n", i);/**/
- num = EOF;
- r = i;
- goto donesel
- :: !eof[i] || n[i] != 0 -> skip
- fi
- :: !(r & (1<<i)) -> skip
- fi;
- i = i+1
- :: i >= NBUFS -> break
- od;
- num = 0;
- lock?get;
- rwant = 0;
- i = 0;
- do
- :: i < NBUFS ->
- if
- :: r & (1<<i) ->
- if
- :: n[i] > 0 || eof[i] ->
- /* printf("Select found %d has n==%d\n", i, n[i]); /**/
- num = num+1
- :: n[i] == 0 && !eof[i] ->
- /* printf("Select asks to wait for %d\n", i); /**/
- r = r &(~(1<<i));
- rwant = rwant | (1<<i)
- fi
- :: !(r & (1<<i)) -> skip
- fi;
- i = i+1
- :: i >= NBUFS -> break
- od;
- if
- :: num > 0 || rwant == 0 ->
- rwant = 0;
- lock!release;
- :: num == 0 && rwant != 0 ->
- selwait = 1;
- lock!release;
- /* printf("Select sleeps\n"); /**/
- sel?fd;
- /* printf("Select wakes up, fd=%d\n", fd); /**/
- if
- :: fd != TIMEOUT ->
- if
- :: (rwant & (1<<fd)) && (n[fd] > 0) ->
- r = r | (1<<fd);
- num = 1
- :: !(rwant & (1<<fd)) || (n[fd] == 0) ->
- num = 0
- fi
- :: fd == TIMEOUT -> skip
- fi;
- rwant = 0
- fi;
- donesel:
- selans!num,r
- :: selkill?b -> break
- od
- }
- /* This routine is written knowing NBUFS == 2 in several places */
- proctype User()
- {
- byte ndone;
- byte i;
- byte rw;
- byte num;
- byte nwant;
- byte fd;
- bool goteof[NBUFS];
- ndone = 0;
- do
- :: ndone == NBUFS -> break
- :: ndone < NBUFS ->
- if
- :: 1->
- /* maybe use Read */
- /* printf("User trying to read. Current goteofs: %d %d\n", goteof[0], goteof[1]); /**/
- /* randomly pick fd 0 or 1 from non-eof ones */
- if
- :: !goteof[0] -> fd = 0
- :: !goteof[1] -> fd = 1
- fi;
- if
- :: nwant = 1
- :: nwant = READMAX
- fi;
- readcall!fd,nwant;
- readans?num;
- if
- :: num == EOF ->
- goteof[fd] = 1;
- ndone = ndone + 1
- :: num != EOF -> assert(num != 0)
- fi
- :: 1->
- /* printf("User trying to select. Current goteofs: %d %d\n", goteof[0], goteof[1]); /**/
- /* maybe use Select, then Read */
- /* randomly set the "i want" bit for non-eof fds */
- if
- :: !goteof[0] && !goteof[1] -> rw = (1<<0) | (1<<1)
- :: !goteof[0] -> rw = (1<<0)
- :: !goteof[1] -> rw = (1<<1)
- fi;
- selcall!rw;
- selans?i,rw;
- if
- :: i == EOF ->
- goteof[rw] = 1;
- ndone = ndone + 1
- :: i != EOF ->
- /* this next statement knows NBUFS == 2 ! */
- if
- :: rw & (1<<0) -> fd = 0
- :: rw & (1<<1) -> fd = 1
- :: rw == 0 -> fd = EOF
- fi;
- if
- :: nwant = 1
- :: nwant = READMAX
- fi;
- if
- :: fd != EOF ->
- readcall!fd,nwant;
- readans?num;
- assert(num != 0)
- :: fd == EOF -> skip
- fi
- fi
- fi
- od;
- lockkill!release;
- selkill!release;
- readkill!release
- }
- init
- {
- byte i;
- atomic {
- run Lockrendez();
- i = 0;
- do
- :: i < NBUFS ->
- run Copy(i);
- i = i+1
- :: i >= NBUFS -> break
- od;
- run Select();
- run Read();
- run User()
- }
- }
|