1 /***** spin: mesg.c *****/ 2 3 /* Copyright (c) 1991,1995 by AT&T Corporation. All Rights Reserved. */ 4 /* 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.att.com */ 12 13 #include "spin.h" 14 #include "y.tab.h" 15 16 #define MAXQ 2500 /* default max # queues */ 17 18 extern RunList *X; 19 extern Symbol *Fname; 20 extern int verbose, TstOnly, s_trail; 21 extern int lineno, depth, xspin, m_loss; 22 23 Queue *qtab = (Queue *) 0; /* linked list of queues */ 24 Queue *ltab[MAXQ]; /* linear list of queues */ 25 int nqs=0; 26 27 int 28 cnt_mpars(Lextok *n) 29 { Lextok *m; 30 int i=0; 31 32 for (m = n; m; m = m->rgt) 33 i += Cnt_flds(m); 34 return i; 35 } 36 37 int 38 qmake(Symbol *s) 39 { Lextok *m; 40 Queue *q; 41 int i; extern int analyze; 42 43 if (!s->ini) 44 return 0; 45 46 if (nqs >= MAXQ) 47 { lineno = s->ini->ln; 48 Fname = s->ini->fn; 49 fatal("too many queues (%s)", s->name); 50 } 51 52 if (s->ini->ntyp != CHAN) 53 return eval(s->ini); 54 55 q = (Queue *) emalloc(sizeof(Queue)); 56 q->qid = ++nqs; 57 q->nslots = s->ini->val; 58 q->nflds = cnt_mpars(s->ini->rgt); 59 q->setat = depth; 60 61 i = max(1, q->nslots); /* 0-slot qs get 1 slot minimum */ 62 63 q->contents = (int *) emalloc(q->nflds*i*sizeof(int)); 64 q->fld_width = (int *) emalloc(q->nflds*sizeof(int)); 65 66 for (m = s->ini->rgt, i = 0; m; m = m->rgt) 67 { if (m->sym && m->ntyp == STRUCT) 68 i = Width_set(q->fld_width, i, getuname(m->sym)); 69 else 70 q->fld_width[i++] = m->ntyp; 71 } 72 q->nxt = qtab; 73 qtab = q; 74 ltab[q->qid-1] = q; 75 76 return q->qid; 77 } 78 79 int 80 qfull(Lextok *n) 81 { int whichq = eval(n->lft)-1; 82 83 if (whichq < MAXQ && whichq >= 0 && ltab[whichq]) 84 return (ltab[whichq]->qlen >= ltab[whichq]->nslots); 85 return 0; 86 } 87 88 int 89 qlen(Lextok *n) 90 { int whichq = eval(n->lft)-1; 91 92 if (whichq < MAXQ && whichq >= 0 && ltab[whichq]) 93 return ltab[whichq]->qlen; 94 return 0; 95 } 96 97 int 98 q_is_sync(Lextok *n) 99 { int whichq = eval(n->lft)-1; 100 101 if (whichq < MAXQ && whichq >= 0 && ltab[whichq]) 102 return (ltab[whichq]->nslots == 0); 103 return 0; 104 } 105 106 int 107 qsend(Lextok *n) 108 { int whichq = eval(n->lft)-1; 109 110 if (whichq == -1) 111 { printf("Error: sending to an uninitialized chan\n"); 112 whichq = 0; 113 return 0; 114 } 115 if (whichq < MAXQ && whichq >= 0 && ltab[whichq]) 116 { ltab[whichq]->setat = depth; 117 if (ltab[whichq]->nslots > 0) 118 return a_snd(ltab[whichq], n); 119 else 120 return s_snd(ltab[whichq], n); 121 } 122 return 0; 123 } 124 125 int 126 qrecv(Lextok *n, int full) 127 { int whichq = eval(n->lft)-1; 128 129 if (whichq == -1) 130 { printf("Error: receiving from an uninitialized chan\n"); 131 whichq = 0; 132 return 0; 133 } 134 if (whichq < MAXQ && whichq >= 0 && ltab[whichq]) 135 { ltab[whichq]->setat = depth; 136 return a_rcv(ltab[whichq], n, full); 137 } 138 return 0; 139 } 140 141 int 142 sa_snd(Queue *q, Lextok *n) /* sorted asynchronous */ 143 { Lextok *m; 144 int i, j, k; 145 int New, Old; 146 147 for (i = 0; i < q->qlen; i++) 148 for (j = 0, m = n->rgt; m && j < q->nflds; m = m->rgt, j++) 149 { New = cast_val(q->fld_width[j], eval(m->lft)); 150 Old = q->contents[i*q->nflds+j]; 151 if (New == Old) continue; 152 if (New > Old) break; /* inner loop */ 153 if (New < Old) goto found; 154 } 155 found: 156 for (j = q->qlen-1; j >= i; j--) 157 for (k = 0; k < q->nflds; k++) 158 { q->contents[(j+1)*q->nflds+k] = 159 q->contents[j*q->nflds+k]; /* shift up */ 160 } 161 return i*q->nflds; /* new q offset */ 162 } 163 164 void 165 typ_ck(int ft, int at, char *s) 166 { 167 if (verbose&32 && ft != at 168 && (ft == CHAN || at == CHAN)) 169 { char buf[128], tag1[32], tag2[32]; 170 (void) sputtype(tag1, ft); 171 (void) sputtype(tag2, at); 172 sprintf(buf, "type-clash in %s, (%s<-> %s)", s, tag1, tag2); 173 non_fatal("%s", buf); 174 } 175 } 176 177 int 178 a_snd(Queue *q, Lextok *n) 179 { Lextok *m; 180 int i = q->qlen*q->nflds; /* q offset */ 181 int j = 0; /* q field# */ 182 183 if (q->nslots > 0 && q->qlen >= q->nslots) 184 return m_loss; /* q is full */ 185 186 if (TstOnly) return 1; 187 188 if (n->val) i = sa_snd(q, n); /* sorted insert */ 189 190 for (m = n->rgt; m && j < q->nflds; m = m->rgt, j++) 191 { int New = eval(m->lft); 192 q->contents[i+j] = cast_val(q->fld_width[j], New); 193 if (verbose&16) 194 sr_talk(n, New, "Send ", "->", j, q); 195 typ_ck(q->fld_width[j], Sym_typ(m->lft), "send"); 196 } 197 if (verbose&16) 198 { for (i = j; i < q->nflds; i++) 199 sr_talk(n, 0, "Send ", "->", i, q); 200 if (j < q->nflds) 201 printf("\twarning: missing params in send\n"); 202 if (m) 203 printf("\twarning: too many params in send\n"); 204 } 205 q->qlen++; 206 return 1; 207 } 208 209 int 210 a_rcv(Queue *q, Lextok *n, int full) 211 { Lextok *m; 212 int i=0, j, k; 213 extern int Rvous; 214 215 if (q->qlen == 0) return 0; /* q is empty */ 216 try_slot: 217 /* test executability */ 218 for (m = n->rgt, j=0; m && j < q->nflds; m = m->rgt, j++) 219 if (m->lft->ntyp == CONST 220 && q->contents[i*q->nflds+j] != m->lft->val) 221 { if (n->val == 0 /* fifo recv */ 222 || ++i >= q->qlen) /* last slot */ 223 return 0; /* no match */ 224 goto try_slot; 225 } 226 227 if (TstOnly) return 1; 228 229 if (verbose&8) 230 { if (j < q->nflds) 231 printf("\twarning: missing params in next recv\n"); 232 else if (m) 233 printf("\twarning: too many params in next recv\n"); 234 } 235 236 /* set the fields */ 237 for (m = n->rgt, j = 0; j < q->nflds; m = (m)?m->rgt:m, j++) 238 { if (verbose&8 && !Rvous) 239 sr_talk(n, q->contents[i*q->nflds+j], 240 (full)?"Recv ":"[Recv] ", "<-", j, q); 241 242 if (m && m->lft->ntyp != CONST) 243 { (void) setval(m->lft, q->contents[i*q->nflds+j]); 244 typ_ck(q->fld_width[j], Sym_typ(m->lft), "recv"); 245 } 246 for (k = i; full && k < q->qlen-1; k++) 247 q->contents[k*q->nflds+j] = 248 q->contents[(k+1)*q->nflds+j]; 249 } 250 if (full) q->qlen--; 251 return 1; 252 } 253 254 int 255 s_snd(Queue *q, Lextok *n) 256 { Lextok *m; 257 RunList *rX, *sX = X; /* rX=recvr, sX=sendr */ 258 int i, j = 0; /* q field# */ 259 260 for (m = n->rgt; m && j < q->nflds; m = m->rgt, j++) 261 { q->contents[j] = cast_val(q->fld_width[j], eval(m->lft)); 262 typ_ck(q->fld_width[j], Sym_typ(m->lft), "rv-send"); 263 } 264 q->qlen = 1; 265 if (!complete_rendez()) 266 { q->qlen = 0; 267 return 0; 268 } 269 if (TstOnly) return 1; 270 if (verbose&16) 271 { m = n->rgt; 272 rX = X; X = sX; 273 for (j = 0; m && j < q->nflds; m = m->rgt, j++) 274 sr_talk(n, eval(m->lft), "Sent ", "->", j, q); 275 for (i = j; i < q->nflds; i++) 276 sr_talk(n, 0, "Sent ", "->", i, q); 277 if (j < q->nflds) 278 printf("\twarning: missing params in rv-send\n"); 279 else if (m) 280 printf("\twarning: too many params in rv-send\n"); 281 X = rX; 282 m = n->rgt; 283 if (!s_trail) 284 for (j = 0; m && j < q->nflds; m = m->rgt, j++) 285 sr_talk(n, eval(m->lft), "Recv ", "<-", j, q); 286 } 287 return 1; 288 } 289 290 void 291 sr_talk(Lextok *n, int v, char *tr, char *a, int j, Queue *q) 292 { char s[64]; 293 if (xspin) 294 { if (verbose&4) 295 sprintf(s, "(state -)\t[values: %d", 296 eval(n->lft)); 297 else 298 sprintf(s, "(state -)\t[%d", eval(n->lft)); 299 if (strncmp(tr, "Sen", 3) == 0) 300 strcat(s, "!"); 301 else 302 strcat(s, "?"); 303 } else 304 { strcpy(s, tr); 305 } 306 if (j == 0) 307 { whoruns(1); 308 printf("line %3d %s %s", 309 n->ln, n->fn->name, s); 310 } else 311 printf(","); 312 sr_mesg(v, q->fld_width[j] == MTYPE); 313 314 if (j == q->nflds - 1) 315 { if (xspin) 316 { printf("]\n"); 317 if (!(verbose&4)) printf("\n"); 318 return; 319 } 320 printf("\t%s queue %d (", a, eval(n->lft)); 321 if (n->sym->type == CHAN) 322 printf("%s", n->sym->name); 323 else if (n->sym->type == NAME) 324 printf("%s", lookup(n->sym->name)->name); 325 else if (n->sym->type == STRUCT) 326 { Symbol *r = n->sym; 327 if (r->context) 328 r = findloc(r); 329 ini_struct(r); 330 printf("%s", r->name); 331 struct_name(n->lft, r, 1); 332 } else 333 printf("-"); 334 if (n->lft->lft) 335 printf("[%d]", eval(n->lft->lft)); 336 printf(")\n"); 337 } 338 fflush(stdout); 339 } 340 341 void 342 sr_mesg(int v, int j) 343 { extern Lextok *Mtype; 344 int cnt = 1; 345 Lextok *n; 346 347 for (n = Mtype; n && j; n = n->rgt, cnt++) 348 if (cnt == v) 349 { printf("%s", n->lft->sym->name); 350 return; 351 } 352 printf("%d", v); 353 } 354 355 void 356 doq(Symbol *s, int n, RunList *r) 357 { Queue *q; 358 int j, k; 359 360 if (!s->val) /* uninitialized queue */ 361 return; 362 for (q = qtab; q; q = q->nxt) 363 if (q->qid == s->val[n]) 364 { if (xspin > 0 365 && (verbose&4) 366 && q->setat < depth) 367 continue; 368 if (q->nslots == 0) 369 continue; /* rv q always empty */ 370 printf("\t\tqueue %d (", q->qid); 371 if (r) 372 printf("%s(%d):", r->n->name, r->pid); 373 if (s->nel != 1) 374 printf("%s[%d]): ", s->name, n); 375 else 376 printf("%s): ", s->name); 377 for (k = 0; k < q->qlen; k++) 378 { printf("["); 379 for (j = 0; j < q->nflds; j++) 380 { if (j > 0) printf(","); 381 sr_mesg(q->contents[k*q->nflds+j], 382 q->fld_width[j] == MTYPE); 383 } 384 printf("]"); 385 } 386 printf("\n"); 387 break; 388 } 389 } 390