sys/src/cmd/spin/sched.c

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