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