123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422423424425426427428429430431432433434435436437438439440441442443444445446447448449450451452453454455456457458459460461462463464465466467468469470471472473474475476477478479480481482483484485486487488489490491492493494495496497498499500501502503504505506507508509510511512513514515516517518519520521522523524525526527528529530531532533534535536537538539540541542543544545546547548549550551552553554555556557558559560561562563564565566567568569570571572573574575576577578579580581582583584585586587588589590591592593594595596597598599600601602603604605606607608609610611612613614615616617618619620621622623624625626627628629630631632633634635636637638639640641642643644645646647648649650651652653654655656657658659660661662663664665666667668669670671672673674675676677678679680681682683684685686687688689690691692693694695696697698699700701702703704705706707708709710711712713714715716717718719720721722723724725726727728729730731732733734735736737738739740741742743744745746747748749750751752753754755756757758759760761762763764765766767768769770771772773774775776777778779780781782783784785786787788789790791792793794795796797798799800801802803804805806807808809810811812813814815816817818819820821822823824825826827828829830831832833834835836837838839840841842843844845846847848849850851852853854855856857858859860861862863864865866867868869870871872873874875876877878879880881882883884885886887888889890891892893894895896897898899900901902903904 |
- /***** spin: sched.c *****/
- /* Copyright (c) 1991-2000 by Lucent Technologies - Bell Laboratories */
- /* All Rights Reserved. This software is for educational purposes only. */
- /* Permission is given to distribute this code provided that this intro- */
- /* ductory message is not removed and no monies are exchanged. */
- /* No guarantee is expressed or implied by the distribution of this code. */
- /* Software written by Gerard J. Holzmann as part of the book: */
- /* `Design and Validation of Computer Protocols,' ISBN 0-13-539925-4, */
- /* Prentice Hall, Englewood Cliffs, NJ, 07632. */
- /* Send bug-reports and/or questions to: gerard@research.bell-labs.com */
- #include <stdlib.h>
- #include "spin.h"
- #ifdef PC
- #include "y_tab.h"
- #else
- #include "y.tab.h"
- #endif
- 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;
- extern short has_enabled, has_provided;
- 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-1;
- r->pc = huntele(p->s->frst, p->s->frst->status);
- r->ps = p->s;
- if (p->s && p->s->last)
- p->s->last->status |= ENDSTATE; /* normal endstate */
- 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, run->n->name);
- pstext(run->pid, Buf);
- } else
- printf("proc %d = %s\n",
- run->pid - Have_claim, run->n->name);
- return;
- }
- #if 1
- if (dumptab
- || analyze
- || s_trail
- || !(verbose&4))
- return;
- #endif
- 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");
- }
- 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)
- { runnable(p, m->val, 0);
- announce((char *) 0);
- setparams(run, p, n);
- setlocals(run); /* after setparams */
- return run->pid - Have_claim; /* pid */
- }
- return 0; /* process not found */
- }
- 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, with 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; /* already there */
- q = run; run = run->nxt;
- q->pid = 0; q->nxt = (RunList *) 0;
- done:
- for (r = run; r; r = r->nxt)
- { r->pid = r->pid+1;
- if (!r->nxt)
- { r->nxt = q;
- break;
- } }
- Have_claim = 1;
- }
- void
- wrapup(int fini)
- {
- 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);
- 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 processes created\n", nproc);
- 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)
- { register 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;
- 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 void
- pickproc(void)
- { SeqList *z; Element *has_else;
- short Choices[256];
- int j, k, nr_else;
- if (nproc <= nstop+1)
- { X = run;
- return;
- }
- 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;
- X = X->nxt;
- if (!X) X = run;
- }
- } else
- { int only_choice = -1;
- int no_choice = 0, proc_no_ch, proc_k;
- 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;
- for (X = run; X; X = X->nxt)
- { if (!X->nxt
- || X->nxt->pid > 255
- || j < Choices[X->nxt->pid])
- {
- MadeChoice = 1+j-Choices[X->pid];
- break;
- } }
- }
- }
- void
- sched(void)
- { Element *e;
- RunList *Y=0; /* previous process in run queue */
- RunList *oX;
- int go, notbeyond;
- #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");
- /* if (interactive) Tval = 1; */
- X = run;
- pickproc();
- notbeyond = 0;
- while (X)
- { context = X->n;
- if (X->pc && X->pc->n)
- { lineno = X->pc->n->ln;
- Fname = X->pc->n->fn;
- }
- #ifdef PC
- if (xspin && !interactive && --bufmax <= 0)
- { /* avoid buffer overflow on pc's */
- printf("spin: type return to proceed\n");
- fflush(stdout);
- getc(stdin);
- bufmax = 100;
- }
- #endif
- depth++; LastStep = ZE;
- oX = X; /* a rendezvous could change it */
- go = 1;
- if (X && X->prov
- && !(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)
- { 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 (xspin) printf("\n");
- }
- if (oX != X) e = silent_moves(e);
- oX->pc = e; LastX = X;
- if (!interactive) Tval = 0;
- memset(is_blocked, 0, 256);
- if ((X->pc->status & (ATOM|L_ATOM))
- && notbeyond == 0)
- { 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->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);
- } else
- { if (p_blocked(X->pid))
- { if (Tval) break;
- Tval = 1;
- if (depth >= jumpsteps)
- dotag(stdout, "timeout\n");
- } } }
- Y = X;
- pickproc();
- 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
- 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 (r)
- { if (n >= r->nel || n < 0)
- { printf("spin: indexing %s[%d] - size is %d\n",
- s->name, n, r->nel);
- non_fatal("indexing array \'%s\'", s->name);
- } else
- { 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 (!r) return 1;
- 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);
- } else
- { if (r->type == STRUCT)
- (void) Lval_struct(p, r, 1, m); /* 1 = check init */
- else
- { if (r->nbits > 0)
- m = (m & ((1<<r->nbits)-1));
- r->val[n] = m;
- 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);
- printf("%3d: proc 0 (NEVER) line %d \"never\" ",
- depth, newnever);
- printf("(state 0)\t[printf('MSC: never\\\\n')]\n");
- } else
- { printf("%3d: proc 0 (NEVER) line %d \"never\"\n",
- depth, newnever);
- }
- 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 endstate>");
- }
- }
- }
- int
- remotelab(Lextok *n)
- { int i;
- lineno = n->ln;
- Fname = n->fn;
- if (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, trick=0;
- RunList *Y;
- lineno = n->ln;
- Fname = n->fn;
- if (!n->lft->lft)
- { non_fatal("missing pid in %s", n->sym->name);
- return 0;
- }
- prno = eval(n->lft->lft); /* pid - can cause recursive call */
- TryAgain:
- i = nproc - nstop;
- for (Y = run; Y; Y = Y->nxt)
- if (--i == prno)
- { if (strcmp(Y->n->name, n->lft->sym->name) != 0)
- { if (!trick && Have_claim)
- { trick = 1; prno++;
- /* assumes user guessed the pid */
- goto TryAgain;
- }
- printf("spin: remote reference error on '%s[%d]'\n",
- n->lft->sym->name, prno-trick);
- 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;
- }
- break;
- }
- printf("remote ref: %s[%d] ", n->lft->sym->name, prno-trick);
- 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;
- }
|