1 /***** spin: mesg.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 #ifdef PC 15 #include "y_tab.h" 16 #else 17 #include "y.tab.h" 18 #endif 19 20 #define MAXQ 2500 /* default max # queues */ 21 22 extern RunList *X; 23 extern Symbol *Fname; 24 extern Lextok *Mtype; 25 extern int verbose, TstOnly, s_trail, analyze, columns; 26 extern int lineno, depth, xspin, m_loss, jumpsteps; 27 extern int nproc, nstop; 28 extern short Have_claim; 29 30 Queue *qtab = (Queue *) 0; /* linked list of queues */ 31 Queue *ltab[MAXQ]; /* linear list of queues */ 32 int nqs = 0, firstrow = 1; 33 char Buf[4096]; 34 35 static Lextok *n_rem = (Lextok *) 0; 36 static Queue *q_rem = (Queue *) 0; 37 38 static int a_rcv(Queue *, Lextok *, int); 39 static int a_snd(Queue *, Lextok *); 40 static int sa_snd(Queue *, Lextok *); 41 static int s_snd(Queue *, Lextok *); 42 extern void sr_buf(int, int); 43 extern void sr_mesg(FILE *, int, int); 44 extern void putarrow(int, int); 45 static void sr_talk(Lextok *, int, char *, char *, int, Queue *); 46 47 int 48 cnt_mpars(Lextok *n) 49 { Lextok *m; 50 int i=0; 51 52 for (m = n; m; m = m->rgt) 53 i += Cnt_flds(m); 54 return i; 55 } 56 57 int 58 qmake(Symbol *s) 59 { Lextok *m; 60 Queue *q; 61 int i; extern int analyze; 62 63 if (!s->ini) 64 return 0; 65 66 if (nqs >= MAXQ) 67 { lineno = s->ini->ln; 68 Fname = s->ini->fn; 69 fatal("too many queues (%s)", s->name); 70 } 71 if (analyze && nqs >= 255) 72 { fatal("too many channel types", (char *)0); 73 } 74 75 if (s->ini->ntyp != CHAN) 76 return eval(s->ini); 77 78 q = (Queue *) emalloc(sizeof(Queue)); 79 q->qid = ++nqs; 80 q->nslots = s->ini->val; 81 q->nflds = cnt_mpars(s->ini->rgt); 82 q->setat = depth; 83 84 i = max(1, q->nslots); /* 0-slot qs get 1 slot minimum */ 85 86 q->contents = (int *) emalloc(q->nflds*i*sizeof(int)); 87 q->fld_width = (int *) emalloc(q->nflds*sizeof(int)); 88 q->stepnr = (int *) emalloc(i*sizeof(int)); 89 90 for (m = s->ini->rgt, i = 0; m; m = m->rgt) 91 { if (m->sym && m->ntyp == STRUCT) 92 i = Width_set(q->fld_width, i, getuname(m->sym)); 93 else 94 q->fld_width[i++] = m->ntyp; 95 } 96 q->nxt = qtab; 97 qtab = q; 98 ltab[q->qid-1] = q; 99 100 return q->qid; 101 } 102 103 int 104 qfull(Lextok *n) 105 { int whichq = eval(n->lft)-1; 106 107 if (whichq < MAXQ && whichq >= 0 && ltab[whichq]) 108 return (ltab[whichq]->qlen >= ltab[whichq]->nslots); 109 return 0; 110 } 111 112 int 113 qlen(Lextok *n) 114 { int whichq = eval(n->lft)-1; 115 116 if (whichq < MAXQ && whichq >= 0 && ltab[whichq]) 117 return ltab[whichq]->qlen; 118 return 0; 119 } 120 121 int 122 q_is_sync(Lextok *n) 123 { int whichq = eval(n->lft)-1; 124 125 if (whichq < MAXQ && whichq >= 0 && ltab[whichq]) 126 return (ltab[whichq]->nslots == 0); 127 return 0; 128 } 129 130 int 131 qsend(Lextok *n) 132 { int whichq = eval(n->lft)-1; 133 134 if (whichq == -1) 135 { printf("Error: sending to an uninitialized chan\n"); 136 whichq = 0; 137 return 0; 138 } 139 if (whichq < MAXQ && whichq >= 0 && ltab[whichq]) 140 { ltab[whichq]->setat = depth; 141 if (ltab[whichq]->nslots > 0) 142 return a_snd(ltab[whichq], n); 143 else 144 return s_snd(ltab[whichq], n); 145 } 146 return 0; 147 } 148 149 int 150 qrecv(Lextok *n, int full) 151 { int whichq = eval(n->lft)-1; 152 153 if (whichq == -1) 154 { if (n->sym && !strcmp(n->sym->name, "STDIN")) 155 { Lextok *m; 156 157 if (TstOnly) return 1; 158 159 for (m = n->rgt; m; m = m->rgt) 160 if (m->lft->ntyp != CONST && m->lft->ntyp != EVAL) 161 { int c = getchar(); 162 (void) setval(m->lft, c); 163 } else 164 fatal("invalid use of STDIN", (char *)0); 165 166 whichq = 0; 167 return 1; 168 } 169 printf("Error: receiving from an uninitialized chan %s\n", 170 n->sym?n->sym->name:""); 171 whichq = 0; 172 return 0; 173 } 174 if (whichq < MAXQ && whichq >= 0 && ltab[whichq]) 175 { ltab[whichq]->setat = depth; 176 return a_rcv(ltab[whichq], n, full); 177 } 178 return 0; 179 } 180 181 static int 182 sa_snd(Queue *q, Lextok *n) /* sorted asynchronous */ 183 { Lextok *m; 184 int i, j, k; 185 int New, Old; 186 187 for (i = 0; i < q->qlen; i++) 188 for (j = 0, m = n->rgt; m && j < q->nflds; m = m->rgt, j++) 189 { New = cast_val(q->fld_width[j], eval(m->lft), 0); 190 Old = q->contents[i*q->nflds+j]; 191 if (New == Old) continue; 192 if (New > Old) break; /* inner loop */ 193 if (New < Old) goto found; 194 } 195 found: 196 for (j = q->qlen-1; j >= i; j--) 197 for (k = 0; k < q->nflds; k++) 198 { q->contents[(j+1)*q->nflds+k] = 199 q->contents[j*q->nflds+k]; /* shift up */ 200 if (k == 0) 201 q->stepnr[j+1] = q->stepnr[j]; 202 } 203 return i*q->nflds; /* new q offset */ 204 } 205 206 void 207 typ_ck(int ft, int at, char *s) 208 { 209 if ((verbose&32) && ft != at 210 && (ft == CHAN || at == CHAN)) 211 { char buf[128], tag1[64], tag2[64]; 212 (void) sputtype(tag1, ft); 213 (void) sputtype(tag2, at); 214 sprintf(buf, "type-clash in %s, (%s<-> %s)", s, tag1, tag2); 215 non_fatal("%s", buf); 216 } 217 } 218 219 static int 220 a_snd(Queue *q, Lextok *n) 221 { Lextok *m; 222 int i = q->qlen*q->nflds; /* q offset */ 223 int j = 0; /* q field# */ 224 225 if (q->nslots > 0 && q->qlen >= q->nslots) 226 return m_loss; /* q is full */ 227 228 if (TstOnly) return 1; 229 230 if (n->val) i = sa_snd(q, n); /* sorted insert */ 231 232 q->stepnr[i/q->nflds] = depth; 233 234 for (m = n->rgt; m && j < q->nflds; m = m->rgt, j++) 235 { int New = eval(m->lft); 236 q->contents[i+j] = cast_val(q->fld_width[j], New, 0); 237 if ((verbose&16) && depth >= jumpsteps) 238 sr_talk(n, New, "Send ", "->", j, q); 239 typ_ck(q->fld_width[j], Sym_typ(m->lft), "send"); 240 } 241 if ((verbose&16) && depth >= jumpsteps) 242 { for (i = j; i < q->nflds; i++) 243 sr_talk(n, 0, "Send ", "->", i, q); 244 if (j < q->nflds) 245 printf("%3d: warning: missing params in send\n", 246 depth); 247 if (m) 248 printf("%3d: warning: too many params in send\n", 249 depth); 250 } 251 q->qlen++; 252 return 1; 253 } 254 255 static int 256 a_rcv(Queue *q, Lextok *n, int full) 257 { Lextok *m; 258 int i=0, oi, j, k; 259 extern int Rvous; 260 261 if (q->qlen == 0) 262 return 0; /* q is empty */ 263 try_slot: 264 /* test executability */ 265 for (m = n->rgt, j=0; m && j < q->nflds; m = m->rgt, j++) 266 if ((m->lft->ntyp == CONST 267 && q->contents[i*q->nflds+j] != m->lft->val) 268 || (m->lft->ntyp == EVAL 269 && q->contents[i*q->nflds+j] != eval(m->lft->lft))) 270 { if (n->val == 0 /* fifo recv */ 271 || n->val == 2 /* fifo poll */ 272 || ++i >= q->qlen) /* last slot */ 273 return 0; /* no match */ 274 goto try_slot; 275 } 276 if (TstOnly) return 1; 277 278 if (verbose&8) 279 { if (j < q->nflds) 280 printf("%3d: warning: missing params in next recv\n", 281 depth); 282 else if (m) 283 printf("%3d: warning: too many params in next recv\n", 284 depth); 285 } 286 287 /* set the fields */ 288 if (Rvous) 289 { n_rem = n; 290 q_rem = q; 291 } 292 293 oi = q->stepnr[i]; 294 for (m = n->rgt, j = 0; m && j < q->nflds; m = m->rgt, j++) 295 { if (columns && !full) /* was columns == 1 */ 296 continue; 297 if ((verbose&8) && !Rvous && depth >= jumpsteps) 298 { sr_talk(n, q->contents[i*q->nflds+j], 299 (full && n->val < 2)?"Recv ":"[Recv] ", "<-", j, q); 300 } 301 if (!full) 302 continue; /* test */ 303 if (m && m->lft->ntyp != CONST && m->lft->ntyp != EVAL) 304 { (void) setval(m->lft, q->contents[i*q->nflds+j]); 305 typ_ck(q->fld_width[j], Sym_typ(m->lft), "recv"); 306 } 307 if (n->val < 2) /* not a poll */ 308 for (k = i; k < q->qlen-1; k++) 309 { q->contents[k*q->nflds+j] = 310 q->contents[(k+1)*q->nflds+j]; 311 if (j == 0) 312 q->stepnr[k] = q->stepnr[k+1]; 313 } 314 } 315 316 if ((!columns || full) 317 && (verbose&8) && !Rvous && depth >= jumpsteps) 318 for (i = j; i < q->nflds; i++) 319 { sr_talk(n, 0, 320 (full && n->val < 2)?"Recv ":"[Recv] ", "<-", i, q); 321 } 322 if (columns == 2 && full && !Rvous && depth >= jumpsteps) 323 putarrow(oi, depth); 324 325 if (full && n->val < 2) 326 q->qlen--; 327 return 1; 328 } 329 330 static int 331 s_snd(Queue *q, Lextok *n) 332 { Lextok *m; 333 RunList *rX, *sX = X; /* rX=recvr, sX=sendr */ 334 int i, j = 0; /* q field# */ 335 336 for (m = n->rgt; m && j < q->nflds; m = m->rgt, j++) 337 { q->contents[j] = cast_val(q->fld_width[j], eval(m->lft), 0); 338 typ_ck(q->fld_width[j], Sym_typ(m->lft), "rv-send"); 339 } 340 q->qlen = 1; 341 if (!complete_rendez()) 342 { q->qlen = 0; 343 return 0; 344 } 345 if (TstOnly) 346 { q->qlen = 0; 347 return 1; 348 } 349 q->stepnr[0] = depth; 350 if ((verbose&16) && depth >= jumpsteps) 351 { m = n->rgt; 352 rX = X; X = sX; 353 for (j = 0; m && j < q->nflds; m = m->rgt, j++) 354 sr_talk(n, eval(m->lft), "Sent ", "->", j, q); 355 for (i = j; i < q->nflds; i++) 356 sr_talk(n, 0, "Sent ", "->", i, q); 357 if (j < q->nflds) 358 printf("%3d: warning: missing params in rv-send\n", 359 depth); 360 else if (m) 361 printf("%3d: warning: too many params in rv-send\n", 362 depth); 363 X = rX; /* restore receiver's context */ 364 if (!s_trail) 365 { if (!n_rem || !q_rem) 366 fatal("cannot happen, s_snd", (char *) 0); 367 m = n_rem->rgt; 368 for (j = 0; m && j < q->nflds; m = m->rgt, j++) 369 { if (m->lft->ntyp != NAME 370 || strcmp(m->lft->sym->name, "_") != 0) 371 i = eval(m->lft); 372 else i = 0; 373 sr_talk(n_rem,i,"Recv ","<-",j,q_rem); 374 } 375 for (i = j; i < q->nflds; i++) 376 sr_talk(n_rem, 0, "Recv ", "<-", j, q_rem); 377 if (columns == 2) 378 putarrow(depth, depth); 379 } 380 n_rem = (Lextok *) 0; 381 q_rem = (Queue *) 0; 382 } 383 return 1; 384 } 385 386 void 387 channm(Lextok *n) 388 { char lbuf[256]; 389 390 if (n->sym->type == CHAN) 391 strcat(Buf, n->sym->name); 392 else if (n->sym->type == NAME) 393 strcat(Buf, lookup(n->sym->name)->name); 394 else if (n->sym->type == STRUCT) 395 { Symbol *r = n->sym; 396 if (r->context) 397 r = findloc(r); 398 ini_struct(r); 399 printf("%s", r->name); 400 struct_name(n->lft, r, 1, lbuf); 401 strcat(Buf, lbuf); 402 } else 403 strcat(Buf, "-"); 404 if (n->lft->lft) 405 { sprintf(lbuf, "[%d]", eval(n->lft->lft)); 406 strcat(Buf, lbuf); 407 } 408 } 409 410 static void 411 difcolumns(Lextok *n, char *tr, int v, int j, Queue *q) 412 { int cnt = 1; extern int pno; 413 Lextok *nn = ZN; 414 415 if (j == 0) 416 { Buf[0] = '\0'; 417 channm(n); 418 strcat(Buf, (strncmp(tr, "Sen", 3))?"?":"!"); 419 } else 420 strcat(Buf, ","); 421 if (tr[0] == '[') strcat(Buf, "["); 422 sr_buf(v, q->fld_width[j] == MTYPE); 423 if (j == q->nflds - 1) 424 { int cnr; 425 if (s_trail) cnr = pno; else cnr = X?X->pid - Have_claim:0; 426 if (tr[0] == '[') strcat(Buf, "]"); 427 pstext(cnr, Buf); 428 } 429 } 430 431 static void 432 docolumns(Lextok *n, char *tr, int v, int j, Queue *q) 433 { int i; 434 435 if (firstrow) 436 { printf("q\\p"); 437 for (i = 0; i < nproc-nstop - Have_claim; i++) 438 printf(" %3d", i); 439 printf("\n"); 440 firstrow = 0; 441 } 442 if (j == 0) 443 { printf("%3d", q->qid); 444 if (X) 445 for (i = 0; i < X->pid - Have_claim; i++) 446 printf(" ."); 447 printf(" "); 448 Buf[0] = '\0'; 449 channm(n); 450 printf("%s%c", Buf, (strncmp(tr, "Sen", 3))?'?':'!'); 451 } else 452 printf(","); 453 if (tr[0] == '[') printf("["); 454 sr_mesg(stdout, v, q->fld_width[j] == MTYPE); 455 if (j == q->nflds - 1) 456 { if (tr[0] == '[') printf("]"); 457 printf("\n"); 458 } 459 } 460 461 typedef struct QH { 462 int n; 463 struct QH *nxt; 464 } QH; 465 QH *qh; 466 467 void 468 qhide(int q) 469 { QH *p = (QH *) emalloc(sizeof(QH)); 470 p->n = q; 471 p->nxt = qh; 472 qh = p; 473 } 474 475 int 476 qishidden(int q) 477 { QH *p; 478 for (p = qh; p; p = p->nxt) 479 if (p->n == q) 480 return 1; 481 return 0; 482 } 483 484 static void 485 sr_talk(Lextok *n, int v, char *tr, char *a, int j, Queue *q) 486 { char s[64]; 487 488 if (qishidden(eval(n->lft))) 489 return; 490 491 if (columns) 492 { if (columns == 2) 493 difcolumns(n, tr, v, j, q); 494 else 495 docolumns(n, tr, v, j, q); 496 return; 497 } 498 if (xspin) 499 { if ((verbose&4) && tr[0] != '[') 500 sprintf(s, "(state -)\t[values: %d", 501 eval(n->lft)); 502 else 503 sprintf(s, "(state -)\t[%d", eval(n->lft)); 504 if (strncmp(tr, "Sen", 3) == 0) 505 strcat(s, "!"); 506 else 507 strcat(s, "?"); 508 } else 509 { strcpy(s, tr); 510 } 511 512 if (j == 0) 513 { whoruns(1); 514 printf("line %3d %s %s", 515 n->ln, n->fn->name, s); 516 } else 517 printf(","); 518 sr_mesg(stdout, v, q->fld_width[j] == MTYPE); 519 520 if (j == q->nflds - 1) 521 { if (xspin) 522 { printf("]\n"); 523 if (!(verbose&4)) printf("\n"); 524 return; 525 } 526 printf("\t%s queue %d (", a, eval(n->lft)); 527 Buf[0] = '\0'; 528 channm(n); 529 printf("%s)\n", Buf); 530 } 531 fflush(stdout); 532 } 533 534 void 535 sr_buf(int v, int j) 536 { int cnt = 1; Lextok *n; 537 char lbuf[128]; 538 539 for (n = Mtype; n && j; n = n->rgt, cnt++) 540 if (cnt == v) 541 { sprintf(lbuf, "%s", n->lft->sym->name); 542 strcat(Buf, lbuf); 543 return; 544 } 545 sprintf(lbuf, "%d", v); 546 strcat(Buf, lbuf); 547 } 548 549 void 550 sr_mesg(FILE *fd, int v, int j) 551 { Buf[0] ='\0'; 552 sr_buf(v, j); 553 fprintf(fd, Buf); 554 } 555 556 void 557 doq(Symbol *s, int n, RunList *r) 558 { Queue *q; 559 int j, k; 560 561 if (!s->val) /* uninitialized queue */ 562 return; 563 for (q = qtab; q; q = q->nxt) 564 if (q->qid == s->val[n]) 565 { if (xspin > 0 566 && (verbose&4) 567 && q->setat < depth) 568 continue; 569 if (q->nslots == 0) 570 continue; /* rv q always empty */ 571 printf("\t\tqueue %d (", q->qid); 572 if (r) 573 printf("%s(%d):", r->n->name, r->pid - Have_claim); 574 if (s->nel != 1) 575 printf("%s[%d]): ", s->name, n); 576 else 577 printf("%s): ", s->name); 578 for (k = 0; k < q->qlen; k++) 579 { printf("["); 580 for (j = 0; j < q->nflds; j++) 581 { if (j > 0) printf(","); 582 sr_mesg(stdout, q->contents[k*q->nflds+j], 583 q->fld_width[j] == MTYPE); 584 } 585 printf("]"); 586 } 587 printf("\n"); 588 break; 589 } 590 } 591 592 void 593 nochan_manip(Lextok *p, Lextok *n, int d) 594 { int e = 1; 595 596 if (d == 0 && p->sym && p->sym->type == CHAN) 597 setaccess(p->sym, ZS, 0, 'L'); 598 599 if (!n || n->ntyp == LEN || n->ntyp == RUN) 600 return; 601 602 if (n->sym && n->sym->type == CHAN) 603 { if (d == 1) 604 fatal("invalid use of chan name", (char *) 0); 605 else 606 setaccess(n->sym, ZS, 0, 'V'); 607 } 608 609 if (n->ntyp == NAME 610 || n->ntyp == '.') 611 e = 0; /* array index or struct element */ 612 613 nochan_manip(p, n->lft, e); 614 nochan_manip(p, n->rgt, 1); 615 } 616