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