ref: f35d5ee5b036b7b4fa59b1839f52fca15b7f99f9
dir: /sys/src/ape/lib/ap/plan9/buf.prom/
#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()
}
}