1 /***** spin: sched.c *****/ 2 3 /* Copyright (c) 1991,1995 by AT&T Corporation. All Rights Reserved. */ 4 /* 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.att.com */ 12 13 #include "spin.h" 14 #include "y.tab.h" 15 16 extern int verbose, s_trail, analyze; 17 extern char *claimproc; 18 extern Symbol *Fname, *context; 19 extern int lineno, nr_errs, dumptab, xspin; 20 extern int has_enabled, u_sync, Elcnt, Interactive; 21 22 RunList *X = (RunList *) 0; 23 RunList *run = (RunList *) 0; 24 RunList *LastX = (RunList *) 0; /* previous executing proc */ 25 ProcList *rdy = (ProcList *) 0; 26 Element *LastStep = ZE; 27 int Have_claim=0, nproc=0, nstop=0, Tval=0; 28 int Rvous=0, depth=0, nrRdy=0, SubChoice; 29 30 void 31 runnable(ProcList *p) 32 { RunList *r = (RunList *) emalloc(sizeof(RunList)); 33 34 r->n = p->n; 35 r->tn = p->tn; 36 r->pid = ++nproc-nstop-1; /* was: nproc++; */ 37 r->pc = huntele(p->s->frst, p->s->frst->status); /* was: s->frst; */ 38 r->ps = p->s; /* was: r->maxseq = s->last->seqno */ 39 r->nxt = run; 40 run = r; 41 } 42 43 ProcList * 44 ready(Symbol *n, Lextok *p, Sequence *s) /* n=name, p=formals, s=body */ 45 { ProcList *r = (ProcList *) emalloc(sizeof(ProcList)); 46 Lextok *fp, *fpt; int j; extern int Npars; 47 48 r->n = n; 49 r->p = p; 50 r->s = s; 51 r->tn = nrRdy++; 52 r->nxt = rdy; 53 rdy = r; 54 55 for (fp = p, j = 0; fp; fp = fp->rgt) 56 for (fpt = fp->lft; fpt; fpt = fpt->rgt) 57 j++; /* count # of parameters */ 58 Npars = max(Npars, j); 59 60 return rdy; 61 } 62 63 int 64 find_maxel(Symbol *s) 65 { ProcList *p; 66 67 for (p = rdy; p; p = p->nxt) 68 if (p->n == s) 69 return p->s->maxel++; 70 return Elcnt++; 71 } 72 73 void 74 formdump(void) 75 { ProcList *p; 76 Lextok *f, *t; 77 int cnt; 78 79 for (p = rdy; p; p = p->nxt) 80 { if (!p->p) continue; 81 cnt = -1; 82 for (f = p->p; f; f = f->rgt) /* types */ 83 for (t = f->lft; t; t = t->rgt) /* formals */ 84 { if (t->ntyp != ',') 85 t->sym->Nid = cnt--; /* overload Nid */ 86 else 87 t->lft->sym->Nid = cnt--; 88 } 89 } 90 } 91 92 int 93 enable(Symbol *s, Lextok *n) /* s=name, n=actuals */ 94 { ProcList *p; 95 96 for (p = rdy; p; p = p->nxt) 97 if (strcmp(s->name, p->n->name) == 0) 98 { runnable(p); 99 setparams(run, p, n); 100 return (nproc-nstop-1); /* pid */ 101 } 102 return 0; /* process not found */ 103 } 104 105 void 106 start_claim(int n) 107 { ProcList *p; 108 109 for (p = rdy; p; p = p->nxt) 110 if (p->tn == n 111 && strcmp(p->n->name, ":never:") == 0) 112 { runnable(p); 113 Have_claim = run->pid; /* was 1 */ 114 return; 115 } 116 fatal("couldn't find claim", (char *) 0); 117 } 118 119 void 120 wrapup(int fini) 121 { 122 if (nproc != nstop) 123 { printf("#processes: %d\n", nproc-nstop); 124 dumpglobals(); 125 verbose &= ~1; /* no more globals */ 126 verbose |= 32; /* add process states */ 127 for (X = run; X; X = X->nxt) 128 talk(X); 129 } 130 printf("%d processes created\n", nproc); 131 132 if (xspin) exit(0); /* avoid an abort from xspin */ 133 if (fini) exit(1); 134 } 135 136 static char is_blocked[256]; 137 138 int 139 p_blocked(int p) 140 { register int i, j; 141 142 is_blocked[p%256] = 1; 143 for (i = j = 0; i < nproc - nstop; i++) 144 j += is_blocked[i]; 145 if (j >= nproc - nstop) 146 { memset(is_blocked, 0, 256); 147 return 1; 148 } 149 return 0; 150 } 151 152 Element * 153 silent_moves(Element *e) 154 { Element *f; 155 156 switch (e->n->ntyp) { 157 case GOTO: 158 if (Rvous) break; 159 f = get_lab(e->n, 1); 160 cross_dsteps(e->n, f->n); 161 return f; /* guard against goto cycles */ 162 case UNLESS: 163 return silent_moves(e->sub->this->frst); 164 case NON_ATOMIC: 165 case ATOMIC: 166 case D_STEP: 167 e->n->sl->this->last->nxt = e->nxt; 168 return silent_moves(e->n->sl->this->frst); 169 case '.': 170 return e->nxt; 171 } 172 return e; 173 } 174 175 void 176 sched(void) 177 { Element *e; 178 RunList *Y=0; /* previous process in run queue */ 179 RunList *oX; 180 SeqList *z; 181 int j, k; 182 short Choices[256]; 183 184 if (dumptab) 185 { formdump(); 186 symdump(); 187 dumplabels(); 188 return; 189 } 190 191 if (has_enabled && u_sync > 0) 192 { printf("spin: error: >> cannot use enabled() in "); 193 printf("models with synchronous channels <<\n"); 194 nr_errs++; 195 } 196 if (analyze) 197 { gensrc(); 198 return; 199 } else if (s_trail) 200 { match_trail(); 201 return; 202 } 203 if (claimproc) 204 printf("warning: claims are ignored in simulations\n"); 205 206 if (Interactive) Tval = 1; 207 208 X = run; 209 while (X) 210 { context = X->n; 211 if (X->pc && X->pc->n) 212 { lineno = X->pc->n->ln; 213 Fname = X->pc->n->fn; 214 } 215 depth++; LastStep = ZE; 216 oX = X; /* a rendezvous could change it */ 217 if (e = eval_sub(X->pc)) 218 { if (verbose&32 || verbose&4) 219 { if (X == oX) 220 { p_talk(X->pc, 1); 221 printf(" ["); 222 if (!LastStep) LastStep = X->pc; 223 comment(stdout, LastStep->n, 0); 224 printf("]\n"); 225 } 226 if (verbose&1) dumpglobals(); 227 if (verbose&2) dumplocal(X); 228 if (xspin) printf("\n"); /* xspin looks for these */ 229 } 230 oX->pc = e; LastX = X; 231 if (!Interactive) Tval = 0; 232 memset(is_blocked, 0, 256); 233 234 /* new implementation of atomic sequences */ 235 if (X->pc->status & (ATOM|L_ATOM)) 236 continue; /* no switch */ 237 } else 238 { depth--; 239 if (X->pc->n->ntyp == '@' 240 && X->pid == (nproc-nstop-1)) 241 { if (X != run) 242 Y->nxt = X->nxt; 243 else 244 run = X->nxt; 245 nstop++; 246 if (verbose&4) 247 { whoruns(1); 248 printf("terminates\n"); 249 } 250 LastX = X; 251 if (!Interactive) Tval = 0; 252 if (nproc == nstop) break; 253 memset(is_blocked, 0, 256); 254 } else 255 { if (!Interactive && p_blocked(X->pid)) 256 { if (Tval) break; 257 Tval = 1; 258 printf("timeout\n"); 259 } } } 260 Y = X; 261 if (Interactive) 262 { 263 try_again: printf("Select a statement\n"); 264 for (X = run, k = 1; X; X = X->nxt) 265 { if (X->pid > 255) break; 266 Choices[X->pid] = 0; 267 if (!X->pc) 268 continue; 269 Choices[X->pid] = k; 270 X->pc = silent_moves(X->pc); 271 if (!X->pc->sub && X->pc->n) 272 { if (!xspin && !Enabled0(X->pc)) 273 { k++; 274 continue; 275 } 276 printf("\tchoice %d: ", k++); 277 p_talk(X->pc, 0); 278 if (!Enabled0(X->pc)) 279 printf(" unexecutable,"); 280 printf(" ["); 281 comment(stdout, X->pc->n, 0); 282 printf("]\n"); 283 } else 284 for (z = X->pc->sub, j=0; z; z = z->nxt) 285 { Element *y = z->this->frst; 286 if (!y) continue; 287 288 if (!xspin && !Enabled0(y)) 289 { k++; 290 continue; 291 } 292 printf("\tchoice %d: ", k++); 293 p_talk(X->pc, 0); 294 if (!Enabled0(y)) 295 printf(" unexecutable,"); 296 printf(" ["); 297 comment(stdout, y->n, 0); 298 printf("]\n"); 299 } } 300 X = run; 301 if (xspin) 302 printf("Make Selection %d\n\n", k-1); 303 else 304 printf("Select [1-%d]: ", k-1); 305 fflush(stdout); 306 scanf("%d", &j); 307 if (j < 1 || j >= k) 308 { printf("\tchoice is outside range\n"); 309 goto try_again; 310 } 311 SubChoice = 0; 312 for (X = run; X; X = X->nxt) 313 { if (!X->nxt 314 || X->nxt->pid > 255 315 || j < Choices[X->nxt->pid]) 316 { 317 SubChoice = 1+j-Choices[X->pid]; 318 break; 319 } 320 } 321 } else 322 { j = (int) Rand()%(nproc-nstop); 323 while (j-- >= 0) 324 { X = X->nxt; 325 if (!X) X = run; 326 } } 327 } 328 context = ZS; 329 wrapup(0); 330 } 331 332 int 333 complete_rendez(void) 334 { RunList *orun = X, *tmp; 335 Element *s_was = LastStep; 336 Element *e; 337 338 if (s_trail) 339 return 1; 340 Rvous = 1; 341 for (X = run; X; X = X->nxt) 342 if (X != orun && (e = eval_sub(X->pc))) 343 { if (verbose&4) 344 { tmp = orun; orun = X; X = tmp; 345 if (!s_was) s_was = X->pc; 346 p_talk(s_was, 1); 347 printf(" ["); 348 comment(stdout, s_was->n, 0); 349 printf("]\n"); 350 tmp = orun; orun = X; X = tmp; 351 /* printf("\t"); */ 352 if (!LastStep) LastStep = X->pc; 353 p_talk(LastStep, 1); 354 printf(" ["); 355 comment(stdout, LastStep->n, 0); 356 printf("]\n"); 357 } 358 X->pc = e; 359 Rvous = 0; 360 return 1; 361 } 362 Rvous = 0; 363 X = orun; 364 return 0; 365 } 366 367 /***** Runtime - Local Variables *****/ 368 369 void 370 addsymbol(RunList *r, Symbol *s) 371 { Symbol *t; 372 int i; 373 374 for (t = r->symtab; t; t = t->next) 375 if (strcmp(t->name, s->name) == 0) 376 return; /* it's already there */ 377 378 t = (Symbol *) emalloc(sizeof(Symbol)); 379 t->name = s->name; 380 t->type = s->type; 381 t->nel = s->nel; 382 t->ini = s->ini; 383 t->setat = depth; 384 if (s->type != STRUCT) 385 { if (s->val) /* if already initialized, copy info */ 386 { t->val = (int *) emalloc(s->nel*sizeof(int)); 387 for (i = 0; i < s->nel; i++) 388 t->val[i] = s->val[i]; 389 } else 390 (void) checkvar(t, 0); /* initialize it */ 391 } else 392 { if (s->Sval) 393 fatal("saw preinitialized struct %s", s->name); 394 t->Slst = s->Slst; 395 t->Snm = s->Snm; 396 t->owner = s->owner; 397 t->context = r->n; 398 } 399 t->next = r->symtab; /* add it */ 400 r->symtab = t; 401 } 402 403 void 404 oneparam(RunList *r, Lextok *t, Lextok *a, ProcList *p) 405 { int k; int at, ft; 406 RunList *oX = X; 407 408 if (!a) 409 fatal("missing actual parameters: '%s'", p->n->name); 410 if (t->sym->nel != 1) 411 fatal("array in parameter list, %s", t->sym->name); 412 k = eval(a->lft); 413 414 at = Sym_typ(a->lft); 415 X = r; /* switch context */ 416 ft = Sym_typ(t); 417 418 if (at != ft && (at == CHAN || ft == CHAN)) 419 { char buf[128], tag1[32], tag2[32]; 420 (void) sputtype(tag1, ft); 421 (void) sputtype(tag2, at); 422 sprintf(buf, "type-clash in param-list of %s(..), (%s<-> %s)", 423 p->n->name, tag1, tag2); 424 non_fatal("%s", buf); 425 } 426 t->ntyp = NAME; 427 addsymbol(r, t->sym); 428 (void) setval(t, k); 429 430 X = oX; 431 } 432 433 void 434 setparams(RunList *r, ProcList *p, Lextok *q) 435 { Lextok *f, *a; /* formal and actual pars */ 436 Lextok *t; /* list of pars of 1 type */ 437 438 if (q) 439 { lineno = q->ln; 440 Fname = q->fn; 441 } 442 for (f = p->p, a = q; f; f = f->rgt) /* one type at a time */ 443 for (t = f->lft; t; t = t->rgt, a = (a)?a->rgt:a) 444 { if (t->ntyp != ',') 445 oneparam(r, t, a, p); /* plain var */ 446 else 447 oneparam(r, t->lft, a, p); /* expanded structure */ 448 } 449 } 450 451 Symbol * 452 findloc(Symbol *s) 453 { Symbol *r; 454 455 if (!X) 456 { /* fatal("error, cannot eval '%s' (no proc)", s->name); */ 457 return ZS; 458 } 459 for (r = X->symtab; r; r = r->next) 460 if (strcmp(r->name, s->name) == 0) 461 break; 462 if (!r) 463 { addsymbol(X, s); 464 r = X->symtab; 465 } 466 return r; 467 } 468 469 int 470 getlocal(Lextok *sn) 471 { Symbol *r, *s = sn->sym; 472 int n = eval(sn->lft); 473 474 r = findloc(s); 475 if (r && r->type == STRUCT) 476 return Rval_struct(sn, r, 1); /* 1 = check init */ 477 if (r) 478 { if (n >= r->nel || n < 0) 479 { printf("spin: indexing %s[%d] - size is %d\n", 480 s->name, n, r->nel); 481 non_fatal("array indexing error %s", s->name); 482 } else 483 { return cast_val(r->type, r->val[n]); 484 } } 485 486 return 0; 487 } 488 489 int 490 setlocal(Lextok *p, int m) 491 { Symbol *r = findloc(p->sym); 492 int n = eval(p->lft); 493 494 if (!r) return 1; 495 496 if (n >= r->nel || n < 0) 497 { printf("spin: indexing %s[%d] - size is %d\n", 498 r->name, n, r->nel); 499 non_fatal("array indexing error %s", r->name); 500 } else 501 { if (r->type == STRUCT) 502 (void) Lval_struct(p, r, 1, m); /* 1 = check init */ 503 else 504 { r->val[n] = m; 505 r->setat = depth; 506 } } 507 508 return 1; 509 } 510 511 void 512 whoruns(int lnr) 513 { if (!X) return; 514 515 if (lnr) printf("%3d: ", depth); 516 printf("proc "); 517 if (Have_claim) 518 { if (X->pid == Have_claim) 519 printf(" -"); 520 else if (X->pid > Have_claim) 521 printf("%2d", X->pid-1); 522 else 523 printf("%2d", X->pid); 524 } else 525 printf("%2d", X->pid); 526 printf(" (%s) ", X->n->name); 527 } 528 529 void 530 talk(RunList *r) 531 { 532 if (verbose&32 || verbose&4) 533 { p_talk(r->pc, 1); 534 printf("\n"); 535 if (verbose&1) dumpglobals(); 536 if (verbose&2) dumplocal(r); 537 } 538 } 539 540 void 541 p_talk(Element *e, int lnr) 542 { 543 whoruns(lnr); 544 if (e) 545 printf("line %3d %s (state %d)", 546 e->n?e->n->ln:-1, 547 e->n?e->n->fn->name:"-", 548 e->seqno); 549 } 550 551 int 552 remotelab(Lextok *n) 553 { int i; 554 555 lineno = n->ln; 556 Fname = n->fn; 557 if (n->sym->type) 558 fatal("not a labelname: '%s'", n->sym->name); 559 if ((i = find_lab(n->sym, n->lft->sym)) == 0) 560 fatal("unknown labelname: %s", n->sym->name); 561 return i; 562 } 563 564 int 565 remotevar(Lextok *n) 566 { int pno, i, trick=0; 567 RunList *Y; 568 569 lineno = n->ln; 570 Fname = n->fn; 571 if (!n->lft->lft) 572 { non_fatal("missing pid in %s", n->sym->name); 573 return 0; 574 } 575 576 pno = eval(n->lft->lft); /* pid - can cause recursive call */ 577 TryAgain: 578 i = nproc - nstop; 579 for (Y = run; Y; Y = Y->nxt) 580 if (--i == pno) 581 { if (strcmp(Y->n->name, n->lft->sym->name) != 0) 582 { if (!trick && Have_claim) 583 { trick = 1; pno++; 584 /* assumes user guessed the pid */ 585 goto TryAgain; 586 } 587 printf("remote ref %s[%d] refers to %s\n", 588 n->lft->sym->name, pno, Y->n->name); 589 non_fatal("wrong proctype %s", Y->n->name); 590 } 591 if (strcmp(n->sym->name, "_p") == 0) 592 return Y->pc->seqno; 593 break; 594 } 595 printf("remote ref: %s[%d] ", n->lft->sym->name, pno); 596 non_fatal("%s not found", n->sym->name); 597 598 return 0; 599 } 600