sys/src/cmd/spin/sched.c

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