/***** spin: pangen1.h *****/ /* Copyright (c) 1991 by AT&T Bell Telephone Laboratories, Inc. * All Rights Reserved. This software is for educational purposes only. * No part of this source code may be reproduced in any form * without explicit written permission from the copyright owner. * This software was written by Gerard J. Holzmann, as part of the book * ``Design and Validation of Computer Protocols,'' ISBN 0-13-539925-4, * Prentice Hall, Englewood Cliffs, NJ, 07632. * Send bug-reports to: gerard@research.att.com */ char *Header[] = { "#define qptr(x) (((uchar *)&now)+q_offset[x])", "#define pptr(x) (((uchar *)&now)+proc_offset[x])", "#define Pptr(x) ((proc_offset[x])?pptr(x):noptr)", "#define q_sz(x) (((Q0 *)qptr(x))->Qlen)\n", "#define MAXQ 255", "#define MAXPROC 255", "#define WS sizeof(long) /* word size in bytes */", "#ifndef VECTORSZ", "#define VECTORSZ 1024 /* sv size in bytes */", "#endif", "extern char *malloc(), *memcpy(), *memset();", "extern void exit();", "extern int abort();\n", "typedef struct Stack { /* for queues and processes */", " short o_delta;", " short o_offset;", " short o_delqs;", " char *body;", " struct Stack *nxt;", " struct Stack *lst;", "} Stack;\n", "typedef struct Svtack { /* for complete state vector */", " short o_delta; /* current size of frame */", " short m_delta; /* maximum size of frame */", "#if SYNC", " short o_boq;", "#endif", " int j1, j2; /* loop detection */", " char *body;", " struct Svtack *nxt;", " struct Svtack *lst;", "} Svtack;\n", "typedef struct Trans {", " short atom; /* is this an atomic transition */", " short st; /* the nextstate */", " short ist; /* intermediate state */", " int forw; /* index for forward transition */", " int back; /* index for return transition */", " struct Trans *nxt;", "} Trans;\n", "Trans ***trans; /* 1 ptr per state per proctype */\n", "int proc_offset[MAXPROC];", "int q_offset[MAXQ];", "int depthfound = -1; /* loop detection */", "short vsize; /* vector size in bytes */", "short boq = -1; /* blocked_on_queue status */", "typedef struct State {", " uchar _nr_pr;", " uchar _nr_qs;", " uchar _p_t; /* loop detection */", 0, }; char *Addp0[] = { /* addproc(....parlist... */ ")", "{", " int j, h = now._nr_pr;", " if (h >= MAXPROC)", " Uerror(\"too many processes\");", " switch (n) {", " case 0: j = sizeof(P0); break;", 0, }; char *Addp1[] = { " default: Uerror(\"bad proc - addproc\");", " }", " if (vsize%%WS && (j > WS-(vsize%%WS)))", " vsize += WS-(vsize%%WS);", " proc_offset[h] = vsize;", " now._nr_pr += 1;", " vsize += j;", " hmax = max(hmax, vsize);", " if (vsize >= VECTORSZ)", " Uerror(\"VECTORSZ is too small, edit pan.h\");", " memset((char *)pptr(h), 0, j);", " switch (n) {", 0, }; char *Addq0[] = { "addqueue(n)", "{ int j=0, i = now._nr_qs;", " if (i >= MAXQ)", " Uerror(\"too many queues\");", " switch (n) {", 0, }; char *Addq1[] = { " case -1: printf(\"queue was deleted\\n\");", " default: Uerror(\"bad queue - addqueue\");", " }", " if (vsize%%WS && (j > WS-(vsize%%WS)))", " vsize += WS-(vsize%%WS);", " q_offset[i] = vsize;", " now._nr_qs += 1;", " vsize += j;", " hmax = max(hmax, vsize);", " if (vsize >= VECTORSZ)", " Uerror(\"VECTORSZ is too small, edit pan.h\");", " memset((char *)qptr(i), 0, j);", " ((Q0 *)qptr(i))->_t = n;", " return i;", "}\n", 0, }; char *Addq11[] = { "{ int j; uchar *z;\n", " if (into >= now._nr_qs || into < 0)", " Uerror(\"qsend bad queue#\");", " z = qptr(into);", " switch (((Q0 *)qptr(into))->_t) {", 0, }; char *Addq2[] = { " case -1: printf(\"queue was deleted\\n\");", " default: Uerror(\"bad queue - qsend\");", " }", "}\n", "#if SYNC", "q_zero(from)", "{", " switch(((Q0 *)qptr(from))->_t) {", 0, }; char *Addq3[] = { " case -1: printf(\"queue was deleted\\n\");", " }", " Uerror(\"bad queue q-zero\");", "}", "#endif", "q_full(from)", "{", " switch(((Q0 *)qptr(from))->_t) {", 0, }; char *Addq4[] = { " case -1: printf(\"queue was deleted\\n\");", " }", " Uerror(\"bad queue - q_full\");", "}\n", "qrecv(from, slot, fld, done)", "{ uchar *z;", " int j, k, r=0;", " if (from >= now._nr_qs || from < 0)", " Uerror(\"qrecv bad queue#\");", " z = qptr(from);", " switch (((Q0 *)qptr(from))->_t) {", 0, }; char *Addq5[] = { " case -1: printf(\"queue was deleted\\n\");", " default: Uerror(\"bad queue - qrecv\");", " }", " return r;", "}\n", 0, }; char *Code0[] = { "run()", "{ memset((char *)&now, 0, sizeof(State));", " vsize = sizeof(State) - VECTORSZ;", " settable();", 0, }; char *Code1[] = { "#define CONNECT %d /* accept labels */", 0, }; char *Code2[] = { " UnBlock; /* disable rendez-vous */", "#ifdef BITSTATE", " SS = (uchar *) emalloc(1<<(ssize-3));", " if (loops)", " LL = (uchar *) emalloc(1<<(ssize-3));", "#if CONNECT>0", " printf(\"warning: acceptance labels are\");", " printf(\" ignored in bit-state mode\\n\");", "#endif", "#else", " hinit();", "#endif", " stack = ( Stack *) emalloc(sizeof(Stack));", " svtack = (Svtack *) emalloc(sizeof(Svtack));", " /* a place to point for Pptr of non-running procs: */", " noptr = (uchar *) emalloc(Maxbody * sizeof(char));", " addproc(0); /* init */", " depth=mreached=0;", " trpt = &trail[depth];", " new_state();", "}\n", "new_state()", "{ register Trans *t;", " char n, m, ot;", " short II, tt;\n", " short From = now._nr_pr-1;", " short To = 0;", "Down:", " if (now._p_t && prognow()) /* loop detection */", " goto Up;", " if (depth >= maxdepth)", " { truncs++;", "#if SYNC", " (trpt+1)->o_n = 1; /* not a deadlock */", "#endif", " goto Up;", " }", "#if CONNECT>0", "#ifndef BITSTATE", " trpt->parent = 0;", "#endif", "#endif", "#ifdef VERI", " if (!(trpt->tau&4)) /* if no claim move */", "#endif", " if (!(trpt->tau&8)) /* if no atomic move */", " {", "#ifdef BITSTATE", " d_hash((uchar *) &now, vsize);", " j3 = (1<<(J1&7)); j1 = J1>>3;", " j4 = (1<<(J2&7)); j2 = J2>>3;", " if ((SS[j2]&j3) && (SS[j1]&j4))", "#else", " if (hstore((char *)&now, vsize))", "#endif", " { truncs++;", "#ifdef BITSTATE", " if (loops && now._p_t", " && LL[j1] && LL[j2] && onstack())", " uerror(\"non-progress cycle\");", "#else", "#if CONNECT>0", " setparent((char *)&now, vsize);", "#endif", "#endif", "#if SYNC", "/* mid rendezvous */ if (boq != -1 && !(((trpt-1)->tau)&1))", " (trpt+1)->o_m = 1; /* not stuck */", "#endif", " goto Up;", " }", "#ifdef BITSTATE", " SS[j2] |= j3; SS[j1] |= j4;", " if (loops)", " { sv_save();", " LL[j1]++; LL[j2]++;", " svtack->j1 = J1;", " svtack->j2 = J2;", " }", "#else", "#if CONNECT>0", " setparent((char *)&now, vsize);", "#endif", "#endif", " nstates++;", " }", " if (depth > mreached)", " mreached = depth;", " trpt->tau &= ~1; n = 0;", "#if SYNC", " (trpt+1)->o_n = 0;", "#endif", "#ifdef VERI", " if (now._nr_pr < 2", " || ((P0 *)pptr(1))->_p == endclaim)", " uerror(\"claim violated!\");", " if (trpt->tau&4) /* must make a claimmove */", " { II = 1;", " goto Veri0;", " }", "#endif", "\nAgain:", " for (II = From; II >= To; II -= 1)", " {", "#ifdef VERI", " if (II == 1) continue;", "#endif", "Veri0: this = pptr(II);", " tt = (short) ((P0 *)this)->_p;", " ot = (uchar) ((P0 *)this)->_t;", " for (t = trans[ot][tt]; t; t = t->nxt)", " {", "#include \"pan.m\"", "P999: /* jumps here when move succeeds */", " depth++; trpt++;", " trpt->pr = II;", " trpt->st = tt;", " if (t->st)", " { ((P0 *)this)->_p = t->st;", " reached[ot][t->st] = 1;", " }", " trpt->o_t = t; trpt->o_n = n;", " trpt->o_ot = ot; trpt->o_tt = tt;", " trpt->o_To = To; trpt->o_m = m;", " if (t->atom&2)", " { From = To = II; nlinks++;", " trpt->tau |= 8;", "#ifdef VERI", " trpt->tau = (trpt-1)->tau&4;", " } else", " { if ((trpt-1)->tau&4)", " trpt->tau = 0;", " else", " trpt->tau = 4;", "#else", " } else", " { trpt->tau &= ~8;", "#endif", " From = now._nr_pr-1; To = 0;", " }", " goto Down; /* pseudo-recursion */", "Up:", " t = trpt->o_t; n = trpt->o_n;", " ot = trpt->o_ot; II = trpt->pr;", " tt = trpt->o_tt; this = pptr(II);", " To = trpt->o_To; m = trpt->o_m;", "#ifdef VERI", "#if SYNC", "/* preserve rendez-vous completion status: */", "/* if the next level was a claim, copy through */", " if (trpt->tau&4)", " trpt->o_n = (trpt+1)->o_n;", "#endif", "#endif", "#include \"pan.b\"", "R999: /* jumps here when done */", " depth--; trpt--;", " if (m>n||(n>3&&m!=0)) n=m;", " ((P0 *)this)->_p = tt;", " } /* all options */", "#ifdef VERI", " if (II == 1) break;", "#endif", " } /* all processes */", " if (n == 0)", " {", "#ifdef VERI", " if (trpt->tau&4) /* claim blocks = ok */", " goto Done;", "#endif", "#if SYNC", " if (boq == -1)", "#endif", " if (!endstate() && now._nr_pr ", " && depth < maxdepth-1)", " { if (!((trpt->tau)&1)) /* timeout */", " { trpt->tau |= 1;", " goto Again;", " }", "#ifdef VERI", " if (n >= 0) goto Done; /* always */", "#else", " if (loops) goto Done; /* do loop det. only */", "#endif", " if (!(trpt->tau&8)) /* no atomic move */", " uerror(\"invalid endstate\");", " else", " Uerror(\"atomic seq blocks\");", " }", " }", "Done:", " if (loops && !(trpt->tau&8))", "#ifdef VERI", " if (!(trpt->tau&4))", "#endif", "#ifdef BITSTATE", " { LL[(svtack->j1)>>3]--;", " LL[(svtack->j2)>>3]--;", " svtack = svtack->lst;", " }", "#else", " htag((char *)&now, vsize);", "#endif", "#if CONNECT>0", "#ifndef BITSTATE", " checkaccept();", "#endif", "#endif", " if (depth > 0) goto Up;", "}\n", "assert(a, s, ii, tt, t)", " char *s;", " Trans *t;", "{ if (!a)", " { printf(\"assertion violated %%s\", s);", " depth++; trpt++;", " trpt->pr = ii;", " trpt->st = tt;", " trpt->o_t = t;", " uerror(\"aborted\");", " depth--; trpt--;", " }", "}\n", "#ifdef MEMCNT", "int memcnt=0;", "#endif", "void", "wrapup()", "{", "#ifdef BITSTATE", " double a, b;\n", " printf(\"bit statespace search \");", "#else", " printf(\"full statespace search \");", "#endif", "#ifdef VERI", " printf(\"on behavior restricted to claim \");", "#endif", " printf(\"for:\\n\tassertion violations\");", "#ifndef VERI", " if (loops)", " printf(\" and non-progress loops\");", " else", " printf(\" and invalid endstates\");", "#endif", "#if CONNECT>0", " printf(\"\\n\\tand absence of acceptance labels\");", " printf(\" in all cycles\");", "#endif", " if (!done) printf(\"\\nsearch was not completed\");", " printf(\"\\nvector %%d byte, depth reached %%d\", ", " hmax, mreached);", " if (loops)", " printf(\", non-progress loops: %%d\\n\", errors);", " else", " printf(\", errors: %%d\\n\", errors);", " printf(\"%%8d states, stored\\n\", nstates);", " printf(\"%%8d states, linked\\n\", nlinks);", " printf(\"%%8d states, matched\t total: %%8d\\n\",", " truncs, nstates+nlinks+truncs);", "#ifdef BITSTATE", " a = (double) (1<100)\\n\");", "#else", " printf(\"hash conflicts: %%d (resolved)\\n\", hcmp);", "#endif", " printf(\"(max size 2^%%d states, \", ssize);", " printf(\"stackframes: %%d/%%d)\\n\\n\", smax, svmax);", "#ifdef MEMCNT", " printf(\"memory used: %%d\\n\", memcnt);", "#endif", " if (done && !loops) do_reach();", " exit(0);", "}\n", "d_hash(cp, om)", " uchar *cp;", "{", " register long z = 0x88888EEFL;", " register long *q, *r;", " register int h;", " register m, n;\n", " h = (om+3)/4;", " m = n = -1;", " q = r = (long *) cp;", " r += (long) h;", " do {", " m += m;", " if (m < 0)", " m ^= z;", " m ^= *q++;", " n += n;", " if (n < 0)", " n ^= z;", " n ^= *--r;", " } while (--h > 0);", " J1 = (m ^ (m>>(8*sizeof(unsigned)-ssize)))&mask;", " J2 = (n ^ (n>>(8*sizeof(unsigned)-ssize)))&mask;", "}\n", "s_hash(cp, om)", " uchar *cp;", "{", " register long z = 0x88888EEFL;", " register long *q;", " register int h;\n", " register m = -1;", " h = (om+3)/4;", " q = (long *) cp;", " do {", " m += m;", " if (m < 0)", " m ^= z;", " m ^= *q++;", " } while (--h > 0);", " j1 = (m ^ (m>>(8*sizeof(unsigned)-ssize)))&mask;", "}\n", "main(argc, argv)", " char *argv[];", "{", " while (argc > 1 && argv[1][0] == '-')", " { switch (argv[1][1]) {", " case 'c': upto = atoi(&argv[1][2]); break;", "#ifndef VERI", " case 'l': loops = 1; break;", "#endif", " case 'm': maxdepth = atoi(&argv[1][2]); break;", " case 'w': ssize = atoi(&argv[1][2]); break;", " default : usage(); exit(1);", " }", " argc--; argv++;", " }", " signal(SIGINT, wrapup);", " mask = ((1< 1< 2) q -= 2;", " }", "#else", " { if (q == 1) continue;", " if (q > 1) q--;", " }", "#endif", " if (trail[i].o_t->ist)", " { sprintf(snap, \"%%d:%%d:%%d:%%d\\n\", j++,", " q, trail[i].o_t->ist, i);", " write(fd, snap, strlen(snap));", " }", " sprintf(snap, \"%%d:%%d:%%d:%%d\\n\", j++, ", " q, trail[i].o_t->st, i);", " write(fd, snap, strlen(snap));", " }", " printf(\"pan: wrote pan.trail\\n\");", " close(fd);", "}\n", "sv_save() /* push state vector onto save stack */", "{ if (!svtack->nxt)", " { svtack->nxt = (Svtack *) emalloc(sizeof(Svtack));", " svtack->nxt->body = emalloc(vsize*sizeof(char));", " svtack->nxt->lst = svtack;", " svtack->nxt->m_delta = vsize;", " svmax++;", " } else if (vsize > svtack->nxt->m_delta)", " { svtack->nxt->body = emalloc(vsize*sizeof(char));", " svtack->nxt->lst = svtack;", " svtack->nxt->m_delta = vsize;", " svmax++;", " }", " svtack = svtack->nxt;", "#if SYNC", " svtack->o_boq = boq;", "#endif", " svtack->o_delta = vsize;", " memcpy((char *)(svtack->body), (char *)&now, vsize);", "}\n", "sv_restor() /* pop state vector from save stack */", "{ memcpy((char *)&now, svtack->body, svtack->o_delta);", "#if SYNC", " boq = svtack->o_boq;", "#endif", " if (vsize != svtack->o_delta)", " Uerror(\"sv_restor\");", " if (!svtack->lst)", " Uerror(\"error: v_restor\");", " svtack = svtack->lst;", "}\n", "p_restor(h)", "{ int i; char *z = (char *) &now;", " proc_offset[h] = stack->o_offset;", " memcpy(z+vsize, stack->body, stack->o_delta);", " vsize += stack->o_delta;", " i = stack->o_delqs;", " now._nr_pr += 1;", " if (!stack->lst) /* debugging */", " Uerror(\"error: p_restor\");", " stack = stack->lst;", " this = pptr(h);", " while (i-- > 0)", " q_restor();", "}\n", "q_restor()", "{ char *z = (char *) &now;", " q_offset[now._nr_qs] = stack->o_offset;", " memcpy(z+vsize, stack->body, stack->o_delta);", " vsize += stack->o_delta;", " now._nr_qs += 1;", " if (!stack->lst) /* debugging */", " Uerror(\"error: q_restor\");", " stack = stack->lst;", "}\n", "delproc(sav, h)", "{ int d, i=0;", "", " if (h+1 != now._nr_pr) return 0;", "", " while (now._nr_qs", " && q_offset[now._nr_qs-1] > proc_offset[h])", " { delq(sav);", " i++;", " }", " d = vsize - proc_offset[h];", " if (sav)", " { if (!stack->nxt)", " { stack->nxt = (Stack *)", " emalloc(sizeof(Stack));", " stack->nxt->body = ", " emalloc(Maxbody*sizeof(char));", " stack->nxt->lst = stack;", " smax++;", " }", " stack = stack->nxt;", " stack->o_offset = proc_offset[h];", " stack->o_delta = d;", " stack->o_delqs = i;", " memcpy(stack->body, (char *)pptr(h), d);", " }", " vsize = proc_offset[h];", " now._nr_pr = now._nr_pr - 1;", " memset((char *)pptr(h), 0, d);", " return 1;", "}\n", "delq(sav)", "{ int h = now._nr_qs - 1;", " int d = vsize - q_offset[now._nr_qs - 1];", " if (sav)", " { if (!stack->nxt)", " { stack->nxt = (Stack *)", " emalloc(sizeof(Stack));", " stack->nxt->body = ", " emalloc(Maxbody*sizeof(char));", " stack->nxt->lst = stack;", " smax++;", " }", " stack = stack->nxt;", " stack->o_offset = q_offset[h];", " stack->o_delta = d;", " memcpy(stack->body, (char *)qptr(h), d);", " }", " vsize = q_offset[h];", " now._nr_qs = now._nr_qs - 1;", " memset((char *)qptr(h), 0, d);", "}\n", "prognow()", "{", " int i; P0 *ptr;", " for (i = 0; i < now._nr_pr; i++)", " { ptr = (P0 *) pptr(i);", " if (progstate[ptr->_t][ptr->_p])", " return 1;", " }", " return 0;", "}\n", "endstate()", "{ int i; P0 *ptr;", " for (i = 0; i < now._nr_pr; i++)", " {", "#ifdef VERI", " if (i == 1) continue;", "#endif", " ptr = (P0 *) pptr(i);", " if (!stopstate[ptr->_t][ptr->_p])", " return 0;", " }", " if (loops)", " uerror(\"non progress sequence\");", " return 1;", "}\n", "onstack()", "{ register Svtack *ptr;", " register char *won = (char *)&now;", " register int j=depth;", " for (ptr = svtack; ptr; ptr = ptr->lst, j--)", " if (ptr->o_delta == vsize", " && ptr->j1 == J1 && ptr->j2 == J2", " && memcmp(ptr->body, won, vsize) == 0)", " { depthfound = j;", " return 1;", " }", " return 0;", "}\n", "#ifndef BITSTATE", "#if CONNECT>0", "struct H_succ {", " struct H_el *succ; /* a successor state */", " Trans *how; /* how you get there */", " int who; /* who got us there */", " struct H_succ *nsucc; /* linked list, if >1 */", "};", "#endif", "struct H_el {", " struct H_el *nxt;", "#if CONNECT>0", " struct H_succ *slst; /* list of successors */", "#endif", " unsigned tagged;", /* bit 30 used in CONNECT mode */ " unsigned state;", "} **H_tab;\n", "hinit()", "{ H_tab = (struct H_el **)", " emalloc((1<0", "setparent(v, n)", " char *v;", "{", " register struct H_el *tmp;", " struct H_succ *yy;", " struct Trail *TR;", " s_hash(v, n);", " for (tmp = H_tab[j1]; tmp; tmp = tmp->nxt)", " { if (memcmp(((char *)&(tmp->state)), v, n) == 0)", " { trpt->parent = tmp;", " /* next: enlist as a child */", " for (TR = trpt-1; !TR->parent; TR--)", " if (TR < trail) return;", " yy = (struct H_succ *)", " emalloc(sizeof(struct H_succ));", " yy->succ = tmp;", " yy->how = (TR+1)->o_t;", " yy->who = (TR+1)->pr;", " yy->nsucc = TR->parent->slst;", " TR->parent->slst = yy;", " return;", " }", " }", " Uerror(\"cannot happen, setparent\");", "}\n", "struct H_el *acc_root;", "checkaccept()", "{ int i; P0 *ptr;", " if (trpt->parent)", " for (i = 0; i < now._nr_pr; i++)", " { ptr = (P0 *) pptr(i);", " if (accpstate[ptr->_t][ptr->_p])", " { acc_root = trpt->parent;", " depthfound = depth;", " dfs_acc(acc_root);", " depthfound = -1;", " break;", " } }", "}\n", "int maxl=0;", "dfs_acc(acc) /* is `acc' part of a cycle? */", " struct H_el *acc;", "{ /* tag all non-tagged successors */", " struct H_succ *zz;", " maxl++;", " for (zz = acc->slst; zz; zz = zz->nsucc)", " if (!(zz->succ->tagged & (1<<30)))", " { zz->succ->tagged |= (1<<30);", " if (zz->succ == acc_root)", " { printf(\"cycle of length \");", " printf(\"%%d (%%d) %%d\\n\",", " maxl, depthfound, depth);", " uerror(\"accept state in cycle\");", " } else", " { trpt++; depth++;", " trpt->pr = zz->who;", " trpt->o_t = zz->how;", " dfs_acc(zz->succ);", " trpt--; depth--;", " } }", " maxl--;", "}", "#endif\n", "htag(v, n)", " char *v;", " short n;", "{", " register struct H_el *tmp;", " s_hash(v, n);", " for (tmp = H_tab[j1]; tmp; tmp = tmp->nxt)", " { if (memcmp(((char *)&(tmp->state)), v, n) == 0)", " { tmp->tagged &= (1<<30);", " return;", " }", " }", " Uerror(\"cannot happen, htag\");", "}\n", "hstore(v, n)", " char *v;", " short n;", "{", " register struct H_el *tmp;\n", " s_hash((uchar *)v, n);", " tmp = H_tab[j1];", " if (!tmp)", " { tmp = (struct H_el *)", " emalloc(sizeof(struct H_el)+n-sizeof(unsigned));", " H_tab[j1] = tmp;", " } else", " { for (;; hcmp++)", " { if (memcmp(&(tmp->state), v, n) == 0)", " { if (loops && now._p_t", " && (tmp->tagged & ~(1<<30)))", " { depthfound = tmp->tagged&~(1<<30);", " uerror(\"non-progress cycle\");", " }", " return 1;", " }", " if (!tmp->nxt) break;", " tmp = tmp->nxt;", " }", " tmp->nxt = (struct H_el *)", " emalloc(sizeof(struct H_el)+n-sizeof(unsigned));", " tmp = tmp->nxt;", " }", " tmp->tagged = depth+1; /* non-zero while on stack */", " memcpy(((char *)&(tmp->state)), v, n);", " return 0;", "}", "#endif", "#include \"pan.t\"", "", "do_reach()", "{", 0, };