Subversion Repositories planix.SVN

#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()

	}

}