/***** spin: sched.c *****/ /* Copyright (c) 1989-2003 by Lucent Technologies, Bell Laboratories.     *//* All Rights Reserved.  This software is for educational purposes only.  *//* No guarantee whatsoever is expressed or implied by the distribution of *//* this code.  Permission is given to distribute this code provided that  *//* this introductory message is not removed and no monies are exchanged.  *//* Software written by Gerard J. Holzmann.  For tool documentation see:   *//*             http://spinroot.com/                                       *//* Send all bug-reports and/or questions to: bugs@spinroot.com            */ #include <stdlib.h>#include "spin.h"#include "y.tab.h" 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, cutoff;extern short	has_enabled;extern int	limited_vis, old_scope_rules, product, nclaims; 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->b  = p->b;	r->pid = nproc++ - nstop + Skip_claim; 	if (!noparams && ((verbose&4) || (verbose&32)))		printf("Starting %s with pid %d\n",			p->n?p->n->name:"--", r->pid); 	if (!p->s)		fatal("parsing error, no sequence %s",			p->n?p->n->name:"--"); 	r->pc = huntele(p->s->frst, p->s->frst->status, -1);	r->ps = p->s; 	if (p->s->last)		p->s->last->status |= ENDSTATE; /* normal end state */ 	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, enum btypes b)	/* 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->b = b;	r->prov = prov;	r->tn = nrRdy++;	if (det != 0 && det != 1)	{	fprintf(stderr, "spin: bad value for det (cannot happen)\n");	}	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 - Have_claim, run->n->name);			pstext(run->pid - Have_claim, Buf);		} else			printf("proc %d = %s\n",			run->pid - Have_claim, run->n->name);		return;	} 	if (dumptab	||  analyze	||  product	||  s_trail	|| !(verbose&4))		return; 	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");} #ifndef MAXP#define MAXP	255	/* matches max nr of processes in verifier */#endif 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)		{	if (nproc-nstop >= MAXP)			{	printf("spin: too many processes (%d max)\n", MAXP);				break;			}			runnable(p, m->val, 0);			announce((char *) 0);			setparams(run, p, n);			setlocals(run); /* after setparams */			return run->pid - Have_claim + Skip_claim; /* effective simu pid */		}	return 0; /* process not found */} voidcheck_param_count(int i, Lextok *m){	ProcList *p;	Symbol *s = m->sym;	/* proctype name */	Lextok *f, *t;		/* formal pars */	int cnt = 0; 	for (p = rdy; p; p = p->nxt)	{	if (strcmp(s->name, p->n->name) == 0)		{	if (m->lft)	/* actual param list */			{	lineno = m->lft->ln;				Fname  = m->lft->fn;			}			for (f = p->p;   f; f = f->rgt) /* one type at a time */			for (t = f->lft; t; t = t->rgt)	/* count formal params */			{	cnt++;			}			if (i != cnt)			{	printf("spin: saw %d parameters, expected %d\n", i, cnt);				non_fatal("wrong number of parameters", "");			}			break;	}	}} voidstart_claim(int n){	ProcList *p;	RunList  *r, *q = (RunList *) 0; 	for (p = rdy; p; p = p->nxt)		if (p->tn == n && p->b == N_CLAIM)		{	runnable(p, 1, 1);			goto found;		}	printf("spin: couldn't find claim %d (ignored)\n", n);	if (verbose&32)	for (p = rdy; p; p = p->nxt)		printf("\t%d = %s\n", p->tn, p->n->name); 	Skip_claim = 1;	goto done;found:	/* move claim to far end of runlist, and reassign it pid 0 */	if (columns == 2)	{	extern char Buf[];		depth = 0;		sprintf(Buf, "%d:%s", 0, p->n->name);		pstext(0, Buf);		for (r = run; r; r = r->nxt)		{	if (r->b != N_CLAIM)			{	sprintf(Buf, "%d:%s", r->pid+1, r->n->name);				pstext(r->pid+1, Buf);	}	}	} 	if (run->pid == 0) return; /* it is the first process started */ 	q = run; run = run->nxt;	q->pid = 0; q->nxt = (RunList *) 0;	/* remove */done:	Have_claim = 1;	for (r = run; r; r = r->nxt)	{	r->pid = r->pid+Have_claim;	/* adjust */		if (!r->nxt)		{	r->nxt = q;			break;	}	}} intf_pid(char *n){	RunList *r;	int rval = -1; 	for (r = run; r; r = r->nxt)		if (strcmp(n, r->n->name) == 0)		{	if (rval >= 0)			{	printf("spin: remote ref to proctype %s, ", n);				printf("has more than one match: %d and %d\n",					rval, r->pid);			} else				rval = r->pid;		}	return rval;} voidwrapup(int fini){	limited_vis = 0;	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 - Have_claim + Skip_claim);		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 process%s created\n",		nproc - Have_claim + Skip_claim,		(xspin || nproc!=1)?"es":"");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){	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; 	if (e->n)	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 RunList *pickproc(RunList *Y){	SeqList *z; Element *has_else;	short Choices[256];	int j, k, nr_else = 0; 	if (nproc <= nstop+1)	{	X = run;		return NULL;	}	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;			Y = X;			X = X->nxt;			if (!X) { Y = NULL; X = run; }		}	} else	{	int only_choice = -1;		int no_choice = 0, proc_no_ch, proc_k; 		Tval = 0;	/* new 4.2.6 */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);			if (scanf("%64s", buf) == 0)			{	printf("\tno input\n");				goto try_again;			}			j = -1;			if (isdigit((int) 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;		Y = NULL;		for (X = run; X; Y = X, X = X->nxt)		{	if (!X->nxt			||   X->nxt->pid > 255			||   j < Choices[X->nxt->pid])			{				MadeChoice = 1+j-Choices[X->pid];				break;		}	}	}	return Y;}

Lines 1–500 of 1093. Load more