sched.c

对软件进行可达性测试的软件

	printf("warning: never claim not used in random simulation\n");
	if (eventmap)
	printf("warning: trace assertion not used in random simulation\n");

	X = run;
	Y = pickproc(Y);

	while (X)
	{	context = X->n;
		if (X->pc && X->pc->n)
		{	lineno = X->pc->n->ln;
			Fname  = X->pc->n->fn;
		}
		if (cutoff > 0 && depth >= cutoff)
		{	printf("-------------\n");
			printf("depth-limit (-u%d steps) reached\n", cutoff);
			break;
		}
#ifdef PC
		if (xspin && !interactive && --bufmax <= 0)
		{	int c; /* avoid buffer overflow on pc's */
			printf("spin: type return to proceed\n");
			fflush(stdout);
			c = getc(stdin);
			if (c == 'q') wrapup(0);
			bufmax = 100;
		}
#endif
		depth++; LastStep = ZE;
		oX = X;	/* a rendezvous could change it */
		go = 1;
		if (X->prov && X->pc
		&& !(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)
				if (!(e->status & D_ATOM) || (verbose&32)) /* no talking in d_steps */
				{	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 (!(e->status & D_ATOM))
				if (xspin)
					printf("\n");
			}
			if (oX != X
			||  (X->pc->status & (ATOM|D_ATOM)))		/* new 5.0 */
			{	e = silent_moves(e);
				notbeyond = 0;
			}
			oX->pc = e; LastX = X;

			if (!interactive) Tval = 0;
			memset(is_blocked, 0, 256);

			if (X->pc && (X->pc->status & (ATOM|L_ATOM))
			&&  (notbeyond == 0 || oX != X))
			{	if ((X->pc->status & L_ATOM))
					notbeyond = 1;
				continue; /* no process switch */
			}
		} else
		{	depth--;
			if (oX->pc && (oX->pc->status & D_ATOM))
			{	non_fatal("stmnt in d_step blocks", (char *)0);
			}
			if (X->pc
			&&  X->pc->n
			&&  X->pc->n->ntyp == '@'
			&&  X->pid == (nproc-nstop-1))
			{	if (X != run && Y != NULL)
					Y->nxt = X->nxt;
				else
					run = X->nxt;
				nstop++;
				Priority_Sum -= X->priority;
				if (verbose&4)
				{	whoruns(1);
					dotag(stdout, "terminates\n");
				}
				LastX = X;
				if (!interactive) Tval = 0;
				if (nproc == nstop) break;
				memset(is_blocked, 0, 256);
				/* proc X is no longer in runlist */
				X = (X->nxt) ? X->nxt : run;
			} else
			{	if (p_blocked(X->pid))
				{	if (Tval) break;
					Tval = 1;
					if (depth >= jumpsteps)
					{	oX = X;
						X = (RunList *) 0; /* to suppress indent */
						dotag(stdout, "timeout\n");
						X = oX;
		}	}	}	}

		if (!run || !X) break;	/* new 5.0 */

		Y = pickproc(X);
		notbeyond = 0;
	}
	context = ZS;
	wrapup(0);
}

int
complete_rendez(void)
{	RunList *orun = X, *tmp;
	Element  *s_was = LastStep;
	Element *e;
	int j, ointer = interactive;

	if (s_trail)
		return 1;
	if (orun->pc->status & D_ATOM)
		fatal("rv-attempt in d_step sequence", (char *)0);
	Rvous = 1;
	interactive = 0;

	j = (int) Rand()%Priority_Sum;	/* randomize start point */
	X = run;
	while (j - X->priority >= 0)
	{	j -= X->priority;
		X = X->nxt;
		if (!X) X = run;
	}
	for (j = nproc - nstop; j > 0; j--)
	{	if (X != orun
		&& (!X->prov || eval(X->prov))
		&& (e = eval_sub(X->pc)))
		{	if (TstOnly)
			{	X = orun;
				Rvous = 0;
				goto out;
			}
			if ((verbose&32) || (verbose&4))
			{	tmp = orun; orun = X; X = tmp;
				if (!s_was) s_was = X->pc;
				p_talk(s_was, 1);
				printf("	[");
				comment(stdout, s_was->n, 0);
				printf("]\n");
				tmp = orun; orun = X; X = tmp;
				if (!LastStep) LastStep = X->pc;
				p_talk(LastStep, 1);
				printf("	[");
				comment(stdout, LastStep->n, 0);
				printf("]\n");
			}
			Rvous = 0; /* before silent_moves */
			X->pc = silent_moves(e);
out:				interactive = ointer;
			return 1;
		}

		X = X->nxt;
		if (!X) X = run;
	}
	Rvous = 0;
	X = orun;
	interactive = ointer;
	return 0;
}

/***** Runtime - Local Variables *****/

