1 /***** spin: sched.c *****/
4 * This file is part of the public release of Spin. It is subject to the
5 * terms in the LICENSE file that is included in this source directory.
6 * Tool documentation is available at http://spinroot.com
13 extern int verbose, s_trail, analyze, no_wrapup;
14 extern char *claimproc, *eventmap, Buf[];
15 extern Ordered *all_names;
16 extern Symbol *Fname, *context;
17 extern int lineno, nr_errs, dumptab, xspin, jumpsteps, columns;
18 extern int u_sync, Elcnt, interactive, TstOnly, cutoff;
19 extern short has_enabled, has_priority, has_code, replay;
20 extern int limited_vis, product, nclaims, old_priority_rules;
21 extern int old_scope_rules, scope_seq[128], scope_level, has_stdin;
23 extern int pc_highest(Lextok *n);
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, Priority_Sum = 0;
31 int Rvous=0, depth=0, nrRdy=0, MadeChoice;
32 short Have_claim=0, Skip_claim=0;
34 static void setlocals(RunList *);
35 static void setparams(RunList *, ProcList *, Lextok *);
36 static void talk(RunList *);
39 runnable(ProcList *p, int weight, int noparams)
40 { RunList *r = (RunList *) emalloc(sizeof(RunList));
45 r->pid = nproc++ - nstop + Skip_claim;
47 p->priority = (unsigned char) weight; /* not quite the best place of course */
49 if (!noparams && ((verbose&4) || (verbose&32)))
50 { printf("Starting %s with pid %d",
51 p->n?p->n->name:"--", r->pid);
52 if (has_priority) printf(" priority %d", r->priority);
56 fatal("parsing error, no sequence %s",
57 p->n?p->n->name:"--");
59 r->pc = huntele(p->s->frst, p->s->frst->status, -1);
63 p->s->last->status |= ENDSTATE; /* normal end state */
67 if (weight < 1 || weight > 255)
68 { fatal("bad process priority, valid range: 1..255", (char *) 0);
71 if (noparams) setlocals(r);
72 Priority_Sum += weight;
78 ready(Symbol *n, Lextok *p, Sequence *s, int det, Lextok *prov, enum btypes b)
79 /* n=name, p=formals, s=body det=deterministic prov=provided */
80 { ProcList *r = (ProcList *) emalloc(sizeof(ProcList));
81 Lextok *fp, *fpt; int j; extern int Npars;
88 r->tn = (short) nrRdy++;
89 n->sc = scope_seq[scope_level]; /* scope_level should be 0 */
91 if (det != 0 && det != 1)
92 { fprintf(stderr, "spin: bad value for det (cannot happen)\n");
94 r->det = (unsigned char) det;
98 for (fp = p, j = 0; fp; fp = fp->rgt)
99 for (fpt = fp->lft; fpt; fpt = fpt->rgt)
100 j++; /* count # of parameters */
101 Npars = max(Npars, j);
107 find_maxel(Symbol *s)
110 for (p = rdy; p; p = p->nxt)
112 return p->s->maxel++;
122 for (p = rdy; p; p = p->nxt)
123 { if (!p->p) continue;
125 for (f = p->p; f; f = f->rgt) /* types */
126 for (t = f->lft; t; t = t->rgt) /* formals */
127 { if (t->ntyp != ',')
128 t->sym->Nid = cnt--; /* overload Nid */
130 t->lft->sym->Nid = cnt--;
143 { sprintf(Buf, "%d:%s",
144 run->pid - Have_claim, run->n->name);
145 pstext(run->pid - Have_claim, Buf);
147 { printf("proc %d = %s\n",
148 run->pid - Have_claim, run->n->name);
161 printf(" 0: proc - (%s) ", w);
164 printf("creates proc %2d (%s)",
165 run->pid - Have_claim,
167 if (run->priority > 1)
168 printf(" priority %d", run->priority);
173 #define MAXP 255 /* matches max nr of processes in verifier */
179 Symbol *s = m->sym; /* proctype name */
180 Lextok *n = m->lft; /* actual parameters */
183 { m->val = 1; /* minimum priority */
185 for (p = rdy; p; p = p->nxt)
186 { if (strcmp(s->name, p->n->name) == 0)
187 { if (nproc-nstop >= MAXP)
188 { printf("spin: too many processes (%d max)\n", MAXP);
191 runnable(p, m->val, 0);
192 announce((char *) 0);
193 setparams(run, p, n);
194 setlocals(run); /* after setparams */
195 return run->pid - Have_claim + Skip_claim; /* effective simu pid */
197 return 0; /* process not found */
201 check_param_count(int i, Lextok *m)
203 Symbol *s = m->sym; /* proctype name */
204 Lextok *f, *t; /* formal pars */
207 for (p = rdy; p; p = p->nxt)
208 { if (strcmp(s->name, p->n->name) == 0)
209 { if (m->lft) /* actual param list */
210 { lineno = m->lft->ln;
213 for (f = p->p; f; f = f->rgt) /* one type at a time */
214 for (t = f->lft; t; t = t->rgt) /* count formal params */
218 { printf("spin: saw %d parameters, expected %d\n", i, cnt);
219 non_fatal("wrong number of parameters", "");
228 RunList *r, *q = (RunList *) 0;
230 for (p = rdy; p; p = p->nxt)
231 if (p->tn == n && p->b == N_CLAIM)
235 printf("spin: couldn't find claim %d (ignored)\n", n);
237 for (p = rdy; p; p = p->nxt)
238 printf("\t%d = %s\n", p->tn, p->n->name);
243 /* move claim to far end of runlist, and reassign it pid 0 */
247 sprintf(Buf, "%d:%s", 0, p->n->name);
249 for (r = run; r; r = r->nxt)
250 { if (r->b != N_CLAIM)
251 { sprintf(Buf, "%d:%s", r->pid+1, r->n->name);
252 pstext(r->pid+1, Buf);
255 if (run->pid == 0) return; /* it is the first process started */
257 q = run; run = run->nxt;
258 q->pid = 0; q->nxt = (RunList *) 0; /* remove */
261 for (r = run; r; r = r->nxt)
262 { r->pid = r->pid+Have_claim; /* adjust */
274 for (r = run; r; r = r->nxt)
275 if (strcmp(n, r->n->name) == 0)
277 { printf("spin: remote ref to proctype %s, ", n);
278 printf("has more than one match: %d and %d\n",
291 { extern void putpostlude(void);
292 if (columns == 2) putpostlude();
294 printf("-------------\nfinal state:\n-------------\n");
300 printf("#processes: %d\n", nproc-nstop - Have_claim + Skip_claim);
304 verbose &= ~1; /* no more globals */
305 verbose |= 32; /* add process states */
306 for (X = run; X; X = X->nxt)
308 verbose = ov; /* restore */
310 printf("%d process%s created\n",
311 nproc - Have_claim + Skip_claim,
312 (xspin || nproc!=1)?"es":"");
314 if (s_trail || xspin) alldone(0); /* avoid an abort from xspin */
315 if (fini) alldone(1);
318 static char is_blocked[256];
324 is_blocked[p%256] = 1;
325 for (i = j = 0; i < nproc - nstop; i++)
327 if (j >= nproc - nstop)
328 { memset(is_blocked, 0, 256);
335 silent_moves(Element *e)
339 switch (e->n->ntyp) {
342 f = get_lab(e->n, 1);
343 cross_dsteps(e->n, f->n);
344 return f; /* guard against goto cycles */
346 return silent_moves(e->sub->this->frst);
350 e->n->sl->this->last->nxt = e->nxt;
351 return silent_moves(e->n->sl->this->frst);
353 return silent_moves(e->nxt);
359 x_can_run(void) /* the currently selected process in X can run */
361 if (X->prov && !eval(X->prov))
363 if (0) printf("pid %d cannot run: not provided\n", X->pid);
366 if (has_priority && !old_priority_rules)
367 { Lextok *n = nn(ZN, CONST, ZN, ZN);
369 if (0) printf("pid %d %s run (priority)\n", X->pid, pc_highest(n)?"can":"cannot");
370 return pc_highest(n);
372 if (0) printf("pid %d can run\n", X->pid);
378 { SeqList *z; Element *has_else;
380 int j, k, nr_else = 0;
382 if (nproc <= nstop+1)
386 if (!interactive || depth < jumpsteps)
387 { if (has_priority && !old_priority_rules) /* new 6.3.2 */
388 { j = Rand()%(nproc-nstop);
389 for (X = run; X; X = X->nxt)
394 { fatal("unexpected, pickproc", (char *)0);
402 X = (X->nxt)?X->nxt:run;
406 if (Priority_Sum < nproc-nstop)
407 fatal("cannot happen - weights", (char *)0);
408 j = (int) Rand()%Priority_Sum;
410 while (j - X->priority >= 0)
414 if (!X) { Y = NULL; X = run; }
418 { int only_choice = -1;
419 int no_choice = 0, proc_no_ch, proc_k;
421 Tval = 0; /* new 4.2.6 */
422 try_again: printf("Select a statement\n");
423 try_more: for (X = run, k = 1; X; X = X->nxt)
424 { if (X->pid > 255) break;
426 Choices[X->pid] = (short) k;
428 if (!X->pc || !x_can_run())
433 X->pc = silent_moves(X->pc);
434 if (!X->pc->sub && X->pc->n)
436 unex = !Enabled0(X->pc);
441 if (!xspin && unex && !(verbose&32))
445 printf("\tchoice %d: ", k++);
448 printf(" unexecutable,");
450 comment(stdout, X->pc->n, 0);
451 if (X->pc->esc) printf(" + Escape");
455 proc_no_ch = no_choice;
457 for (z = X->pc->sub, j=0; z; z = z->nxt)
458 { Element *y = silent_moves(z->this->frst);
462 if (y->n->ntyp == ELSE)
463 { has_else = (Rvous)?ZE:y;
473 if (!xspin && unex && !(verbose&32))
477 printf("\tchoice %d: ", k++);
480 printf(" unexecutable,");
482 comment(stdout, y->n, 0);
486 { if (no_choice-proc_no_ch >= (k-proc_k)-1)
487 { only_choice = nr_else;
488 printf("\tchoice %d: ", nr_else);
493 printf("\tchoice %d: ", nr_else);
495 printf(" unexecutable, [else]\n");
499 if (k - no_choice < 2 && Tval == 0)
501 no_choice = 0; only_choice = -1;
505 printf("Make Selection %d\n\n", k-1);
507 { if (k - no_choice < 2)
508 { printf("no executable choices\n");
511 printf("Select [1-%d]: ", k-1);
513 if (!xspin && k - no_choice == 2)
514 { printf("%d\n", only_choice);
519 if (scanf("%64s", buf) == 0)
520 { printf("\tno input\n");
524 if (isdigit((int) buf[0]))
531 { printf("\tchoice is outside range\n");
536 for (X = run; X; Y = X, X = X->nxt)
539 || j < Choices[X->nxt->pid])
541 MadeChoice = 1+j-Choices[X->pid];
550 { ProcList *p, *q = NULL;
553 { printf(" the model contains %d never claims:", nclaims);
554 for (p = rdy; p; p = p->nxt)
555 { if (p->b == N_CLAIM)
556 { printf("%s%s", q?", ":" ", p->n->name);
560 printf(" only one claim is used in a verification run\n");
561 printf(" choose which one with ./pan -a -N name (defaults to -N %s)\n",
563 printf(" or use e.g.: spin -search -ltl %s %s\n",
564 q?q->n->name:"--", Fname?Fname->name:"filename");
571 RunList *Y = NULL; /* previous process in run queue */
573 int go, notbeyond = 0;
583 if (has_code && !analyze)
584 { printf("spin: warning: c_code fragments remain uninterpreted\n");
585 printf(" in random simulations with spin; use ./pan -r instead\n");
588 if (has_enabled && u_sync > 0)
589 { printf("spin: error, cannot use 'enabled()' in ");
590 printf("models with synchronous channels.\n");
597 if (analyze && (!replay || has_code))
602 if (replay && !has_code)
611 printf("warning: never claim not used in random simulation\n");
613 printf("warning: trace assertion not used in random simulation\n");
620 if (X->pc && X->pc->n)
621 { lineno = X->pc->n->ln;
622 Fname = X->pc->n->fn;
624 if (cutoff > 0 && depth >= cutoff)
625 { printf("-------------\n");
626 printf("depth-limit (-u%d steps) reached\n", cutoff);
630 if (xspin && !interactive && --bufmax <= 0)
631 { int c; /* avoid buffer overflow on pc's */
632 printf("spin: type return to proceed\n");
635 if (c == 'q') wrapup(0);
639 depth++; LastStep = ZE;
640 oX = X; /* a rendezvous could change it */
643 && !(X->pc->status & D_ATOM)
645 { if (!xspin && ((verbose&32) || (verbose&4)))
647 printf("\t<<Not Enabled>>\n");
651 if (go && (e = eval_sub(X->pc)))
652 { if (depth >= jumpsteps
653 && ((verbose&32) || (verbose&4)))
655 if (!(e->status & D_ATOM) || (verbose&32)) /* no talking in d_steps */
656 { if (!LastStep) LastStep = X->pc;
657 /* A. Tanaka, changed order */
660 comment(stdout, LastStep->n, 0);
663 if (verbose&1) dumpglobals();
664 if (verbose&2) dumplocal(X);
666 if (!(e->status & D_ATOM))
671 || (X->pc->status & (ATOM|D_ATOM))) /* new 5.0 */
672 { e = silent_moves(e);
675 oX->pc = e; LastX = X;
677 if (!interactive) Tval = 0;
678 memset(is_blocked, 0, 256);
680 if (X->pc && (X->pc->status & (ATOM|L_ATOM))
681 && (notbeyond == 0 || oX != X))
682 { if ((X->pc->status & L_ATOM))
684 continue; /* no process switch */
688 if (oX->pc && (oX->pc->status & D_ATOM))
689 { non_fatal("stmnt in d_step blocks", (char *)0);
693 && X->pc->n->ntyp == '@'
694 && X->pid == (nproc-nstop-1))
695 { if (X != run && Y != NULL)
700 Priority_Sum -= X->priority;
703 dotag(stdout, "terminates\n");
706 if (!interactive) Tval = 0;
707 if (nproc == nstop) break;
708 memset(is_blocked, 0, 256);
709 /* proc X is no longer in runlist */
710 X = (X->nxt) ? X->nxt : run;
712 { if (p_blocked(X->pid))
713 { if (Tval && !has_stdin)
716 if (!Tval && depth >= jumpsteps)
718 X = (RunList *) 0; /* to suppress indent */
719 dotag(stdout, "timeout\n");
724 if (!run || !X) break; /* new 5.0 */
734 complete_rendez(void)
735 { RunList *orun = X, *tmp;
736 Element *s_was = LastStep;
738 int j, ointer = interactive;
742 if (orun->pc->status & D_ATOM)
743 fatal("rv-attempt in d_step sequence", (char *)0);
747 j = (int) Rand()%Priority_Sum; /* randomize start point */
749 while (j - X->priority >= 0)
754 for (j = nproc - nstop; j > 0; j--)
756 && (!X->prov || eval(X->prov))
757 && (e = eval_sub(X->pc)))
763 if ((verbose&32) || (verbose&4))
764 { tmp = orun; orun = X; X = tmp;
765 if (!s_was) s_was = X->pc;
768 comment(stdout, s_was->n, 0);
770 tmp = orun; /* orun = X; */ X = tmp;
771 if (!LastStep) LastStep = X->pc;
774 comment(stdout, LastStep->n, 0);
777 Rvous = 0; /* before silent_moves */
778 X->pc = silent_moves(e);
779 out: interactive = ointer;
788 interactive = ointer;
792 /***** Runtime - Local Variables *****/
795 addsymbol(RunList *r, Symbol *s)
799 for (t = r->symtab; t; t = t->next)
800 if (strcmp(t->name, s->name) == 0
802 || strcmp((const char *)t->bscp, (const char *)s->bscp) == 0))
803 return; /* it's already there */
805 t = (Symbol *) emalloc(sizeof(Symbol));
808 t->hidden = s->hidden;
809 t->isarray = s->isarray;
816 t->bscp = (unsigned char *) emalloc(strlen((const char *)s->bscp)+1);
817 strcpy((char *)t->bscp, (const char *)s->bscp);
819 if (s->type != STRUCT)
820 { if (s->val) /* if already initialized, copy info */
821 { t->val = (int *) emalloc(s->nel*sizeof(int));
822 for (i = 0; i < s->nel; i++)
823 t->val[i] = s->val[i];
825 { (void) checkvar(t, 0); /* initialize it */
829 fatal("saw preinitialized struct %s", s->name);
833 /* t->context = r->n; */
835 t->next = r->symtab; /* add it */
840 setlocals(RunList *r)
846 for (walk = all_names; walk; walk = walk->next)
850 && strcmp(sp->context->name, r->n->name) == 0
852 && (sp->type == UNSIGNED
859 || sp->type == STRUCT))
861 non_fatal("setlocals: cannot happen '%s'",
869 oneparam(RunList *r, Lextok *t, Lextok *a, ProcList *p)
874 fatal("missing actual parameters: '%s'", p->n->name);
875 if (t->sym->nel > 1 || t->sym->isarray)
876 fatal("array in parameter list, %s", t->sym->name);
879 at = Sym_typ(a->lft);
880 X = r; /* switch context */
883 if (at != ft && (at == CHAN || ft == CHAN))
884 { char buf[256], tag1[64], tag2[64];
885 (void) sputtype(tag1, ft);
886 (void) sputtype(tag2, at);
887 sprintf(buf, "type-clash in params of %s(..), (%s<-> %s)",
888 p->n->name, tag1, tag2);
889 non_fatal("%s", buf);
892 addsymbol(r, t->sym);
899 setparams(RunList *r, ProcList *p, Lextok *q)
900 { Lextok *f, *a; /* formal and actual pars */
901 Lextok *t; /* list of pars of 1 type */
907 for (f = p->p, a = q; f; f = f->rgt) /* one type at a time */
908 for (t = f->lft; t; t = t->rgt, a = (a)?a->rgt:a)
909 { if (t->ntyp != ',')
910 oneparam(r, t, a, p); /* plain var */
912 oneparam(r, t->lft, a, p); /* expanded struct */
921 { /* fatal("error, cannot eval '%s' (no proc)", s->name); */
924 for (r = X->symtab; r; r = r->next)
925 { if (strcmp(r->name, s->name) == 0
927 || strcmp((const char *)r->bscp, (const char *)s->bscp) == 0))
938 in_bound(Symbol *r, int n)
942 if (n >= r->nel || n < 0)
943 { printf("spin: indexing %s[%d] - size is %d\n",
945 non_fatal("indexing array \'%s\'", r->name);
953 { Symbol *r, *s = sn->sym;
954 int n = eval(sn->lft);
957 if (r && r->type == STRUCT)
958 return Rval_struct(sn, r, 1); /* 1 = check init */
960 return cast_val(r->type, r->val[n], r->nbits);
965 setlocal(Lextok *p, int m)
966 { Symbol *r = findloc(p->sym);
967 int n = eval(p->lft);
970 { if (r->type == STRUCT)
971 (void) Lval_struct(p, r, 1, m); /* 1 = check init */
976 m = (m & ((1<<r->nbits)-1));
979 r->val[n] = cast_val(r->type, m, r->nbits);
991 if (lnr) printf("%3d: ", depth);
993 if (Have_claim && X->pid == 0)
996 printf("%2d", X->pid - Have_claim);
997 if (old_priority_rules)
998 { printf(" (%s) ", X->n->name);
1000 { printf(" (%s:%d) ", X->n->name, X->priority);
1007 if ((verbose&32) || (verbose&4))
1010 if (verbose&1) dumpglobals();
1011 if (verbose&2) dumplocal(r);
1016 p_talk(Element *e, int lnr)
1017 { static int lastnever = -1;
1018 static char nbuf[128];
1022 newnever = e->n->ln;
1024 if (Have_claim && X && X->pid == 0
1025 && lastnever != newnever && e)
1027 { printf("MSC: ~G line %d\n", newnever);
1029 printf("%3d: proc - (NEVER) line %d \"never\" ",
1031 printf("(state 0)\t[printf('MSC: never\\\\n')]\n");
1033 { printf("%3d: proc - (NEVER) line %d \"never\"\n",
1037 lastnever = newnever;
1043 { char *ptr = e->n->fn->name;
1045 while (*ptr != '\0')
1053 { strcpy(nbuf, "-");
1055 printf("%s:%d (state %d)",
1060 && ((e->status&ENDSTATE) || has_lab(e, 2))) /* 2=end */
1061 { printf(" <valid end state>");
1067 remotelab(Lextok *n)
1072 if (n->sym->type != 0 && n->sym->type != LABEL)
1073 { printf("spin: error, type: %d\n", n->sym->type);
1074 fatal("not a labelname: '%s'", n->sym->name);
1076 if (n->indstep >= 0)
1077 { fatal("remote ref to label '%s' inside d_step",
1080 if ((i = find_lab(n->sym, n->lft->sym, 1)) == 0) /* remotelab */
1081 { fatal("unknown labelname: %s", n->sym->name);
1087 remotevar(Lextok *n)
1088 { int prno, i, added=0;
1097 prno = f_pid(n->lft->sym->name);
1099 { prno = eval(n->lft->lft); /* pid - can cause recursive call */
1101 if (n->lft->lft->ntyp == CONST) /* user-guessed pid */
1103 { prno += Have_claim;
1108 { return 0; /* non-existing process */
1112 for (Y = run; Y; Y = Y->nxt)
1114 printf(" %s: i=%d, prno=%d, ->pid=%d\n", Y->n->name, i, prno, Y->pid);
1117 i = nproc - nstop + Skip_claim; /* 6.0: added Skip_claim */
1118 for (Y = run; Y; Y = Y->nxt)
1120 { if (strcmp(Y->n->name, n->lft->sym->name) != 0)
1121 { printf("spin: remote reference error on '%s[%d]'\n",
1122 n->lft->sym->name, prno-added);
1123 non_fatal("refers to wrong proctype '%s'", Y->n->name);
1125 if (strcmp(n->sym->name, "_p") == 0)
1127 { return Y->pc->seqno;
1129 /* harmless, can only happen with -t */
1133 /* check remote variables */
1141 if (!n->sym->context)
1142 { n->sym->context = Y->n;
1144 { int rs = old_scope_rules;
1145 old_scope_rules = 1; /* 6.4.0 */
1146 n->sym = findloc(n->sym);
1147 old_scope_rules = rs;
1156 printf("remote ref: %s[%d] ", n->lft->sym->name, prno-added);
1157 non_fatal("%s not found", n->sym->name);
1158 printf("have only:\n");
1159 i = nproc - nstop - 1;
1160 for (Y = run; Y; Y = Y->nxt, i--)
1161 if (!strcmp(Y->n->name, n->lft->sym->name))
1162 printf("\t%d\t%s\n", i, Y->n->name);