![[BACK]](/cvsweb/icons/back.gif){kind=icon}
Return to trace3.c CVS log ![[TXT]](/cvsweb/icons/text.gif){kind=icon}
![[DIR]](/cvsweb/icons/dir.gif){kind=icon}
Up to [Research Unix] / researchv8dc / cmd / trace|
Return to trace3.c CVS log | Up to [Research Unix] / researchv8dc / cmd / trace |
1.1 ! root 1: #include "stdio.h" ! 2: #include "trace.h" ! 3: #include "trace.d" ! 4: ! 5: #define BS(n) ((n) & ~(PASSED)) ! 6: ! 7: extern struct TBL *tbl; ! 8: extern struct LBT *lbt; ! 9: extern struct MBOX *mbox; ! 10: extern struct MNAME *fullname; ! 11: extern struct PROCSTACK **procstack; ! 12: ! 13: extern struct VARPARS *procpars; ! 14: extern struct TBLPARS *tblpars; ! 15: ! 16: extern struct LOCVARS *tblvars; ! 17: extern struct TBLPARS *tablpars; ! 18: ! 19: extern struct QUEUE **starter, **head, **tail; ! 20: extern struct QUEUE *s_first, *s_last; ! 21: extern struct VISIT *lastvisit; ! 22: ! 23: extern int *reftasks, *processes, *basics; ! 24: extern int *globvars, *inits, *state, *qsize; ! 25: extern int assertbl, abase, errortbl, ebase; ! 26: ! 27: extern int nrtbl, nrqs, nrrefs, nrprocs, nrinit; ! 28: extern int nrvars, nrmesgs, msgbase; ! 29: extern int maxlevel, maxreached; ! 30: ! 31: extern char noshortcut, prbyq, timedd, blast, qandirty, muststore; ! 32: extern char maxxed, completed, lockplus, firstlock; ! 33: ! 34: extern long locksf, normf, loopsf; ! 35: ! 36: short lastqueue; /* the last queue addressed */ ! 37: int level = 0; ! 38: double COUNT = 0; ! 39: ! 40: char *emalloc(), *Realloc(), *Emalloc(); ! 41: ! 42: #include "assert.c" ! 43: ! 44: determine(m) ! 45: { ! 46: if (m >= 3*MANY) ! 47: return 0; /* constant */ ! 48: else if (m >= 2*MANY) ! 49: return 1; /* parameter */ ! 50: else if (m >= MANY) ! 51: return 2; /* local */ ! 52: else if (m >= 0) ! 53: return 3; /* global */ ! 54: else if (m < -3*MANY) ! 55: return 5; /* negative number */ ! 56: else if (m <= -2) ! 57: return 4; /* expression */ ! 58: else ! 59: whoops("cannot happen - determine"); ! 60: } ! 61: ! 62: convert(m, pr) ! 63: { int res; ! 64: int n = m; ! 65: ! 66: /* convert a pvar: global, local, parameter, or a constant */ ! 67: ! 68: switch (determine(n)) { ! 69: case 5: res = n + 3*MANY; ! 70: break; ! 71: case 4: res = evalcond(-(m+2), pr); ! 72: break; ! 73: case 0: res = n - 3*MANY; ! 74: break; ! 75: case 1: res = wapper(m, pr); ! 76: break; ! 77: case 2: n -= MANY; ! 78: if (n >= 0 && n < (int) procpars[pr].nrlvars) ! 79: res = (int) procpars[pr].lvarvals[n]; ! 80: else ! 81: whoops("cannot happen 1 - convert"); ! 82: break; ! 83: case 3: if (n >= 0 && n < nrvars) ! 84: res = globvars[n]; ! 85: else ! 86: whoops("cannot happen 2 - convert"); ! 87: break; ! 88: default: ! 89: whoops("cannot happen 3 - convert"); /* a parameter */ ! 90: break; ! 91: } ! 92: ! 93: return res; ! 94: } ! 95: ! 96: wapper(n, pr) ! 97: { int x = n - 2*MANY; ! 98: int y; ! 99: if (x < 0 || x >= MANY) ! 100: return n; /* not a parameter */ ! 101: if (x >= procpars[pr].nrvs) ! 102: whoops("cannot happen 1 - wapper"); ! 103: ! 104: y = (int) procpars[pr].vs[x]; ! 105: ! 106: if (y >= 2*MANY && y < 3*MANY) ! 107: whoops("cannot happen 2 - wapper"); ! 108: return y; ! 109: } ! 110: ! 111: mapper(n, pr) /* convert a message parameter */ ! 112: { register int x = n - MANY; ! 113: ! 114: if (x < 0 || x >= MANY) ! 115: return n; /* not a parameter */ ! 116: if (x >= procpars[pr].nrms) ! 117: whoops("cannot happen - mapper"); ! 118: return ((int)procpars[pr].ms[x]); ! 119: } ! 120: ! 121: matchon(n, m, t, trial, TT, pr) ! 122: { ! 123: if (trial == 2) ! 124: return (TT == TMO && qsize[m] == 0); ! 125: else ! 126: { ! 127: switch (TT) { ! 128: case FCT : ! 129: case SPN : return 1; ! 130: case CND : return (evalcond(n, pr)); ! 131: case DFL : return (qsize[m] > 0 && no_other(t,head[m]->mesg,pr)); ! 132: case INP : return (qsize[m] > 0 && BS(head[m]->mesg) == n); ! 133: case TMO : return (noshortcut && qsize[m] == 0); ! 134: case OUTP: return (qsize[m] < mbox[m].limit); ! 135: default : whoops("cannot happen - matchon"); ! 136: } ! 137: } ! 138: } ! 139: ! 140: no_other(x, yy, pr) ! 141: { struct TBL *tmp = &(tbl[x]); ! 142: int y = BS(yy); ! 143: int j = tmp->nrcols; ! 144: int h = state[pr]; ! 145: int i; ! 146: ! 147: for (i = 0; i < j; i++) ! 148: { if (tmp->coltyp[i] == INP ! 149: && tmp->ptr[h][i].nrpils > 0 ! 150: && y == lbt[pr].mapcol[i]) ! 151: return 0; ! 152: } ! 153: return 1; ! 154: } ! 155: ! 156: send(m, to, with, pr) ! 157: { struct QUEUE *tmp; ! 158: struct QUEUE *hook = tail[to]; ! 159: int what = NONE; ! 160: ! 161: if (with != NONE) ! 162: { if ((what = convert(with, pr)) >= USED - 1 || what < 0) ! 163: { fprintf(stderr, "cargo: %d\n", what); ! 164: whoops("cargo too large or negative"); ! 165: } ! 166: hook->cargo = (unsigned short) ( what | USED ); ! 167: } else ! 168: hook->cargo = (unsigned short) 0; ! 169: ! 170: if (qsize[to] >= mbox[to].limit) ! 171: whoops("shouldn't happen - send"); ! 172: ! 173: tmp = (struct QUEUE *) emalloc(sizeof(struct QUEUE)); ! 174: tmp->last = hook; ! 175: ! 176: hook->mesg = (short) m; ! 177: hook->next = tmp; ! 178: hook->s_back = s_last; ! 179: hook->s_forw = NULL; ! 180: if (s_last == NULL) ! 181: s_first = hook; ! 182: else ! 183: s_last->s_forw = hook; ! 184: ! 185: s_last = hook; ! 186: tail[to] = tmp; ! 187: qsize[to]++; ! 188: ! 189: require(OUTP, m, to, with, pr); ! 190: ! 191: return 1; ! 192: } ! 193: ! 194: receive(from, with, pr, ice) ! 195: struct FREEZE *ice; ! 196: { struct QUEUE *hook; ! 197: int what, wither; ! 198: ! 199: if (qsize[from] <= 0) ! 200: whoops("cannot happen - receive"); ! 201: ! 202: hook = head[from]; ! 203: if (hook->cargo & USED) ! 204: { what = (int) ((hook->cargo) & (~USED)); ! 205: if (with == NONE) ! 206: fprintf(stderr, "cargo %d sent but not expected\n", what); ! 207: else ! 208: { ice->whichvar = wither = wapper(with, pr); ! 209: if (wither >= 3*MANY || wither <= -3*MANY) ! 210: whoops("receiving into a constant..."); ! 211: if (wither < MANY) ! 212: { ice->oldvalue = globvars[wither]; ! 213: globvars[wither] = what; ! 214: } else ! 215: { int n = wither - MANY; ! 216: if (n >= 0 && n < (int) procpars[pr].nrlvars) ! 217: { ice->oldvalue = procpars[pr].lvarvals[n]; ! 218: procpars[pr].lvarvals[n] = (short) what; ! 219: } else ! 220: whoops("cannot happen 2 - receive"); ! 221: } ! 222: } ! 223: } else if (with != NONE) ! 224: fprintf(stderr, "cargo expected %d but none sent\n", with); ! 225: ! 226: hook->mesg |= PASSED; ! 227: ! 228: head[from] = hook->next; ! 229: qsize[from]--; ! 230: ! 231: require(INP, (hook->mesg & (~PASSED)), from, what, pr); ! 232: ! 233: return 1; ! 234: } ! 235: ! 236: unrecv(from) ! 237: { ! 238: if (head[from] == starter[from]) ! 239: whoops("cannot happen - unrecv"); ! 240: ! 241: head[from] = head[from]->last; ! 242: head[from]->mesg &= (~PASSED); ! 243: ! 244: qsize[from]++; ! 245: } ! 246: ! 247: unsend() ! 248: { short i = lastqueue; ! 249: if (tail[i] == starter[i] || (tail[i] = tail[i]->last) != s_last) ! 250: whoops("cannot happen - unsend"); ! 251: ! 252: if ((s_last = s_last->s_back) != NULL) ! 253: s_last->s_forw = NULL; ! 254: else ! 255: s_first = NULL; ! 256: efree(tail[i]->next); ! 257: ! 258: qsize[i]--; ! 259: } ! 260: ! 261: output(tag, willabort) ! 262: char *tag; ! 263: { struct QUEUE *tmp; ! 264: ! 265: printf("%s", tag); ! 266: ! 267: if ((tmp = s_first) != NULL) ! 268: { formatted(); ! 269: if (prbyq != 2) ! 270: do putname(tmp); while ((tmp = tmp->s_forw) != NULL); ! 271: putchar('\n'); ! 272: } else ! 273: printf("null output\n"); ! 274: ! 275: if (willabort == 2 || (firstlock && willabort == 1)) ! 276: { completed = 1; ! 277: postlude(); ! 278: } ! 279: } ! 280: ! 281: putname(tmp) ! 282: struct QUEUE *tmp; ! 283: { int k = (int) (BS(tmp->mesg)) - msgbase; ! 284: ! 285: if (tmp->mesg & PASSED) ! 286: printf("%s", fullname[k].mname); ! 287: else ! 288: printf("[%s]", fullname[k].mname); ! 289: ! 290: if (tmp->cargo & USED) ! 291: printf("(%d),", (tmp->cargo & (~USED))); ! 292: else ! 293: putchar(','); ! 294: } ! 295: ! 296: inendstate() ! 297: { int i, j, k; ! 298: ! 299: for (i = 0, k = nrprocs; i < nrprocs; i++) ! 300: { j = processes[i]; ! 301: if (j != basics[i] || tbl[j].endrow[state[i]] != 1) ! 302: k--; ! 303: } ! 304: return k; ! 305: } ! 306: ! 307: formatted() ! 308: { struct QUEUE *tmp = s_first; ! 309: int i; ! 310: ! 311: if (tmp == NULL) ! 312: return; ! 313: ! 314: switch((int) prbyq) { ! 315: case 0: break; ! 316: case 1: ! 317: for (i = 0; i < nrqs; i++) ! 318: { printf("\n\t%s = {", mbox[i].qname); ! 319: for (tmp = starter[i]; tmp != tail[i]; tmp = tmp->next) ! 320: putname(tmp); ! 321: printf("}"); ! 322: } ! 323: printf("\nexecution sequence:\n\t"); ! 324: break; ! 325: case 2: putchar('\n'); ! 326: for (i = 0; i < nrqs; i++) ! 327: printf("%2d = %s\n", i, mbox[i].qname); ! 328: for (i = 0; i < nrqs; i++) ! 329: printf("\t%2d", i); ! 330: putchar('\n'); ! 331: do ! 332: { for (i = whichq(BS(tmp->mesg)); i >= 0; i--) ! 333: putchar('\t'); ! 334: putname(tmp); ! 335: putchar('\n'); ! 336: } while ((tmp = tmp->s_forw) != NULL); ! 337: break; ! 338: } ! 339: } ! 340: ! 341: putloop(now, aa) ! 342: struct STUFF *now; char aa; ! 343: { register struct QUEUE *tmp = s_first; ! 344: struct QUEUE *at = now->s; ! 345: ! 346: if (aa) ! 347: printf("loop:\t"); ! 348: else ! 349: printf("assertion violated: "); ! 350: ! 351: if (s_first != NULL) ! 352: { formatted(); ! 353: if (prbyq != 2) ! 354: { do ! 355: { putname(tmp); ! 356: if (tmp == at) ! 357: printf("//"); ! 358: } while ((tmp = tmp->s_forw) != NULL); ! 359: printf("//\n"); ! 360: } ! 361: } else ! 362: printf("null output\n"); ! 363: } ! 364: ! 365: ppop(pr) ! 366: { struct PROCSTACK *tmp = procstack[pr]; ! 367: int i = (int) procstack[pr]->uptable; ! 368: ! 369: if (procstack[pr] == NULL) ! 370: whoops("cannot happen - ppop"); ! 371: restorvarpars(tmp->varparsaved, pr); ! 372: ! 373: procstack[pr] = procstack[pr]->follow; ! 374: ! 375: efree(tmp->varparsaved); ! 376: efree(tmp); ! 377: ! 378: return i; /* we're returing to this table */ ! 379: } ! 380: ! 381: ppush(pr, what, tr) ! 382: { struct PROCSTACK *tmp; ! 383: ! 384: tmp = (struct PROCSTACK *) ! 385: emalloc(sizeof(struct PROCSTACK)); ! 386: ! 387: tmp->varparsaved = (struct VARPARS *) ! 388: emalloc(sizeof(struct VARPARS)); ! 389: ! 390: savevarpars (tmp->varparsaved, pr); ! 391: ! 392: tmp->uptable = (short) what; ! 393: tmp->uptransf = (short) tr; ! 394: tmp->follow = procstack[pr]; ! 395: procstack[pr] = tmp; ! 396: } ! 397: ! 398: setlvars(to, pr) ! 399: { register int i; ! 400: short z = tblvars[to].nrlvars; ! 401: ! 402: if (z > tablpars[pr].nrlvars) ! 403: { if (tablpars[pr].nrlvars > 0) ! 404: procpars[pr].lvarvals = (short *) ! 405: Realloc(procpars[pr].lvarvals, z * sizeof(short)); ! 406: else ! 407: procpars[pr].lvarvals = (short *) ! 408: Emalloc(z * sizeof(short)); ! 409: ! 410: tablpars[pr].nrlvars = z; ! 411: } ! 412: procpars[pr].nrlvars = z; ! 413: ! 414: for (i = 0; i < z; i++) ! 415: procpars[pr].lvarvals[i] = convert(tblvars[to].lvarvals[i], pr); ! 416: } ! 417: ! 418: setpars(from, to, pr) ! 419: struct CPARS *from; ! 420: { struct VARPARS tbuff; ! 421: register int i; ! 422: short x = tblpars[to].nrms; ! 423: short y = tblpars[to].nrvs; ! 424: ! 425: savemapped(&tbuff, from, pr); /* mapper() needs old nrms & nrvs */ ! 426: ! 427: if (x > tablpars[pr].nrms) ! 428: { if (tablpars[pr].nrms > 0) ! 429: procpars[pr].ms = (short *) ! 430: Realloc(procpars[pr].ms, x * sizeof(short)); ! 431: else ! 432: procpars[pr].ms = (short *) ! 433: Emalloc(x * sizeof(short)); ! 434: ! 435: tablpars[pr].nrms = x; ! 436: } ! 437: if (y > tablpars[pr].nrvs) ! 438: { if (tablpars[pr].nrvs > 0) ! 439: procpars[pr].vs = (short *) ! 440: Realloc(procpars[pr].vs, y * sizeof(short)); ! 441: else ! 442: procpars[pr].vs = (short *) ! 443: Emalloc(y * sizeof(short)); ! 444: ! 445: tablpars[pr].nrvs = y; ! 446: } ! 447: ! 448: procpars[pr].nrms = tbuff.nrms; ! 449: procpars[pr].nrvs = tbuff.nrvs; ! 450: ! 451: for (i = 0; i < procpars[pr].nrms; i++) ! 452: procpars[pr].ms[i] = tbuff.ms[i]; ! 453: ! 454: for (i = 0; i < procpars[pr].nrvs; i++) ! 455: procpars[pr].vs[i] = tbuff.vs[i]; ! 456: ! 457: efree(tbuff.ms); efree(tbuff.vs); ! 458: } ! 459: ! 460: retable(prc, ice) ! 461: struct FREEZE *ice; ! 462: { struct CUBE *it, *here; ! 463: int t = processes[prc]; ! 464: ! 465: if (ice->cube == NULL) ! 466: { here = ice->cube = (struct CUBE *) ! 467: emalloc(sizeof(struct CUBE)); ! 468: here->pntr = here->rtnp = NULL; ! 469: } else ! 470: { for (it = ice->cube; it->pntr != NULL; it = it->pntr) ! 471: ; ! 472: it->pntr = (struct CUBE *) ! 473: emalloc(sizeof(struct CUBE)); ! 474: it->pntr->rtnp = it; ! 475: here = it->pntr; ! 476: here->pntr = NULL; ! 477: } ! 478: here->poporpush = POP; ! 479: here->which = (short) prc; ! 480: here->procsaved = (short) t; ! 481: here->transfsaved = procstack[prc]->uptransf; ! 482: here->varparsaved = (struct VARPARS *) emalloc(sizeof(struct VARPARS)); ! 483: ! 484: savevarpars(here->varparsaved, prc); ! 485: ! 486: processes[prc] = ppop(prc); ! 487: fiddler(prc); ! 488: state[prc] = (int) here->transfsaved; ! 489: muststore = tbl[processes[prc]].labrow[state[prc]]; ! 490: ! 491: } ! 492: ! 493: savevarpars(at, j) ! 494: struct VARPARS *at; ! 495: { register int i; ! 496: struct VARPARS *it; ! 497: ! 498: it = &(procpars[j]); ! 499: at->nrms = it->nrms; ! 500: at->nrvs = it->nrvs; ! 501: at->nrlvars = it->nrlvars; ! 502: ! 503: at->ms = (short *) emalloc(it->nrms * sizeof(short)); ! 504: at->vs = (short *) emalloc(it->nrvs * sizeof(short)); ! 505: at->lvarvals = (short *) emalloc(it->nrlvars * sizeof(short)); ! 506: ! 507: for (i = 0; i < at->nrms; i++) ! 508: at->ms[i] = it->ms[i]; ! 509: for (i = 0; i < at->nrvs; i++) ! 510: at->vs[i] = it->vs[i]; ! 511: for (i = 0; i < it->nrlvars; i++) ! 512: at->lvarvals[i] = it->lvarvals[i]; ! 513: ! 514: } ! 515: ! 516: savemapped(at, it, j) ! 517: struct VARPARS *at; ! 518: struct CPARS *it; ! 519: { register int i; ! 520: ! 521: at->nrms = it->nrms; ! 522: at->nrvs = it->nrvs; ! 523: ! 524: at->ms = (short *) emalloc(it->nrms * sizeof(short)); ! 525: at->vs = (short *) emalloc(it->nrvs * sizeof(short)); ! 526: ! 527: for (i = 0; i < at->nrms; i++) ! 528: at->ms[i] = (short) mapper(it->ms[i], j); ! 529: for (i = 0; i < at->nrvs; i++) ! 530: at->vs[i] = (short) convert(it->vs[i], j); ! 531: } ! 532: ! 533: restorvarpars(at, pr) ! 534: struct VARPARS *at; ! 535: { register int i; ! 536: ! 537: procpars[pr].nrms = at->nrms; ! 538: procpars[pr].nrvs = at->nrvs; ! 539: procpars[pr].nrlvars = at->nrlvars; ! 540: ! 541: for (i = 0; i < at->nrms; i++) ! 542: procpars[pr].ms[i] = at->ms[i]; ! 543: for (i = 0; i < at->nrvs; i++) ! 544: procpars[pr].vs[i] = at->vs[i]; ! 545: for (i = 0; i < at->nrlvars; i++) ! 546: procpars[pr].lvarvals[i] = at->lvarvals[i]; ! 547: ! 548: efree(at->ms); ! 549: efree(at->vs); ! 550: efree(at->lvarvals); ! 551: ! 552: } ! 553: ! 554: freeze(icy) ! 555: struct FREEZE *icy; ! 556: { register int i; ! 557: struct FREEZE *ice = icy; ! 558: ! 559: ice->statsaved = (short *) emalloc(nrprocs * sizeof(short)); ! 560: ice->varsaved = (short *) emalloc(nrvars * sizeof(short)); ! 561: ! 562: ice->lastsav = lastqueue; ! 563: ice->cube = NULL; ! 564: ! 565: for (i = 0; i < nrvars; i++) ! 566: ice->varsaved[i] = (short) globvars[i]; ! 567: ! 568: for (i = 0; i < nrprocs; i++) ! 569: { ice->statsaved[i] = (short) state[i]; ! 570: ! 571: while (tbl[processes[i]].deadrow[state[i]] && procstack[i] != NULL) ! 572: retable(i, ice); ! 573: } ! 574: } ! 575: ! 576: unfreeze(ice) ! 577: struct FREEZE *ice; ! 578: { struct CUBE *here; ! 579: register int i; ! 580: ! 581: lastqueue = ice->lastsav; ! 582: ! 583: for (i = 0; i < nrprocs; i++) ! 584: state[i] = (int) ice->statsaved[i]; ! 585: for (i = 0; i < nrvars; i++) ! 586: globvars[i] = (int) ice->varsaved[i]; ! 587: ! 588: if ((here = ice->cube) != NULL) ! 589: while (here->pntr != NULL) ! 590: here = here->pntr; ! 591: ! 592: for (; here != NULL;) ! 593: { i = (int) here->which; ! 594: if (here->poporpush == PUSH) ! 595: processes[i] = ppop(i); ! 596: else ! 597: { /* use cube to restore the values from before the ppop */ ! 598: ppush(i, processes[i], (int) here->transfsaved); ! 599: restorvarpars (here->varparsaved, i); ! 600: ! 601: processes[i] = (int) here->procsaved; ! 602: efree(here->varparsaved); ! 603: } ! 604: efree(here); ! 605: fiddler(i); ! 606: ! 607: if (here == ice->cube) ! 608: break; ! 609: else ! 610: here = here->rtnp; ! 611: } ! 612: efree(ice->statsaved); ! 613: efree(ice->varsaved); ! 614: } ! 615: ! 616: FSE(I) ! 617: { short g, h, i, j, k, t, x, y, z, X, Y, how; ! 618: char progress=0, internal; ! 619: struct FREEZE delta; ! 620: struct STATE *inloop(), *iam = NULL; ! 621: struct VISIT *ticket; ! 622: ! 623: if (level >= maxreached) ! 624: { ! 625: if (maxxed && level >= maxlevel) ! 626: return; ! 627: ! 628: if (level > maxreached) ! 629: maxreached = level; ! 630: } ! 631: freeze(&delta); ! 632: ! 633: if (muststore && (iam = inloop()) == NULL) ! 634: { unfreeze(&delta); ! 635: return; ! 636: } ! 637: ! 638: /* ! 639: * this state has not been seen before; the state ! 640: * information has now been saved in the structure ! 641: * `STATE'; queue information has been saved in the ! 642: * last (iam->nrvisits) `VISIT' template of this state; ! 643: * we must save a pointer to this template in a local variable: ! 644: * to be able to mark it `analyzed' when we return ! 645: * for efficiency a pointer to the last visit is kept in a global `lastvisit' ! 646: */ ! 647: ticket = lastvisit; ! 648: level++; ! 649: COUNT += (double) 1; ! 650: ! 651: /* three tries: ! 652: * 1st try accepts internal moves (no timeouts, no outputs), ! 653: * 2nd try accepts any moves except timeouts, ! 654: * 3rd try accepts only timeouts. ! 655: */ ! 656: ! 657: for (X = 0; X <= 2; X++) ! 658: { internal = 0; ! 659: for (g = 0, i = I; g < nrprocs; g++, i = (i+1)%nrprocs) ! 660: { t = processes[i]; ! 661: k = state[i]; ! 662: ! 663: if (X == 0 && tbl[t].badrow[k]) ! 664: continue; ! 665: ! 666: for (j = 0; j < tbl[t].nrcols; j++) ! 667: { if ((z = tbl[t].ptr[k][j].nrpils) == 0) ! 668: continue; ! 669: ! 670: x = lbt[i].mapcol[j]; ! 671: y = lbt[i].orgcol[j]; ! 672: Y = tbl[t].coltyp[j]; ! 673: ! 674: if (matchon(x, y, t, X, Y, i)) ! 675: { for (h = 0; h < z; h++) ! 676: { how = forward(t, k, j, h, x, y, i, Y, &delta); ! 677: ! 678: if (qandirty || how == 0 || how >= LV || how == TC) ! 679: internal = 1; ! 680: ! 681: progress++; ! 682: FSE(0); ! 683: backup(k, how, y, i, &delta); ! 684: } } /* innermost loop: non-determinism */ ! 685: if (blast && progress > 0) ! 686: break; ! 687: } /* inner loop: options per process */ ! 688: if (internal) break; ! 689: } /* outer loop: parallelism */ ! 690: if (progress) break; /* normal exit */ ! 691: } /* outermost loop: 2 trials */ ! 692: if (progress == 0) ! 693: { ! 694: if ((k = inendstate()) == nrprocs) ! 695: { normf++; ! 696: if (assertholds()) ! 697: output("endstate: ", 0); ! 698: else ! 699: output("assertion violated: ", 0); ! 700: } ! 701: else ! 702: { locksf++; ! 703: if (k == 0) ! 704: output("deadlock: ", 1); ! 705: else ! 706: output("partial lock: ", 1); ! 707: } ! 708: } ! 709: level--; ! 710: ! 711: unfreeze(&delta); ! 712: if (iam != NULL) ! 713: { mark(iam, ticket); /* mark visit `analyzed' in hash table */ ! 714: if (progress == 0 || level >= maxlevel-3) ! 715: swiffle(iam, ticket); /* save pointers in fast lookup table */ ! 716: else ! 717: addspoke(iam, ticket); /* make hook in 2nd order lookup table */ ! 718: } ! 719: } ! 720: ! 721: forward(tb, k, j, h, m, from, pr, TT, ice) ! 722: struct FREEZE *ice; ! 723: { int how = 0, n = m; ! 724: struct ELM *at; ! 725: ! 726: ice->whichvar = NONE; ! 727: ! 728: at = &(tbl[tb].ptr[k][j].one[h]); ! 729: ! 730: switch (TT) { ! 731: case SPN: how = evalexpr(at->valtrans, pr, ice); ! 732: break; ! 733: case CND: break; /* `matchon()' already checked it */ ! 734: case FCT: m = (int) tbl[tb].calls[n].callwhat; ! 735: ppush(pr, processes[pr], (int) at->transf); ! 736: setpars(&(tbl[tb].calls[n]), reftasks[m], pr); ! 737: setlvars(reftasks[m], pr); ! 738: processes[pr] = reftasks[m]; ! 739: fiddler(pr); ! 740: state[pr] = 0; ! 741: muststore = tbl[processes[pr]].labrow[0]; ! 742: return TC; ! 743: case TMO: send(m, from, NONE, pr); ! 744: receive(from, NONE, pr, ice); ! 745: lastqueue = (short) from; ! 746: how = TO; ! 747: break; ! 748: case DFL: ! 749: case INP: receive(from, (int) at->valtrans, pr, ice); ! 750: how = RO; ! 751: break; ! 752: case OUTP: send(m, from, (int) at->valtrans, pr); ! 753: lastqueue = (short) from; ! 754: how |= SO; ! 755: break; ! 756: } ! 757: state[pr] = (int) at->transf; ! 758: muststore = tbl[processes[pr]].labrow[state[pr]]; ! 759: ! 760: return (how); ! 761: } ! 762: ! 763: backup(k, how, bx, i, ice) ! 764: struct FREEZE *ice; ! 765: { int u = (int) ice->whichvar; ! 766: ! 767: if (u != NONE) ! 768: { if (u >= MANY) ! 769: procpars[i].lvarvals[u-MANY] = ice->oldvalue; ! 770: else ! 771: globvars[u] = ice->oldvalue; ! 772: } ! 773: switch (how) { ! 774: case TC: u = processes[i]; ! 775: processes[i] = ppop(i); ! 776: fiddler(i); ! 777: break; ! 778: case TO: unrecv(bx); ! 779: case SO: unsend(); ! 780: peekassert(ice); ! 781: break; ! 782: case SR: unsend(); ! 783: case RO: unrecv(bx); ! 784: peekassert(ice); ! 785: default: break; ! 786: } state[i] = k; ! 787: } ! 788: ! 789: fiddler(pr) ! 790: { register int i; ! 791: register int t = processes[pr]; ! 792: ! 793: for (i = 0; i < tbl[t].nrcols; i++) ! 794: if (tbl[t].colmap[i] >= MANY) ! 795: { lbt[pr].mapcol[i] = mapper(tbl[t].colmap[i], pr); ! 796: lbt[pr].orgcol[i] = whichq(lbt[pr].mapcol[i]); ! 797: } else ! 798: { lbt[pr].mapcol[i] = tbl[t].colmap[i]; ! 799: lbt[pr].orgcol[i] = tbl[t].colorg[i]; ! 800: } ! 801: ! 802: }
This archive runs on limited infrastructure. Preserving old code on modern bandwidth. Automated agents are requested to crawl responsibly.