static void
addsymbol(RunList *r, Symbol  *s)
{	Symbol *t;
	int i;

	for (t = r->symtab; t; t = t->next)
		if (strcmp(t->name, s->name) == 0)
			return;		/* it's already there */

	t = (Symbol *) emalloc(sizeof(Symbol));
	t->name = s->name;
	t->type = s->type;
	t->hidden = s->hidden;
	t->nbits  = s->nbits;
	t->nel  = s->nel;
	t->ini  = s->ini;
	t->setat = depth;
	t->context = r->n;
	if (s->type != STRUCT)
	{	if (s->val)	/* if already initialized, copy info */
		{	t->val = (int *) emalloc(s->nel*sizeof(int));
			for (i = 0; i < s->nel; i++)
				t->val[i] = s->val[i];
		} else
			(void) checkvar(t, 0);	/* initialize it */
	} else
	{	if (s->Sval)
			fatal("saw preinitialized struct %s", s->name);
		t->Slst = s->Slst;
		t->Snm  = s->Snm;
		t->owner = s->owner;
	/*	t->context = r->n; */
	}
	t->next = r->symtab;	/* add it */
	r->symtab = t;
}

static void
setlocals(RunList *r)
{	Ordered	*walk;
	Symbol	*sp;
	RunList	*oX = X;

	X = r;
	for (walk = all_names; walk; walk = walk->next)
	{	sp = walk->entry;
		if (sp
		&&  sp->context
		&&  strcmp(sp->context->name, r->n->name) == 0
		&&  sp->Nid >= 0
		&& (sp->type == UNSIGNED
		||  sp->type == BIT
		||  sp->type == MTYPE
		||  sp->type == BYTE
		||  sp->type == CHAN
		||  sp->type == SHORT
		||  sp->type == INT
		||  sp->type == STRUCT))
		{	if (!findloc(sp))
			non_fatal("setlocals: cannot happen '%s'",
				sp->name);
		}
	}
	X = oX;
}

static void
oneparam(RunList *r, Lextok *t, Lextok *a, ProcList *p)
{	int k; int at, ft;
	RunList *oX = X;

	if (!a)
		fatal("missing actual parameters: '%s'", p->n->name);
	if (t->sym->nel != 1)
		fatal("array in parameter list, %s", t->sym->name);
	k = eval(a->lft);

	at = Sym_typ(a->lft);
	X = r;	/* switch context */
	ft = Sym_typ(t);

	if (at != ft && (at == CHAN || ft == CHAN))
	{	char buf[256], tag1[64], tag2[64];
		(void) sputtype(tag1, ft);
		(void) sputtype(tag2, at);
		sprintf(buf, "type-clash in params of %s(..), (%s<-> %s)",
			p->n->name, tag1, tag2);
		non_fatal("%s", buf);
	}
	t->ntyp = NAME;
	addsymbol(r, t->sym);
	(void) setval(t, k);
	
	X = oX;
}

static void
setparams(RunList *r, ProcList *p, Lextok *q)
{	Lextok *f, *a;	/* formal and actual pars */
	Lextok *t;	/* list of pars of 1 type */

	if (q)
	{	lineno = q->ln;
		Fname  = q->fn;
	}
	for (f = p->p, a = q; f; f = f->rgt) /* one type at a time */
	for (t = f->lft; t; t = t->rgt, a = (a)?a->rgt:a)
	{	if (t->ntyp != ',')
			oneparam(r, t, a, p);	/* plain var */
		else
			oneparam(r, t->lft, a, p); /* expanded struct */
	}
}

Symbol *
findloc(Symbol *s)
{	Symbol *r;

	if (!X)
	{	/* fatal("error, cannot eval '%s' (no proc)", s->name); */
		return ZS;
	}
	for (r = X->symtab; r; r = r->next)
		if (strcmp(r->name, s->name) == 0)
			break;
	if (!r)
	{	addsymbol(X, s);
		r = X->symtab;
	}
	return r;
}

int
in_bound(Symbol *r, int n)
{
	if (!r)	return 0;

	if (n >= r->nel || n < 0)
	{	printf("spin: indexing %s[%d] - size is %d\n",
			r->name, n, r->nel);
		non_fatal("indexing array \'%s\'", r->name);
		return 0;
	}
	return 1;
}

int
getlocal(Lextok *sn)
{	Symbol *r, *s = sn->sym;
	int n = eval(sn->lft);

	r = findloc(s);
	if (r && r->type == STRUCT)
		return Rval_struct(sn, r, 1); /* 1 = check init */
	if (in_bound(r, n))
		return cast_val(r->type, r->val[n], r->nbits);
	return 0;
}

