xref: /plan9/sys/src/cmd/spin/sched.c (revision 00d970127b9d44d2b22f4f656717a212dec1f1d2)
1 /***** spin: sched.c *****/
2 
3 /* Copyright (c) 1989-2003 by Lucent Technologies, Bell Laboratories.     */
4 /* All Rights Reserved.  This software is for educational purposes only.  */
5 /* No guarantee whatsoever is expressed or implied by the distribution of */
6 /* this code.  Permission is given to distribute this code provided that  */
7 /* this introductory message is not removed and no monies are exchanged.  */
8 /* Software written by Gerard J. Holzmann.  For tool documentation see:   */
9 /*             http://spinroot.com/                                       */
10 /* Send all bug-reports and/or questions to: bugs@spinroot.com            */
11 
12 #include <stdlib.h>
13 #include "spin.h"
14 #include "y.tab.h"
15 
16 extern int	verbose, s_trail, analyze, no_wrapup;
17 extern char	*claimproc, *eventmap, Buf[];
18 extern Ordered	*all_names;
19 extern Symbol	*Fname, *context;
20 extern int	lineno, nr_errs, dumptab, xspin, jumpsteps, columns;
21 extern int	u_sync, Elcnt, interactive, TstOnly, cutoff;
22 extern short	has_enabled;
23 extern int	limited_vis, old_scope_rules, product, nclaims;
24 
25 RunList		*X   = (RunList  *) 0;
26 RunList		*run = (RunList  *) 0;
27 RunList		*LastX  = (RunList  *) 0; /* previous executing proc */
28 ProcList	*rdy = (ProcList *) 0;
29 Element		*LastStep = ZE;
30 int		nproc=0, nstop=0, Tval=0;
31 int		Rvous=0, depth=0, nrRdy=0, MadeChoice;
32 short		Have_claim=0, Skip_claim=0;
33 
34 static int	Priority_Sum = 0;
35 static void	setlocals(RunList *);
36 static void	setparams(RunList *, ProcList *, Lextok *);
37 static void	talk(RunList *);
38 
39 void
runnable(ProcList * p,int weight,int noparams)40 runnable(ProcList *p, int weight, int noparams)
41 {	RunList *r = (RunList *) emalloc(sizeof(RunList));
42 
43 	r->n  = p->n;
44 	r->tn = p->tn;
45 	r->b  = p->b;
46 	r->pid = nproc++ - nstop + Skip_claim;
47 
48 	if (!noparams && ((verbose&4) || (verbose&32)))
49 		printf("Starting %s with pid %d\n",
50 			p->n?p->n->name:"--", r->pid);
51 
52 	if (!p->s)
53 		fatal("parsing error, no sequence %s",
54 			p->n?p->n->name:"--");
55 
56 	r->pc = huntele(p->s->frst, p->s->frst->status, -1);
57 	r->ps = p->s;
58 
59 	if (p->s->last)
60 		p->s->last->status |= ENDSTATE; /* normal end state */
61 
62 	r->nxt = run;
63 	r->prov = p->prov;
64 	r->priority = weight;
65 
66 	if (noparams) setlocals(r);
67 	Priority_Sum += weight;
68 
69 	run = r;
70 }
71 
72 ProcList *
ready(Symbol * n,Lextok * p,Sequence * s,int det,Lextok * prov,enum btypes b)73 ready(Symbol *n, Lextok *p, Sequence *s, int det, Lextok *prov, enum btypes b)
74 	/* n=name, p=formals, s=body det=deterministic prov=provided */
75 {	ProcList *r = (ProcList *) emalloc(sizeof(ProcList));
76 	Lextok *fp, *fpt; int j; extern int Npars;
77 
78 	r->n = n;
79 	r->p = p;
80 	r->s = s;
81 	r->b = b;
82 	r->prov = prov;
83 	r->tn = nrRdy++;
84 	if (det != 0 && det != 1)
85 	{	fprintf(stderr, "spin: bad value for det (cannot happen)\n");
86 	}
87 	r->det = (short) det;
88 	r->nxt = rdy;
89 	rdy = r;
90 
91 	for (fp  = p, j = 0;  fp;  fp = fp->rgt)
92 	for (fpt = fp->lft;  fpt; fpt = fpt->rgt)
93 		j++;	/* count # of parameters */
94 	Npars = max(Npars, j);
95 
96 	return rdy;
97 }
98 
99 int
find_maxel(Symbol * s)100 find_maxel(Symbol *s)
101 {	ProcList *p;
102 
103 	for (p = rdy; p; p = p->nxt)
104 		if (p->n == s)
105 			return p->s->maxel++;
106 	return Elcnt++;
107 }
108 
109 static void
formdump(void)110 formdump(void)
111 {	ProcList *p;
112 	Lextok *f, *t;
113 	int cnt;
114 
115 	for (p = rdy; p; p = p->nxt)
116 	{	if (!p->p) continue;
117 		cnt = -1;
118 		for (f = p->p; f; f = f->rgt)	/* types */
119 		for (t = f->lft; t; t = t->rgt)	/* formals */
120 		{	if (t->ntyp != ',')
121 				t->sym->Nid = cnt--;	/* overload Nid */
122 			else
123 				t->lft->sym->Nid = cnt--;
124 		}
125 	}
126 }
127 
128 void
announce(char * w)129 announce(char *w)
130 {
131 	if (columns)
132 	{	extern char Buf[];
133 		extern int firstrow;
134 		firstrow = 1;
135 		if (columns == 2)
136 		{	sprintf(Buf, "%d:%s",
137 			run->pid - Have_claim, run->n->name);
138 			pstext(run->pid - Have_claim, Buf);
139 		} else
140 			printf("proc %d = %s\n",
141 			run->pid - Have_claim, run->n->name);
142 		return;
143 	}
144 
145 	if (dumptab
146 	||  analyze
147 	||  product
148 	||  s_trail
149 	|| !(verbose&4))
150 		return;
151 
152 	if (w)
153 		printf("  0:	proc  - (%s) ", w);
154 	else
155 		whoruns(1);
156 	printf("creates proc %2d (%s)",
157 		run->pid - Have_claim,
158 		run->n->name);
159 	if (run->priority > 1)
160 		printf(" priority %d", run->priority);
161 	printf("\n");
162 }
163 
164 #ifndef MAXP
165 #define MAXP	255	/* matches max nr of processes in verifier */
166 #endif
167 
168 int
enable(Lextok * m)169 enable(Lextok *m)
170 {	ProcList *p;
171 	Symbol *s = m->sym;	/* proctype name */
172 	Lextok *n = m->lft;	/* actual parameters */
173 
174 	if (m->val < 1) m->val = 1;	/* minimum priority */
175 	for (p = rdy; p; p = p->nxt)
176 		if (strcmp(s->name, p->n->name) == 0)
177 		{	if (nproc-nstop >= MAXP)
178 			{	printf("spin: too many processes (%d max)\n", MAXP);
179 				break;
180 			}
181 			runnable(p, m->val, 0);
182 			announce((char *) 0);
183 			setparams(run, p, n);
184 			setlocals(run); /* after setparams */
185 			return run->pid - Have_claim + Skip_claim; /* effective simu pid */
186 		}
187 	return 0; /* process not found */
188 }
189 
190 void
check_param_count(int i,Lextok * m)191 check_param_count(int i, Lextok *m)
192 {	ProcList *p;
193 	Symbol *s = m->sym;	/* proctype name */
194 	Lextok *f, *t;		/* formal pars */
195 	int cnt = 0;
196 
197 	for (p = rdy; p; p = p->nxt)
198 	{	if (strcmp(s->name, p->n->name) == 0)
199 		{	if (m->lft)	/* actual param list */
200 			{	lineno = m->lft->ln;
201 				Fname  = m->lft->fn;
202 			}
203 			for (f = p->p;   f; f = f->rgt) /* one type at a time */
204 			for (t = f->lft; t; t = t->rgt)	/* count formal params */
205 			{	cnt++;
206 			}
207 			if (i != cnt)
208 			{	printf("spin: saw %d parameters, expected %d\n", i, cnt);
209 				non_fatal("wrong number of parameters", "");
210 			}
211 			break;
212 	}	}
213 }
214 
215 void
start_claim(int n)216 start_claim(int n)
217 {	ProcList *p;
218 	RunList  *r, *q = (RunList *) 0;
219 
220 	for (p = rdy; p; p = p->nxt)
221 		if (p->tn == n && p->b == N_CLAIM)
222 		{	runnable(p, 1, 1);
223 			goto found;
224 		}
225 	printf("spin: couldn't find claim %d (ignored)\n", n);
226 	if (verbose&32)
227 	for (p = rdy; p; p = p->nxt)
228 		printf("\t%d = %s\n", p->tn, p->n->name);
229 
230 	Skip_claim = 1;
231 	goto done;
232 found:
233 	/* move claim to far end of runlist, and reassign it pid 0 */
234 	if (columns == 2)
235 	{	extern char Buf[];
236 		depth = 0;
237 		sprintf(Buf, "%d:%s", 0, p->n->name);
238 		pstext(0, Buf);
239 		for (r = run; r; r = r->nxt)
240 		{	if (r->b != N_CLAIM)
241 			{	sprintf(Buf, "%d:%s", r->pid+1, r->n->name);
242 				pstext(r->pid+1, Buf);
243 	}	}	}
244 
245 	if (run->pid == 0) return; /* it is the first process started */
246 
247 	q = run; run = run->nxt;
248 	q->pid = 0; q->nxt = (RunList *) 0;	/* remove */
249 done:
250 	Have_claim = 1;
251 	for (r = run; r; r = r->nxt)
252 	{	r->pid = r->pid+Have_claim;	/* adjust */
253 		if (!r->nxt)
254 		{	r->nxt = q;
255 			break;
256 	}	}
257 }
258 
259 int
f_pid(char * n)260 f_pid(char *n)
261 {	RunList *r;
262 	int rval = -1;
263 
264 	for (r = run; r; r = r->nxt)
265 		if (strcmp(n, r->n->name) == 0)
266 		{	if (rval >= 0)
267 			{	printf("spin: remote ref to proctype %s, ", n);
268 				printf("has more than one match: %d and %d\n",
269 					rval, r->pid);
270 			} else
271 				rval = r->pid;
272 		}
273 	return rval;
274 }
275 
276 void
wrapup(int fini)277 wrapup(int fini)
278 {
279 	limited_vis = 0;
280 	if (columns)
281 	{	extern void putpostlude(void);
282 		if (columns == 2) putpostlude();
283 		if (!no_wrapup)
284 		printf("-------------\nfinal state:\n-------------\n");
285 	}
286 	if (no_wrapup)
287 		goto short_cut;
288 	if (nproc != nstop)
289 	{	int ov = verbose;
290 		printf("#processes: %d\n", nproc-nstop - Have_claim + Skip_claim);
291 		verbose &= ~4;
292 		dumpglobals();
293 		verbose = ov;
294 		verbose &= ~1;	/* no more globals */
295 		verbose |= 32;	/* add process states */
296 		for (X = run; X; X = X->nxt)
297 			talk(X);
298 		verbose = ov;	/* restore */
299 	}
300 	printf("%d process%s created\n",
301 		nproc - Have_claim + Skip_claim,
302 		(xspin || nproc!=1)?"es":"");
303 short_cut:
304 	if (xspin) alldone(0);	/* avoid an abort from xspin */
305 	if (fini)  alldone(1);
306 }
307 
308 static char is_blocked[256];
309 
310 static int
p_blocked(int p)311 p_blocked(int p)
312 {	int i, j;
313 
314 	is_blocked[p%256] = 1;
315 	for (i = j = 0; i < nproc - nstop; i++)
316 		j += is_blocked[i];
317 	if (j >= nproc - nstop)
318 	{	memset(is_blocked, 0, 256);
319 		return 1;
320 	}
321 	return 0;
322 }
323 
324 static Element *
silent_moves(Element * e)325 silent_moves(Element *e)
326 {	Element *f;
327 
328 	if (e->n)
329 	switch (e->n->ntyp) {
330 	case GOTO:
331 		if (Rvous) break;
332 		f = get_lab(e->n, 1);
333 		cross_dsteps(e->n, f->n);
334 		return f; /* guard against goto cycles */
335 	case UNLESS:
336 		return silent_moves(e->sub->this->frst);
337 	case NON_ATOMIC:
338 	case ATOMIC:
339 	case D_STEP:
340 		e->n->sl->this->last->nxt = e->nxt;
341 		return silent_moves(e->n->sl->this->frst);
342 	case '.':
343 		return silent_moves(e->nxt);
344 	}
345 	return e;
346 }
347 
348 static RunList *
pickproc(RunList * Y)349 pickproc(RunList *Y)
350 {	SeqList *z; Element *has_else;
351 	short Choices[256];
352 	int j, k, nr_else = 0;
353 
354 	if (nproc <= nstop+1)
355 	{	X = run;
356 		return NULL;
357 	}
358 	if (!interactive || depth < jumpsteps)
359 	{	/* was: j = (int) Rand()%(nproc-nstop); */
360 		if (Priority_Sum < nproc-nstop)
361 			fatal("cannot happen - weights", (char *)0);
362 		j = (int) Rand()%Priority_Sum;
363 
364 		while (j - X->priority >= 0)
365 		{	j -= X->priority;
366 			Y = X;
367 			X = X->nxt;
368 			if (!X) { Y = NULL; X = run; }
369 		}
370 	} else
371 	{	int only_choice = -1;
372 		int no_choice = 0, proc_no_ch, proc_k;
373 
374 		Tval = 0;	/* new 4.2.6 */
375 try_again:	printf("Select a statement\n");
376 try_more:	for (X = run, k = 1; X; X = X->nxt)
377 		{	if (X->pid > 255) break;
378 
379 			Choices[X->pid] = (short) k;
380 
381 			if (!X->pc
382 			||  (X->prov && !eval(X->prov)))
383 			{	if (X == run)
384 					Choices[X->pid] = 0;
385 				continue;
386 			}
387 			X->pc = silent_moves(X->pc);
388 			if (!X->pc->sub && X->pc->n)
389 			{	int unex;
390 				unex = !Enabled0(X->pc);
391 				if (unex)
392 					no_choice++;
393 				else
394 					only_choice = k;
395 				if (!xspin && unex && !(verbose&32))
396 				{	k++;
397 					continue;
398 				}
399 				printf("\tchoice %d: ", k++);
400 				p_talk(X->pc, 0);
401 				if (unex)
402 					printf(" unexecutable,");
403 				printf(" [");
404 				comment(stdout, X->pc->n, 0);
405 				if (X->pc->esc) printf(" + Escape");
406 				printf("]\n");
407 			} else {
408 			has_else = ZE;
409 			proc_no_ch = no_choice;
410 			proc_k = k;
411 			for (z = X->pc->sub, j=0; z; z = z->nxt)
412 			{	Element *y = silent_moves(z->this->frst);
413 				int unex;
414 				if (!y) continue;
415 
416 				if (y->n->ntyp == ELSE)
417 				{	has_else = (Rvous)?ZE:y;
418 					nr_else = k++;
419 					continue;
420 				}
421 
422 				unex = !Enabled0(y);
423 				if (unex)
424 					no_choice++;
425 				else
426 					only_choice = k;
427 				if (!xspin && unex && !(verbose&32))
428 				{	k++;
429 					continue;
430 				}
431 				printf("\tchoice %d: ", k++);
432 				p_talk(X->pc, 0);
433 				if (unex)
434 					printf(" unexecutable,");
435 				printf(" [");
436 				comment(stdout, y->n, 0);
437 				printf("]\n");
438 			}
439 			if (has_else)
440 			{	if (no_choice-proc_no_ch >= (k-proc_k)-1)
441 				{	only_choice = nr_else;
442 					printf("\tchoice %d: ", nr_else);
443 					p_talk(X->pc, 0);
444 					printf(" [else]\n");
445 				} else
446 				{	no_choice++;
447 					printf("\tchoice %d: ", nr_else);
448 					p_talk(X->pc, 0);
449 					printf(" unexecutable, [else]\n");
450 			}	}
451 		}	}
452 		X = run;
453 		if (k - no_choice < 2 && Tval == 0)
454 		{	Tval = 1;
455 			no_choice = 0; only_choice = -1;
456 			goto try_more;
457 		}
458 		if (xspin)
459 			printf("Make Selection %d\n\n", k-1);
460 		else
461 		{	if (k - no_choice < 2)
462 			{	printf("no executable choices\n");
463 				alldone(0);
464 			}
465 			printf("Select [1-%d]: ", k-1);
466 		}
467 		if (!xspin && k - no_choice == 2)
468 		{	printf("%d\n", only_choice);
469 			j = only_choice;
470 		} else
471 		{	char buf[256];
472 			fflush(stdout);
473 			if (scanf("%64s", buf) == 0)
474 			{	printf("\tno input\n");
475 				goto try_again;
476 			}
477 			j = -1;
478 			if (isdigit((int) buf[0]))
479 				j = atoi(buf);
480 			else
481 			{	if (buf[0] == 'q')
482 					alldone(0);
483 			}
484 			if (j < 1 || j >= k)
485 			{	printf("\tchoice is outside range\n");
486 				goto try_again;
487 		}	}
488 		MadeChoice = 0;
489 		Y = NULL;
490 		for (X = run; X; Y = X, X = X->nxt)
491 		{	if (!X->nxt
492 			||   X->nxt->pid > 255
493 			||   j < Choices[X->nxt->pid])
494 			{
495 				MadeChoice = 1+j-Choices[X->pid];
496 				break;
497 		}	}
498 	}
499 	return Y;
500 }
501 
502 void
multi_claims(void)503 multi_claims(void)
504 {	ProcList *p, *q = NULL;
505 
506 	if (nclaims > 1)
507 	{	printf("  the model contains %d never claims:", nclaims);
508 		for (p = rdy; p; p = p->nxt)
509 		{	if (p->b == N_CLAIM)
510 			{	printf("%s%s", q?", ":" ", p->n->name);
511 				q = p;
512 		}	}
513 		printf("\n");
514 		printf("  only one claim is used in a verification run\n");
515 		printf("  choose which one with ./pan -N name (defaults to -N %s)\n",
516 			q?q->n->name:"--");
517 	}
518 }
519 
520 void
sched(void)521 sched(void)
522 {	Element *e;
523 	RunList *Y = NULL;	/* previous process in run queue */
524 	RunList *oX;
525 	int go, notbeyond = 0;
526 #ifdef PC
527 	int bufmax = 100;
528 #endif
529 	if (dumptab)
530 	{	formdump();
531 		symdump();
532 		dumplabels();
533 		return;
534 	}
535 
536 	if (has_enabled && u_sync > 0)
537 	{	printf("spin: error, cannot use 'enabled()' in ");
538 		printf("models with synchronous channels.\n");
539 		nr_errs++;
540 	}
541 	if (product)
542 	{	sync_product();
543 		alldone(0);
544 	}
545 	if (analyze)
546 	{	gensrc();
547 		multi_claims();
548 		return;
549 	}
550 	if (s_trail)
551 	{	match_trail();
552 		return;
553 	}
554 	if (claimproc)
555 	printf("warning: never claim not used in random simulation\n");
556 	if (eventmap)
557 	printf("warning: trace assertion not used in random simulation\n");
558 
559 	X = run;
560 	Y = pickproc(Y);
561 
562 	while (X)
563 	{	context = X->n;
564 		if (X->pc && X->pc->n)
565 		{	lineno = X->pc->n->ln;
566 			Fname  = X->pc->n->fn;
567 		}
568 		if (cutoff > 0 && depth >= cutoff)
569 		{	printf("-------------\n");
570 			printf("depth-limit (-u%d steps) reached\n", cutoff);
571 			break;
572 		}
573 #ifdef PC
574 		if (xspin && !interactive && --bufmax <= 0)
575 		{	int c; /* avoid buffer overflow on pc's */
576 			printf("spin: type return to proceed\n");
577 			fflush(stdout);
578 			c = getc(stdin);
579 			if (c == 'q') wrapup(0);
580 			bufmax = 100;
581 		}
582 #endif
583 		depth++; LastStep = ZE;
584 		oX = X;	/* a rendezvous could change it */
585 		go = 1;
586 		if (X->prov && X->pc
587 		&& !(X->pc->status & D_ATOM)
588 		&& !eval(X->prov))
589 		{	if (!xspin && ((verbose&32) || (verbose&4)))
590 			{	p_talk(X->pc, 1);
591 				printf("\t<<Not Enabled>>\n");
592 			}
593 			go = 0;
594 		}
595 		if (go && (e = eval_sub(X->pc)))
596 		{	if (depth >= jumpsteps
597 			&& ((verbose&32) || (verbose&4)))
598 			{	if (X == oX)
599 				if (!(e->status & D_ATOM) || (verbose&32)) /* no talking in d_steps */
600 				{	p_talk(X->pc, 1);
601 					printf("	[");
602 					if (!LastStep) LastStep = X->pc;
603 					comment(stdout, LastStep->n, 0);
604 					printf("]\n");
605 				}
606 				if (verbose&1) dumpglobals();
607 				if (verbose&2) dumplocal(X);
608 
609 				if (!(e->status & D_ATOM))
610 				if (xspin)
611 					printf("\n");
612 			}
613 			if (oX != X
614 			||  (X->pc->status & (ATOM|D_ATOM)))		/* new 5.0 */
615 			{	e = silent_moves(e);
616 				notbeyond = 0;
617 			}
618 			oX->pc = e; LastX = X;
619 
620 			if (!interactive) Tval = 0;
621 			memset(is_blocked, 0, 256);
622 
623 			if (X->pc && (X->pc->status & (ATOM|L_ATOM))
624 			&&  (notbeyond == 0 || oX != X))
625 			{	if ((X->pc->status & L_ATOM))
626 					notbeyond = 1;
627 				continue; /* no process switch */
628 			}
629 		} else
630 		{	depth--;
631 			if (oX->pc && (oX->pc->status & D_ATOM))
632 			{	non_fatal("stmnt in d_step blocks", (char *)0);
633 			}
634 			if (X->pc
635 			&&  X->pc->n
636 			&&  X->pc->n->ntyp == '@'
637 			&&  X->pid == (nproc-nstop-1))
638 			{	if (X != run && Y != NULL)
639 					Y->nxt = X->nxt;
640 				else
641 					run = X->nxt;
642 				nstop++;
643 				Priority_Sum -= X->priority;
644 				if (verbose&4)
645 				{	whoruns(1);
646 					dotag(stdout, "terminates\n");
647 				}
648 				LastX = X;
649 				if (!interactive) Tval = 0;
650 				if (nproc == nstop) break;
651 				memset(is_blocked, 0, 256);
652 				/* proc X is no longer in runlist */
653 				X = (X->nxt) ? X->nxt : run;
654 			} else
655 			{	if (p_blocked(X->pid))
656 				{	if (Tval) break;
657 					Tval = 1;
658 					if (depth >= jumpsteps)
659 					{	oX = X;
660 						X = (RunList *) 0; /* to suppress indent */
661 						dotag(stdout, "timeout\n");
662 						X = oX;
663 		}	}	}	}
664 
665 		if (!run || !X) break;	/* new 5.0 */
666 
667 		Y = pickproc(X);
668 		notbeyond = 0;
669 	}
670 	context = ZS;
671 	wrapup(0);
672 }
673 
674 int
complete_rendez(void)675 complete_rendez(void)
676 {	RunList *orun = X, *tmp;
677 	Element  *s_was = LastStep;
678 	Element *e;
679 	int j, ointer = interactive;
680 
681 	if (s_trail)
682 		return 1;
683 	if (orun->pc->status & D_ATOM)
684 		fatal("rv-attempt in d_step sequence", (char *)0);
685 	Rvous = 1;
686 	interactive = 0;
687 
688 	j = (int) Rand()%Priority_Sum;	/* randomize start point */
689 	X = run;
690 	while (j - X->priority >= 0)
691 	{	j -= X->priority;
692 		X = X->nxt;
693 		if (!X) X = run;
694 	}
695 	for (j = nproc - nstop; j > 0; j--)
696 	{	if (X != orun
697 		&& (!X->prov || eval(X->prov))
698 		&& (e = eval_sub(X->pc)))
699 		{	if (TstOnly)
700 			{	X = orun;
701 				Rvous = 0;
702 				goto out;
703 			}
704 			if ((verbose&32) || (verbose&4))
705 			{	tmp = orun; orun = X; X = tmp;
706 				if (!s_was) s_was = X->pc;
707 				p_talk(s_was, 1);
708 				printf("	[");
709 				comment(stdout, s_was->n, 0);
710 				printf("]\n");
711 				tmp = orun; orun = X; X = tmp;
712 				if (!LastStep) LastStep = X->pc;
713 				p_talk(LastStep, 1);
714 				printf("	[");
715 				comment(stdout, LastStep->n, 0);
716 				printf("]\n");
717 			}
718 			Rvous = 0; /* before silent_moves */
719 			X->pc = silent_moves(e);
720 out:				interactive = ointer;
721 			return 1;
722 		}
723 
724 		X = X->nxt;
725 		if (!X) X = run;
726 	}
727 	Rvous = 0;
728 	X = orun;
729 	interactive = ointer;
730 	return 0;
731 }
732 
733 /***** Runtime - Local Variables *****/
734 
735 static void
addsymbol(RunList * r,Symbol * s)736 addsymbol(RunList *r, Symbol  *s)
737 {	Symbol *t;
738 	int i;
739 
740 	for (t = r->symtab; t; t = t->next)
741 		if (strcmp(t->name, s->name) == 0
742 		&& (old_scope_rules
743 		 || strcmp((const char *)t->bscp, (const char *)s->bscp) == 0))
744 			return;		/* it's already there */
745 
746 	t = (Symbol *) emalloc(sizeof(Symbol));
747 	t->name = s->name;
748 	t->type = s->type;
749 	t->hidden = s->hidden;
750 	t->nbits  = s->nbits;
751 	t->nel  = s->nel;
752 	t->ini  = s->ini;
753 	t->setat = depth;
754 	t->context = r->n;
755 
756 	t->bscp  = (unsigned char *) emalloc(strlen((const char *)s->bscp)+1);
757 	strcpy((char *)t->bscp, (const char *)s->bscp);
758 
759 	if (s->type != STRUCT)
760 	{	if (s->val)	/* if already initialized, copy info */
761 		{	t->val = (int *) emalloc(s->nel*sizeof(int));
762 			for (i = 0; i < s->nel; i++)
763 				t->val[i] = s->val[i];
764 		} else
765 		{	(void) checkvar(t, 0);	/* initialize it */
766 		}
767 	} else
768 	{	if (s->Sval)
769 			fatal("saw preinitialized struct %s", s->name);
770 		t->Slst = s->Slst;
771 		t->Snm  = s->Snm;
772 		t->owner = s->owner;
773 	/*	t->context = r->n; */
774 	}
775 	t->next = r->symtab;	/* add it */
776 	r->symtab = t;
777 }
778 
779 static void
setlocals(RunList * r)780 setlocals(RunList *r)
781 {	Ordered	*walk;
782 	Symbol	*sp;
783 	RunList	*oX = X;
784 
785 	X = r;
786 	for (walk = all_names; walk; walk = walk->next)
787 	{	sp = walk->entry;
788 		if (sp
789 		&&  sp->context
790 		&&  strcmp(sp->context->name, r->n->name) == 0
791 		&&  sp->Nid >= 0
792 		&& (sp->type == UNSIGNED
793 		||  sp->type == BIT
794 		||  sp->type == MTYPE
795 		||  sp->type == BYTE
796 		||  sp->type == CHAN
797 		||  sp->type == SHORT
798 		||  sp->type == INT
799 		||  sp->type == STRUCT))
800 		{	if (!findloc(sp))
801 			non_fatal("setlocals: cannot happen '%s'",
802 				sp->name);
803 		}
804 	}
805 	X = oX;
806 }
807 
808 static void
oneparam(RunList * r,Lextok * t,Lextok * a,ProcList * p)809 oneparam(RunList *r, Lextok *t, Lextok *a, ProcList *p)
810 {	int k; int at, ft;
811 	RunList *oX = X;
812 
813 	if (!a)
814 		fatal("missing actual parameters: '%s'", p->n->name);
815 	if (t->sym->nel > 1 || t->sym->isarray)
816 		fatal("array in parameter list, %s", t->sym->name);
817 	k = eval(a->lft);
818 
819 	at = Sym_typ(a->lft);
820 	X = r;	/* switch context */
821 	ft = Sym_typ(t);
822 
823 	if (at != ft && (at == CHAN || ft == CHAN))
824 	{	char buf[256], tag1[64], tag2[64];
825 		(void) sputtype(tag1, ft);
826 		(void) sputtype(tag2, at);
827 		sprintf(buf, "type-clash in params of %s(..), (%s<-> %s)",
828 			p->n->name, tag1, tag2);
829 		non_fatal("%s", buf);
830 	}
831 	t->ntyp = NAME;
832 	addsymbol(r, t->sym);
833 	(void) setval(t, k);
834 
835 	X = oX;
836 }
837 
838 static void
setparams(RunList * r,ProcList * p,Lextok * q)839 setparams(RunList *r, ProcList *p, Lextok *q)
840 {	Lextok *f, *a;	/* formal and actual pars */
841 	Lextok *t;	/* list of pars of 1 type */
842 
843 	if (q)
844 	{	lineno = q->ln;
845 		Fname  = q->fn;
846 	}
847 	for (f = p->p, a = q; f; f = f->rgt) /* one type at a time */
848 	for (t = f->lft; t; t = t->rgt, a = (a)?a->rgt:a)
849 	{	if (t->ntyp != ',')
850 			oneparam(r, t, a, p);	/* plain var */
851 		else
852 			oneparam(r, t->lft, a, p); /* expanded struct */
853 	}
854 }
855 
856 Symbol *
findloc(Symbol * s)857 findloc(Symbol *s)
858 {	Symbol *r;
859 
860 	if (!X)
861 	{	/* fatal("error, cannot eval '%s' (no proc)", s->name); */
862 		return ZS;
863 	}
864 	for (r = X->symtab; r; r = r->next)
865 		if (strcmp(r->name, s->name) == 0
866 		&& (old_scope_rules || strcmp((const char *)r->bscp, (const char *)s->bscp) == 0))
867 			break;
868 	if (!r)
869 	{	addsymbol(X, s);
870 		r = X->symtab;
871 	}
872 	return r;
873 }
874 
875 int
in_bound(Symbol * r,int n)876 in_bound(Symbol *r, int n)
877 {
878 	if (!r)	return 0;
879 
880 	if (n >= r->nel || n < 0)
881 	{	printf("spin: indexing %s[%d] - size is %d\n",
882 			r->name, n, r->nel);
883 		non_fatal("indexing array \'%s\'", r->name);
884 		return 0;
885 	}
886 	return 1;
887 }
888 
889 int
getlocal(Lextok * sn)890 getlocal(Lextok *sn)
891 {	Symbol *r, *s = sn->sym;
892 	int n = eval(sn->lft);
893 
894 	r = findloc(s);
895 	if (r && r->type == STRUCT)
896 		return Rval_struct(sn, r, 1); /* 1 = check init */
897 	if (in_bound(r, n))
898 		return cast_val(r->type, r->val[n], r->nbits);
899 	return 0;
900 }
901 
902 int
setlocal(Lextok * p,int m)903 setlocal(Lextok *p, int m)
904 {	Symbol *r = findloc(p->sym);
905 	int n = eval(p->lft);
906 
907 	if (in_bound(r, n))
908 	{	if (r->type == STRUCT)
909 			(void) Lval_struct(p, r, 1, m); /* 1 = check init */
910 		else
911 		{
912 #if 0
913 			if (r->nbits > 0)
914 				m = (m & ((1<<r->nbits)-1));
915 			r->val[n] = m;
916 #else
917 			r->val[n] = cast_val(r->type, m, r->nbits);
918 #endif
919 			r->setat = depth;
920 	}	}
921 
922 	return 1;
923 }
924 
925 void
whoruns(int lnr)926 whoruns(int lnr)
927 {	if (!X) return;
928 
929 	if (lnr) printf("%3d:	", depth);
930 	printf("proc ");
931 	if (Have_claim && X->pid == 0)
932 		printf(" -");
933 	else
934 		printf("%2d", X->pid - Have_claim);
935 	printf(" (%s) ", X->n->name);
936 }
937 
938 static void
talk(RunList * r)939 talk(RunList *r)
940 {
941 	if ((verbose&32) || (verbose&4))
942 	{	p_talk(r->pc, 1);
943 		printf("\n");
944 		if (verbose&1) dumpglobals();
945 		if (verbose&2) dumplocal(r);
946 	}
947 }
948 
949 void
p_talk(Element * e,int lnr)950 p_talk(Element *e, int lnr)
951 {	static int lastnever = -1;
952 	static char nbuf[128];
953 	int newnever = -1;
954 
955 	if (e && e->n)
956 		newnever = e->n->ln;
957 
958 	if (Have_claim && X && X->pid == 0
959 	&&  lastnever != newnever && e)
960 	{	if (xspin)
961 		{	printf("MSC: ~G line %d\n", newnever);
962 #if 0
963 			printf("%3d:	proc  - (NEVER) line   %d \"never\" ",
964 				depth, newnever);
965 			printf("(state 0)\t[printf('MSC: never\\\\n')]\n");
966 		} else
967 		{	printf("%3d:	proc  - (NEVER) line   %d \"never\"\n",
968 				depth, newnever);
969 #endif
970 		}
971 		lastnever = newnever;
972 	}
973 
974 	whoruns(lnr);
975 	if (e)
976 	{	if (e->n)
977 		{	char *ptr = e->n->fn->name;
978 			char *qtr = nbuf;
979 			while (*ptr != '\0')
980 			{	if (*ptr != '"')
981 				{	*qtr++ = *ptr;
982 				}
983 				ptr++;
984 			}
985 			*qtr = '\0';
986 		} else
987 		{	strcpy(nbuf, "-");
988 		}
989 		printf("%s:%d (state %d)",
990 			nbuf,
991 			e->n?e->n->ln:-1,
992 			e->seqno);
993 		if (!xspin
994 		&&  ((e->status&ENDSTATE) || has_lab(e, 2)))	/* 2=end */
995 		{	printf(" <valid end state>");
996 		}
997 	}
998 }
999 
1000 int
remotelab(Lextok * n)1001 remotelab(Lextok *n)
1002 {	int i;
1003 
1004 	lineno = n->ln;
1005 	Fname  = n->fn;
1006 	if (n->sym->type != 0 && n->sym->type != LABEL)
1007 	{	printf("spin: error, type: %d\n", n->sym->type);
1008 		fatal("not a labelname: '%s'", n->sym->name);
1009 	}
1010 	if (n->indstep >= 0)
1011 	{	fatal("remote ref to label '%s' inside d_step",
1012 			n->sym->name);
1013 	}
1014 	if ((i = find_lab(n->sym, n->lft->sym, 1)) == 0)
1015 		fatal("unknown labelname: %s", n->sym->name);
1016 	return i;
1017 }
1018 
1019 int
remotevar(Lextok * n)1020 remotevar(Lextok *n)
1021 {	int prno, i, added=0;
1022 	RunList *Y, *oX;
1023 	Lextok *onl;
1024 	Symbol *os;
1025 
1026 	lineno = n->ln;
1027 	Fname  = n->fn;
1028 
1029 	if (!n->lft->lft)
1030 		prno = f_pid(n->lft->sym->name);
1031 	else
1032 	{	prno = eval(n->lft->lft); /* pid - can cause recursive call */
1033 #if 0
1034 		if (n->lft->lft->ntyp == CONST)	/* user-guessed pid */
1035 #endif
1036 		{	prno += Have_claim;
1037 			added = Have_claim;
1038 	}	}
1039 
1040 	if (prno < 0)
1041 		return 0;	/* non-existing process */
1042 #if 0
1043 	i = nproc - nstop;
1044 	for (Y = run; Y; Y = Y->nxt)
1045 	{	--i;
1046 		printf("	%s: i=%d, prno=%d, ->pid=%d\n", Y->n->name, i, prno, Y->pid);
1047 	}
1048 #endif
1049 	i = nproc - nstop + Skip_claim;	/* 6.0: added Skip_claim */
1050 	for (Y = run; Y; Y = Y->nxt)
1051 	if (--i == prno)
1052 	{	if (strcmp(Y->n->name, n->lft->sym->name) != 0)
1053 		{	printf("spin: remote reference error on '%s[%d]'\n",
1054 				n->lft->sym->name, prno-added);
1055 			non_fatal("refers to wrong proctype '%s'", Y->n->name);
1056 		}
1057 		if (strcmp(n->sym->name, "_p") == 0)
1058 		{	if (Y->pc)
1059 				return Y->pc->seqno;
1060 			/* harmless, can only happen with -t */
1061 			return 0;
1062 		}
1063 #if 1
1064 		/* new 4.0 allow remote variables */
1065 		oX = X;
1066 		X = Y;
1067 
1068 		onl = n->lft;
1069 		n->lft = n->rgt;
1070 
1071 		os = n->sym;
1072 		n->sym = findloc(n->sym);
1073 
1074 		i = getval(n);
1075 
1076 		n->sym = os;
1077 		n->lft = onl;
1078 		X = oX;
1079 		return i;
1080 #else
1081 		break;
1082 #endif
1083 	}
1084 	printf("remote ref: %s[%d] ", n->lft->sym->name, prno-added);
1085 	non_fatal("%s not found", n->sym->name);
1086 	printf("have only:\n");
1087 	i = nproc - nstop - 1;
1088 	for (Y = run; Y; Y = Y->nxt, i--)
1089 		if (!strcmp(Y->n->name, n->lft->sym->name))
1090 		printf("\t%d\t%s\n", i, Y->n->name);
1091 
1092 	return 0;
1093 }
1094