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