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