int
setlocal(Lextok *p, int m)
{	Symbol *r = findloc(p->sym);
	int n = eval(p->lft);

	if (in_bound(r, n))
	{	if (r->type == STRUCT)
			(void) Lval_struct(p, r, 1, m); /* 1 = check init */
		else
		{
#if 0
			if (r->nbits > 0)
				m = (m & ((1<<r->nbits)-1));
			r->val[n] = m;
#else
			r->val[n] = cast_val(r->type, m, r->nbits);
#endif
			r->setat = depth;
	}	}

	return 1;
}

void
whoruns(int lnr)
{	if (!X) return;

	if (lnr) printf("%3d:	", depth);
	printf("proc ");
	if (Have_claim && X->pid == 0)
		printf(" -");
	else
		printf("%2d", X->pid - Have_claim);
	printf(" (%s) ", X->n->name);
}

static void
talk(RunList *r)
{
	if ((verbose&32) || (verbose&4))
	{	p_talk(r->pc, 1);
		printf("\n");
		if (verbose&1) dumpglobals();
		if (verbose&2) dumplocal(r);
	}
}

void
p_talk(Element *e, int lnr)
{	static int lastnever = -1;
	int newnever = -1;

	if (e && e->n)
		newnever = e->n->ln;

	if (Have_claim && X && X->pid == 0
	&&  lastnever != newnever && e)
	{	if (xspin)
		{	printf("MSC: ~G line %d\n", newnever);
#if 0
			printf("%3d:	proc  - (NEVER) line   %d \"never\" ",
				depth, newnever);
			printf("(state 0)\t[printf('MSC: never\\\\n')]\n");
		} else
		{	printf("%3d:	proc  - (NEVER) line   %d \"never\"\n",
				depth, newnever);
#endif
		}
		lastnever = newnever;
	}

	whoruns(lnr);
	if (e)
	{	printf("line %3d %s (state %d)",
			e->n?e->n->ln:-1,
			e->n?e->n->fn->name:"-",
			e->seqno);
		if (!xspin
		&&  ((e->status&ENDSTATE) || has_lab(e, 2)))	/* 2=end */
		{	printf(" <valid end state>");
		}
	}
}

int
remotelab(Lextok *n)
{	int i;

	lineno = n->ln;
	Fname  = n->fn;
	if (n->sym->type != 0 && n->sym->type != LABEL)
	{	printf("spin: error, type: %d\n", n->sym->type);
		fatal("not a labelname: '%s'", n->sym->name);
	}
	if (n->indstep >= 0)
	{	fatal("remote ref to label '%s' inside d_step",
			n->sym->name);
	}
	if ((i = find_lab(n->sym, n->lft->sym, 1)) == 0)
		fatal("unknown labelname: %s", n->sym->name);
	return i;
}

int
remotevar(Lextok *n)
{	int prno, i, added=0;
	RunList *Y, *oX;
	Lextok *onl;
	Symbol *os;

	lineno = n->ln;
	Fname  = n->fn;

	if (!n->lft->lft)
		prno = f_pid(n->lft->sym->name);
	else
	{	prno = eval(n->lft->lft); /* pid - can cause recursive call */
#if 0
		if (n->lft->lft->ntyp == CONST)	/* user-guessed pid */
#endif
		{	prno += Have_claim;
			added = Have_claim;
	}	}

	if (prno < 0)
		return 0;	/* non-existing process */
#if 0
	i = nproc - nstop;
	for (Y = run; Y; Y = Y->nxt)
	{	--i;
		printf("	%s: i=%d, prno=%d, ->pid=%d\n", Y->n->name, i, prno, Y->pid);
	}
#endif
	i = nproc - nstop;
	for (Y = run; Y; Y = Y->nxt)
	if (--i == prno)
	{	if (strcmp(Y->n->name, n->lft->sym->name) != 0)
		{	printf("spin: remote reference error on '%s[%d]'\n",
				n->lft->sym->name, prno-added);
			non_fatal("refers to wrong proctype '%s'", Y->n->name);
		}
		if (strcmp(n->sym->name, "_p") == 0)
		{	if (Y->pc)
				return Y->pc->seqno;
			/* harmless, can only happen with -t */
			return 0;
		}
#if 1
		/* new 4.0 allow remote variables */
		oX = X;
		X = Y;

		onl = n->lft;
		n->lft = n->rgt;

		os = n->sym;
		n->sym = findloc(n->sym);

		i = getval(n);

		n->sym = os;
		n->lft = onl;
		X = oX;
		return i;
#else
		break;
#endif
	}
	printf("remote ref: %s[%d] ", n->lft->sym->name, prno-added);
	non_fatal("%s not found", n->sym->name);
	printf("have only:\n");
	i = nproc - nstop - 1;
	for (Y = run; Y; Y = Y->nxt, i--)
		if (!strcmp(Y->n->name, n->lft->sym->name))
		printf("\t%d\t%s\n", i, Y->n->name);

	return 0;
}