1 /***** spin: guided.c *****/ 2 3 /* Copyright (c) 1991-2000 by Lucent Technologies - Bell Laboratories */ 4 /* All Rights Reserved. This software is for educational purposes only. */ 5 /* Permission is given to distribute this code provided that this intro- */ 6 /* ductory message is not removed and no monies are exchanged. */ 7 /* No guarantee is expressed or implied by the distribution of this code. */ 8 /* Software written by Gerard J. Holzmann as part of the book: */ 9 /* `Design and Validation of Computer Protocols,' ISBN 0-13-539925-4, */ 10 /* Prentice Hall, Englewood Cliffs, NJ, 07632. */ 11 /* Send bug-reports and/or questions to: gerard@research.bell-labs.com */ 12 13 #include "spin.h" 14 #include <sys/types.h> 15 #include <sys/stat.h> 16 #ifdef PC 17 #include "y_tab.h" 18 #else 19 #include "y.tab.h" 20 #endif 21 22 extern RunList *run, *X; 23 extern Element *Al_El; 24 extern Symbol *Fname, *oFname; 25 extern int verbose, lineno, xspin, jumpsteps, depth, merger; 26 extern int nproc, nstop, Tval, Rvous, m_loss, ntrail, columns; 27 extern short Have_claim, Skip_claim; 28 extern void ana_src(int, int); 29 30 int TstOnly = 0, pno; 31 32 static int lastclaim = -1; 33 static FILE *fd; 34 static void lost_trail(void); 35 36 static void 37 whichproc(int p) 38 { RunList *oX; 39 40 for (oX = run; oX; oX = oX->nxt) 41 if (oX->pid == p) 42 { printf("(%s) ", oX->n->name); 43 break; 44 } 45 } 46 47 static int 48 newer(char *f1, char *f2) 49 { struct stat x, y; 50 51 if (stat(f1, (struct stat *)&x) < 0) return 0; 52 if (stat(f2, (struct stat *)&y) < 0) return 1; 53 if (x.st_mtime < y.st_mtime) return 0; 54 55 return 1; 56 } 57 58 void 59 hookup(void) 60 { Element *e; 61 62 for (e = Al_El; e; e = e->Nxt) 63 if (e->n && e->n->ntyp == ATOMIC 64 || e->n && e->n->ntyp == NON_ATOMIC 65 || e->n && e->n->ntyp == D_STEP) 66 (void) huntstart(e); 67 } 68 69 void 70 match_trail(void) 71 { int i, a, nst; 72 Element *dothis; 73 RunList *oX; 74 char snap[256]; 75 76 if (ntrail) 77 sprintf(snap, "%s%d.trail", oFname->name, ntrail); 78 else 79 sprintf(snap, "%s.trail", oFname->name); 80 if (!(fd = fopen(snap, "r"))) 81 { snap[strlen(snap)-2] = '\0'; /* .tra on some pc's */ 82 if (!(fd = fopen(snap, "r"))) 83 { printf("spin: cannot find trail file\n"); 84 alldone(1); 85 } } 86 87 if (xspin == 0 && newer(oFname->name, snap)) 88 printf("spin: warning, \"%s\" is newer than %s\n", 89 oFname->name, snap); 90 91 Tval = m_loss = 1; /* timeouts and losses may be part of trail */ 92 93 hookup(); 94 95 while (fscanf(fd, "%d:%d:%d\n", &depth, &pno, &nst) == 3) 96 { if (depth == -2) { start_claim(pno); continue; } 97 if (depth == -4) { merger = 1; ana_src(0, 1); continue; } 98 if (depth == -1) 99 { if (verbose) 100 { if (columns == 2) 101 dotag(stdout, " CYCLE>\n"); 102 else 103 dotag(stdout, "<<<<<START OF CYCLE>>>>>\n"); 104 } 105 continue; 106 } 107 if (Skip_claim && pno == 0) continue; 108 109 for (dothis = Al_El; dothis; dothis = dothis->Nxt) 110 { if (dothis->Seqno == nst) 111 break; 112 } 113 if (!dothis) 114 { printf("%3d: proc %d, no matching stmnt %d\n", 115 depth, pno, nst); 116 lost_trail(); 117 } 118 i = nproc - nstop + Skip_claim; 119 if (dothis->n->ntyp == '@') 120 { if (pno == i-1) 121 { run = run->nxt; 122 nstop++; 123 if (verbose&4) 124 { if (columns == 2) 125 { dotag(stdout, "<end>\n"); 126 continue; 127 } 128 printf("%3d: proc %d terminates\n", 129 depth, pno); 130 } 131 continue; 132 } 133 if (pno <= 1) continue; /* init dies before never */ 134 printf("%3d: stop error, ", depth); 135 printf("proc %d (i=%d) trans %d, %c\n", 136 pno, i, nst, dothis->n->ntyp); 137 lost_trail(); 138 } 139 for (X = run; X; X = X->nxt) 140 { if (--i == pno) 141 break; 142 } 143 if (!X) 144 { printf("%3d: no process %d ", depth, pno); 145 printf("(state %d)\n", nst); 146 lost_trail(); 147 } 148 X->pc = dothis; 149 lineno = dothis->n->ln; 150 Fname = dothis->n->fn; 151 oX = X; /* a rendezvous could change it */ 152 if (dothis->n->ntyp == D_STEP) 153 { Element *g, *og = dothis; 154 do { 155 g = eval_sub(og); 156 if (g && depth >= jumpsteps 157 && ((verbose&32) || (verbose&4))) 158 { if (columns != 2) 159 { p_talk(og, 1); 160 161 if (og->n->ntyp == D_STEP) 162 og = og->n->sl->this->frst; 163 164 printf("\t["); 165 comment(stdout, og->n, 0); 166 printf("]\n"); 167 } 168 if (verbose&1) dumpglobals(); 169 if (verbose&2) dumplocal(X); 170 if (xspin) printf("\n"); 171 } 172 og = g; 173 } while (g && g != dothis->nxt); 174 X->pc = g?huntele(g, 0):g; 175 } else 176 { 177 keepgoing: X->pc = eval_sub(dothis); 178 X->pc = huntele(X->pc, 0); 179 if (dothis->merge_start) 180 a = dothis->merge_start; 181 else 182 a = dothis->merge; 183 184 if (depth >= jumpsteps 185 && ((verbose&32) || (verbose&4))) 186 { if (columns != 2) 187 { p_talk(dothis, 1); 188 189 if (dothis->n->ntyp == D_STEP) 190 dothis = dothis->n->sl->this->frst; 191 192 printf("\t["); 193 comment(stdout, dothis->n, 0); 194 printf("]"); 195 if (a && (verbose&32)) 196 printf("\t<merge %d now @%d>", 197 dothis->merge, 198 X->pc?X->pc->seqno:-1); 199 printf("\n"); 200 } 201 if (verbose&1) dumpglobals(); 202 if (verbose&2) dumplocal(X); 203 if (xspin) printf("\n"); 204 } 205 if (a && X->pc && X->pc->seqno != a) 206 { dothis = X->pc; 207 goto keepgoing; 208 } 209 } 210 211 if (Have_claim && X && X->pid == 0 212 && dothis && dothis->n 213 && lastclaim != dothis->n->ln) 214 { lastclaim = dothis->n->ln; 215 if (columns == 2) 216 { char t[128]; 217 sprintf(t, "#%d", lastclaim); 218 pstext(0, t); 219 } else 220 { 221 printf("Never claim moves to line %d\t[", lastclaim); 222 comment(stdout, dothis->n, 0); 223 printf("]\n"); 224 } 225 } } 226 printf("spin: trail ends after %d steps\n", depth); 227 wrapup(0); 228 } 229 230 static void 231 lost_trail(void) 232 { int d, p, n, l; 233 234 while (fscanf(fd, "%d:%d:%d:%d\n", &d, &p, &n, &l) == 4) 235 { printf("step %d: proc %d ", d, p); whichproc(p); 236 printf("(state %d) - d %d\n", n, l); 237 } 238 wrapup(1); /* no return */ 239 } 240 241 int 242 pc_value(Lextok *n) 243 { int i = nproc - nstop; 244 int pid = eval(n); 245 RunList *Y; 246 247 for (Y = run; Y; Y = Y->nxt) 248 { if (--i == pid) 249 return Y->pc->seqno; 250 } 251 return 0; 252 } 253