Import sources from 2011-03-30 iso image

1 files changed, 1025 insertions, 0 deletions

diff --git a/sys/src/cmd/spin/sched.c b/sys/src/cmd/spin/sched.c
new file mode 100755
index 000000000..ee5b87403
--- /dev/null
+++ b/sys/src/cmd/spin/sched.c
@@ -0,0 +1,1025 @@
+/***** 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;
+
+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 *);
+
+void
+runnable(ProcList *p, int weight, int noparams)
+{	RunList *r = (RunList *) emalloc(sizeof(RunList));
+
+	r->n  = p->n;
+	r->tn = p->tn;
+	r->pid = nproc++ - nstop + Skip_claim;
+
+	if ((verbose&4) || (verbose&32))
+		printf("Starting %s with pid %d\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)
+	/* 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;
+}
+
+int
+find_maxel(Symbol *s)
+{	ProcList *p;
+
+	for (p = rdy; p; p = p->nxt)
+		if (p->n == s)
+			return p->s->maxel++;
+	return Elcnt++;
+}
+
+static void
+formdump(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--;
+		}
+	}
+}
+
+void
+announce(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
+	||  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
+
+int
+enable(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 */
+}
+
+void
+check_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;
+	}	}
+}
+
+void
+start_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, and reassign it 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; /* 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;
+	}	}
+}
+
+int
+f_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;
+}
+
+void
+wrapup(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 int
+p_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);
+			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;
+		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;
+}
+
+void
+sched(void)
+{	Element *e;
+	RunList *Y = NULL;	/* previous process in run queue */
+	RunList *oX;
+	int go, notbeyond = 0;
+#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");
+
+	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 && 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)
+			{	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->status & D_ATOM)
+			 non_fatal("stmnt in d_step blocks", (char *)0);
+
+			if (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;
+		}	}	}	}
+		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[128], 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;
+}