|
|
1.1 ! root 1: # To unbundle, sh this file ! 2: echo assert.c 1>&2 ! 3: sed 's/.//' >assert.c <<'//GO.SYSIN DD assert.c' ! 4: -#include "trace.h" ! 5: -#include "trace.d" ! 6: - ! 7: - extern struct TBL *tbl; ! 8: - extern int *globvars, nrvars; ! 9: - extern int assertbl, abase, errortbl, ebase; ! 10: - ! 11: -require(TT, stuff, by) ! 12: -{ ! 13: - if (assertbl != NONE) ! 14: - assert(TT, stuff, by); ! 15: - if (errortbl != NONE) ! 16: - errort(TT, stuff, by); ! 17: -} ! 18: - ! 19: -inscope(TT, stuff, by) ! 20: -{ register int i; ! 21: - ! 22: - for (i = 0; i < tbl[assertbl].nrcols; i++) ! 23: - if (TT == tbl[assertbl].coltyp[i] ! 24: - && stuff == tbl[assertbl].colmap[i] ! 25: - && by == tbl[assertbl].colorg[i]) ! 26: - return 1; ! 27: - ! 28: - return 0; ! 29: -} ! 30: - ! 31: -assert(TT, stuff, by) ! 32: -{ int h, i, j, x, frst; ! 33: - ! 34: - for (frst = 0; frst < tbl[assertbl].nrcols; frst++) ! 35: - if (tbl[assertbl].coltyp[frst] == TT ! 36: - && stuff == tbl[assertbl].colmap[frst] ! 37: - && by == tbl[assertbl].colorg[frst]) ! 38: - break; ! 39: - ! 40: - if (frst == tbl[assertbl].nrcols) ! 41: - return; /* not within assertion's scope */ ! 42: - ! 43: - for (i = 0; i < tbl[assertbl].nrrows; i++) ! 44: - { ! 45: - if (globvars[i+abase] != 1) ! 46: - continue; ! 47: - ! 48: - for (j = frst; j < tbl[assertbl].nrcols; j++) ! 49: - { ! 50: - if (TT == tbl[assertbl].coltyp[j] ! 51: - && stuff == tbl[assertbl].colmap[j] ! 52: - && by == tbl[assertbl].colorg[j]) ! 53: - { ! 54: - if (tbl[assertbl].ptr[i][j].nrpils == 0) ! 55: - output("assertion violated: ", 1); ! 56: - else ! 57: - for (h = 0; h < tbl[assertbl].ptr[i][j].nrpils; h++) ! 58: - { x = tbl[assertbl].ptr[i][j].one[h].transf; ! 59: - globvars[x+abase] = 2; ! 60: - globvars[i+abase] = 0; ! 61: - } } }} ! 62: - for (i = abase; i < nrvars; i++) ! 63: - if (globvars[i] == 2) ! 64: - globvars[i] = 1; ! 65: -} ! 66: - ! 67: -assertholds() ! 68: -{ int i; ! 69: - if (assertbl == NONE) ! 70: - return 1; ! 71: - ! 72: - for (i = abase; i < nrvars; i++) ! 73: - if (globvars[i] && tbl[assertbl].endrow[i-abase]) ! 74: - return 1; ! 75: - return 0; ! 76: -} ! 77: - ! 78: -errort(TT, stuff, by) ! 79: -{ int h, i, j, x, frst; ! 80: - ! 81: - for (frst = 0; frst < tbl[errortbl].nrcols; frst++) ! 82: - if (tbl[errortbl].coltyp[frst] == TT ! 83: - && stuff == tbl[errortbl].colmap[frst] ! 84: - && by == tbl[errortbl].colorg[frst]) ! 85: - break; ! 86: - ! 87: - if (frst == tbl[errortbl].nrcols) ! 88: - return; /* not within assertion's scope */ ! 89: - ! 90: - for (i = 0; i < tbl[errortbl].nrrows; i++) ! 91: - { ! 92: - if (globvars[i+ebase] != 1) ! 93: - continue; ! 94: - ! 95: - for (j = frst; j < tbl[errortbl].nrcols; j++) ! 96: - { ! 97: - if (TT == tbl[errortbl].coltyp[j] ! 98: - && stuff == tbl[errortbl].colmap[j] ! 99: - && by == tbl[errortbl].colorg[j]) ! 100: - { ! 101: - if (tbl[errortbl].ptr[i][j].nrpils == 0) ! 102: - globvars[i+ebase] = 0; ! 103: - else ! 104: - for (h = 0; h < tbl[errortbl].ptr[i][j].nrpils; h++) ! 105: - { x = tbl[errortbl].ptr[i][j].one[h].transf; ! 106: - globvars[x+ebase] = 2; ! 107: - globvars[i+ebase] = 0; ! 108: - } ! 109: - } ! 110: - } ! 111: - } ! 112: - for (i = ebase; i < nrvars; i++) ! 113: - if (globvars[i] == 2) ! 114: - { globvars[i] = 1; ! 115: - if (tbl[errortbl].endrow[i-ebase]) ! 116: - output("error matched: ", 2); ! 117: - } ! 118: - globvars[ebase] = 1; ! 119: -} ! 120: - ! 121: -peekassert(ice) ! 122: - struct FREEZE *ice; ! 123: -{ register int i; ! 124: - if (assertbl != NONE) ! 125: - for (i = abase; i < nrvars; i++) ! 126: - globvars[i] = ice->varsaved[i]; ! 127: - else if (errortbl != NONE) ! 128: - for (i = ebase; i < nrvars; i++) ! 129: - globvars[i] = ice->varsaved[i]; ! 130: -} ! 131: //GO.SYSIN DD assert.c ! 132: echo cmalloc.c 1>&2 ! 133: sed 's/.//' >cmalloc.c <<'//GO.SYSIN DD cmalloc.c' ! 134: -#ifdef debug ! 135: -#define ASSERT(p) if(!(p))botch("p");else ! 136: -botch(s) ! 137: -char *s; ! 138: -{ ! 139: - printf("assertion botched: %s\n",s); ! 140: - abort(); ! 141: -} ! 142: -#else ! 143: -#define ASSERT(p) ! 144: -#endif ! 145: - ! 146: -/* C storage allocator ! 147: - * circular first-fit strategy ! 148: - * works with noncontiguous, but monotonically linked, arena ! 149: - * each block is preceded by a ptr to the (pointer of) ! 150: - * the next following block ! 151: - * blocks are exact number of words long ! 152: - * aligned to the data type requirements of ALIGN ! 153: - * pointers to blocks must have BUSY bit 0 ! 154: - * bit in ptr is 1 for busy, 0 for idle ! 155: - * gaps in arena are merely noted as busy blocks ! 156: - * last block of arena is empty and ! 157: - * has a pointer to first ! 158: - * idle blocks are coalesced during space search ! 159: - * ! 160: - * a different implementation may need to redefine ! 161: - * ALIGN, NALIGN, BLOCK, BUSY, INT ! 162: - * where INT is integer type to which a pointer can be cast ! 163: -*/ ! 164: -#define INT int ! 165: -#define ALIGN int ! 166: -#define NALIGN 1 ! 167: -#define WORD sizeof(union store) ! 168: -#define BLOCK 1024 ! 169: -#define BUSY 1 ! 170: -#define NULL 0 ! 171: -#define testbusy(p) ((INT)(p)&BUSY) ! 172: -#define setbusy(p) (union store *)((INT)(p)|BUSY) ! 173: -#define clearbusy(p) (union store *)((INT)(p)&~BUSY) ! 174: - ! 175: -union store { ! 176: - union store *ptr; ! 177: - ALIGN dummy[NALIGN]; ! 178: - int calloc; /*calloc clears an array of integers*/ ! 179: -}; ! 180: - ! 181: -static union store alloca; /* initial arena */ ! 182: -static union store *allocb = &alloca; /*arena base*/ ! 183: -static union store *allocp = &alloca; /*search ptr*/ ! 184: -static union store *alloct = &alloca; /*arena top; for speedier ialloc*/ ! 185: -static union store allocx, allocy; /*for benefit of realloc*/ ! 186: -extern char *sbrk(); ! 187: - ! 188: -/* a cache list of frequently-used sizes is maintained. From each ! 189: - * cache entry hangs a chain of available blocks (marked busy ! 190: - * to keep out of the first fit search) ! 191: -*/ ! 192: -#define CACHEMAX 100 /* largest block to be cached (in words) */ ! 193: -#ifndef pdp11 ! 194: -#define CACHESIZ 13 /* number of entries (prime) */ ! 195: -#else ! 196: -#define CACHESIZ 0 ! 197: -#endif ! 198: -static struct cache { ! 199: - int size; ! 200: - union store *chain; ! 201: -} cache[CACHESIZ]; ! 202: - ! 203: -char * ! 204: -malloc(nbytes) ! 205: -unsigned nbytes; ! 206: -{ ! 207: - register union store *p, *q; ! 208: - register nw; ! 209: - register temp; ! 210: - register struct cache *cp; ! 211: - ! 212: - ASSERT(allock(allocp)&1); ! 213: - nw = (nbytes+WORD+WORD-1)/WORD; ! 214: - if(CACHESIZ && nw<CACHEMAX && nw>2) { /* see note + below */ ! 215: - cp = cache + nw%CACHESIZ; ! 216: - p = cp->chain; ! 217: - if(p && nw==cp->size) { ! 218: - cp->chain = p[1].ptr; ! 219: - ASSERT(testbusy(p->ptr)); ! 220: - ASSERT(clearbusy(p->ptr)-p==nw); ! 221: - return (char*)(p+1); ! 222: - } ! 223: - } ! 224: - ASSERT(allock(allocp)&3); ! 225: - for(; ; ) { /* done at most twice */ ! 226: - p = allocp; ! 227: - if(alloca.ptr!=0) /*C can't initialize union*/ ! 228: - for(temp=0; ; ) { ! 229: - if(!testbusy(p->ptr)) { ! 230: - while(!testbusy((q=p->ptr)->ptr)) { ! 231: - ASSERT(q>p); ! 232: - p->ptr = q->ptr; ! 233: - } ! 234: - allocp = p; ! 235: - if(q>=p+nw && p+nw>=p) /*room; no wrap*/ ! 236: - goto found; ! 237: - } ! 238: - q = p; ! 239: - p = clearbusy(p->ptr); ! 240: - if(p <= q) { ! 241: - ASSERT(p==allocb); ! 242: - if(++temp>1) ! 243: - break; ! 244: - } ! 245: - } ! 246: - temp = nw; ! 247: - p = (union store *)sbrk(0); ! 248: - q = allocp->ptr; ! 249: - if(!testbusy(q) && q+1 == p) ! 250: - temp -= p - allocp; ! 251: - temp = ((temp+BLOCK/WORD)/(BLOCK/WORD))*(BLOCK/WORD); ! 252: - if(p+temp <= p) ! 253: - return(NULL); ! 254: - for( ; ; ) { ! 255: - register s; ! 256: - q = (union store *)sbrk(temp*WORD); ! 257: - if((INT)q != -1) ! 258: - break; ! 259: - for(cp=cache; cp<cache+CACHESIZ; cp++) { ! 260: - for(p=cp->chain; p; p=p[1].ptr) { ! 261: - ASSERT(testbusy(p->ptr)); ! 262: - p->ptr = clearbusy(p->ptr); ! 263: - ASSERT(p->ptr-p==cp->size); ! 264: - } ! 265: - cp->chain = 0; ! 266: - } ! 267: - s = (temp-nw)/2; ! 268: - if(s <= 0) ! 269: - return(NULL); ! 270: - temp -= s; ! 271: - } ! 272: - ialloc((char *)q, (unsigned)temp*WORD); ! 273: - } ! 274: -found: ! 275: - q = p + nw; ! 276: - if(p->ptr > q) { ! 277: - allocx = *q; ! 278: - q->ptr = p->ptr; ! 279: - } ! 280: - p->ptr = setbusy(q); ! 281: - ASSERT(allock(allocp)&7); ! 282: - return((char *)(p+1)); ! 283: -} ! 284: -/* + note CACHESIZ is tested for conditional compilation; nw>2 assumes there's ! 285: - * no point in caching smaller sizes (they are rarely used and always ! 286: - * can be allocated) and protects against the old storage compaction trick: ! 287: - * free(p); free(dummy);dummy=malloc(1);realloc(p) ! 288: - * (otherwise free(dummy) would destroy allocy, which pertains to p) ! 289: -*/ ! 290: - ! 291: -/* freeing strategy tuned for LIFO allocation ! 292: -*/ ! 293: -free(ap) ! 294: -char *ap; ! 295: -{ ! 296: - register union store *p = (union store *)ap, *q; ! 297: - register nw; ! 298: - register struct cache *cp; ! 299: - ! 300: - --p; ! 301: - ASSERT(allock(p)); ! 302: - ASSERT(testbusy(p->ptr)); ! 303: - nw = clearbusy(p->ptr) - p; ! 304: - ASSERT(nw>0); ! 305: - if(CACHESIZ && nw<CACHEMAX && nw>2) { ! 306: - cp = cache + nw%CACHESIZ; ! 307: - if(nw != cp->size) { ! 308: - q = cp->chain; ! 309: - if(q) { ! 310: - ASSERT(testbusy(q->ptr)); ! 311: - q->ptr = clearbusy(q->ptr); ! 312: - ASSERT(q->ptr-q==cp->size); ! 313: - cp->chain = q[1].ptr; ! 314: - } ! 315: - if(!q) ! 316: - cp->size = nw; ! 317: - else ! 318: - goto nocache; ! 319: - } ! 320: - allocy = p[1]; ! 321: - p[1].ptr = cp->chain; ! 322: - cp->chain = p; ! 323: - ASSERT(allock(allocp)&017); ! 324: - return; ! 325: - } ! 326: -nocache: ! 327: - allocp = p; ! 328: - p->ptr = clearbusy(p->ptr); ! 329: - ASSERT(allock(allocp)&037); ! 330: - ASSERT(p->ptr<=alloct); ! 331: -} ! 332: - ! 333: -/* ialloc(q, nbytes) inserts a block that did not come ! 334: - * from malloc into the arena ! 335: - * ! 336: - * q points to new block ! 337: - * r points to last of new block ! 338: - * p points to last cell of arena before new block ! 339: - * s points to first cell of arena after new block ! 340: -*/ ! 341: -ialloc(qq, nbytes) ! 342: -char *qq; ! 343: -unsigned nbytes; ! 344: -{ ! 345: - register union store *p, *q, *s; ! 346: - union store *r; ! 347: - ! 348: - q = (union store *)qq; ! 349: - r = q + (nbytes/WORD) - 1; ! 350: - q->ptr = r; ! 351: - if(alloca.ptr==0) /*C can't initialize union*/ ! 352: - alloca.ptr = &alloca; ! 353: - if(q > alloct) { ! 354: - p = alloct; ! 355: - alloct = r; ! 356: - } else ! 357: - allocp = p = allocb; ! 358: - for( ; ; p=s) { ! 359: - s = clearbusy(p->ptr); ! 360: - if(s==allocb) ! 361: - break; ! 362: - ASSERT(s>p); ! 363: - if(s>r) { ! 364: - if(p<q) ! 365: - break; ! 366: - else ! 367: - ASSERT(p>r); ! 368: - } ! 369: - } ! 370: - p->ptr = q==p+1? q: setbusy(q); ! 371: - r->ptr = s==r+1? s: setbusy(s); ! 372: - if(allocb > q) ! 373: - allocp = allocb = q; ! 374: -} ! 375: - ! 376: -/* realloc(p, nbytes) reallocates a block obtained from malloc() ! 377: - * and freed since last call of malloc() ! 378: - * to have new size nbytes, and old content ! 379: - * returns new location, or 0 on failure ! 380: -*/ ! 381: - ! 382: -char * ! 383: -realloc(pp, nbytes) ! 384: -char *pp; ! 385: -unsigned nbytes; ! 386: -{ ! 387: - register union store *q; ! 388: - register union store *p = (union store *)pp; ! 389: - register union store *s, *t; ! 390: - register unsigned nw; ! 391: - struct cache *cp; ! 392: - unsigned onw; ! 393: - ! 394: - q = p-1; ! 395: - ASSERT(allock(q)); ! 396: - if(testbusy(q->ptr)) { ! 397: - allocp = q; ! 398: - q->ptr = clearbusy(q->ptr); ! 399: - if(CACHESIZ) { ! 400: - nw = q->ptr - q; ! 401: - cp = cache + nw%CACHESIZ; ! 402: - if(cp->chain==q) { ! 403: - ASSERT(cp->size==nw); ! 404: - cp->chain = p->ptr; /*p->ptr==q[1].ptr*/ ! 405: - *p = allocy; ! 406: - } else ! 407: - ASSERT(notonchain(q,cp->chain)); ! 408: - } ! 409: - } ! 410: - onw = q->ptr - p; ! 411: - q = (union store *)malloc(nbytes); ! 412: - if(q==NULL || q==p) ! 413: - return((char *)q); ! 414: - ASSERT(q<p||q>p[-1].ptr); ! 415: - s = p; ! 416: - t = q; ! 417: - nw = (nbytes+WORD-1)/WORD; ! 418: - if(nw<onw) ! 419: - onw = nw; ! 420: - while(onw--!=0) ! 421: - *t++ = *s++; ! 422: - ASSERT(clearbusy(q[-1].ptr)-q==nw); ! 423: - if(q<p && q+nw>=p) ! 424: - q[q+nw-p] = allocx; ! 425: - ASSERT(allock(q-1)); ! 426: - return((char *)q); ! 427: -} ! 428: - ! 429: -#ifdef debug ! 430: - ! 431: -notonchain(p,q) ! 432: -union store *p, *q; ! 433: -{ ! 434: - for(;q; q=clearbusy(q->ptr)) ! 435: - if(q==p) ! 436: - return 0; ! 437: - return 1; ! 438: -} ! 439: - ! 440: -allock(q) ! 441: -union store *q; ! 442: -{ ! 443: -#ifdef longdebug ! 444: - register union store *p, *r; ! 445: - int x; ! 446: - for(x=0; x<CACHESIZ; x++) { ! 447: - p = cache[x].chain; ! 448: - if(p==0) ! 449: - continue; ! 450: - for( ; p; p=p[1].ptr) { ! 451: - ASSERT(testbusy(p->ptr)); ! 452: - ASSERT(clearbusy(p->ptr)-p==cache[x].size); ! 453: - } ! 454: - } ! 455: - x = 0; ! 456: - p = allocb; ! 457: - if(alloca.ptr==0) ! 458: - return(1); ! 459: - for( ; (r=clearbusy(p->ptr)) > p; p=r) { ! 460: - if(p==q) ! 461: - x++; ! 462: - } ! 463: - return(r==allocb&(x==1|p==q)); ! 464: -#else ! 465: - return(q>=allocb); ! 466: -#endif ! 467: -} ! 468: -#endif ! 469: //GO.SYSIN DD cmalloc.c ! 470: echo makefile 1>&2 ! 471: sed 's/.//' >makefile <<'//GO.SYSIN DD makefile' ! 472: -CFLAGS = -g ! 473: -OBJS = malloc_t.o cmalloc.o trace.expr.o trace1.o trace2.o trace3.o trace4.o trace5.o trace6.o trace7.o trace8.o trace9.o assert.o ! 474: - ! 475: -# FILES: ! 476: -# trace.h constants and macro definitions ! 477: -# trace.d data structures ! 478: -# trace1.c reads in the tables, sets up data structures ! 479: -# trace2.c memory allocation ! 480: -# trace3.c the symbolic execution procedures ! 481: -# trace4.c state space handler ! 482: -# trace5.c lookup table for system states ! 483: -# trace6.c lookup table for queue states ! 484: -# trace7.c lookup table for leaf-states ! 485: -# trace8.c lookup table for variable & parameter states ! 486: -# trace9.c lookup table for process states ! 487: -# trace.expr.c evaluation of expressions ! 488: -# malloc_t.c memory allocation interface to cmalloc.c ! 489: -# assert.c assertion primitives ! 490: - ! 491: -trace: $(OBJS) ! 492: - cc $(CFLAGS) $(OBJS) -o trace ! 493: - ! 494: -%.o: %.c trace.d trace.h ! 495: - cc $(CFLAGS) -c $%.c ! 496: - ! 497: -clean: ! 498: - rm -f *.o pret.* mon.out core a.out ! 499: - ! 500: -install: ! 501: - cp trace /usr/bin ! 502: - ! 503: //GO.SYSIN DD makefile ! 504: echo malloc_t.c 1>&2 ! 505: sed 's/.//' >malloc_t.c <<'//GO.SYSIN DD malloc_t.c' ! 506: -#include <stdio.h> ! 507: -#include "trace.h" ! 508: - ! 509: -#define DEBUG 0 ! 510: - ! 511: -#if DEBUG ! 512: -#define log(e, u, d) event[e][u] += (long) d; ! 513: -#else ! 514: -#define log(e, u, d) ! 515: -#endif ! 516: - ! 517: -#define A_LARGE 64 ! 518: -#define A_USER 0x55000000 ! 519: - ! 520: -#define POOL 0 ! 521: -#define ALLOC 1 ! 522: -#define FREE 2 ! 523: -#define NREVENT 3 ! 524: - ! 525: - union M { ! 526: - long size; ! 527: - union M *link; ! 528: - }; ! 529: - ! 530: - union M *freelist[A_LARGE]; ! 531: - long req[A_LARGE]; ! 532: - long event[NREVENT][A_LARGE]; ! 533: - ! 534: -char * ! 535: -talloc(u) ! 536: - long u; ! 537: -{ union M *m; ! 538: - register r; ! 539: - char *Smalloc(); ! 540: - ! 541: - u = ((u-1)/sizeof(union M) + 2); ! 542: - ! 543: - if( u >= A_LARGE ) ! 544: - { log(ALLOC, 0, (long) 1); ! 545: - m = (union M *) malloc( u * sizeof(union M) ); ! 546: - if (m == NULL) ! 547: - whoops("malloc fault"); ! 548: - } else ! 549: - { if( freelist[u] == NULL ) ! 550: - { r = req[u] += req[u] ? req[u] : 1; ! 551: - if (r > NOTOOBIG) ! 552: - r = req[u] = NOTOOBIG+1; ! 553: - log(POOL, (int) u, (long) r); ! 554: - freelist[u] = (union M *) Smalloc( r*u*sizeof(union M) ); ! 555: - if (freelist[u] == NULL) ! 556: - whoops("malloc fault"); ! 557: - ! 558: - (freelist[u] + u*(r-1))->link = 0; ! 559: - for (m = freelist[u] + u*(r-2); m >= freelist[u]; m -= u) ! 560: - m->link = m+u; ! 561: - } ! 562: - log(ALLOC, (int) u, (long) 1); ! 563: - ! 564: - m = freelist[u]; ! 565: - freelist[u] = m->link; ! 566: - } ! 567: - m->size = u | A_USER; ! 568: -/* ! 569: - for (r = 1; r < u; ) ! 570: - (&m->size)[r++] = 0; ! 571: -*/ ! 572: - return (char *) (m+1); ! 573: -} ! 574: - ! 575: -tfree(v) ! 576: - char *v; ! 577: -{ register union M *m = (union M *) v; ! 578: - register long u; ! 579: - ! 580: - --m; ! 581: - if ( (m->size&0xFF000000) != A_USER) ! 582: - { fprintf(stderr, "panic: releasing a free block\n"); ! 583: - kill(getpid(), 3); ! 584: - } ! 585: - ! 586: - u = (m->size &= 0xFFFFFF); ! 587: - if ( u >= A_LARGE ) ! 588: - { log(FREE, (int) 0, (long) 1); ! 589: - free(m); ! 590: - } ! 591: - else ! 592: - { log(FREE, (int) u, (long) 1); ! 593: - m->link = freelist[u]; ! 594: - freelist[u] = m; ! 595: - } ! 596: -} ! 597: - ! 598: -#if DEBUG ! 599: -double ! 600: -a_stats() ! 601: -{ register int i; ! 602: - long p, a, f, j; ! 603: - long sum = 0; ! 604: - ! 605: - fprintf(stderr, "chunk\t pool\tallocs\t frees\t spill\n"); ! 606: - for (i = 0; i < A_LARGE; i++) ! 607: - { ! 608: - p = event[POOL][i]; ! 609: - a = event[ALLOC][i]; ! 610: - f = event[FREE][i]; ! 611: - ! 612: - if( !(p|a|f) ) ! 613: - continue; ! 614: - ! 615: - j = (long) (i * sizeof(union M)); ! 616: - fprintf(stderr, "%5d\t%6ld\t%6ld\t%6ld\t%6ld\n", j, p, a, f, a-f); ! 617: - ! 618: - sum += p*j; ! 619: - } ! 620: - fprintf(stderr, "total pools %7u\n", sum); ! 621: - ! 622: - return (double) sum; ! 623: -} ! 624: -#endif ! 625: //GO.SYSIN DD malloc_t.c ! 626: echo trace.d 1>&2 ! 627: sed 's/.//' >trace.d <<'//GO.SYSIN DD trace.d' ! 628: - struct ELM { ! 629: - short transf; /* next state function */ ! 630: - short valtrans; /* value transferred */ ! 631: - }; ! 632: - ! 633: - struct IND { ! 634: - short nrpils; ! 635: - struct ELM *one; ! 636: - }; ! 637: - ! 638: - struct VARPARS { ! 639: - short nrms, *ms; /* message parameters */ ! 640: - short nrvs, *vs; /* pvar parameters */ ! 641: - short nrlvars, *lvarvals; /* local variables */ ! 642: - }; ! 643: - ! 644: - struct TBLPARS { ! 645: - short nrms; ! 646: - short nrvs; /* max available space for params */ ! 647: - short nrlvars; /* max available space for locvars */ ! 648: - }; ! 649: - ! 650: - struct LOCVARS { ! 651: - short nrlvars, *lvarvals; ! 652: - }; ! 653: - ! 654: - struct CPARS { ! 655: - short callwhat; ! 656: - short nrms, *ms; /* message parameters */ ! 657: - short nrvs, *vs; /* pvar parameters */ ! 658: - }; ! 659: - ! 660: - struct LBT { ! 661: - int *mapcol, *orgcol; /* mapped versions of colmap and colorg */ ! 662: - }; ! 663: - ! 664: -/* ! 665: - * endrow: proper endstates of the process table ! 666: - * deadrow: set if deadend (eg return state) ! 667: - * badrow: row with at least one output option ! 668: - * labrow: labeled row (potential start of a loop) ! 669: - */ ! 670: - ! 671: - struct TBL { ! 672: - int nrrows, nrcols; ! 673: - int *endrow, *deadrow, *badrow, *labrow; ! 674: - int *colmap, *colorg, *coltyp; ! 675: - char **rowname; ! 676: - ! 677: - struct IND **ptr; ! 678: - struct CPARS *calls; ! 679: - }; ! 680: - ! 681: - struct MBOX { ! 682: - char limit; /* length of queue */ ! 683: - char owner; /* the process reading from this queue */ ! 684: - char qname[PLENTY]; /* user-level name for the queue */ ! 685: - }; ! 686: - ! 687: - struct MNAME { ! 688: - char mname[PLENTY]; ! 689: - }; ! 690: - ! 691: - struct BLTIN { ! 692: - short target; ! 693: - short type; ! 694: - short value; ! 695: - }; ! 696: - ! 697: - struct REVPOL { ! 698: - char toktyp; ! 699: - short tokval; ! 700: - }; ! 701: - ! 702: - struct PROCSTACK { ! 703: - short uptable; /* table where we come from */ ! 704: - short uptransf; /* pending transition in that table */ ! 705: - ! 706: - struct VARPARS *varparsaved; /* saves parameters and locals */ ! 707: - struct PROCSTACK *follow; /* next stackframe */ ! 708: - }; ! 709: - ! 710: -#define USED 32768 ! 711: -#define PASSED 16384 ! 712: -#define TRAIL 1 ! 713: - ! 714: - struct QUEUE { ! 715: - short mesg; /* on rcv PASSED is OR'ed in */ ! 716: - unsigned short cargo; /* when set USED is OR'ed in */ ! 717: -#if TRAIL ! 718: - short tstate[2]; /* linecode reference */ ! 719: -#endif TRAIL ! 720: - struct QUEUE *next; ! 721: - struct QUEUE *last; ! 722: - struct QUEUE *s_forw; ! 723: - struct QUEUE *s_back; ! 724: - }; ! 725: - ! 726: - struct CONTS { ! 727: - short mesg; ! 728: - unsigned short cargo; ! 729: - }; ! 730: - ! 731: - struct TEMPLATE { ! 732: - short *g_vars; /* current globals */ ! 733: - struct LOCVARS **l_vars; /* current local vars */ ! 734: - struct PROCSTACK **traceback; /* traceback of complete stack */ ! 735: - }; ! 736: - ! 737: - struct STATE { ! 738: - unsigned short *pstate; /* old states & maps */ ! 739: - struct TEMPLATE *pcon; /* variables and stacks */ ! 740: - struct VISIT *next; ! 741: - }; ! 742: - ! 743: -#define ANALYZED 16384 ! 744: - ! 745: - struct VISIT { ! 746: - unsigned int howmany; /* which queues are nonempty */ ! 747: - struct CONTS **c; /* queue contents */ ! 748: - union { ! 749: - struct QUEUE *s; /* when searching, last message sent */ ! 750: - short countme; /* when analyzed, counts nr of returns */ ! 751: - } prop; ! 752: - unsigned short depth; /* level of first visit, ANALYZED is OR'ed in */ ! 753: - struct VISIT *next; ! 754: - }; ! 755: - ! 756: -#define ISANA(x) (x->depth & ANALYZED) ! 757: -#define DEPTH(x) (x->depth & ~ANALYZED) ! 758: - ! 759: -/* ! 760: - * normal ppushes (via forward()) save the parameters in the procstack ! 761: - * so that the corresponding ppop (via backup()) can reset them properly ! 762: - * ! 763: - * series of ppushes and ppops, performed in a single freeze() call ! 764: - * (via the retable() and dotable() subroutines) are different: ! 765: - * ! 766: - * additional ppushes are no problem, since they save the ! 767: - * proper state information via the normal route ! 768: - * ! 769: - * additional ppops however would lose the procstacked info ! 770: - * that info is stored in the CUBE structure so that when ! 771: - * a ppop from freeze() is undone in unfreeze() ! 772: - * the proper state information can be restored onto the procstack ! 773: - */ ! 774: - ! 775: - struct CUBE { ! 776: - short poporpush; ! 777: - short which; ! 778: - short procsaved; ! 779: - short transfsaved; ! 780: - ! 781: - struct VARPARS *varparsaved; /* parameter map and local var map */ ! 782: - ! 783: - struct CUBE *pntr; ! 784: - struct CUBE *rtnp; ! 785: - }; ! 786: - ! 787: - struct FREEZE { ! 788: - short lastsav; ! 789: - short *statsaved; /* save states of tables */ ! 790: - short *varsaved; /* save global variables */ ! 791: - short whichvar; /* set if a var changed */ ! 792: - short oldvalue; /* of that loc var */ ! 793: - ! 794: - struct CUBE *cube; /* place to save stackframe */ ! 795: - }; ! 796: - ! 797: - struct Swiffle { ! 798: - struct STATE *st; ! 799: - struct VISIT *vi; ! 800: - struct Swiffle *next; ! 801: - struct Swiffle *last; ! 802: - }; ! 803: //GO.SYSIN DD trace.d ! 804: echo trace.expr.c 1>&2 ! 805: sed 's/.//' >trace.expr.c <<'//GO.SYSIN DD trace.expr.c' ! 806: -#include <stdio.h> ! 807: -#include <math.h> ! 808: -#include "trace.h" ! 809: -#include "trace.d" ! 810: - ! 811: -#define DEBUG 0 ! 812: - ! 813: -#define setv 1 ! 814: -#define addeq 2 ! 815: -#define subeq 3 ! 816: -#define muleq 4 ! 817: -#define diveq 5 ! 818: -#define modeq 6 ! 819: -#define plus 7 ! 820: -#define minus 8 ! 821: -#define times 9 ! 822: -#define div 10 ! 823: -#define mod 11 ! 824: -#define power 12 ! 825: -#define uminus 13 ! 826: -#define gt 14 ! 827: -#define lt 15 ! 828: -#define ge 16 ! 829: -#define le 17 ! 830: -#define eq 18 ! 831: -#define ne 19 ! 832: -#define land 20 ! 833: -#define lor 21 ! 834: -#define lnot 22 ! 835: -#define princ 23 ! 836: -#define prdec 24 ! 837: -#define poinc 25 ! 838: -#define podec 26 ! 839: - ! 840: -#define OP 0 ! 841: -#define NM 1 ! 842: - ! 843: -#define unary(c) (c == uminus || c == lnot || c >= princ) ! 844: -#define binary(c) !unary(c) ! 845: - ! 846: - extern struct REVPOL **expr; ! 847: - extern int nexpr, nrvars, *globvars; ! 848: - extern struct VARPARS *procpars; ! 849: - ! 850: - struct REVPOL *rev; ! 851: - int curproc, revp; ! 852: - ! 853: - struct { ! 854: - char how; ! 855: - short whichvar; ! 856: - short oldvalue; ! 857: - } storewhere; ! 858: - ! 859: -evalexpr(n, pr, b) ! 860: - struct FREEZE *b; ! 861: -{ int i; ! 862: - if (n == NONE) ! 863: - return 0; ! 864: - if (n < 0 || n >= nexpr) ! 865: - whoops("unknown expression"); ! 866: - ! 867: - rev = expr[n]; ! 868: - revp = 0; ! 869: - curproc = pr; ! 870: - storewhere.how = 0; ! 871: - ! 872: - if ((i = getval()) < 0) ! 873: - i += 3*MANY; ! 874: - else ! 875: - i -= 3*MANY; /* should return stripped constant */ ! 876: -#if DEBUG ! 877: - fprintf(stderr, "evaluated expr %d, process %d, result %d\n", n, pr, i); ! 878: -#endif ! 879: - ! 880: - b->whichvar = storewhere.whichvar; ! 881: - b->oldvalue = storewhere.oldvalue; ! 882: - ! 883: - return storewhere.how; ! 884: -} ! 885: - ! 886: -evalcond(n, pr) ! 887: -{ int i; ! 888: - if (n < 0 || n >= nexpr) ! 889: - { fprintf(stderr, "%d\n", n); ! 890: - whoops("unknown expression - evalcond"); ! 891: - } ! 892: - ! 893: - rev = expr[n]; ! 894: - revp = 0; ! 895: - curproc = pr; ! 896: - storewhere.how = 0; ! 897: - ! 898: - if ((i = getval()) < 0) ! 899: - i += 3*MANY; ! 900: - else ! 901: - i -= 3*MANY; /* should return stripped constant */ ! 902: -#if DEBUG ! 903: - fprintf(stderr, "evaluated cond %d, process %d, result %d\n", n, pr, i); ! 904: -#endif ! 905: - if (storewhere.how != 0) ! 906: - whoops("illegal assignment in expression"); ! 907: - ! 908: - return i; ! 909: -} ! 910: - ! 911: -unoper(c, n) ! 912: -{ int i = convert(n, curproc); ! 913: - switch (c) ! 914: - { case uminus: return (-i); ! 915: - case lnot : return (!i); ! 916: - case princ : remem(n); setvar(n, i+1); return i; ! 917: - case prdec : remem(n); setvar(n, i-1); return i; ! 918: - case poinc : remem(n); return setvar(n, i+1); ! 919: - case podec : remem(n); return setvar(n, i-1); ! 920: - default : whoops("unknown unary operator"); ! 921: - } ! 922: -} ! 923: - ! 924: -bioper(c, n, m) ! 925: -{ int i, j; ! 926: - double a, b; ! 927: - ! 928: - if (c != setv) ! 929: - i = convert(n, curproc); ! 930: - j = convert(m, curproc); ! 931: - switch (c) ! 932: - { case setv: remem(n); return setvar(n, j); ! 933: - case addeq: remem(n); return setvar(n, i+j); ! 934: - case subeq: remem(n); return setvar(n, i-j); ! 935: - case muleq: remem(n); return setvar(n, i*j); ! 936: - case diveq: remem(n); return setvar(n, i/j); ! 937: - case modeq: remem(n); return setvar(n, i%j); ! 938: - case plus: return (i+j); ! 939: - case minus: return (i-j); ! 940: - case times: return (i*j); ! 941: - case div: return (i/j); ! 942: - case mod: return (i%j); ! 943: - case gt : return (i>j); ! 944: - case lt : return (i<j); ! 945: - case ge : return (i>=j); ! 946: - case le : return (i<=j); ! 947: - case eq : return (i==j); ! 948: - case ne : return (i!=j); ! 949: - case land: return (i&&j); ! 950: - case lor: return (i||j); ! 951: - default: whoops("unkown binary operator"); ! 952: - } ! 953: -} ! 954: - ! 955: -getval() ! 956: -{ int tok = revp++; ! 957: - int res; ! 958: - ! 959: - if (rev[tok].toktyp == NM) ! 960: - res = rev[tok].tokval; ! 961: - else ! 962: - { if (unary(rev[tok].tokval)) ! 963: - res = unoper(rev[tok].tokval, getval()); ! 964: - else ! 965: - res = bioper(rev[tok].tokval, getval(), getval()); ! 966: - ! 967: - if (res < 0) ! 968: - res -= 3*MANY; ! 969: - else ! 970: - res += 3*MANY; ! 971: - } ! 972: - ! 973: - return res; ! 974: -} ! 975: - ! 976: -setvar(which, v) ! 977: -{ int u = wapper(which, curproc); ! 978: - int towhat = v; ! 979: - ! 980: - if (u >= 2*MANY || u < 0) ! 981: - whoops("lhs of assignment not a variable"); ! 982: - ! 983: - if (u < MANY) ! 984: - { if (u >= nrvars) ! 985: - { fprintf(stderr, "setvar %d %d %d\n", which, v, u); ! 986: - whoops("illegal assignment"); ! 987: - } ! 988: - ! 989: - globvars[u] = (short) towhat; ! 990: - } ! 991: - else ! 992: - { u -= MANY; ! 993: - if (u >= (int) procpars[curproc].nrlvars) ! 994: - whoops("unknown local variable"); ! 995: - procpars[curproc].lvarvals[u] = (short) towhat; ! 996: - } ! 997: - ! 998: - return towhat; ! 999: -} ! 1000: - ! 1001: -remem(u) ! 1002: -{ if (storewhere.how != 0) ! 1003: - whoops("multiple assignment in expression"); ! 1004: - ! 1005: - if (u < MANY) ! 1006: - { ! 1007: -#if DEBUG ! 1008: - fprintf(stderr, "setting global %d\n", u); ! 1009: -#endif ! 1010: - storewhere.whichvar = (short) u; ! 1011: - storewhere.oldvalue = globvars[u]; ! 1012: - storewhere.how = GV; ! 1013: - } ! 1014: - else ! 1015: - { storewhere.whichvar = (short) u; ! 1016: - ! 1017: - u -= MANY; ! 1018: -#if DEBUG ! 1019: - fprintf(stderr, "setting local %d\n", u); ! 1020: -#endif ! 1021: - storewhere.oldvalue = procpars[curproc].lvarvals[u]; ! 1022: - storewhere.how = LV; ! 1023: - } ! 1024: -} ! 1025: //GO.SYSIN DD trace.expr.c ! 1026: echo trace.h 1>&2 ! 1027: sed 's/.//' >trace.h <<'//GO.SYSIN DD trace.h' ! 1028: -#define NONE -1 ! 1029: -#define MAXPROC 16 ! 1030: -#define PLENTY 16 /* max namelength */ ! 1031: - ! 1032: -#define MANY 512 /* range globals: 0 - MANY */ ! 1033: - /* range locals : MANY - 2*MANY */ ! 1034: - /* range params : 2*MANY and 3*MANY */ ! 1035: - /* range constants: 3*MANY++ or 3*MANY-- */ ! 1036: - ! 1037: - /* `column types:' */ ! 1038: -#define INP 10 /* recv specific message */ ! 1039: -#define DFL 11 /* default input from q */ ! 1040: -#define TMO 12 /* transition on timeout */ ! 1041: -#define OUTP 13 /* append message to a q */ ! 1042: -#define SPN 14 /* builtin call or transit state */ ! 1043: -#define CND 15 /* conditional */ ! 1044: -#define FCT 16 /* function call */ ! 1045: - ! 1046: -#define INCR 16 /* increment a sequence number */ ! 1047: -#define DECR 17 /* decrement a sequence number */ ! 1048: -#define SUBT 18 /* subtract */ ! 1049: -#define ADDT 19 /* add */ ! 1050: -#define SETV 32 /* set seq. number to initial value */ ! 1051: -#define ISEQ 256 /* compare two variables (s.numbers) */ ! 1052: -#define NTEQ 257 /* != */ ! 1053: -#define GREQ 258 /* >= */ ! 1054: -#define SMEQ 259 /* <= */ ! 1055: -#define GRNQ 260 /* > */ ! 1056: -#define SMNQ 261 /* < */ ! 1057: - ! 1058: -#define POP 1 ! 1059: -#define PUSH -1 ! 1060: - ! 1061: -#define SO 2 /* send only */ ! 1062: -#define RO 4 /* recv only */ ! 1063: -#define SR 6 /* send & recv */ ! 1064: -#define TC 8 /* reftask call */ ! 1065: -#define TO 16 /* timeout */ ! 1066: -#define LV 32 /* local var updated */ ! 1067: -#define GV 64 /* global var updated */ ! 1068: - ! 1069: -#define FAIL -1 /* backward receive: cargo mismatch */ ! 1070: - ! 1071: -#define NOREF(i) (i < 0 || i >= MAXPROC) ! 1072: -#define NOTOOBIG 16383 /* was 32767 */ ! 1073: //GO.SYSIN DD trace.h ! 1074: echo trace1.c 1>&2 ! 1075: sed 's/.//' >trace1.c <<'//GO.SYSIN DD trace1.c' ! 1076: -#include <stdio.h> ! 1077: -#include <signal.h> ! 1078: -#include "trace.h" ! 1079: -#include "trace.d" ! 1080: - ! 1081: -#if 0 ! 1082: -#define debug(s1, s2, s3, s4, s5) printf(s1, s2, s3, s4, s5) ! 1083: -#else ! 1084: -#define debug(s1, s2, s3, s4, s5) ! 1085: -#endif ! 1086: - ! 1087: - struct TBL *tbl; ! 1088: - struct LBT *lbt; ! 1089: - struct MBOX *mbox; ! 1090: - struct MNAME *fullname; ! 1091: - ! 1092: - struct REVPOL **expr; ! 1093: - struct PROCSTACK **procstack; ! 1094: - ! 1095: - struct VARPARS *procpars; ! 1096: - struct TBLPARS *tblpars; ! 1097: - struct LOCVARS *tblvars; ! 1098: - struct TBLPARS *tablpars; ! 1099: - ! 1100: - struct QUEUE **starter, **head, **tail; ! 1101: - struct QUEUE *s_first, *s_last; ! 1102: - ! 1103: -/* ! 1104: - * reftasks : mapping of logic reftask id to table number ! 1105: - * processes: mapping of logic process id to table number ! 1106: - * basics : initial process table ! 1107: - */ ! 1108: - ! 1109: - int *state, *reftasks, *processes, *basics; ! 1110: - int *qsize, *globvars, *inits, *xob; ! 1111: - ! 1112: - /* ! 1113: - * the state-set of an assertion table is mapped ! 1114: - * onto the global variables (to simplify state checking) ! 1115: - * the first global that is an element from the state set ! 1116: - * is given by integer `abase' ! 1117: - */ ! 1118: - ! 1119: - int abase = -1; /* base of assertion table state set */ ! 1120: - int ebase = -1; /* base of error table state set */ ! 1121: - int assertbl = -1; /* table used for assertion checking */ ! 1122: - int errortbl = -1; /* table used for assertion checking */ ! 1123: - int msgbase = -1, maxlevel = -1, maxreached = -1; ! 1124: - ! 1125: - int maxcol=0, nrtbl=0, nrqs=0, nrprocs=0, nrrefs=0; ! 1126: - int nrinit=0, nrvars=0, nexpr=0, nrmesgs=0, linecode=0; ! 1127: - int QMAX=2; ! 1128: - ! 1129: - char qoverride = 0; ! 1130: - char noshortcut = 0; /* disable timeout heuristics */ ! 1131: - char prbyq = 2; /* controls output format */ ! 1132: - char blast = 0; /* blast search mode */ ! 1133: - char qandirty = 0; /* scatter search mode */ ! 1134: - char lockplus = 0; /* report both buffer locks and loops */ ! 1135: - char firstlock = 0; /* stop at first buffer lock found */ ! 1136: - char maxxed = 0; /* bound on search depth */ ! 1137: - char prefix = 0; /* print all prefixes too */ ! 1138: - char timedd = 0; /* verbose mode */ ! 1139: - char completed = 0; /* not interrupted */ ! 1140: - char muststore = 0; /* must perform loop check and store state */ ! 1141: - char sensible = 0; /* default mode: try a sensible partial search */ ! 1142: - ! 1143: - double zapper = (double) 30000; ! 1144: - double tryswiff=0, noswiff=0, cannot=0; ! 1145: - ! 1146: - long zapped = 0, locksf = 0, loopsf = 0; ! 1147: - long normf = 0, callno = 0; ! 1148: - ! 1149: - int *effnrstates; /* effective nr of table states per process */ ! 1150: - int aperiod = 120; ! 1151: - ! 1152: - char *topofmem, *sbrk(), *Smalloc(); ! 1153: - char fname[64]; ! 1154: - ! 1155: - FILE *mb; ! 1156: - ! 1157: - extern double iseen, ireseen, painful, kurshan; ! 1158: - ! 1159: -onalarm() ! 1160: -{ float t; ! 1161: - struct { long u, p, cu, cp; } tim; ! 1162: - ! 1163: - times(&tim); ! 1164: - t = (float) (tim.u + tim.p)/ (float) 60.0; ! 1165: - ! 1166: - if (++callno%10 == 1) ! 1167: - { fprintf(stderr, " seconds depth states zapped"); ! 1168: - fprintf(stderr, " prefix terms loops locks memory\n"); ! 1169: - } ! 1170: - fprintf(stderr, "%8.2f %6d ", t, maxreached); ! 1171: - fprintf(stderr, "%6g %8ld %7g ", iseen+ireseen, zapped, kurshan); ! 1172: - fprintf(stderr, "%5ld %5ld ", normf, loopsf); ! 1173: - fprintf(stderr, "%5ld %8u\n", locksf, sbrk(0) - topofmem); ! 1174: - signal(SIGALRM, onalarm); ! 1175: - alarm(aperiod); ! 1176: -} ! 1177: - ! 1178: -postlude() ! 1179: -{ struct { long u, p, cu, cp; } tim; ! 1180: - extern double COUNT; ! 1181: - float u, s; ! 1182: - ! 1183: - fflush(stdout); ! 1184: - if (!completed) ! 1185: - fprintf(stderr, "trace: interrupted\n"); ! 1186: - ! 1187: - if (timedd) ! 1188: - { times(&tim); ! 1189: - u = (float) tim.u / (float) 60.0; ! 1190: - s = (float) tim.p / (float) 60.0; ! 1191: - ! 1192: - fprintf(stderr, "\ttime: %.2fs u + ", u); ! 1193: - fprintf(stderr, "%.2fs sys = %.2fs\n\n", s, u+s); ! 1194: - fprintf(stderr, "\t%g states cached, ", iseen+ireseen); ! 1195: - fprintf(stderr, "%ld states zapped\n", zapped); ! 1196: - fprintf(stderr, "\tsearch depth reached: %d; ", maxreached); ! 1197: - fprintf(stderr, "memory used: %u\n\t", sbrk(0) - topofmem ); ! 1198: - fprintf(stderr, "%ld deadlocks, ", locksf); ! 1199: - fprintf(stderr, "%ld loops, ", loopsf); ! 1200: - fprintf(stderr, "%ld terminating executions, and ", normf); ! 1201: - fprintf(stderr, "%g prefixes\n", kurshan); ! 1202: - fprintf(stderr, "\t%g edges traversed", COUNT); ! 1203: - fprintf(stderr, ", %g states analyzed twice\n", painful); ! 1204: - if (cannot > 0) ! 1205: - fprintf(stderr, "\t%g cache replacements failed\n", cannot); ! 1206: - if (tryswiff > 0) ! 1207: - fprintf(stderr, "\ttryswiff %5g noswiff %g\n",tryswiff,noswiff); ! 1208: - } ! 1209: - exit(completed == 0); ! 1210: -} ! 1211: - ! 1212: -wisdom() ! 1213: -{ ! 1214: - if (sensible) ! 1215: - { timedd = firstlock = qandirty = 1; ! 1216: - fprintf(stderr, "default search: "); ! 1217: - fprintf(stderr, "-vxjqm %d %d\n", QMAX, maxlevel); ! 1218: - } else ! 1219: - { fprintf(stderr, "%s search, ", (blast) ? "blast" : ! 1220: - (qandirty) ? "scatter" : "exhaustive"); ! 1221: - fprintf(stderr, "depth bound %d\n", maxlevel); ! 1222: - } ! 1223: -} ! 1224: - ! 1225: -main(argc, argv) ! 1226: - char **argv; ! 1227: -{ ! 1228: - char c; ! 1229: - int i=1, j, base=2; ! 1230: - ! 1231: - strcpy(fname, "pret.out"); ! 1232: - if (argc > 1 && argv[1][0] == '-') ! 1233: - { base++; ! 1234: - while ((c = argv[1][i++]) != '\0') ! 1235: - switch (c) { ! 1236: - case 'a': prefix = 1; break; ! 1237: - case 'b': blast = qandirty = 1; break; ! 1238: - case 'c': if (argc >= base) ! 1239: - { sscanf(argv[base-1], "%d", &j); ! 1240: - base++; ! 1241: - } else ! 1242: - usage("missing argument for `c' flag"); ! 1243: - firstlock = lockplus = timedd = 1; ! 1244: - switch (j) { ! 1245: - case 0: blast = qandirty = 1; break; ! 1246: - case 1: maxxed = 3; /* fall through */ ! 1247: - case 2: qandirty = 1; break; ! 1248: - case 3: maxxed = 2; break; /* 1{ x effnr */ ! 1249: - case 4: maxxed = 3; /* 2 x effnr */ ! 1250: - case 5: break; /* 8 x effnr */ ! 1251: - default: usage("unknown validation class"); ! 1252: - } ! 1253: - break; ! 1254: - case 'f': prbyq = 1; break; ! 1255: - case 'F': prbyq = 0; break; ! 1256: - case 'j': firstlock = 1; break; ! 1257: - case 'k': if (argc >= base) ! 1258: - { sscanf(argv[base-1], "%d", &j); ! 1259: - zapper = (double) (j * 1000); ! 1260: - base++; ! 1261: - } else ! 1262: - usage("missing argument for `k' flag"); ! 1263: - break; ! 1264: - case 'l': lockplus = 1; break; ! 1265: - case 'm': maxxed = 1; ! 1266: - if (argc >= base) ! 1267: - { sscanf(argv[base-1], "%d", &maxlevel); ! 1268: - base++; ! 1269: - } else ! 1270: - usage("missing argument for `m' flag"); ! 1271: - break; ! 1272: - case 'n': noshortcut = 1; break; ! 1273: - case 'q': qoverride = 1; ! 1274: - if (argc >= base) ! 1275: - { sscanf(argv[base-1], "%d", &QMAX); ! 1276: - base++; ! 1277: - } else ! 1278: - usage("missing argument for `q' flag"); ! 1279: - break; ! 1280: - case 'r': if (argc >= base) ! 1281: - { sscanf(argv[base-1], "%d", &j); ! 1282: - base++; ! 1283: - } else ! 1284: - usage("missing argument for `r' flag"); ! 1285: - signal(SIGALRM, postlude); ! 1286: - aperiod = 0; ! 1287: - alarm(j*60); ! 1288: - break; ! 1289: - case 'R': if (argc >= base) ! 1290: - { sscanf(argv[base-1], "%d", &j); ! 1291: - base++; ! 1292: - } else ! 1293: - usage("missing argument for `R' flag"); ! 1294: - aperiod = j*60; ! 1295: - break; ! 1296: - case 's': setup(); showtables(timedd); exit(0); ! 1297: - break; ! 1298: - case 'v': timedd = 1; break; ! 1299: - case 'x': qandirty = 1; break; ! 1300: - default : usage("unknown option"); ! 1301: - } ! 1302: - } else ! 1303: - { sensible = qoverride = 1; ! 1304: - } ! 1305: - ! 1306: - if (argc >= base-1) ! 1307: - sscanf(argv[base-1], "%s", fname); ! 1308: - else ! 1309: - strcpy(fname, "pret.out"); ! 1310: - ! 1311: - setup(); ! 1312: - init(); ! 1313: - topofmem = sbrk(0); ! 1314: - ! 1315: - if (maxxed != 1) ! 1316: - { ! 1317: - for (j = maxlevel = 0; j < nrprocs; j++) ! 1318: - maxlevel += effnrstates[processes[j]]; ! 1319: - ! 1320: - switch (maxxed) { ! 1321: - case 3: maxlevel *= 2; break; ! 1322: - case 2: maxlevel = (3*maxlevel)/2; break; ! 1323: - case 0: if (sensible) ! 1324: - maxlevel *= 2; ! 1325: - else ! 1326: - maxlevel *= 8; /* avoid pathetic cases */ ! 1327: - break; ! 1328: - default: whoops("cannot happen - main"); ! 1329: - } ! 1330: - maxxed = 1; ! 1331: - } ! 1332: - if (aperiod > 0) ! 1333: - { signal(SIGALRM, onalarm); ! 1334: - alarm(aperiod); ! 1335: - } signal(SIGINT, postlude); ! 1336: - ! 1337: - wisdom(); ! 1338: - muststore = 1; /* must always store initial state */ ! 1339: - FSE(0); ! 1340: - completed = 1; ! 1341: - postlude(); ! 1342: -} ! 1343: - ! 1344: -setup() ! 1345: -{ ! 1346: - if ((mb = fopen(fname, "r")) == NULL) ! 1347: - { fprintf(stderr, "cannot find `%s'\n", fname); ! 1348: - exit(1); ! 1349: - } ! 1350: - ! 1351: - getglobals(); ! 1352: - gettables(); ! 1353: - getexprs(); ! 1354: - ! 1355: - fclose(mb); ! 1356: -} ! 1357: - ! 1358: -getglobals() ! 1359: -{ register int i, j; ! 1360: - int a, b, c, x, y, z; ! 1361: - ! 1362: - if (fscanf(mb, "%d linecode\n", &linecode) != 1) ! 1363: - badinput("linecode"); ! 1364: - a = fscanf(mb, "%d procedures (assert %d/%d)\n", &x, &assertbl, &errortbl); ! 1365: - if (a != 3) ! 1366: - badinput("procedures"); ! 1367: - if (fscanf(mb, "%d processes\n", &y) != 1) ! 1368: - badinput("processes"); ! 1369: - if (fscanf(mb, "%d queues:\n", &z) != 1) ! 1370: - badinput("queues"); ! 1371: - ! 1372: - debug("%d procs, %d functions, %d queues, assert %d\n", y, x, z, assertbl); ! 1373: - ! 1374: - nrtbl = x + y; ! 1375: - nrqs = z; ! 1376: - alloc1(x, y, z); ! 1377: - ! 1378: - getmesnames(); ! 1379: - ! 1380: - for (i = 0; i < z; i++) ! 1381: - { if (fscanf(mb, "%s\t%d/%d/%d: ", mbox[i].qname, &b, &a, &c) != 4) ! 1382: - badinput("queue sorts"); ! 1383: - alloc2(i, a, b); ! 1384: - for (j = 0; j < c; j++) ! 1385: - { fscanf(mb, "%d,", &b); ! 1386: - xob[b] = i; ! 1387: - } ! 1388: - } ! 1389: - ! 1390: - if (fscanf(mb, "%d inits:\n", &nrinit) != 1) ! 1391: - badinput("queue inits"); ! 1392: - ! 1393: - alloc3(nrinit); ! 1394: - for (i = 0; i < nrinit; i++) ! 1395: - fscanf(mb, "%d,", &(inits[i])); ! 1396: - ! 1397: - if (fscanf(mb, "%d g-variables: ", &nrvars) != 1) ! 1398: - badinput("g-variables"); ! 1399: - ! 1400: - alloc4(nrvars); ! 1401: - ! 1402: - for (i = 0; i < nrvars; i++) ! 1403: - if (fscanf(mb, "%d,", &a) != 1) ! 1404: - badinput("g-var-inits"); ! 1405: - else ! 1406: - { if ((b = determine(a)) == 1 || b == 2) ! 1407: - badinput("g-var bad init"); ! 1408: - else ! 1409: - globvars[i] = (short) a; ! 1410: - } ! 1411: -} ! 1412: - ! 1413: -getmesnames() ! 1414: -{ register int i; ! 1415: - if (fscanf(mb, "%d messages, base %d:\n", &nrmesgs, &msgbase) != 2) ! 1416: - badinput("messages"); ! 1417: - ! 1418: - alloc45(nrmesgs); ! 1419: - ! 1420: - for (i = 0; i < nrmesgs; i++) ! 1421: - if (fscanf(mb, "%s ", fullname[i].mname) != 1) ! 1422: - badinput("mesg"); ! 1423: -} ! 1424: - ! 1425: -gettables() ! 1426: -{ register int i, j; ! 1427: - int a, b, c, d; ! 1428: - char name[32]; ! 1429: - ! 1430: - processes[0] = -1; ! 1431: - if (nrtbl >= 64) ! 1432: - badinput("too many process tables..."); ! 1433: - for (i = 0; i < nrtbl; i++) ! 1434: - { if ((j = fscanf(mb, "%s %d:%d/%d:", name, &a, &b, &c)) != 4) ! 1435: - { printf("matched %d: %s %d\n", j, name, a); ! 1436: - badinput("table header"); ! 1437: - } ! 1438: - ! 1439: - debug("table %d: %s (%d) ", i, name, a, 0); ! 1440: - debug("r/c: %d/%d\n", b, c, 0, 0); ! 1441: - ! 1442: - if (b >= 1024) ! 1443: - badinput("too many states"); ! 1444: - if ((tbl[i].nrrows = b) == 0) ! 1445: - badinput("empty table"); ! 1446: - tbl[i].nrcols = c; ! 1447: - ! 1448: - if (strcmp(name, "REF") == 0) ! 1449: - { reftasks[a] = i; ! 1450: - nrrefs++; ! 1451: - } else ! 1452: - { processes[a] = basics[a] = i; ! 1453: - nrprocs++; ! 1454: - effnrstates[i] = b; ! 1455: - } ! 1456: - ! 1457: - if (b > 0) ! 1458: - { alloc5(i); ! 1459: - for (j = 0; j < c; j++) ! 1460: - { if (fscanf(mb, "%d(%d),", &b, &d) != 2) ! 1461: - badinput("column header"); ! 1462: - ! 1463: - debug("%d(%d),\n", b, d, 0, 0); ! 1464: - ! 1465: - tbl[i].coltyp[j] = d; ! 1466: - tbl[i].colmap[j] = b; ! 1467: - if (d != FCT && d != SPN && d != CND) ! 1468: - tbl[i].colorg[j] = whichq(b); ! 1469: - else ! 1470: - tbl[i].colorg[j] = -1; ! 1471: - } ! 1472: - getrows(i); ! 1473: - getspecials(i); ! 1474: - getcalls(i); ! 1475: - getparams(a, i); ! 1476: - getlocvars(a, i); ! 1477: -} } } ! 1478: - ! 1479: -getrows(nn) ! 1480: -{ int a, b, c; ! 1481: - int n = nn; ! 1482: - char tmp[128]; ! 1483: - ! 1484: - for (;;) ! 1485: - { if (fscanf(mb, "%d/%d (%d) ", &a, &b, &c) != 3) ! 1486: - badinput("row"); ! 1487: - ! 1488: - if (a == 0 && b == 0 && c == 0) ! 1489: - break; ! 1490: - ! 1491: - debug("row %d, col %d, size %d:\n", a, b, c, 0); ! 1492: - ! 1493: - if (c == 0) ! 1494: - continue; ! 1495: - ! 1496: - tbl[n].deadrow[a] = 0; ! 1497: - getentries(n, a, b, c); ! 1498: - } ! 1499: - if (!linecode) return; ! 1500: - ! 1501: - if (fscanf(mb, "%s\n", tmp) != 1 || strcmp(tmp, "rownames:") != 0) ! 1502: - badinput("rownames"); ! 1503: - for (a = 0; a < tbl[n].nrrows; a++) ! 1504: - { for (b = 0; (tbl[n].rowname[a][b] = getc(mb)) != '\n'; b++) ; ! 1505: - tbl[n].rowname[a][b] = '\0'; ! 1506: - } ! 1507: -} ! 1508: - ! 1509: -getentries(nn, m, p, q) ! 1510: -{ register int i; ! 1511: - int x, y, n = nn; ! 1512: - ! 1513: - tbl[n].ptr[m][p].nrpils = (short) q; ! 1514: - ! 1515: - alloc6(n, m, p, q); ! 1516: - ! 1517: - for (i = 0; i < q; i++) ! 1518: - { if (fscanf(mb, "[%d,%d] ", &x, &y) != 2) ! 1519: - badinput("table entry"); ! 1520: - tbl[n].ptr[m][p].one[i].transf = (short) x; ! 1521: - tbl[n].ptr[m][p].one[i].valtrans = (short) y; ! 1522: - ! 1523: - debug("\t[%d,%d] \n", x, y, 0, 0); ! 1524: - } ! 1525: -} ! 1526: - ! 1527: -getspecials(in) ! 1528: -{ register int i; ! 1529: - int n, m; ! 1530: - char stri[64]; ! 1531: - if (fscanf(mb, "ENDSTATES %d: ", &n) != 1) ! 1532: - badinput("endstates"); ! 1533: - ! 1534: - for (i = 0; i < n; i++) ! 1535: - { if (fscanf(mb, "%d,", &m) != 1 || m < 0 || m >= tbl[in].nrrows) ! 1536: - badinput("endstate"); ! 1537: - tbl[in].endrow[m] = 1; ! 1538: - } ! 1539: - if ((m = fscanf(mb, "%s %d: ", stri, &n)) != 2 || ! 1540: - strcmp(stri, "BADSTATES") != 0) ! 1541: - { printf("read %s %d\n", stri, n); ! 1542: - badinput("badstates"); ! 1543: - } ! 1544: - ! 1545: - for (i = 0; i < n; i++) ! 1546: - { if (fscanf(mb, "%d,", &m) != 1 || m < 0 || m >= tbl[in].nrrows) ! 1547: - badinput("badstate"); ! 1548: - tbl[in].badrow[m] = 1; ! 1549: - } ! 1550: - ! 1551: - if ((m = fscanf(mb, "%s %d: ", stri, &n)) != 2 || ! 1552: - strcmp(stri, "LABSTATES") != 0) ! 1553: - { printf("read %s %d\n", stri, n); ! 1554: - badinput("labstates"); ! 1555: - } ! 1556: - ! 1557: - for (i = 0; i < n; i++) ! 1558: - { if (fscanf(mb, "%d,", &m) != 1 || m < 0 || m >= tbl[in].nrrows) ! 1559: - badinput("labstate"); ! 1560: - tbl[in].labrow[m] = 1; ! 1561: - } ! 1562: - debug("specials:\n", 0, 0, 0, 0); ! 1563: - for (i = 0; i < tbl[in].nrrows; i++) ! 1564: - { n = tbl[in].endrow[i]; ! 1565: - m = tbl[in].badrow[i]; ! 1566: - debug("\t%d: %d/%d/%d\n", i, n, m, tbl[in].labrow[i]); ! 1567: - } ! 1568: -} ! 1569: - ! 1570: -getparams(pr, tb) ! 1571: -{ int n, m; ! 1572: - char stri[64]; ! 1573: - if (fscanf(mb, "%s %d/%d", stri, &n, &m) != 3) ! 1574: - { printf("read %s %d/%d\n", stri, n, m); ! 1575: - badinput("parameters"); ! 1576: - } ! 1577: - ! 1578: - tblpars[tb].nrms = (short) n; /* required sizes */ ! 1579: - tblpars[tb].nrvs = (short) m; ! 1580: - ! 1581: - if (processes[pr] == tb) ! 1582: - alloc8(pr, 2*n, 2*m); /* avalaible sizes */ ! 1583: -} ! 1584: - ! 1585: -getlocvars(p, tb) ! 1586: -{ register int i; ! 1587: - int n, m; ! 1588: - if (fscanf(mb, "%d l-variables: ", &n) != 1) ! 1589: - badinput("l-variables"); ! 1590: - ! 1591: - if (processes[p] != tb) ! 1592: - { tblvars[tb].nrlvars = (short) n; /* required size */ ! 1593: - if (n > 0) ! 1594: - tblvars[tb].lvarvals = (short *) ! 1595: - Smalloc(n * sizeof(short)); ! 1596: - for (i = 0; i < n; i++) ! 1597: - if (fscanf(mb, "%d,", &m) != 1) ! 1598: - badinput("l-vars"); ! 1599: - else ! 1600: - tblvars[tb].lvarvals[i] = (short) m; ! 1601: - } else ! 1602: - { tablpars[p].nrlvars = (short) (2*n); /* available size */ ! 1603: - procpars[p].nrlvars = (short) n; /* actually used */ ! 1604: - if (n > 0) ! 1605: - procpars[p].lvarvals = (short *) ! 1606: - Emalloc((2*n) * sizeof(short)); ! 1607: - for (i = 0; i < n; i++) ! 1608: - if (fscanf(mb, "%d,", &m) != 1) ! 1609: - badinput("lvar-inits"); ! 1610: - else ! 1611: - procpars[p].lvarvals[i] = (short) m; ! 1612: - } ! 1613: -} ! 1614: - ! 1615: -getcalls(in) ! 1616: -{ register int i, j; ! 1617: - int k, n, m, a, b, N; ! 1618: - char stri[64]; ! 1619: - if (fscanf(mb, "%s %d", stri, &n) != 2) /* FCTS */ ! 1620: - { printf("read %s %d\n", stri, n); ! 1621: - badinput("function calls"); ! 1622: - } ! 1623: - alloc9(in, n); ! 1624: - for (i = 0, N = n; i < N; i++) ! 1625: - { if (fscanf(mb, "%d-%d/%d: ", &n, &m, &k) != 3) ! 1626: - badinput("fct call"); ! 1627: - ! 1628: - alloc10(in, i, n, m, k); ! 1629: - ! 1630: - effnrstates[in] += tbl[reftasks[n]].nrrows; ! 1631: - ! 1632: - for (j = m+k, a = b = 0; j > 0; j--) ! 1633: - { if (fscanf(mb, "%d/%d", &n, &m) != 2) ! 1634: - badinput("fct call entry"); ! 1635: - if (n == 0) ! 1636: - tbl[in].calls[i].ms[a++] = (short) m; ! 1637: - else ! 1638: - tbl[in].calls[i].vs[b++] = (short) m; ! 1639: - } } ! 1640: -} ! 1641: - ! 1642: -getexprs() ! 1643: -{ int i, j, a, b, c; ! 1644: - char name[32]; ! 1645: - ! 1646: - if (fscanf(mb, "%s %d\n", name, &nexpr) != 2) ! 1647: - badinput("nexpr"); ! 1648: - if (strcmp(name, "EXPR") != 0) ! 1649: - badinput("expressions"); ! 1650: - ! 1651: - expr = (struct REVPOL **) ! 1652: - Smalloc(nexpr * sizeof(struct REVPOL *)); ! 1653: - ! 1654: - for (i = 0; i < nexpr; i++) ! 1655: - { fscanf(mb, "%d: ", &a); ! 1656: - ! 1657: - expr[i] = (struct REVPOL *) ! 1658: - Smalloc(a * sizeof(struct REVPOL)); ! 1659: - ! 1660: - for (j = 0; j < a; j++) ! 1661: - { fscanf(mb, "%d/%d: %d\n", &b, &c); ! 1662: - expr[i][j].toktyp = b; ! 1663: - expr[i][j].tokval = c; ! 1664: - } } ! 1665: -} ! 1666: - ! 1667: -showtables(how) ! 1668: -{ register int i, j; ! 1669: - int k, n, m, p; ! 1670: - char table[2*MAXPROC][64]; ! 1671: - ! 1672: - for (i = 0; i < nrprocs; i++) ! 1673: - { j = processes[i]; ! 1674: - sprintf(table[j], "process %d", i); ! 1675: - } ! 1676: - for (i = 0; i < nrrefs; i++) ! 1677: - { j = reftasks[i]; ! 1678: - sprintf(table[j], "reftask %d", i); ! 1679: - } ! 1680: - ! 1681: - for (i = 0; i < nrtbl; i++) ! 1682: - { ! 1683: - printf("\n%s (table %d):\n", table[i], i); ! 1684: - if (how && linecode) ! 1685: - { for (j = 2+strlen(tbl[i].rowname[0]); j > 0; j--) ! 1686: - putchar(' '); ! 1687: - } else printf(" "); ! 1688: - putchar('\t'); ! 1689: - for (k = 0; k < tbl[i].nrcols; k++) ! 1690: - { switch(tbl[i].coltyp[k]) { ! 1691: - case INP: printf("I:"); break; ! 1692: - case DFL: printf("D:"); break; ! 1693: - case TMO: printf("T:"); break; ! 1694: - case OUTP: printf("O:"); break; ! 1695: - case SPN: printf("S:"); break; ! 1696: - case CND: printf("C:"); break; ! 1697: - case FCT: printf("F:"); break; ! 1698: - } ! 1699: - if (tbl[i].colorg[k] != -1) ! 1700: - printf("%d/%d\t", tbl[i].colmap[k], tbl[i].colorg[k]); ! 1701: - else ! 1702: - printf("%d \t", tbl[i].colmap[k]); ! 1703: - } ! 1704: - ! 1705: - for (j = 0; j < tbl[i].nrrows; j++) ! 1706: - { if (!how || !linecode) ! 1707: - printf("\n%2d\t", j); ! 1708: - else ! 1709: - printf("\n%2d/%s\t", j, tbl[i].rowname[j]); ! 1710: - for (k = 0; k < tbl[i].nrcols; k++) ! 1711: - { if (how) ! 1712: - { ! 1713: - for (p = 0; p < tbl[i].ptr[j][k].nrpils; p++) ! 1714: - { n = (int) tbl[i].ptr[j][k].one[p].transf; ! 1715: - printf("%d,", n); ! 1716: - } ! 1717: - } else ! 1718: - { ! 1719: - if (tbl[i].ptr[j][k].nrpils > 0) ! 1720: - { n = (int) tbl[i].ptr[j][k].one[0].transf; ! 1721: - m = (int) tbl[i].ptr[j][k].one[0].valtrans; ! 1722: - printf("%d(%d)", n, m); ! 1723: - } ! 1724: - if (tbl[i].ptr[j][k].nrpils > 1) ! 1725: - putchar('+'); ! 1726: - } ! 1727: - putchar('\t'); ! 1728: - } ! 1729: - } } ! 1730: - putchar('\n'); ! 1731: -} ! 1732: - ! 1733: -whichq(n) ! 1734: -{ int i; ! 1735: - if (n < 0 || n >= MANY) ! 1736: - return -1; ! 1737: - ! 1738: - if ((i = xob[n]) == -1) ! 1739: - badinput("mbox sort incomplete"); ! 1740: - ! 1741: - return i; ! 1742: -} ! 1743: - ! 1744: -init() ! 1745: -{ register int i, m; ! 1746: - state = (int *) ! 1747: - Smalloc(nrprocs * sizeof(int)); ! 1748: - qsize = (int *) ! 1749: - Smalloc(nrqs * sizeof(int)); ! 1750: - head = (struct QUEUE **) ! 1751: - Smalloc(nrqs * sizeof(struct QUEUE *)); ! 1752: - tail = (struct QUEUE **) ! 1753: - Smalloc(nrqs * sizeof(struct QUEUE *)); ! 1754: - starter = (struct QUEUE **) ! 1755: - Smalloc(nrqs * sizeof(struct QUEUE *)); ! 1756: - ! 1757: - ! 1758: - for (i = 0; i < nrqs; i++) ! 1759: - { starter[i] = (struct QUEUE *) ! 1760: - Smalloc(sizeof(struct QUEUE)); ! 1761: - starter[i]->next = NULL; ! 1762: - qsize[i] = 0; ! 1763: - head[i] = tail[i] = starter[i]; ! 1764: - } ! 1765: - ! 1766: - decode(); ! 1767: - initable(); /* do not change the order of inits */ ! 1768: - iniqtable(); ! 1769: - inihash(); ! 1770: - ! 1771: - for (i = 0; i < nrprocs; i++) ! 1772: - { state[i] = 0; ! 1773: - procstack[i] = NULL; ! 1774: - ! 1775: - lbt[i].mapcol = (int *) ! 1776: - Smalloc(maxcol * sizeof(int)); ! 1777: - lbt[i].orgcol = (int *) ! 1778: - Smalloc(maxcol * sizeof(int)); ! 1779: - fiddler(i); ! 1780: - } ! 1781: - ! 1782: - s_last = NULL; ! 1783: - ! 1784: - for (i = 0; i < nrinit; i++) ! 1785: - { m = inits[i]; ! 1786: - if (send(m, whichq(m), NONE, NONE, 0) == 0) ! 1787: - badinput("qsize too small for initial string..."); ! 1788: - } ! 1789: - if (assertbl != NONE) ! 1790: - { assertbl = reftasks[assertbl]; ! 1791: - ! 1792: - abase = nrvars; ! 1793: - nrvars += tbl[assertbl].nrrows; ! 1794: - ! 1795: - if (abase > 0) ! 1796: - globvars = (int *) ! 1797: - Realloc(globvars, nrvars * sizeof(int)); ! 1798: - else ! 1799: - globvars = (int *) ! 1800: - Smalloc(nrvars * sizeof(int)); ! 1801: - ! 1802: - globvars[abase] = 1; ! 1803: - for (i = abase+1; i < nrvars; i++) ! 1804: - globvars[i] = 0; ! 1805: - } ! 1806: - if (errortbl != NONE) ! 1807: - { errortbl = reftasks[errortbl]; ! 1808: - ! 1809: - ebase = nrvars; ! 1810: - nrvars += tbl[errortbl].nrrows; ! 1811: - ! 1812: - if (ebase > 0) ! 1813: - globvars = (int *) ! 1814: - Realloc(globvars, nrvars * sizeof(int)); ! 1815: - else ! 1816: - globvars = (int *) ! 1817: - Smalloc(nrvars * sizeof(int)); ! 1818: - ! 1819: - globvars[ebase] = 1; ! 1820: - for (i = ebase+1; i < nrvars; i++) ! 1821: - globvars[i] = 0; ! 1822: - } ! 1823: -} ! 1824: - ! 1825: -decode() ! 1826: -{ register int i, j, m; ! 1827: - ! 1828: - for (i = 0; i < nrvars; i++) ! 1829: - { m = convert(globvars[i], NONE); ! 1830: - globvars[i] = (short) m; ! 1831: - } ! 1832: - for (i = 0; i < nrprocs; i++) ! 1833: - for (j = 0; j < procpars[i].nrlvars; j++) ! 1834: - { m = convert(procpars[i].lvarvals[j], i); ! 1835: - procpars[i].lvarvals[j] = (short) m; ! 1836: - } ! 1837: -} ! 1838: //GO.SYSIN DD trace1.c ! 1839: echo trace2.c 1>&2 ! 1840: sed 's/.//' >trace2.c <<'//GO.SYSIN DD trace2.c' ! 1841: -#include <stdio.h> ! 1842: -#include <errno.h> ! 1843: -#include "trace.h" ! 1844: -#include "trace.d" ! 1845: - ! 1846: - extern struct TBL *tbl; ! 1847: - extern struct LBT *lbt; ! 1848: - extern struct MBOX *mbox; ! 1849: - extern struct MNAME *fullname; ! 1850: - extern struct REVPOL **expr; ! 1851: - extern struct PROCSTACK **procstack; ! 1852: - ! 1853: - extern struct VARPARS *procpars; ! 1854: - extern struct TBLPARS *tblpars; ! 1855: - ! 1856: - extern struct LOCVARS *tblvars; ! 1857: - extern struct TBLPARS *tablpars; ! 1858: - ! 1859: - extern int *reftasks, *processes, *basics; ! 1860: - extern int *globvars, *inits, *xob, *effnrstates; ! 1861: - ! 1862: - extern char qoverride; ! 1863: - extern int QMAX, msgbase, maxcol, assertbl, errortbl; ! 1864: - ! 1865: -#define tell(s) fprintf(stderr, s) ! 1866: - ! 1867: -usage(str) ! 1868: - char *str; ! 1869: -{ fprintf(stderr, "trace: %s\n", str); ! 1870: - tell("usage: trace [-?] [N]\n"); ! 1871: - tell("\t-a show all prefixes leading into old states\n"); ! 1872: - tell("\t-b `blast mode' (quick, very partial search)\n"); ! 1873: - tell("\t-c N perform class N validation (N: 0..5) \n"); ! 1874: - tell("\t-f or -F alternative formats for printing queue histories\n"); ! 1875: - tell("\t-j stop at the first buffer lock found\n"); ! 1876: - tell("\t-k N restrict the state space cache to N thousand states\n"); ! 1877: - tell("\t-l show normal execution sequences and loops, but no prefixes\n"); ! 1878: - tell("\t-m N restrict search depth to N steps\n"); ! 1879: - tell("\t-n don't use timeout heuristics\n"); ! 1880: - tell("\t-q N set bound N on maximum queue size used\n"); ! 1881: - tell("\t-r N restrict the runtime to N minutes\n"); ! 1882: - tell("\t-R N report on progress every N minutes\n"); ! 1883: - tell("\t-s show the transition tables (different if combined with `v')\n"); ! 1884: - tell("\t-v verbose - print execution times, etc.\n"); ! 1885: - tell("\t-x perform a scatter search\n"); ! 1886: - tell("\tno flag: try a sensible partial search\n"); ! 1887: - exit(1); ! 1888: -} ! 1889: - ! 1890: -/* ! 1891: - * calls on Emalloc and Realloc go straight to the library malloc ! 1892: - * it is used for data that may be realloced but is never released ! 1893: - * - Smalloc claims memory that is never realloced and never released ! 1894: - * - emalloc and efree handle memory that is never realloced but often released ! 1895: - * - talloc and tfree are direct calls on the tac-package (used via emalloc) ! 1896: - */ ! 1897: - ! 1898: -char * ! 1899: -Stake(n) ! 1900: -{ char *try, *sbrk(), *Emalloc(); ! 1901: - extern int errno; ! 1902: - ! 1903: - do { ! 1904: - try = sbrk(n); ! 1905: - } while ((int) try == -1 && errno == EINTR); ! 1906: - ! 1907: - if ((int) try == -1) ! 1908: - return Emalloc(n); /* maybe some mem left here */ ! 1909: - ! 1910: - return try; ! 1911: -} ! 1912: - ! 1913: -#define CHUNK 4096 ! 1914: - ! 1915: -char *have; ! 1916: -long left = 0; ! 1917: - ! 1918: -char * ! 1919: -Smalloc(n) ! 1920: - unsigned n; ! 1921: -{ char *try; ! 1922: - ! 1923: - if (n == 0) ! 1924: - return (char *) NULL; ! 1925: - if (left < n) ! 1926: - { unsigned grow = (n < CHUNK) ? CHUNK : n; ! 1927: - have = Stake(grow); ! 1928: - left = grow; ! 1929: - } ! 1930: - try = have; ! 1931: - have += n; ! 1932: - left -= n; ! 1933: - ! 1934: - return try; ! 1935: -} ! 1936: - ! 1937: -char * ! 1938: -Emalloc(n) ! 1939: - unsigned n; ! 1940: -{ char *try, *malloc(); ! 1941: - ! 1942: - if (n == 0) ! 1943: - return (char *) NULL; ! 1944: - if ((try = malloc(n)) == NULL) ! 1945: - whoops("malloc fault"); ! 1946: - ! 1947: - return try; ! 1948: -} ! 1949: - ! 1950: -char * ! 1951: -Realloc(a, b) ! 1952: - char *a; unsigned b; ! 1953: -{ char *try, *realloc(); ! 1954: - ! 1955: - if (b == 0) ! 1956: - return (char *) NULL; ! 1957: - if ((try = realloc(a, b)) == NULL) ! 1958: - whoops("realloc returns 0"); ! 1959: - ! 1960: - return try; ! 1961: -} ! 1962: - ! 1963: -char * ! 1964: -emalloc(n) ! 1965: - unsigned n; ! 1966: -{ char *try; ! 1967: - char *talloc(); ! 1968: - ! 1969: - if (n == 0) ! 1970: - return (char *) NULL; ! 1971: - if ((try = talloc(n)) == NULL) ! 1972: - whoops("talloc fault"); ! 1973: - ! 1974: - return try; ! 1975: -} ! 1976: - ! 1977: -efree(at) ! 1978: - char *at; ! 1979: -{ ! 1980: - if (at) tfree(at); ! 1981: -} ! 1982: - ! 1983: -alloc1(x, y, z) ! 1984: -{ int n = x+y; ! 1985: - tbl = (struct TBL *) ! 1986: - Smalloc(n * sizeof(struct TBL)); ! 1987: - tblpars = (struct TBLPARS *) ! 1988: - Smalloc(n * sizeof(struct TBLPARS)); ! 1989: - tblvars = (struct LOCVARS *) ! 1990: - Smalloc(n * sizeof(struct LOCVARS)); ! 1991: - reftasks = (int *) ! 1992: - Smalloc(x * sizeof(int)); ! 1993: - processes = (int *) ! 1994: - Smalloc(y * sizeof(int)); ! 1995: - lbt = (struct LBT *) ! 1996: - Smalloc(y * sizeof(struct LBT)); ! 1997: - procpars = (struct VARPARS *) ! 1998: - Smalloc(y * sizeof(struct VARPARS)); ! 1999: - ! 2000: - tablpars = (struct TBLPARS *) ! 2001: - Smalloc(y * sizeof(struct TBLPARS)); ! 2002: - ! 2003: - basics = (int *) ! 2004: - Smalloc(y * sizeof(int)); ! 2005: - procstack = (struct PROCSTACK **) ! 2006: - Smalloc(y * sizeof(struct PROCSTACK *)); ! 2007: - mbox = (struct MBOX *) ! 2008: - Smalloc(z * sizeof(struct MBOX)); ! 2009: - ! 2010: - effnrstates = (int *) ! 2011: - Smalloc(n * sizeof(int)); ! 2012: -} ! 2013: - ! 2014: -alloc2(n, p, who) ! 2015: -{ char x; ! 2016: - ! 2017: - x = (qoverride && p > QMAX)? QMAX : p; ! 2018: - ! 2019: - if (x >= 256) ! 2020: - whoops("illegal queue size"); ! 2021: - if (x >= 16) ! 2022: - fprintf(stderr, "warning, very large qsize (%d), queue %d\n", x, n); ! 2023: - ! 2024: - mbox[n].limit = x; ! 2025: - mbox[n].owner = (who >= 0) ? who : 0; ! 2026: -} ! 2027: - ! 2028: -alloc3(n) ! 2029: -{ inits = (int *) ! 2030: - Smalloc(n * sizeof(int)); ! 2031: -} ! 2032: - ! 2033: -alloc4(n) ! 2034: -{ if (assertbl == NONE && errortbl == NONE) ! 2035: - globvars = (int *) ! 2036: - Smalloc(n * sizeof(int)); ! 2037: - else ! 2038: - globvars = (int *) ! 2039: - Emalloc(n * sizeof(int)); ! 2040: -} ! 2041: - ! 2042: -alloc45(n) ! 2043: -{ register int i; ! 2044: - fullname = (struct MNAME *) ! 2045: - Smalloc(n * sizeof(struct MNAME)); ! 2046: - xob = (int *) ! 2047: - Smalloc((n+msgbase) * sizeof(int)); ! 2048: - for (i = 0; i < n+msgbase; i++) ! 2049: - xob[i] = -1; ! 2050: -} ! 2051: - ! 2052: -alloc5(n) ! 2053: -{ register int i, j, r, c; ! 2054: - ! 2055: - r = tbl[n].nrrows; ! 2056: - if ((c = tbl[n].nrcols) > maxcol) ! 2057: - maxcol = c; ! 2058: - ! 2059: - tbl[n].endrow = (int *) Smalloc(r * sizeof(int)); ! 2060: - tbl[n].deadrow = (int *) Smalloc(r * sizeof(int)); ! 2061: - tbl[n].badrow = (int *) Smalloc(r * sizeof(int)); ! 2062: - tbl[n].labrow = (int *) Smalloc(r * sizeof(int)); ! 2063: - tbl[n].colmap = (int *) Smalloc(c * sizeof(int)); ! 2064: - tbl[n].colorg = (int *) Smalloc(c * sizeof(int)); ! 2065: - tbl[n].coltyp = (int *) Smalloc(c * sizeof(int)); ! 2066: - tbl[n].ptr = (struct IND **) Smalloc(r * sizeof(struct IND *)); ! 2067: - tbl[n].rowname = (char **) Smalloc(r * sizeof(char *)); ! 2068: - ! 2069: - for (i = 0; i < r; i++) ! 2070: - { tbl[n].ptr[i] = (struct IND *) ! 2071: - Smalloc(c * sizeof(struct IND)); ! 2072: - tbl[n].rowname[i] = (char *) ! 2073: - Smalloc(128 * sizeof(char)); ! 2074: - ! 2075: - for (j = 0; j < c; j++) ! 2076: - tbl[n].ptr[i][j].nrpils = 0; ! 2077: - tbl[n].deadrow[i] = 1; ! 2078: - tbl[n].endrow[i] = tbl[n].badrow[i] = 0; ! 2079: - tbl[n].labrow[i] = 0; ! 2080: - } ! 2081: - tbl[n].labrow[0] = 1; /* make sure initial state is always checked */ ! 2082: -} ! 2083: - ! 2084: -alloc6(n, m, p, q) ! 2085: -{ tbl[n].ptr[m][p].one = (struct ELM *) ! 2086: - Smalloc(q * sizeof(struct ELM)); ! 2087: -} ! 2088: - ! 2089: -alloc8(pr, p, q) ! 2090: -{ ! 2091: - tablpars[pr].nrms = (short) p; /* available */ ! 2092: - tablpars[pr].nrvs = (short) q; ! 2093: - ! 2094: - procpars[pr].ms = (short *) ! 2095: - Emalloc(p * sizeof(short)); ! 2096: - procpars[pr].vs = (short *) ! 2097: - Emalloc(q * sizeof(short)); ! 2098: - ! 2099: - procpars[pr].nrms = 0; /* actually used */ ! 2100: - procpars[pr].nrvs = 0; ! 2101: -} ! 2102: - ! 2103: -alloc9(in, p) ! 2104: -{ ! 2105: - tbl[in].calls = (struct CPARS *) ! 2106: - Smalloc(p * sizeof(struct CPARS)); ! 2107: -} ! 2108: - ! 2109: -alloc10(in, cn, p, q, r) ! 2110: -{ ! 2111: - tbl[in].calls[cn].callwhat = (short) p; ! 2112: - tbl[in].calls[cn].nrms = (short) q; ! 2113: - tbl[in].calls[cn].nrvs = (short) r; ! 2114: - ! 2115: - tbl[in].calls[cn].ms = (short *) ! 2116: - Smalloc(q * sizeof (short)); ! 2117: - ! 2118: - tbl[in].calls[cn].vs = (short *) ! 2119: - Smalloc(r * sizeof (short)); ! 2120: -} ! 2121: - ! 2122: -whoops(s) ! 2123: - char *s; ! 2124: -{ ! 2125: - fprintf(stderr, "trace: %s\n", s); ! 2126: - postlude(); ! 2127: - exit(1); ! 2128: -} ! 2129: - ! 2130: -badinput(s) ! 2131: - char *s; ! 2132: -{ extern char fname[]; ! 2133: - ! 2134: - fflush(stdout); ! 2135: - fprintf(stderr, "trace: read error `%s': %s\n", s, fname); ! 2136: - exit(1); ! 2137: -} ! 2138: //GO.SYSIN DD trace2.c ! 2139: echo trace3.c 1>&2 ! 2140: sed 's/.//' >trace3.c <<'//GO.SYSIN DD trace3.c' ! 2141: -#include <stdio.h> ! 2142: -#include "trace.h" ! 2143: -#include "trace.d" ! 2144: - ! 2145: -#define DEBUG 0 ! 2146: - ! 2147: -#define BS(n) ((n) & ~(PASSED)) ! 2148: - ! 2149: - extern struct TBL *tbl; ! 2150: - extern struct LBT *lbt; ! 2151: - extern struct MBOX *mbox; ! 2152: - extern struct MNAME *fullname; ! 2153: - extern struct PROCSTACK **procstack; ! 2154: - ! 2155: - extern struct VARPARS *procpars; ! 2156: - extern struct TBLPARS *tblpars; ! 2157: - ! 2158: - extern struct LOCVARS *tblvars; ! 2159: - extern struct TBLPARS *tablpars; ! 2160: - ! 2161: - extern struct QUEUE **starter, **head, **tail; ! 2162: - extern struct QUEUE *s_first, *s_last; ! 2163: - extern struct VISIT *lastvisit; ! 2164: - ! 2165: - extern int *reftasks, *processes, *basics; ! 2166: - extern int *globvars, *inits, *state, *qsize; ! 2167: - ! 2168: - extern int nrtbl, nrqs, nrrefs, nrprocs, nrinit; ! 2169: - extern int nrvars, nrmesgs, msgbase; ! 2170: - extern int maxlevel, maxreached; ! 2171: - ! 2172: - extern char noshortcut, prbyq, timedd, blast, qandirty, muststore; ! 2173: - extern char maxxed, completed, lockplus, firstlock; ! 2174: - ! 2175: - extern long locksf, normf, loopsf; ! 2176: - extern double zapper; ! 2177: - ! 2178: - short lastqueue; /* the last queue addressed */ ! 2179: - int level = 0; ! 2180: - double COUNT = 0; ! 2181: - ! 2182: - char *emalloc(), *Realloc(), *Emalloc(); ! 2183: - ! 2184: -determine(m) ! 2185: -{ ! 2186: - if (m >= 3*MANY) return 0; /* constant */ ! 2187: - else if (m >= 2*MANY) return 1; /* parameter */ ! 2188: - else if (m >= MANY) return 2; /* local */ ! 2189: - else if (m >= 0) return 3; /* global */ ! 2190: - else if (m < -3*MANY) return 5; /* negative number */ ! 2191: - else if (m <= -2) return 4; /* expression */ ! 2192: - else ! 2193: - whoops("cannot happen - determine"); ! 2194: -} ! 2195: - ! 2196: -convert(m, pr) ! 2197: -{ int res, n = m; ! 2198: - ! 2199: - /* convert a pvar: global, local, parameter, or a constant */ ! 2200: - ! 2201: - switch (determine(n)) { ! 2202: - case 5: res = n + 3*MANY; break; ! 2203: - case 4: res = evalcond(-(m+2), pr); break; ! 2204: - case 0: res = n - 3*MANY; break; ! 2205: - case 1: res = wapper(m, pr); break; ! 2206: - case 2: n -= MANY; ! 2207: - if (n >= 0 && n < (int) procpars[pr].nrlvars) ! 2208: - res = (int) procpars[pr].lvarvals[n]; ! 2209: - else ! 2210: - whoops("reference to non-existing local var"); ! 2211: - break; ! 2212: - case 3: if (n >= 0 && n < nrvars) ! 2213: - res = globvars[n]; ! 2214: - else ! 2215: - whoops("reference to non-existing global var"); ! 2216: - break; ! 2217: - default: ! 2218: - whoops("cannot happen - convert"); /* got a parameter */ ! 2219: - break; ! 2220: - } ! 2221: - return res; ! 2222: -} ! 2223: - ! 2224: -wapper(n, pr) ! 2225: -{ int x = n - 2*MANY; ! 2226: - int y; ! 2227: - if (x < 0 || x >= MANY) ! 2228: - return n; /* not a parameter */ ! 2229: - else ! 2230: - { if (x >= procpars[pr].nrvs) ! 2231: - whoops("unknown parameter of type pvar"); ! 2232: - y = (int) procpars[pr].vs[x]; ! 2233: - if (y >= 2*MANY && y < 3*MANY) ! 2234: - whoops("unresolved parameter reference"); ! 2235: - return y; ! 2236: - } ! 2237: -} ! 2238: - ! 2239: -mapper(n, pr) /* convert a message parameter */ ! 2240: -{ register int x = n - MANY; ! 2241: - ! 2242: - if (x < 0 || x >= MANY) ! 2243: - return n; /* not a parameter */ ! 2244: - else ! 2245: - { if (x >= procpars[pr].nrms) ! 2246: - whoops("bad news: illegal message parameter"); ! 2247: - return ((int)procpars[pr].ms[x]); ! 2248: - } ! 2249: -} ! 2250: - ! 2251: -matchon(n, m, t, trial, TT, pr) ! 2252: -{ ! 2253: -#if DEBUG ! 2254: - printf("trial %d, pr %d; ", trial, pr); ! 2255: - if (TT == INP || TT == OUTP) ! 2256: - printf("msg %s, ", fullname[n-msgbase].mname); ! 2257: - else ! 2258: - printf("code %d, ", n); ! 2259: - printf("q %d, tbl %d, type %d\n", m, t, TT); ! 2260: -#endif ! 2261: - ! 2262: - if (trial == 2) ! 2263: - return (TT == TMO && qsize[m] == 0); ! 2264: - else ! 2265: - { ! 2266: - switch (TT) { ! 2267: - case FCT : ! 2268: - case SPN : return 1; ! 2269: - case CND : return (evalcond(n, pr)); ! 2270: - case DFL : return (qsize[m] > 0 && no_other(t,head[m]->mesg,pr)); ! 2271: - case INP : return (qsize[m] > 0 && BS(head[m]->mesg) == n); ! 2272: - case TMO : return (noshortcut && qsize[m] == 0); ! 2273: - case OUTP: return (qsize[m] < mbox[m].limit); ! 2274: - default : whoops("unknown type in column head"); ! 2275: - } ! 2276: - } ! 2277: -} ! 2278: - ! 2279: -no_other(x, yy, pr) ! 2280: -{ struct TBL *tmp = &(tbl[x]); ! 2281: - int y = BS(yy); ! 2282: - int j = tmp->nrcols; ! 2283: - int h = state[pr]; ! 2284: - int i; ! 2285: - ! 2286: - for (i = 0; i < j; i++) ! 2287: - { if (tmp->coltyp[i] == INP ! 2288: - && tmp->ptr[h][i].nrpils > 0 ! 2289: - && y == lbt[pr].mapcol[i]) ! 2290: - return 0; ! 2291: - } ! 2292: - return 1; ! 2293: -} ! 2294: - ! 2295: -send(m, to, with, pr, nst) ! 2296: -{ struct QUEUE *tmp; ! 2297: - register struct QUEUE *hook = tail[to]; ! 2298: - int what = NONE; ! 2299: - ! 2300: - if (with != NONE) ! 2301: - { if ((what = convert(with, pr)) >= USED - 1 || what < 0) ! 2302: - { output("aborted: ", 0); ! 2303: - whoops("cargo too large or negative"); ! 2304: - } ! 2305: - hook->cargo = (unsigned short) ( what | USED ); ! 2306: - } else ! 2307: - hook->cargo = (unsigned short) 0; ! 2308: - ! 2309: - if (qsize[to] >= mbox[to].limit) ! 2310: - whoops("cannot happen - send"); ! 2311: - ! 2312: - tmp = (struct QUEUE *) emalloc(sizeof(struct QUEUE)); ! 2313: - tmp->last = hook; ! 2314: -#if TRAIL ! 2315: - hook->tstate[0] = (short) processes[pr]; ! 2316: - hook->tstate[1] = (short) nst; ! 2317: -#endif TRAIL ! 2318: - ! 2319: - hook->mesg = (short) m; ! 2320: - hook->next = tmp; ! 2321: - hook->s_back = s_last; ! 2322: - hook->s_forw = NULL; ! 2323: - if (s_last == NULL) ! 2324: - s_first = hook; ! 2325: - else ! 2326: - s_last->s_forw = hook; ! 2327: - ! 2328: - s_last = hook; ! 2329: - tail[to] = tmp; ! 2330: - qsize[to]++; ! 2331: -#if DEBUG ! 2332: - printf("\tsent %d to %d, size %d, ", m, to, qsize[to]); ! 2333: - printf("cargo %d [%d]\n", what, hook->cargo); ! 2334: -#endif ! 2335: - require(OUTP, m, to); ! 2336: - ! 2337: - return 1; ! 2338: -} ! 2339: - ! 2340: -receive(from, with, pr, ice) ! 2341: - struct FREEZE *ice; ! 2342: -{ struct QUEUE *hook; ! 2343: - int what=NONE, wither; ! 2344: - ! 2345: - if (qsize[from] <= 0) ! 2346: - whoops("trying to receive from empty queue"); ! 2347: - ! 2348: - hook = head[from]; ! 2349: - if (hook->cargo & USED) ! 2350: - { what = (int) ((hook->cargo) & (~USED)); ! 2351: - if (with == NONE) ! 2352: - { fprintf(stderr, "value %d sent (msg: ", what); ! 2353: - putname(hook, 1); ! 2354: - fprintf(stderr, ") but not expected\n"); ! 2355: - } ! 2356: - else ! 2357: - { ice->whichvar = wither = wapper(with, pr); ! 2358: - if (wither >= 3*MANY || wither <= -3*MANY) ! 2359: - whoops("receiving into a constant..."); ! 2360: - if (wither < MANY) ! 2361: - { ice->oldvalue = globvars[wither]; ! 2362: - globvars[wither] = what; ! 2363: - } else ! 2364: - { int n = wither - MANY; ! 2365: - if (n >= 0 && n < (int) procpars[pr].nrlvars) ! 2366: - { ice->oldvalue = procpars[pr].lvarvals[n]; ! 2367: - procpars[pr].lvarvals[n] = (short) what; ! 2368: - } else ! 2369: - whoops("unknown local var"); ! 2370: - } ! 2371: - } ! 2372: - } else ! 2373: - { if (with != NONE) ! 2374: - { fprintf(stderr, "value %d expected (msg: ", with); ! 2375: - putname(hook, 1); ! 2376: - fprintf(stderr, ") but not sent\n"); ! 2377: - } ! 2378: - } ! 2379: - ! 2380: - hook->mesg |= PASSED; ! 2381: -#if DEBUG ! 2382: - printf("\trecv %d from queue %d, ", head[from]->mesg & (~PASSED), from); ! 2383: - printf("cargo %d [%d], into var %d\n", what, hook->cargo, with); ! 2384: -#endif ! 2385: - ! 2386: - head[from] = hook->next; ! 2387: - qsize[from]--; ! 2388: - ! 2389: - require(INP, (hook->mesg & (~PASSED)), from); ! 2390: - ! 2391: - return 1; ! 2392: -} ! 2393: - ! 2394: -unrecv(from) ! 2395: -{ ! 2396: - if (head[from] == starter[from]) ! 2397: - whoops("unreceiving beyond initial state"); ! 2398: - ! 2399: - head[from] = head[from]->last; ! 2400: - head[from]->mesg &= (~PASSED); ! 2401: - ! 2402: - qsize[from]++; ! 2403: -} ! 2404: - ! 2405: -unsend() ! 2406: -{ short i = lastqueue; ! 2407: - ! 2408: - if (tail[i] == starter[i]) ! 2409: - whoops("unsending beyond initial state"); ! 2410: - if ((tail[i] = tail[i]->last) != s_last) ! 2411: - whoops("unsend: tail not last sent message"); ! 2412: - ! 2413: - if ((s_last = s_last->s_back) != NULL) ! 2414: - s_last->s_forw = NULL; ! 2415: - else ! 2416: - s_first = NULL; ! 2417: - efree(tail[i]->next); ! 2418: - ! 2419: - qsize[i]--; ! 2420: -} ! 2421: - ! 2422: -output(tag, willabort) ! 2423: - char *tag; ! 2424: -{ struct QUEUE *tmp; ! 2425: - ! 2426: - printf("%s", tag); ! 2427: - ! 2428: - if ((tmp = s_first) != NULL) ! 2429: - { formatted((struct QUEUE *) 0); ! 2430: - if (prbyq != 2) ! 2431: - do putname(tmp, 0); while ((tmp = tmp->s_forw) != NULL); ! 2432: - putchar('\n'); ! 2433: - } else ! 2434: - printf("null output\n"); ! 2435: - ! 2436: - if (willabort == 2 || (firstlock && willabort == 1)) ! 2437: - { completed = 1; ! 2438: - postlude(); ! 2439: - } ! 2440: -} ! 2441: - ! 2442: -putname(tmp, how) ! 2443: - struct QUEUE *tmp; ! 2444: -{ int i, k = (int) (BS(tmp->mesg)) - msgbase; ! 2445: - char nnn[128]; ! 2446: - ! 2447: - i = strlen(fullname[k].mname); ! 2448: - if (tmp->mesg & PASSED) ! 2449: - sprintf(nnn, "%s", fullname[k].mname); ! 2450: - else ! 2451: - { sprintf(nnn, "[%s]", fullname[k].mname); ! 2452: - i += 2; ! 2453: - } ! 2454: - ! 2455: - if (tmp->cargo & USED) ! 2456: - sprintf(&nnn[i], "(%d),", (tmp->cargo & (~USED))); ! 2457: - else ! 2458: - sprintf(&nnn[i], ","); ! 2459: - ! 2460: - if (how) ! 2461: - fprintf(stderr, "%s", nnn); ! 2462: - else ! 2463: - printf("%s", nnn); ! 2464: - ! 2465: - return strlen(nnn); ! 2466: -} ! 2467: - ! 2468: -inendstate() ! 2469: -{ int i, j, k; ! 2470: - ! 2471: - for (i = 0, k = nrprocs; i < nrprocs; i++) ! 2472: - { j = processes[i]; ! 2473: - if (j != basics[i] || tbl[j].endrow[state[i]] != 1) ! 2474: - k--; ! 2475: - } ! 2476: - return k; ! 2477: -} ! 2478: - ! 2479: -formatted(at) ! 2480: - struct QUEUE *at; ! 2481: -{ struct QUEUE *tmp = s_first; ! 2482: - int i, j; extern int linecode; ! 2483: - ! 2484: - if (tmp == NULL) ! 2485: - return; ! 2486: - ! 2487: - switch((int) prbyq) { ! 2488: - case 0: break; ! 2489: - case 1: ! 2490: - for (i = 0; i < nrqs; i++) ! 2491: - { printf("\n\t%s = {", mbox[i].qname); ! 2492: - for (tmp = starter[i]; tmp != tail[i]; tmp = tmp->next) ! 2493: - putname(tmp, 0); ! 2494: - printf("}"); ! 2495: - } ! 2496: - printf("\nexecution sequence:\n\t"); ! 2497: - break; ! 2498: - case 2: putchar('\n'); ! 2499: - for (i = 0; i < nrqs; i++) ! 2500: - printf("%2d = %s\n", i, mbox[i].qname); ! 2501: - for (i = 0; i < nrqs; i++) ! 2502: - printf("\t%2d", i); ! 2503: -#if TRAIL ! 2504: - if (linecode) ! 2505: - printf(" \tsource"); ! 2506: -#endif TRAIL ! 2507: - putchar('\n'); ! 2508: - do ! 2509: - { if (tmp == at) ! 2510: - printf(" >>"); ! 2511: - for (i = j = whichq(BS(tmp->mesg)); i >= 0; i--) ! 2512: - putchar('\t'); ! 2513: - i = putname(tmp, 0); ! 2514: -#if TRAIL ! 2515: - if (linecode) ! 2516: - { for (i = 16-i; i > 0; i--) putchar(' '); ! 2517: - for (j = nrqs-j; j > 0; j--) putchar('\t'); ! 2518: - printf("%s", tbl[tmp->tstate[0]].rowname[tmp->tstate[1]]); ! 2519: - } ! 2520: -#endif TRAIL ! 2521: - putchar('\n'); ! 2522: - } while ((tmp = tmp->s_forw) != NULL); ! 2523: - if (at != NULL) ! 2524: - printf(" >>\n"); ! 2525: - break; ! 2526: - } ! 2527: -} ! 2528: - ! 2529: -putloop(at, aa) ! 2530: - struct QUEUE *at; ! 2531: - char aa; ! 2532: -{ register struct QUEUE *tmp = s_first; ! 2533: - ! 2534: - if (aa) ! 2535: - printf("loop:\t"); ! 2536: - else ! 2537: - printf("assertion violated: "); ! 2538: - ! 2539: - if (s_first != NULL) ! 2540: - { formatted(at); ! 2541: - if (prbyq != 2) ! 2542: - { do ! 2543: - { putname(tmp, 0); ! 2544: - if (tmp == at) ! 2545: - printf("//"); ! 2546: - } while ((tmp = tmp->s_forw) != NULL); ! 2547: - printf("//\n"); ! 2548: - } ! 2549: - } else ! 2550: - printf("null output\n"); ! 2551: -} ! 2552: - ! 2553: -ppop(pr) ! 2554: -{ struct PROCSTACK *tmp = procstack[pr]; ! 2555: - int i = (int) procstack[pr]->uptable; ! 2556: - ! 2557: - if (procstack[pr] == NULL) ! 2558: - whoops("null stack"); ! 2559: - ! 2560: - restorvarpars(tmp->varparsaved, pr); ! 2561: - procstack[pr] = procstack[pr]->follow; ! 2562: - ! 2563: - efree(tmp->varparsaved); ! 2564: - efree(tmp); ! 2565: - ! 2566: - return i; /* we're returing to this table */ ! 2567: -} ! 2568: - ! 2569: -ppush(pr, what, tr) ! 2570: -{ struct PROCSTACK *tmp; ! 2571: - ! 2572: - tmp = (struct PROCSTACK *) ! 2573: - emalloc(sizeof(struct PROCSTACK)); ! 2574: - ! 2575: - tmp->varparsaved = (struct VARPARS *) ! 2576: - emalloc(sizeof(struct VARPARS)); ! 2577: - ! 2578: - savevarpars (tmp->varparsaved, pr); ! 2579: - ! 2580: - tmp->uptable = (short) what; ! 2581: - tmp->uptransf = (short) tr; ! 2582: - tmp->follow = procstack[pr]; ! 2583: - procstack[pr] = tmp; ! 2584: -} ! 2585: - ! 2586: -setlvars(to, pr) ! 2587: -{ register int i; ! 2588: - short z = tblvars[to].nrlvars; ! 2589: - ! 2590: - if (z > tablpars[pr].nrlvars) ! 2591: - { if (tablpars[pr].nrlvars > 0) ! 2592: - procpars[pr].lvarvals = (short *) ! 2593: - Realloc(procpars[pr].lvarvals, z * sizeof(short)); ! 2594: - else ! 2595: - procpars[pr].lvarvals = (short *) ! 2596: - Emalloc(z * sizeof(short)); ! 2597: - ! 2598: - tablpars[pr].nrlvars = z; ! 2599: - } ! 2600: - ! 2601: - procpars[pr].nrlvars = z; ! 2602: - ! 2603: - for (i = 0; i < z; i++) ! 2604: - procpars[pr].lvarvals[i] = convert(tblvars[to].lvarvals[i], pr); ! 2605: -} ! 2606: - ! 2607: -setpars(from, to, pr) ! 2608: - struct CPARS *from; ! 2609: -{ struct VARPARS tbuff; ! 2610: - register int i; ! 2611: - short x = tblpars[to].nrms; ! 2612: - short y = tblpars[to].nrvs; ! 2613: - ! 2614: - savemapped(&tbuff, from, pr); /* mapper() needs old nrms & nrvs */ ! 2615: - ! 2616: - if (x > tablpars[pr].nrms) ! 2617: - { if (tablpars[pr].nrms > 0) ! 2618: - procpars[pr].ms = (short *) ! 2619: - Realloc(procpars[pr].ms, x * sizeof(short)); ! 2620: - else ! 2621: - procpars[pr].ms = (short *) ! 2622: - Emalloc(x * sizeof(short)); ! 2623: - ! 2624: - tablpars[pr].nrms = x; ! 2625: - } ! 2626: - if (y > tablpars[pr].nrvs) ! 2627: - { if (tablpars[pr].nrvs > 0) ! 2628: - procpars[pr].vs = (short *) ! 2629: - Realloc(procpars[pr].vs, y * sizeof(short)); ! 2630: - else ! 2631: - procpars[pr].vs = (short *) ! 2632: - Emalloc(y * sizeof(short)); ! 2633: - ! 2634: - tablpars[pr].nrvs = y; ! 2635: - } ! 2636: - ! 2637: - procpars[pr].nrms = tbuff.nrms; ! 2638: - procpars[pr].nrvs = tbuff.nrvs; ! 2639: - ! 2640: - for (i = 0; i < procpars[pr].nrms; i++) ! 2641: - procpars[pr].ms[i] = tbuff.ms[i]; ! 2642: - ! 2643: - for (i = 0; i < procpars[pr].nrvs; i++) ! 2644: - procpars[pr].vs[i] = tbuff.vs[i]; ! 2645: - ! 2646: - efree(tbuff.ms); efree(tbuff.vs); ! 2647: -} ! 2648: - ! 2649: -#if DEBUG ! 2650: -showstate() ! 2651: -{ int i, j; ! 2652: - printf("%2d: S:", level); ! 2653: - for (i = 0; i < nrprocs; i++) ! 2654: - printf("%d,", state[i]); ! 2655: - printf("M:"); ! 2656: - for (i = 0; i < nrprocs; i++) ! 2657: - printf("%d,", processes[i]); ! 2658: - printf("Q:"); ! 2659: - for (i = 0; i < nrqs; i++) ! 2660: - printf("%d,", qsize[i]); ! 2661: - printf("H:"); ! 2662: - for (i = 0; i < nrqs; i++) ! 2663: - if (qsize[i] == 0) ! 2664: - printf("-,"); ! 2665: - else ! 2666: - { j = (int) BS(head[i]->mesg); ! 2667: - printf("%s,", fullname[j-msgbase].mname); ! 2668: - } ! 2669: - printf("\tV:"); ! 2670: - for (i = 0; i < nrprocs; i++) ! 2671: - { for (j = 0; j < procpars[i].nrlvars; j++) ! 2672: - printf("%d ", procpars[i].lvarvals[j]); ! 2673: - putchar(';'); ! 2674: - } ! 2675: - putchar('\n'); ! 2676: -} ! 2677: -#endif ! 2678: - ! 2679: -retable(prc, ice) ! 2680: - struct FREEZE *ice; ! 2681: -{ struct CUBE *it, *here; ! 2682: - int t = processes[prc]; ! 2683: - ! 2684: - if (ice->cube == NULL) ! 2685: - { here = ice->cube = (struct CUBE *) ! 2686: - emalloc(sizeof(struct CUBE)); ! 2687: - here->pntr = here->rtnp = NULL; ! 2688: - } else ! 2689: - { for (it = ice->cube; it->pntr != NULL; it = it->pntr) ! 2690: - ; ! 2691: - it->pntr = (struct CUBE *) ! 2692: - emalloc(sizeof(struct CUBE)); ! 2693: - it->pntr->rtnp = it; ! 2694: - here = it->pntr; ! 2695: - here->pntr = NULL; ! 2696: - } ! 2697: - here->poporpush = POP; ! 2698: - here->which = (short) prc; ! 2699: - here->procsaved = (short) t; ! 2700: - here->transfsaved = procstack[prc]->uptransf; ! 2701: - here->varparsaved = (struct VARPARS *) ! 2702: - emalloc(sizeof(struct VARPARS)); ! 2703: - ! 2704: - savevarpars(here->varparsaved, prc); ! 2705: - processes[prc] = ppop(prc); ! 2706: - fiddler(prc); ! 2707: - state[prc] = (int) here->transfsaved; ! 2708: - muststore = tbl[processes[prc]].labrow[state[prc]]; ! 2709: -} ! 2710: - ! 2711: -savevarpars(at, j) ! 2712: - struct VARPARS *at; ! 2713: -{ register int i; ! 2714: - struct VARPARS *it; ! 2715: - ! 2716: - it = &(procpars[j]); ! 2717: - at->nrms = it->nrms; ! 2718: - at->nrvs = it->nrvs; ! 2719: - at->nrlvars = it->nrlvars; ! 2720: - ! 2721: - at->ms = (short *) emalloc(it->nrms * sizeof(short)); ! 2722: - at->vs = (short *) emalloc(it->nrvs * sizeof(short)); ! 2723: - at->lvarvals = (short *) emalloc(it->nrlvars * sizeof(short)); ! 2724: - ! 2725: - for (i = 0; i < at->nrms; i++) ! 2726: - at->ms[i] = it->ms[i]; ! 2727: - for (i = 0; i < at->nrvs; i++) ! 2728: - at->vs[i] = it->vs[i]; ! 2729: - for (i = 0; i < it->nrlvars; i++) ! 2730: - at->lvarvals[i] = it->lvarvals[i]; ! 2731: -} ! 2732: - ! 2733: -savemapped(at, it, j) ! 2734: - struct VARPARS *at; ! 2735: - struct CPARS *it; ! 2736: -{ register int i; ! 2737: - ! 2738: - at->nrms = it->nrms; ! 2739: - at->nrvs = it->nrvs; ! 2740: - ! 2741: - at->ms = (short *) ! 2742: - emalloc(it->nrms * sizeof(short)); ! 2743: - at->vs = (short *) ! 2744: - emalloc(it->nrvs * sizeof(short)); ! 2745: - ! 2746: - for (i = 0; i < at->nrms; i++) ! 2747: - at->ms[i] = (short) mapper(it->ms[i], j); ! 2748: - ! 2749: - for (i = 0; i < at->nrvs; i++) ! 2750: - at->vs[i] = (short) convert(it->vs[i], j); ! 2751: -} ! 2752: - ! 2753: -restorvarpars(at, pr) ! 2754: - struct VARPARS *at; ! 2755: -{ register int i; ! 2756: - ! 2757: - procpars[pr].nrms = at->nrms; ! 2758: - procpars[pr].nrvs = at->nrvs; ! 2759: - procpars[pr].nrlvars = at->nrlvars; ! 2760: - ! 2761: - for (i = 0; i < at->nrms; i++) ! 2762: - procpars[pr].ms[i] = at->ms[i]; ! 2763: - ! 2764: - for (i = 0; i < at->nrvs; i++) ! 2765: - procpars[pr].vs[i] = at->vs[i]; ! 2766: - ! 2767: - for (i = 0; i < at->nrlvars; i++) ! 2768: - procpars[pr].lvarvals[i] = at->lvarvals[i]; ! 2769: - ! 2770: - efree(at->ms); ! 2771: - efree(at->vs); ! 2772: - efree(at->lvarvals); ! 2773: -} ! 2774: - ! 2775: -freeze(icy) ! 2776: - struct FREEZE *icy; ! 2777: -{ register int i; ! 2778: - struct FREEZE *ice = icy; ! 2779: - ! 2780: - ice->statsaved = (short *) emalloc(nrprocs * sizeof(short)); ! 2781: - ice->varsaved = (short *) emalloc(nrvars * sizeof(short)); ! 2782: - ! 2783: - ice->lastsav = lastqueue; ! 2784: - ice->cube = NULL; ! 2785: - ! 2786: - for (i = 0; i < nrvars; i++) ! 2787: - ice->varsaved[i] = (short) globvars[i]; ! 2788: - ! 2789: - for (i = 0; i < nrprocs; i++) ! 2790: - { ! 2791: - ice->statsaved[i] = (short) state[i]; ! 2792: - ! 2793: - while (tbl[processes[i]].deadrow[state[i]] && procstack[i] != NULL) ! 2794: - retable(i, ice); ! 2795: - } ! 2796: -} ! 2797: - ! 2798: -unfreeze(ice) ! 2799: - struct FREEZE *ice; ! 2800: -{ struct CUBE *here; ! 2801: - register int i; ! 2802: - ! 2803: - lastqueue = ice->lastsav; ! 2804: - ! 2805: - for (i = 0; i < nrprocs; i++) ! 2806: - state[i] = (int) ice->statsaved[i]; ! 2807: - for (i = 0; i < nrvars; i++) ! 2808: - globvars[i] = (int) ice->varsaved[i]; ! 2809: - ! 2810: - if ((here = ice->cube) != NULL) ! 2811: - while (here->pntr != NULL) ! 2812: - here = here->pntr; ! 2813: - ! 2814: - for (; here != NULL;) ! 2815: - { i = (int) here->which; ! 2816: - if (here->poporpush == PUSH) ! 2817: - { processes[i] = ppop(i); ! 2818: - } else ! 2819: - { /* use cube to restore the values from before the ppop */ ! 2820: - ppush(i, processes[i], (int) here->transfsaved); ! 2821: - restorvarpars (here->varparsaved, i); ! 2822: - processes[i] = (int) here->procsaved; ! 2823: - efree(here->varparsaved); ! 2824: - } ! 2825: - efree(here); ! 2826: - fiddler(i); ! 2827: - ! 2828: - if (here == ice->cube) ! 2829: - break; ! 2830: - else ! 2831: - here = here->rtnp; ! 2832: - } ! 2833: - efree(ice->statsaved); ! 2834: - efree(ice->varsaved); ! 2835: -} ! 2836: - ! 2837: -FSE(I) ! 2838: -{ short g, h, i, j, k, t, x, y, z, X, Y, how; ! 2839: - char progress = 0, internal; ! 2840: - struct FREEZE *delta = (struct FREEZE *) emalloc(sizeof(struct FREEZE)); ! 2841: - struct STATE *iam = NULL, *inloop(); ! 2842: - struct VISIT *ticket; ! 2843: - ! 2844: - if (level >= maxreached) ! 2845: - { if (maxxed && level >= maxlevel) ! 2846: - { efree(delta); ! 2847: - return; ! 2848: - } ! 2849: - if (level > maxreached) ! 2850: - maxreached = level; ! 2851: - } ! 2852: - freeze(delta); ! 2853: - ! 2854: - if (muststore && (iam = inloop()) == NULL) ! 2855: - { unfreeze(delta); ! 2856: - efree(delta); ! 2857: - return; ! 2858: - } ! 2859: - ! 2860: -/* ! 2861: - * this state has not been seen before; the state ! 2862: - * information has been saved in the structure ! 2863: - * `STATE'; queue information has been saved in the ! 2864: - * last `VISIT' template of this state; ! 2865: - * we save a pointer to this template in a local variable: ! 2866: - * to be able to mark the state `analyzed' when we return ! 2867: - * for efficiency a pointer to the last visit is kept in a global `lastvisit' ! 2868: - */ ! 2869: - ticket = lastvisit; ! 2870: - level++; ! 2871: - COUNT += (double) 1; ! 2872: - ! 2873: -/* three tries: ! 2874: - * 1st try accepts internal moves (no timeouts, no outputs), ! 2875: - * 2nd try accepts any moves except timeouts, ! 2876: - * 3rd try accepts only timeouts. ! 2877: - */ ! 2878: - ! 2879: - for (X = 0; X <= 2; X++) ! 2880: - { internal = 0; ! 2881: - for (g = 0, i = I; g < nrprocs; g++, i = (i+1)%nrprocs) ! 2882: - { t = processes[i]; ! 2883: - k = state[i]; ! 2884: - ! 2885: - if (X == 0 && tbl[t].badrow[k]) ! 2886: - continue; /* first try: skip fsm without receives */ ! 2887: - ! 2888: - for (j = 0; j < tbl[t].nrcols; j++) ! 2889: - { if ((z = tbl[t].ptr[k][j].nrpils) == 0) ! 2890: - continue; ! 2891: - ! 2892: - x = lbt[i].mapcol[j]; ! 2893: - y = lbt[i].orgcol[j]; ! 2894: - Y = tbl[t].coltyp[j]; ! 2895: - ! 2896: - if (matchon(x, y, t, X, Y, i)) ! 2897: - { for (h = 0; h < z; h++) ! 2898: - { how = forward(t, k, j, h, x, y, i, Y, delta); ! 2899: - ! 2900: - if (qandirty || how == 0 || how >= LV || how == TC) ! 2901: - internal = 1; ! 2902: - ! 2903: - progress++; ! 2904: -#if DEBUG ! 2905: - printf("\tdown - %d/%d/%d\n", t, j, h); ! 2906: - showstate(); ! 2907: -#endif ! 2908: - /* FSE(mbox[lastqueue].owner); */ ! 2909: - FSE(0); ! 2910: - ! 2911: - backup(k, how, y, i, delta); ! 2912: -#if DEBUG ! 2913: - printf("\tup - %d/%d/%d\n", t, j, h); ! 2914: - showstate(); ! 2915: -#endif ! 2916: - } } /* innermost loop: non-determinism */ ! 2917: - if (blast && progress > 0) ! 2918: - break; ! 2919: - } /* inner loop: options per process */ ! 2920: - if (internal) ! 2921: - break; ! 2922: - } /* outer loop: parallelism */ ! 2923: - if (progress) ! 2924: - break; /* normal exit */ ! 2925: - } /* outermost loop: 2 trials */ ! 2926: - if (progress == 0) ! 2927: - { ! 2928: - if ((k = inendstate()) == nrprocs) ! 2929: - { normf++; ! 2930: - if (assertholds()) ! 2931: - { if (lockplus) output("endstate: ", 0); ! 2932: - } else ! 2933: - output("assertion violated: ", 0); ! 2934: - } ! 2935: - else ! 2936: - { locksf++; ! 2937: - if (k == 0) ! 2938: - output("deadlock: ", 1); ! 2939: - else ! 2940: - output("partial lock: ", 1); ! 2941: - if (linecode) ! 2942: - { printf("State at time of lock:\n"); ! 2943: - for (i = 0; i < nrprocs; i++) ! 2944: - printf("\tprocess %3d: state %s\n", i, ! 2945: - tbl[processes[i]].rowname[state[i]]); ! 2946: - putchar('\n'); ! 2947: - } } } ! 2948: - ! 2949: - level--; ! 2950: - ! 2951: - unfreeze(delta); efree(delta); ! 2952: - if (iam != NULL) ! 2953: - { mark(iam, ticket); ! 2954: - if (zapper > 0 && (progress == 0 || level >= maxlevel-3)) ! 2955: - swiffle(iam, ticket); ! 2956: - } ! 2957: -} ! 2958: - ! 2959: -forward(tb, k, j, h, m, from, pr, TT, ice) ! 2960: - struct FREEZE *ice; ! 2961: -{ int how=0, n=m; ! 2962: - struct ELM *at; ! 2963: - ! 2964: - ice->whichvar = NONE; ! 2965: - ! 2966: - at = &(tbl[tb].ptr[k][j].one[h]); ! 2967: - ! 2968: - switch (TT) { ! 2969: - case SPN: how = evalexpr(at->valtrans, pr, ice); ! 2970: - break; ! 2971: - case CND: break; /* `matchon()' already checked it */ ! 2972: - case FCT: m = (int) tbl[tb].calls[n].callwhat; ! 2973: - ppush(pr, processes[pr], (int) at->transf); ! 2974: - setpars(&(tbl[tb].calls[n]), reftasks[m], pr); ! 2975: - setlvars(reftasks[m], pr); ! 2976: - processes[pr] = reftasks[m]; ! 2977: - fiddler(pr); ! 2978: - state[pr] = 0; ! 2979: - muststore = tbl[processes[pr]].labrow[0]; ! 2980: - return TC; ! 2981: - case TMO: send(m, from, NONE, pr, at->transf); ! 2982: - receive(from, NONE, pr, ice); ! 2983: - lastqueue = (short) from; ! 2984: - how = TO; ! 2985: - break; ! 2986: - case DFL: ! 2987: - case INP: receive(from, (int) at->valtrans, pr, ice); ! 2988: - how = RO; ! 2989: - break; ! 2990: - case OUTP: send(m, from, (int) at->valtrans, pr, at->transf); ! 2991: - lastqueue = (short) from; ! 2992: - how |= SO; ! 2993: - break; ! 2994: - } ! 2995: - state[pr] = (int) at->transf; ! 2996: - muststore = tbl[processes[pr]].labrow[state[pr]]; ! 2997: - ! 2998: - return (how); ! 2999: -} ! 3000: - ! 3001: -backup(k, how, bx, i, ice) ! 3002: - struct FREEZE *ice; ! 3003: -{ int u = (int) ice->whichvar; ! 3004: - ! 3005: - if (u != NONE) ! 3006: - { if (u >= MANY) ! 3007: - procpars[i].lvarvals[u-MANY] = ice->oldvalue; ! 3008: - else ! 3009: - globvars[u] = ice->oldvalue; ! 3010: - } ! 3011: - switch (how) { ! 3012: - case TC: u = processes[i]; ! 3013: - processes[i] = ppop(i); ! 3014: - fiddler(i); ! 3015: - break; ! 3016: - case TO: unrecv(bx); ! 3017: - case SO: unsend(); ! 3018: - peekassert(ice); ! 3019: - break; ! 3020: - case SR: unsend(); ! 3021: - case RO: unrecv(bx); ! 3022: - peekassert(ice); ! 3023: - default: break; ! 3024: - } state[i] = k; ! 3025: -} ! 3026: - ! 3027: -fiddler(pr) ! 3028: -{ register int i, t = processes[pr]; ! 3029: - ! 3030: - for (i = 0; i < tbl[t].nrcols; i++) ! 3031: - if (tbl[t].colmap[i] >= MANY) ! 3032: - { lbt[pr].mapcol[i] = mapper(tbl[t].colmap[i], pr); ! 3033: - lbt[pr].orgcol[i] = whichq(lbt[pr].mapcol[i]); ! 3034: - } else ! 3035: - { lbt[pr].mapcol[i] = tbl[t].colmap[i]; ! 3036: - lbt[pr].orgcol[i] = tbl[t].colorg[i]; ! 3037: - } ! 3038: - ! 3039: -} ! 3040: //GO.SYSIN DD trace3.c ! 3041: echo trace4.c 1>&2 ! 3042: sed 's/.//' >trace4.c <<'//GO.SYSIN DD trace4.c' ! 3043: -#include <stdio.h> ! 3044: -#include "trace.h" ! 3045: -#include "trace.d" ! 3046: - ! 3047: - extern char lockplus, prefix; ! 3048: - extern struct QUEUE *s_last; ! 3049: - extern int *processes, *globvars, *state, *qsize; ! 3050: - extern int nrprocs, nrrefs, nrvars, nrqs, level, assertbl, nrtbl; ! 3051: - extern long loopsf, zapped; ! 3052: - extern struct TBL *tbl; ! 3053: - extern struct PROCSTACK **procstack; ! 3054: - extern struct VARPARS *procpars; ! 3055: - ! 3056: - short *Factor, maxr = 0; ! 3057: - double iseen=0, ireseen=0, painful=0, kurshan=0; ! 3058: - ! 3059: - struct VISIT *lastvisit; ! 3060: - struct STATE *giveme(), *setstate(); ! 3061: - char *Smalloc(), *emalloc(); ! 3062: - ! 3063: -struct STATE * ! 3064: -inloop() ! 3065: -{ struct STATE *tmp; ! 3066: - register struct VISIT *hook; ! 3067: - register int x; char aa; ! 3068: - int i, nrnonempty=0, nrnon=0; ! 3069: - short h, hashvalue(); ! 3070: - ! 3071: - for (i = 0; i < nrqs; i++) ! 3072: - if (qsize[i] > 0) ! 3073: - { nrnonempty += (1<<i); ! 3074: - nrnon++; ! 3075: - } ! 3076: - h = hashvalue(nrnonempty); ! 3077: - for (x = member(h); x > 0; x--) ! 3078: - { tmp = giveme(h, x); ! 3079: - if (samestate(tmp)) ! 3080: - { for (hook = tmp->next; hook != NULL; hook = hook->next) ! 3081: - { ! 3082: - if (hook->howmany != nrnonempty ! 3083: - || !Queuesmatch(hook, nrnon)) ! 3084: - continue; ! 3085: - ! 3086: - if (ISANA(hook)) ! 3087: - { if (DEPTH(hook) > level) ! 3088: - { painful += 1; ! 3089: - continue; ! 3090: - } ! 3091: - if (prefix) ! 3092: - output("prefix: ", 0); ! 3093: - hook->prop.countme += 1; ! 3094: - kurshan += (double) 1; ! 3095: - return NULL; ! 3096: - } else ! 3097: - { loopsf++; ! 3098: - aa = (assertbl == NONE)? 1 : assertholds(); ! 3099: - if (aa == 0 || lockplus) ! 3100: - putloop(hook->prop.s, aa); ! 3101: - return NULL; ! 3102: - } } ! 3103: - return setstate(tmp, h); ! 3104: - } ! 3105: - } ! 3106: - return setstate((struct STATE *) NULL, h); ! 3107: -} ! 3108: - ! 3109: -cmplvars(one, two) ! 3110: - struct LOCVARS *one; ! 3111: - struct VARPARS *two; ! 3112: -{ int i; ! 3113: - ! 3114: - if (one->nrlvars != two->nrlvars) ! 3115: - return 0; ! 3116: - ! 3117: - for (i = 0; i < one->nrlvars; i++) ! 3118: - if (one->lvarvals[i] != two->lvarvals[i]) ! 3119: - return 0; ! 3120: - ! 3121: - return 1; ! 3122: -} ! 3123: - ! 3124: -cmplocals(one, two) ! 3125: - struct VARPARS *one, *two; ! 3126: -{ int i; ! 3127: - ! 3128: - if (one->nrlvars != two->nrlvars) ! 3129: - return 0; ! 3130: - ! 3131: - for (i = 0; i < one->nrlvars; i++) ! 3132: - if (one->lvarvals[i] != two->lvarvals[i]) ! 3133: - return 0; ! 3134: - ! 3135: - return 1; ! 3136: -} ! 3137: - ! 3138: -cmparams(one, two) ! 3139: - struct VARPARS *one, *two; ! 3140: -{ int i; ! 3141: - ! 3142: - if (one->nrms != two->nrms || one->nrvs != two->nrvs) ! 3143: - whoops("cannot happen - cmparams"); ! 3144: - ! 3145: - for (i = 0; i < one->nrms; i++) ! 3146: - if (one->ms[i] != two->ms[i]) ! 3147: - return 0; ! 3148: - ! 3149: - for (i = 0; i < one->nrvs; i++) ! 3150: - if (one->vs[i] != two->vs[i]) ! 3151: - return 0; ! 3152: - ! 3153: - return 1; ! 3154: -} ! 3155: - ! 3156: -cmpstacks(older, newer) ! 3157: - struct PROCSTACK *older, *newer; ! 3158: -{ struct PROCSTACK *tmp1 = older; ! 3159: - struct PROCSTACK *tmp2 = newer; ! 3160: - ! 3161: - while (tmp2 != NULL) ! 3162: - { ! 3163: - if (tmp1->uptable != tmp2->uptable ! 3164: - || tmp1->uptransf != tmp2->uptransf) ! 3165: - return 0; ! 3166: - ! 3167: - if (cmplocals(tmp1->varparsaved, tmp2->varparsaved) == 0 ! 3168: - || cmparams (tmp1->varparsaved, tmp2->varparsaved) == 0) ! 3169: - return 0; ! 3170: - ! 3171: - tmp1 = tmp1->follow; ! 3172: - tmp2 = tmp2->follow; ! 3173: - } ! 3174: - return 1; ! 3175: -} ! 3176: - ! 3177: -samestate(at) ! 3178: - struct STATE *at; ! 3179: -{ ! 3180: - return (sameP(at->pstate) && sametempl(at->pcon)); ! 3181: -} ! 3182: - ! 3183: -cpylvars(into, from) ! 3184: - struct LOCVARS *into; ! 3185: - struct VARPARS *from; ! 3186: -{ register int i; ! 3187: - ! 3188: - into->nrlvars = from->nrlvars; ! 3189: - into->lvarvals = (short *) ! 3190: - Smalloc(from->nrlvars * sizeof(short)); ! 3191: - for (i = 0; i < from->nrlvars; i++) ! 3192: - into->lvarvals[i] = from->lvarvals[i]; ! 3193: -} ! 3194: - ! 3195: -cpylocals(into, from) ! 3196: - struct VARPARS *into, *from; ! 3197: -{ register int i; ! 3198: - ! 3199: - into->nrlvars = from->nrlvars; ! 3200: - into->lvarvals = (short *) ! 3201: - Smalloc(from->nrlvars * sizeof(short)); ! 3202: - for (i = 0; i < from->nrlvars; i++) ! 3203: - into->lvarvals[i] = from->lvarvals[i]; ! 3204: -} ! 3205: - ! 3206: -cpyparams(into, from) ! 3207: - struct VARPARS *into, *from; ! 3208: -{ int i; ! 3209: - ! 3210: - into->nrms = from->nrms; ! 3211: - into->ms = (short *) ! 3212: - Smalloc(from->nrms * sizeof(short)); ! 3213: - for (i = 0; i < from->nrms; i++) ! 3214: - into->ms[i] = from->ms[i]; ! 3215: - ! 3216: - into->nrvs = from->nrvs; ! 3217: - into->vs = (short *) ! 3218: - Smalloc(from->nrvs * sizeof(short)); ! 3219: - for (i = 0; i < from->nrvs; i++) ! 3220: - into->vs[i] = from->vs[i]; ! 3221: -} ! 3222: - ! 3223: -cpystacks(left, right) ! 3224: - struct PROCSTACK *left, *right; ! 3225: -{ struct PROCSTACK *into = left; ! 3226: - struct PROCSTACK *from = right; ! 3227: - ! 3228: - while (from != NULL) ! 3229: - { into->varparsaved = (struct VARPARS *) ! 3230: - Smalloc(sizeof(struct VARPARS)); ! 3231: - cpylocals(into->varparsaved, from->varparsaved); ! 3232: - cpyparams(into->varparsaved, from->varparsaved); ! 3233: - ! 3234: - into->uptable = from->uptable; ! 3235: - into->uptransf = from->uptransf; ! 3236: - ! 3237: - if ((from = from->follow) != NULL) ! 3238: - { into->follow = (struct PROCSTACK *) ! 3239: - Smalloc(sizeof(struct PROCSTACK)); ! 3240: - into = into->follow; ! 3241: - } } ! 3242: -} ! 3243: - ! 3244: -struct STATE * ! 3245: -newstate(pha) ! 3246: - int pha; ! 3247: -{ struct STATE *hook; ! 3248: - struct VISIT *findastate(); ! 3249: - struct TEMPLATE *inTtable(); ! 3250: - unsigned short *inPtable(); ! 3251: - ! 3252: - hook = (struct STATE *) Smalloc(sizeof(struct STATE)); ! 3253: - hook->pstate = inPtable(); ! 3254: - hook->pcon = inTtable(); ! 3255: - hook->next = findastate(hook); /* first visit */ ! 3256: - ! 3257: - insert(pha, hook); ! 3258: - ! 3259: - return hook; ! 3260: -} ! 3261: - ! 3262: -struct VISIT * ! 3263: -oldstate(where) ! 3264: - struct STATE *where; ! 3265: -{ register struct VISIT *tmp; ! 3266: - struct VISIT *try, *findastate(); ! 3267: - ! 3268: - ireseen += (double)1; ! 3269: - try = findastate(where); ! 3270: - ! 3271: - if (where->next == NULL) ! 3272: - where->next = try; ! 3273: - else ! 3274: - { for (tmp = where->next; tmp->next != NULL; tmp = tmp->next) ! 3275: - ; ! 3276: - tmp->next = try; ! 3277: - } ! 3278: - ! 3279: - return try; ! 3280: -} ! 3281: - ! 3282: -struct STATE * ! 3283: -setstate(where, ha) ! 3284: - struct STATE *where; ! 3285: -{ struct STATE *tmp; ! 3286: - struct VISIT *work; ! 3287: - ! 3288: - if (where == NULL) ! 3289: - { tmp = newstate(ha); ! 3290: - work = tmp->next; ! 3291: - } else ! 3292: - { tmp = where; ! 3293: - work = oldstate(where); ! 3294: - } ! 3295: - ! 3296: - work->prop.s = s_last; ! 3297: - work->depth = (short) level; ! 3298: - ! 3299: - lastvisit = work; ! 3300: - relink(work); ! 3301: - ! 3302: - return tmp; ! 3303: -} ! 3304: - ! 3305: -struct VISIT * ! 3306: -pickstate(at) ! 3307: - struct STATE *at; ! 3308: -{ struct VISIT *latter = NULL; ! 3309: - register struct VISIT *hook = at->next; ! 3310: - ! 3311: - for (hook = at->next; hook != NULL; hook = hook->next) ! 3312: - { if (ISANA(hook)) ! 3313: - { if (latter == NULL) ! 3314: - at->next = hook->next; ! 3315: - else ! 3316: - latter->next = hook->next; ! 3317: - ! 3318: - efree(hook->c); ! 3319: - hook->next = NULL; ! 3320: - zapped++; ! 3321: - ! 3322: - return hook; ! 3323: - } ! 3324: - latter = hook; ! 3325: - } ! 3326: - return NULL; ! 3327: -} ! 3328: - ! 3329: -struct VISIT * ! 3330: -picknown(at, want) ! 3331: - struct STATE *at; ! 3332: - struct VISIT *want; ! 3333: -{ struct VISIT *latter = NULL; ! 3334: - register struct VISIT *hook; ! 3335: - ! 3336: - for (hook = at->next; hook != NULL; hook = hook->next) ! 3337: - { if (hook == want) ! 3338: - break; ! 3339: - latter = hook; ! 3340: - } ! 3341: - if (hook == NULL) ! 3342: - whoops("cannot happen - picknown"); ! 3343: - ! 3344: - if (latter == NULL) ! 3345: - at->next = hook->next; ! 3346: - else ! 3347: - latter->next = hook->next; ! 3348: - ! 3349: - efree(hook->c); ! 3350: - hook->next = NULL; ! 3351: - ! 3352: - zapped++; ! 3353: - return hook; ! 3354: -} ! 3355: - ! 3356: -inihash() ! 3357: -{ register int i; ! 3358: - char *Smalloc(); ! 3359: - ! 3360: - for (i = 0; i < nrtbl; i++) ! 3361: - if (tbl[i].nrrows > maxr) ! 3362: - maxr = tbl[i].nrrows; ! 3363: - ! 3364: - Factor = (short *) ! 3365: - Smalloc(maxr * sizeof(short)); ! 3366: - ! 3367: - for (i = 0; i < maxr; i++) ! 3368: - Factor[i] = rand()%NOTOOBIG; /* number between 0 and 16k */ ! 3369: -} ! 3370: - ! 3371: -short ! 3372: -hashvalue(g) ! 3373: -{ register int i, h; ! 3374: - ! 3375: - for (i = h = 0; i < nrprocs; i++) ! 3376: - { h = ((h << 2) | (h >> 13)); /* rotate */ ! 3377: - h ^= Factor[state[i]] ^ Factor[processes[i]]; ! 3378: - } ! 3379: - h += g; ! 3380: - return (h & NOTOOBIG); ! 3381: -} ! 3382: //GO.SYSIN DD trace4.c ! 3383: echo trace5.c 1>&2 ! 3384: sed 's/.//' >trace5.c <<'//GO.SYSIN DD trace5.c' ! 3385: -#include <stdio.h> ! 3386: -#include "trace.h" ! 3387: -#include "trace.d" ! 3388: - ! 3389: - extern struct QUEUE **head, **tail; ! 3390: - extern int *qsize, nrqs, level, maxreached; ! 3391: - extern double iseen, ireseen, zapper; ! 3392: - extern double tryswiff, noswiff, cannot; ! 3393: - char *Realloc(), *Emalloc(), *Smalloc(), *emalloc(); ! 3394: - ! 3395: - struct HTABLE { ! 3396: - struct STATE **index; /* index [h] [ibound] */ ! 3397: - short ibound; /* nr of available slots */ ! 3398: - short nr; /* nr of occupied slots */ ! 3399: - } oldstates[NOTOOBIG+1]; /* index of hash values */ ! 3400: - ! 3401: - int hbound=0, hlast=0; ! 3402: - ! 3403: -growindex(h) ! 3404: -{ int nsz = (int) oldstates[h].ibound + 8; ! 3405: - ! 3406: - if (nsz == 8) ! 3407: - oldstates[h].index = (struct STATE **) ! 3408: - Emalloc(nsz * sizeof(struct STATE *)); ! 3409: - else ! 3410: - oldstates[h].index = (struct STATE **) ! 3411: - Realloc(oldstates[h].index, nsz * sizeof(struct STATE *)); ! 3412: - ! 3413: - oldstates[h].ibound = (short) nsz; ! 3414: -} ! 3415: - ! 3416: -initable() ! 3417: -{ register int i; ! 3418: - ! 3419: - for (i = 0; i < NOTOOBIG+1; i++) ! 3420: - { oldstates[i].nr = 0; ! 3421: - oldstates[i].ibound = 0; ! 3422: - } ! 3423: - hbound = NOTOOBIG+1; ! 3424: -} ! 3425: - ! 3426: -insert(h, pnt) /* enter state pointer into the table at hash value h */ ! 3427: - struct STATE *pnt; ! 3428: -{ short cin; ! 3429: - ! 3430: - if (h >= hbound) ! 3431: - { fprintf(stderr, "h %d, hbound %d, NOTOOBIG %d\n",h,hbound,NOTOOBIG); ! 3432: - whoops("cannot happen - insert"); ! 3433: - } ! 3434: - cin = oldstates[h].nr++; ! 3435: - iseen += (double) 1; ! 3436: - ! 3437: - if (cin >= oldstates[h].ibound) ! 3438: - growindex(h); ! 3439: - ! 3440: - oldstates[h].index[cin] = pnt; ! 3441: -} ! 3442: - ! 3443: -mark(stt, vis) ! 3444: - struct STATE *stt; ! 3445: - struct VISIT *vis; ! 3446: -{ ! 3447: - vis->prop.countme = 0; ! 3448: - vis->depth |= ANALYZED; ! 3449: -} ! 3450: - ! 3451: -relink(vis) ! 3452: - struct VISIT *vis; ! 3453: -{ struct CONTS *inqtable(); ! 3454: - register int i, j, k; ! 3455: - ! 3456: - for (i = j = k = 0; i < nrqs ; i++) ! 3457: - if (qsize[i] > 0) ! 3458: - { j++; ! 3459: - k += (1 << i); ! 3460: - } ! 3461: - vis->howmany = k; ! 3462: - ! 3463: - if (zapper == 0) /* grow without bound */ ! 3464: - vis->c = (struct CONTS **) ! 3465: - Smalloc(j * sizeof(struct CONTS *)); ! 3466: - else ! 3467: - vis->c = (struct CONTS **) ! 3468: - emalloc(j * sizeof(struct CONTS *)); ! 3469: - ! 3470: - for (i = k = 0; i < nrqs; i++) ! 3471: - { if (qsize[i] == 0) ! 3472: - continue; ! 3473: - ! 3474: - vis->c[k++] = inqtable(i); ! 3475: - } ! 3476: -} ! 3477: - ! 3478: -member(h) { return (h < hbound) ? oldstates[h].nr : 0; } ! 3479: - ! 3480: -struct STATE * ! 3481: -giveme(h, n) ! 3482: -{ int m = n - 1; ! 3483: - if (h >= hbound || oldstates[h].nr <= m || oldstates[h].index[m] == NULL) ! 3484: - whoops("cannot happen - giveme"); ! 3485: - ! 3486: - return oldstates[h].index[m]; ! 3487: -} ! 3488: - ! 3489: -struct VISIT * ! 3490: -findany(avoid) ! 3491: - struct STATE *avoid; ! 3492: -{ register int i, j; ! 3493: - struct VISIT *try, *pickstate(); ! 3494: - ! 3495: - for (i = (hlast+1)%hbound; i != hlast; i++, i %= hbound) ! 3496: - for (j = 0; j < oldstates[i].nr; j++) ! 3497: - if (oldstates[i].index[j] != avoid ! 3498: - && (try = pickstate(oldstates[i].index[j])) != NULL) ! 3499: - { hlast = i; ! 3500: - return try; ! 3501: - } ! 3502: - ! 3503: - cannot += (double) 1; /* couldn't find a victim */ ! 3504: - try = (struct VISIT *) Smalloc(sizeof(struct VISIT)); ! 3505: - try->next = NULL; ! 3506: - ! 3507: - return try; ! 3508: -} ! 3509: - ! 3510: -struct VISIT * ! 3511: -findastate(avoid) ! 3512: - struct STATE *avoid; ! 3513: -{ struct VISIT *try = NULL; ! 3514: - struct VISIT *findany(), *picknown(); ! 3515: - struct Swiffle *unswiffle(), *trs; ! 3516: - ! 3517: - if (ireseen < zapper || zapper == 0) ! 3518: - { try = (struct VISIT *) Smalloc(sizeof(struct VISIT)); ! 3519: - try->next = NULL; ! 3520: - return try; ! 3521: - } ! 3522: - tryswiff += (double) 1; ! 3523: - if ((trs = unswiffle(avoid)) != NULL ! 3524: - && (try = picknown(trs->st, trs->vi)) != NULL) ! 3525: - return try; ! 3526: - noswiff += (double) 1; ! 3527: - ! 3528: - return findany(avoid); ! 3529: -} ! 3530: //GO.SYSIN DD trace5.c ! 3531: echo trace6.c 1>&2 ! 3532: sed 's/.//' >trace6.c <<'//GO.SYSIN DD trace6.c' ! 3533: -#include <stdio.h> ! 3534: -#include "trace.h" ! 3535: -#include "trace.d" ! 3536: - ! 3537: - extern struct QUEUE **head, **tail; ! 3538: - extern int *qsize, nrqs, level; ! 3539: - ! 3540: - char *Realloc(), *Emalloc(), *Smalloc(); ! 3541: - ! 3542: - struct CONTS ***oldqueues; /* index of queue states */ ! 3543: - long *nrqstates, *qbound; ! 3544: - ! 3545: -iniqtable() ! 3546: -{ register int i; ! 3547: - nrqstates = (long *) ! 3548: - Smalloc(nrqs * sizeof(long)); ! 3549: - qbound = (long *) ! 3550: - Smalloc(nrqs * sizeof(long)); ! 3551: - ! 3552: - oldqueues = (struct CONTS ***) ! 3553: - Smalloc(nrqs * sizeof(struct CONTS **)); ! 3554: - ! 3555: - for (i = 0; i < nrqs; i++) ! 3556: - nrqstates[i] = qbound[i] = 0; ! 3557: -} ! 3558: - ! 3559: -growqtable(p) ! 3560: -{ int nsz = qbound[p] + 32; ! 3561: - ! 3562: - if (nsz == 32) ! 3563: - oldqueues[p] = (struct CONTS **) ! 3564: - Emalloc(nsz * sizeof(struct CONTS *)); ! 3565: - else ! 3566: - oldqueues[p] = (struct CONTS **) ! 3567: - Realloc(oldqueues[p], nsz * sizeof(struct CONTS *)); ! 3568: - ! 3569: - qbound[p] = nsz; ! 3570: -} ! 3571: - ! 3572: -struct CONTS * ! 3573: -Qinsert(p) ! 3574: -{ struct CONTS * try; ! 3575: - struct QUEUE * tmp; ! 3576: - register int i, j; ! 3577: - ! 3578: - i = p; ! 3579: - j = qsize[p]; ! 3580: - ! 3581: - if (nrqstates[p] >= qbound[p]) ! 3582: - growqtable(p); ! 3583: - ! 3584: - try = (struct CONTS *) ! 3585: - Smalloc((j+1) * sizeof(struct CONTS)); ! 3586: - ! 3587: - try[0].mesg = i; ! 3588: - try[0].cargo = j; ! 3589: - ! 3590: - for (tmp = head[i], j = 1; tmp != tail[i]; tmp = tmp->next, j++) ! 3591: - { try[j].mesg = (tmp->mesg & ~PASSED); ! 3592: - try[j].cargo = tmp->cargo; ! 3593: - } ! 3594: - ! 3595: - if (--j != qsize[p]) ! 3596: - whoops("cannot happen - Qinsert"); ! 3597: - ! 3598: - oldqueues[p][nrqstates[p]] = try; ! 3599: - nrqstates[p] += 1; ! 3600: - ! 3601: - return try; ! 3602: -} ! 3603: - ! 3604: -struct CONTS * ! 3605: -inqtable(p) ! 3606: -{ register int i; ! 3607: - ! 3608: - if (qsize[p] == 0) ! 3609: - whoops("cannot happen - inqtable"); ! 3610: - ! 3611: - for (i = 0; i < nrqstates[p]; i++) ! 3612: - if (samequeue(oldqueues[p][i])) ! 3613: - return oldqueues[p][i]; ! 3614: - ! 3615: - return Qinsert(p); ! 3616: -} ! 3617: - ! 3618: -samequeue(at) ! 3619: - struct CONTS *at; ! 3620: -{ ! 3621: - register struct QUEUE *tmp; ! 3622: - register int j, k, m; ! 3623: - ! 3624: - k = at[0].mesg; /* which queue is this */ ! 3625: - m = at[0].cargo; /* how many elements are here */ ! 3626: - ! 3627: - if (qsize[k] != m) ! 3628: - return 0; ! 3629: - ! 3630: - for (tmp = head[k], j = 1; tmp != tail[k]; tmp = tmp->next, j++) ! 3631: - { if (at[j].mesg != (tmp->mesg & ~PASSED) ! 3632: - || at[j].cargo != tmp->cargo) ! 3633: - return 0; ! 3634: - } ! 3635: - return 1; ! 3636: -} ! 3637: - ! 3638: -Queuesmatch(vis, k) ! 3639: - struct VISIT *vis; ! 3640: - register int k; ! 3641: -{ ! 3642: - register int i; ! 3643: - ! 3644: - for (i = 0; i < k; i++) ! 3645: - if (samequeue(vis->c[i]) == 0) ! 3646: - return 0; ! 3647: - return 1; ! 3648: -} ! 3649: //GO.SYSIN DD trace6.c ! 3650: echo trace7.c 1>&2 ! 3651: sed 's/.//' >trace7.c <<'//GO.SYSIN DD trace7.c' ! 3652: -#include <stdio.h> ! 3653: -#include "trace.h" ! 3654: -#include "trace.d" ! 3655: - ! 3656: -struct Swiffle *slist, *slast, *flast; ! 3657: -int nswiff = 0, fswiff = 0; ! 3658: - ! 3659: -struct Swiffle * ! 3660: -unswiffle(avoid) ! 3661: - struct STATE *avoid; ! 3662: -{ ! 3663: - register struct Swiffle *try; ! 3664: - register int i; ! 3665: - struct Swiffle *result = (struct Swiffle *) NULL; ! 3666: - ! 3667: - for (i = nswiff, try = slist; i > 0; i--, try = try->next) ! 3668: - if (try->st != avoid) ! 3669: - { result = try; ! 3670: - getput(try, i); ! 3671: - break; ! 3672: - } ! 3673: - ! 3674: - return result; ! 3675: -} ! 3676: - ! 3677: -swiffle(this, that) ! 3678: - struct STATE *this; ! 3679: - struct VISIT *that; ! 3680: -{ ! 3681: - struct Swiffle *getswiff(), *try; ! 3682: - ! 3683: - try = getswiff(); ! 3684: - try->st = this; ! 3685: - try->vi = that; ! 3686: - ! 3687: - if (nswiff++ == 0) ! 3688: - slist = try; ! 3689: - else ! 3690: - { slast->next = try; ! 3691: - try->last = slast; ! 3692: - } ! 3693: - slast = try; ! 3694: -} ! 3695: - ! 3696: -getput(try, n) ! 3697: - struct Swiffle *try; ! 3698: -{ ! 3699: -/* unlink from slist: */ ! 3700: - if (try == slist) ! 3701: - slist = try->next; ! 3702: - else ! 3703: - try->last->next = try->next; ! 3704: - ! 3705: - if (n > 1) ! 3706: - try->next->last = try->last; ! 3707: - ! 3708: - if (try == slast) ! 3709: - { if (try == slist) ! 3710: - slast = (struct Swiffle *) NULL; ! 3711: - else ! 3712: - slast = try->last; ! 3713: - } ! 3714: - nswiff--; ! 3715: - ! 3716: -/* relink in flist: */ ! 3717: - ! 3718: - try->next = (struct Swiffle *) NULL; ! 3719: - ! 3720: - if (fswiff++ == 0) ! 3721: - try->last = (struct Swiffle *) NULL; ! 3722: - else ! 3723: - { flast->next = try; ! 3724: - try->last = flast; ! 3725: - } ! 3726: - flast = try; ! 3727: -} ! 3728: - ! 3729: -struct Swiffle * ! 3730: -getswiff() ! 3731: -{ struct Swiffle *try; ! 3732: - char *Smalloc(); ! 3733: - ! 3734: - if (fswiff == 0) ! 3735: - try = (struct Swiffle *) Smalloc(sizeof(struct Swiffle)); ! 3736: - else ! 3737: - { fswiff--; ! 3738: - try = flast; ! 3739: - if ((flast = try->last) != NULL) ! 3740: - flast->next = (struct Swiffle *) NULL; ! 3741: - } ! 3742: - try->next = try->last = (struct Swiffle *) NULL; ! 3743: - ! 3744: - return try; ! 3745: -} ! 3746: //GO.SYSIN DD trace7.c ! 3747: echo trace8.c 1>&2 ! 3748: sed 's/.//' >trace8.c <<'//GO.SYSIN DD trace8.c' ! 3749: -#include <stdio.h> ! 3750: -#include "trace.h" ! 3751: -#include "trace.d" ! 3752: - ! 3753: - extern int *globvars; ! 3754: - extern int nrprocs, nrrefs, nrvars; ! 3755: - extern struct PROCSTACK **procstack; ! 3756: - extern struct VARPARS *procpars; ! 3757: - ! 3758: - char *Realloc(), *Emalloc(), *Smalloc(); ! 3759: - ! 3760: - struct TEMPLATE **templates; ! 3761: - int nrtemplates = 0, tbound = 0; ! 3762: - ! 3763: -growttable() ! 3764: -{ int nsz = tbound + 32; ! 3765: - ! 3766: - if (nsz == 32) ! 3767: - templates = (struct TEMPLATE **) ! 3768: - Emalloc(nsz * sizeof(struct TEMPLATE *)); ! 3769: - else ! 3770: - templates = (struct TEMPLATE **) ! 3771: - Realloc(templates, nsz * sizeof(struct TEMPLATE *)); ! 3772: - ! 3773: - tbound = nsz; ! 3774: - ! 3775: -} ! 3776: - ! 3777: -struct TEMPLATE * ! 3778: -Tinsert() ! 3779: -{ struct TEMPLATE *try; ! 3780: - register int i; ! 3781: - ! 3782: - if (nrtemplates >= tbound) ! 3783: - growttable(); ! 3784: - ! 3785: - try = (struct TEMPLATE *) ! 3786: - Smalloc(sizeof(struct TEMPLATE)); ! 3787: - try->l_vars = (struct LOCVARS **) ! 3788: - Smalloc(nrprocs * sizeof(struct LOCVARS *)); ! 3789: - try->g_vars = (short *) ! 3790: - Smalloc(nrvars * sizeof(short)); ! 3791: - ! 3792: - for (i = 0; i < nrvars; i++) ! 3793: - try->g_vars[i] = (short) globvars[i]; ! 3794: - ! 3795: - if (nrrefs > 0) ! 3796: - try->traceback = (struct PROCSTACK **) ! 3797: - Smalloc(nrprocs * sizeof(struct PROCSTACK *)); ! 3798: - ! 3799: - for (i = 0; i < nrprocs; i++) ! 3800: - { try->l_vars[i] = (struct LOCVARS *) ! 3801: - Smalloc(sizeof(struct LOCVARS)); ! 3802: - ! 3803: - cpylvars(try->l_vars[i], &(procpars[i])); ! 3804: - ! 3805: - if (nrrefs > 0) ! 3806: - { if (procstack[i] == NULL) ! 3807: - { try->traceback[i] = NULL; ! 3808: - continue; ! 3809: - } ! 3810: - try->traceback[i] = (struct PROCSTACK *) ! 3811: - Smalloc(sizeof(struct PROCSTACK)); ! 3812: - cpystacks(try->traceback[i], procstack[i]); ! 3813: - } } ! 3814: - ! 3815: - templates[nrtemplates] = try; ! 3816: - nrtemplates++; ! 3817: - ! 3818: - return try; ! 3819: -} ! 3820: - ! 3821: -struct TEMPLATE * ! 3822: -inTtable() ! 3823: -{ register int i; ! 3824: - ! 3825: - for (i = 0; i < nrtemplates; i++) ! 3826: - if (sametempl(templates[i])) ! 3827: - return templates[i]; ! 3828: - ! 3829: - return Tinsert(); ! 3830: -} ! 3831: - ! 3832: -sametempl(at) ! 3833: - struct TEMPLATE *at; ! 3834: -{ register int i; ! 3835: - ! 3836: - for (i = 0; i < nrprocs; i++) ! 3837: - { if (cmplvars(at->l_vars[i], &(procpars[i])) == 0 || ! 3838: - (nrrefs > 0 && cmpstacks(at->traceback[i], procstack[i]) == 0)) ! 3839: - return 0; ! 3840: - } ! 3841: - ! 3842: - for (i = 0; i < nrvars; i++) ! 3843: - if (at->g_vars[i] != (short) globvars[i]) ! 3844: - return 0; ! 3845: - ! 3846: - return 1; ! 3847: -} ! 3848: //GO.SYSIN DD trace8.c ! 3849: echo trace9.c 1>&2 ! 3850: sed 's/.//' >trace9.c <<'//GO.SYSIN DD trace9.c' ! 3851: -#include <stdio.h> ! 3852: -#include "trace.h" ! 3853: -#include "trace.d" ! 3854: - ! 3855: - extern int nrprocs, *processes, *state; ! 3856: - ! 3857: - char *Realloc(), *Emalloc(), *Smalloc(); ! 3858: - ! 3859: - unsigned short **pstates; ! 3860: - int pgrowth = 32; ! 3861: - int nrpstates = 0; ! 3862: - int pbound = 0; ! 3863: - ! 3864: -growPtable() ! 3865: -{ int p = pbound + pgrowth; ! 3866: - ! 3867: - if (p == pgrowth) ! 3868: - pstates = (unsigned short **) ! 3869: - Emalloc(p * sizeof(unsigned short *)); ! 3870: - else ! 3871: - pstates = (unsigned short **) ! 3872: - Realloc(pstates, p * sizeof(unsigned short *)); ! 3873: - pbound = p; ! 3874: -} ! 3875: - ! 3876: -unsigned short * ! 3877: -Pinsert() ! 3878: -{ unsigned short *try; ! 3879: - register int i; ! 3880: - ! 3881: - if (nrpstates >= pbound) ! 3882: - growPtable(); ! 3883: - ! 3884: - try = (unsigned short *) ! 3885: - Smalloc(nrprocs * sizeof(unsigned short)); ! 3886: - ! 3887: - for (i = 0; i < nrprocs; i++) ! 3888: - try[i] = (unsigned short) (state[i] + (processes[i]<<10)); ! 3889: - ! 3890: - pstates[nrpstates++] = try; ! 3891: - ! 3892: - return try; ! 3893: -} ! 3894: - ! 3895: -unsigned short * ! 3896: -inPtable() ! 3897: -{ register int i; ! 3898: - ! 3899: - for (i = 0; i < nrpstates; i++) ! 3900: - if (sameP(pstates[i])) ! 3901: - return pstates[i]; ! 3902: - ! 3903: - return Pinsert(); ! 3904: -} ! 3905: - ! 3906: -sameP(at) ! 3907: - unsigned short *at; ! 3908: -{ register int i; ! 3909: - ! 3910: - for (i = 0; i < nrprocs; i++) ! 3911: - { if ((at[i]&1023) != (unsigned short) state[i] ! 3912: - || at[i]>>10 != (unsigned short) processes[i]) ! 3913: - return 0; ! 3914: - } ! 3915: - return 1; ! 3916: -} ! 3917: //GO.SYSIN DD trace9.c
This archive runs on limited infrastructure. Preserving old code on modern bandwidth. Automated agents are requested to crawl responsibly.