/***** spin: sched.c *****/ /* Copyright (c) 1991-2000 by Lucent Technologies - Bell Laboratories     *//* All Rights Reserved.  This software is for educational purposes only.  *//* Permission is given to distribute this code provided that this intro-  *//* ductory message is not removed and no monies are exchanged.            *//* No guarantee is expressed or implied by the distribution of this code. *//* Software written by Gerard J. Holzmann as part of the book:            *//* `Design and Validation of Computer Protocols,' ISBN 0-13-539925-4,     *//* Prentice Hall, Englewood Cliffs, NJ, 07632.                            *//* Send bug-reports and/or questions to: gerard@research.bell-labs.com    */ #include <stdlib.h>#include "spin.h"#ifdef PC#include "y_tab.h"#else#include "y.tab.h"#endif extern int	verbose, s_trail, analyze, no_wrapup;extern char	*claimproc, *eventmap, Buf[];extern Ordered	*all_names;extern Symbol	*Fname, *context;extern int	lineno, nr_errs, dumptab, xspin, jumpsteps, columns;extern int	u_sync, Elcnt, interactive, TstOnly;extern short	has_enabled, has_provided; RunList		*X   = (RunList  *) 0;RunList		*run = (RunList  *) 0;RunList		*LastX  = (RunList  *) 0; /* previous executing proc */ProcList	*rdy = (ProcList *) 0;Element		*LastStep = ZE;int		nproc=0, nstop=0, Tval=0;int		Rvous=0, depth=0, nrRdy=0, MadeChoice;short		Have_claim=0, Skip_claim=0; static int	Priority_Sum = 0;static void	setlocals(RunList *);static void	setparams(RunList *, ProcList *, Lextok *);static void	talk(RunList *); voidrunnable(ProcList *p, int weight, int noparams){	RunList *r = (RunList *) emalloc(sizeof(RunList)); 	r->n  = p->n;	r->tn = p->tn;	r->pid = ++nproc-nstop-1;	r->pc = huntele(p->s->frst, p->s->frst->status);	r->ps = p->s;	if (p->s && p->s->last)		p->s->last->status |= ENDSTATE; /* normal endstate */	r->nxt = run;	r->prov = p->prov;	r->priority = weight;	if (noparams) setlocals(r);	Priority_Sum += weight;	run = r;} ProcList *ready(Symbol *n, Lextok *p, Sequence *s, int det, Lextok *prov)	/* n=name, p=formals, s=body det=deterministic prov=provided */{	ProcList *r = (ProcList *) emalloc(sizeof(ProcList));	Lextok *fp, *fpt; int j; extern int Npars; 	r->n = n;	r->p = p;	r->s = s;	r->prov = prov;	r->tn = nrRdy++;	r->det = (short) det;	r->nxt = rdy;	rdy = r; 	for (fp  = p, j = 0;  fp;  fp = fp->rgt)	for (fpt = fp->lft;  fpt; fpt = fpt->rgt)		j++;	/* count # of parameters */	Npars = max(Npars, j); 	return rdy;} intfind_maxel(Symbol *s){	ProcList *p; 	for (p = rdy; p; p = p->nxt)		if (p->n == s)			return p->s->maxel++;	return Elcnt++;} static voidformdump(void){	ProcList *p;	Lextok *f, *t;	int cnt; 	for (p = rdy; p; p = p->nxt)	{	if (!p->p) continue;		cnt = -1;		for (f = p->p; f; f = f->rgt)	/* types */		for (t = f->lft; t; t = t->rgt)	/* formals */		{	if (t->ntyp != ',')				t->sym->Nid = cnt--;	/* overload Nid */			else				t->lft->sym->Nid = cnt--;		}	}} voidannounce(char *w){	if (columns)	{	extern char Buf[];		extern int firstrow;		firstrow = 1;		if (columns == 2)		{	sprintf(Buf, "%d:%s",			run->pid, run->n->name);			pstext(run->pid, Buf);		} else			printf("proc %d = %s\n",			run->pid - Have_claim, run->n->name);		return;	}#if 1	if (dumptab	||  analyze	||  s_trail	|| !(verbose&4))		return;#endif	if (w)		printf("  0:	proc - (%s) ", w);	else		whoruns(1);	printf("creates proc %2d (%s)",		run->pid - Have_claim,		run->n->name);	if (run->priority > 1)		printf(" priority %d", run->priority);	printf("\n");} intenable(Lextok *m){	ProcList *p;	Symbol *s = m->sym;	/* proctype name */	Lextok *n = m->lft;	/* actual parameters */ 	if (m->val < 1) m->val = 1;	/* minimum priority */	for (p = rdy; p; p = p->nxt)		if (strcmp(s->name, p->n->name) == 0)		{	runnable(p, m->val, 0);			announce((char *) 0);			setparams(run, p, n);			setlocals(run); /* after setparams */			return run->pid - Have_claim;	/* pid */		}	return 0; /* process not found */} voidstart_claim(int n){	ProcList *p;	RunList  *r, *q = (RunList *) 0; 	for (p = rdy; p; p = p->nxt)		if (p->tn == n		&&  strcmp(p->n->name, ":never:") == 0)		{	runnable(p, 1, 1);			goto found;		}	printf("spin: couldn't find claim (ignored)\n");	Skip_claim = 1;	goto done;found:	/* move claim to far end of runlist, with pid 0 */	if (columns == 2)	{	depth = 0;		pstext(0, "0::never:");		for (r = run; r; r = r->nxt)		{	if (!strcmp(r->n->name, ":never:"))				continue;			sprintf(Buf, "%d:%s",				r->pid+1, r->n->name);			pstext(r->pid+1, Buf);	}	}	if (run->pid == 0) return;	/* already there */ 	q = run; run = run->nxt;	q->pid = 0; q->nxt = (RunList *) 0;done:	for (r = run; r; r = r->nxt)	{	r->pid = r->pid+1;		if (!r->nxt)		{	r->nxt = q;			break;	}	}	Have_claim = 1;} voidwrapup(int fini){	if (columns)	{	extern void putpostlude(void);		if (columns == 2) putpostlude();		if (!no_wrapup)		printf("-------------\nfinal state:\n-------------\n");	}	if (no_wrapup)		goto short_cut;	if (nproc != nstop)	{	int ov = verbose;		printf("#processes: %d\n", nproc-nstop);		verbose &= ~4;		dumpglobals();		verbose = ov;		verbose &= ~1;	/* no more globals */		verbose |= 32;	/* add process states */		for (X = run; X; X = X->nxt)			talk(X);		verbose = ov;	/* restore */	}	printf("%d processes created\n", nproc);short_cut:	if (xspin) alldone(0);	/* avoid an abort from xspin */	if (fini)  alldone(1);} static char is_blocked[256]; static intp_blocked(int p){	register int i, j; 	is_blocked[p%256] = 1;	for (i = j = 0; i < nproc - nstop; i++)		j += is_blocked[i];	if (j >= nproc - nstop)	{	memset(is_blocked, 0, 256);		return 1;	}	return 0;} static Element *silent_moves(Element *e){	Element *f; 	switch (e->n->ntyp) {	case GOTO:		if (Rvous) break;		f = get_lab(e->n, 1);		cross_dsteps(e->n, f->n);		return f; /* guard against goto cycles */	case UNLESS:		return silent_moves(e->sub->this->frst);	case NON_ATOMIC:	case ATOMIC:	case D_STEP:		e->n->sl->this->last->nxt = e->nxt;		return silent_moves(e->n->sl->this->frst);	case '.':		return silent_moves(e->nxt);	}	return e;} static voidpickproc(void){	SeqList *z; Element *has_else;	short Choices[256];	int j, k, nr_else; 	if (nproc <= nstop+1)	{	X = run;		return;	}	if (!interactive || depth < jumpsteps)	{	/* was: j = (int) Rand()%(nproc-nstop); */		if (Priority_Sum < nproc-nstop)			fatal("cannot happen - weights", (char *)0);		j = (int) Rand()%Priority_Sum;		while (j - X->priority >= 0)		{	j -= X->priority;			X = X->nxt;			if (!X) X = run;		}	} else	{	int only_choice = -1;		int no_choice = 0, proc_no_ch, proc_k;try_again:	printf("Select a statement\n");try_more:	for (X = run, k = 1; X; X = X->nxt)		{	if (X->pid > 255) break; 			Choices[X->pid] = (short) k; 			if (!X->pc			||  (X->prov && !eval(X->prov)))			{	if (X == run)					Choices[X->pid] = 0;				continue;			}			X->pc = silent_moves(X->pc);			if (!X->pc->sub && X->pc->n)			{	int unex;				unex = !Enabled0(X->pc);				if (unex)					no_choice++;				else					only_choice = k;				if (!xspin && unex && !(verbose&32))				{	k++;					continue;				}				printf("\tchoice %d: ", k++);				p_talk(X->pc, 0);				if (unex)					printf(" unexecutable,");				printf(" [");				comment(stdout, X->pc->n, 0);				if (X->pc->esc) printf(" + Escape");				printf("]\n");			} else {			has_else = ZE;			proc_no_ch = no_choice;			proc_k = k;			for (z = X->pc->sub, j=0; z; z = z->nxt)			{	Element *y = silent_moves(z->this->frst);				int unex;				if (!y) continue; 				if (y->n->ntyp == ELSE)				{	has_else = (Rvous)?ZE:y;					nr_else = k++;					continue;				} 				unex = !Enabled0(y);				if (unex)					no_choice++;				else					only_choice = k;				if (!xspin && unex && !(verbose&32))				{	k++;					continue;				}				printf("\tchoice %d: ", k++);				p_talk(X->pc, 0);				if (unex)					printf(" unexecutable,");				printf(" [");				comment(stdout, y->n, 0);				printf("]\n");			}			if (has_else)			{	if (no_choice-proc_no_ch >= (k-proc_k)-1)				{	only_choice = nr_else;					printf("\tchoice %d: ", nr_else);					p_talk(X->pc, 0);					printf(" [else]\n");				} else				{	no_choice++;					printf("\tchoice %d: ", nr_else);					p_talk(X->pc, 0);					printf(" unexecutable, [else]\n");			}	}		}	}		X = run;		if (k - no_choice < 2 && Tval == 0)		{	Tval = 1;			no_choice = 0; only_choice = -1;			goto try_more;		}		if (xspin)			printf("Make Selection %d\n\n", k-1);		else		{	if (k - no_choice < 2)			{	printf("no executable choices\n");				alldone(0);			}			printf("Select [1-%d]: ", k-1);		}		if (!xspin && k - no_choice == 2)		{	printf("%d\n", only_choice);			j = only_choice;		} else		{	char buf[256];			fflush(stdout);			scanf("%s", buf);			j = -1;			if (isdigit(buf[0]))				j = atoi(buf);			else			{	if (buf[0] == 'q')					alldone(0);			}			if (j < 1 || j >= k)			{	printf("\tchoice is outside range\n");				goto try_again;		}	}		MadeChoice = 0;		for (X = run; X; X = X->nxt)		{	if (!X->nxt			||   X->nxt->pid > 255			||   j < Choices[X->nxt->pid])			{				MadeChoice = 1+j-Choices[X->pid];				break;		}	}	}} voidsched(void){	Element *e;	RunList *Y=0;	/* previous process in run queue */	RunList *oX;	int go, notbeyond;#ifdef PC	int bufmax = 100;#endif	if (dumptab)	{	formdump();		symdump();		dumplabels();		return;	} 	if (has_enabled && u_sync > 0)	{	printf("spin: error, cannot use 'enabled()' in ");		printf("models with synchronous channels.\n");		nr_errs++;	}	if (analyze)	{	gensrc();		return;	} else if (s_trail)	{	match_trail();		return;	}	if (claimproc)	printf("warning: never claim not used in random simulation\n");	if (eventmap)	printf("warning: trace assertion not used in random simulation\n"); /*	if (interactive) Tval = 1; */ 	X = run;	pickproc();	notbeyond = 0; 	while (X)	{	context = X->n;		if (X->pc && X->pc->n)		{	lineno = X->pc->n->ln;			Fname  = X->pc->n->fn;		}#ifdef PC		if (xspin && !interactive && --bufmax <= 0)		{	/* avoid buffer overflow on pc's */			printf("spin: type return to proceed\n");			fflush(stdout);			getc(stdin);			bufmax = 100;		}#endif		depth++; LastStep = ZE;		oX = X;	/* a rendezvous could change it */		go = 1;		if (X && X->prov		&& !(X->pc->status & D_ATOM)		&& !eval(X->prov))		{	if (!xspin && ((verbose&32) || (verbose&4)))			{	p_talk(X->pc, 1);				printf("\t<<Not Enabled>>\n");			}			go = 0;		}		if (go && (e = eval_sub(X->pc)))		{	if (depth >= jumpsteps			&& ((verbose&32) || (verbose&4)))			{	if (X == oX)				{	p_talk(X->pc, 1);					printf("	[");					if (!LastStep) LastStep = X->pc;					comment(stdout, LastStep->n, 0);					printf("]\n");				}				if (verbose&1) dumpglobals();				if (verbose&2) dumplocal(X);				if (xspin) printf("\n");			}			if (oX != X)  e = silent_moves(e);

Lines 1–500 of 904. Load more