ref: 24e73840072b4214b3c5e2167a85bdc408fd3b03
dir: /sys/src/cmd/spin/mesg.c/
/***** spin: mesg.c *****/ /* Copyright (c) 1989-2003 by Lucent Technologies, Bell Laboratories. */ /* All Rights Reserved. This software is for educational purposes only. */ /* No guarantee whatsoever is expressed or implied by the distribution of */ /* this code. Permission is given to distribute this code provided that */ /* this introductory message is not removed and no monies are exchanged. */ /* Software written by Gerard J. Holzmann. For tool documentation see: */ /* http://spinroot.com/ */ /* Send all bug-reports and/or questions to: bugs@spinroot.com */ #include "spin.h" #include "y.tab.h" #ifndef MAXQ #define MAXQ 2500 /* default max # queues */ #endif extern RunList *X; extern Symbol *Fname; extern Lextok *Mtype; extern int verbose, TstOnly, s_trail, analyze, columns; extern int lineno, depth, xspin, m_loss, jumpsteps; extern int nproc, nstop; extern short Have_claim; Queue *qtab = (Queue *) 0; /* linked list of queues */ Queue *ltab[MAXQ]; /* linear list of queues */ int nqs = 0, firstrow = 1; char Buf[4096]; static Lextok *n_rem = (Lextok *) 0; static Queue *q_rem = (Queue *) 0; static int a_rcv(Queue *, Lextok *, int); static int a_snd(Queue *, Lextok *); static int sa_snd(Queue *, Lextok *); static int s_snd(Queue *, Lextok *); extern void sr_buf(int, int); extern void sr_mesg(FILE *, int, int); extern void putarrow(int, int); static void sr_talk(Lextok *, int, char *, char *, int, Queue *); int cnt_mpars(Lextok *n) { Lextok *m; int i=0; for (m = n; m; m = m->rgt) i += Cnt_flds(m); return i; } int qmake(Symbol *s) { Lextok *m; Queue *q; int i; if (!s->ini) return 0; if (nqs >= MAXQ) { lineno = s->ini->ln; Fname = s->ini->fn; fatal("too many queues (%s)", s->name); } if (analyze && nqs >= 255) { fatal("too many channel types", (char *)0); } if (s->ini->ntyp != CHAN) return eval(s->ini); q = (Queue *) emalloc(sizeof(Queue)); q->qid = ++nqs; q->nslots = s->ini->val; q->nflds = cnt_mpars(s->ini->rgt); q->setat = depth; i = max(1, q->nslots); /* 0-slot qs get 1 slot minimum */ q->contents = (int *) emalloc(q->nflds*i*sizeof(int)); q->fld_width = (int *) emalloc(q->nflds*sizeof(int)); q->stepnr = (int *) emalloc(i*sizeof(int)); for (m = s->ini->rgt, i = 0; m; m = m->rgt) { if (m->sym && m->ntyp == STRUCT) i = Width_set(q->fld_width, i, getuname(m->sym)); else q->fld_width[i++] = m->ntyp; } q->nxt = qtab; qtab = q; ltab[q->qid-1] = q; return q->qid; } int qfull(Lextok *n) { int whichq = eval(n->lft)-1; if (whichq < MAXQ && whichq >= 0 && ltab[whichq]) return (ltab[whichq]->qlen >= ltab[whichq]->nslots); return 0; } int qlen(Lextok *n) { int whichq = eval(n->lft)-1; if (whichq < MAXQ && whichq >= 0 && ltab[whichq]) return ltab[whichq]->qlen; return 0; } int q_is_sync(Lextok *n) { int whichq = eval(n->lft)-1; if (whichq < MAXQ && whichq >= 0 && ltab[whichq]) return (ltab[whichq]->nslots == 0); return 0; } int qsend(Lextok *n) { int whichq = eval(n->lft)-1; if (whichq == -1) { printf("Error: sending to an uninitialized chan\n"); whichq = 0; return 0; } if (whichq < MAXQ && whichq >= 0 && ltab[whichq]) { ltab[whichq]->setat = depth; if (ltab[whichq]->nslots > 0) return a_snd(ltab[whichq], n); else return s_snd(ltab[whichq], n); } return 0; } int qrecv(Lextok *n, int full) { int whichq = eval(n->lft)-1; if (whichq == -1) { if (n->sym && !strcmp(n->sym->name, "STDIN")) { Lextok *m; if (TstOnly) return 1; for (m = n->rgt; m; m = m->rgt) if (m->lft->ntyp != CONST && m->lft->ntyp != EVAL) { int c = getchar(); (void) setval(m->lft, c); } else fatal("invalid use of STDIN", (char *)0); whichq = 0; return 1; } printf("Error: receiving from an uninitialized chan %s\n", n->sym?n->sym->name:""); whichq = 0; return 0; } if (whichq < MAXQ && whichq >= 0 && ltab[whichq]) { ltab[whichq]->setat = depth; return a_rcv(ltab[whichq], n, full); } return 0; } static int sa_snd(Queue *q, Lextok *n) /* sorted asynchronous */ { Lextok *m; int i, j, k; int New, Old; for (i = 0; i < q->qlen; i++) for (j = 0, m = n->rgt; m && j < q->nflds; m = m->rgt, j++) { New = cast_val(q->fld_width[j], eval(m->lft), 0); Old = q->contents[i*q->nflds+j]; if (New == Old) continue; if (New > Old) break; /* inner loop */ if (New < Old) goto found; } found: for (j = q->qlen-1; j >= i; j--) for (k = 0; k < q->nflds; k++) { q->contents[(j+1)*q->nflds+k] = q->contents[j*q->nflds+k]; /* shift up */ if (k == 0) q->stepnr[j+1] = q->stepnr[j]; } return i*q->nflds; /* new q offset */ } void typ_ck(int ft, int at, char *s) { if ((verbose&32) && ft != at && (ft == CHAN || at == CHAN)) { char buf[128], tag1[64], tag2[64]; (void) sputtype(tag1, ft); (void) sputtype(tag2, at); sprintf(buf, "type-clash in %s, (%s<-> %s)", s, tag1, tag2); non_fatal("%s", buf); } } static int a_snd(Queue *q, Lextok *n) { Lextok *m; int i = q->qlen*q->nflds; /* q offset */ int j = 0; /* q field# */ if (q->nslots > 0 && q->qlen >= q->nslots) return m_loss; /* q is full */ if (TstOnly) return 1; if (n->val) i = sa_snd(q, n); /* sorted insert */ q->stepnr[i/q->nflds] = depth; for (m = n->rgt; m && j < q->nflds; m = m->rgt, j++) { int New = eval(m->lft); q->contents[i+j] = cast_val(q->fld_width[j], New, 0); if ((verbose&16) && depth >= jumpsteps) sr_talk(n, New, "Send ", "->", j, q); typ_ck(q->fld_width[j], Sym_typ(m->lft), "send"); } if ((verbose&16) && depth >= jumpsteps) { for (i = j; i < q->nflds; i++) sr_talk(n, 0, "Send ", "->", i, q); if (j < q->nflds) printf("%3d: warning: missing params in send\n", depth); if (m) printf("%3d: warning: too many params in send\n", depth); } q->qlen++; return 1; } static int a_rcv(Queue *q, Lextok *n, int full) { Lextok *m; int i=0, oi, j, k; extern int Rvous; if (q->qlen == 0) return 0; /* q is empty */ try_slot: /* test executability */ for (m = n->rgt, j=0; m && j < q->nflds; m = m->rgt, j++) if ((m->lft->ntyp == CONST && q->contents[i*q->nflds+j] != m->lft->val) || (m->lft->ntyp == EVAL && q->contents[i*q->nflds+j] != eval(m->lft->lft))) { if (n->val == 0 /* fifo recv */ || n->val == 2 /* fifo poll */ || ++i >= q->qlen) /* last slot */ return 0; /* no match */ goto try_slot; } if (TstOnly) return 1; if (verbose&8) { if (j < q->nflds) printf("%3d: warning: missing params in next recv\n", depth); else if (m) printf("%3d: warning: too many params in next recv\n", depth); } /* set the fields */ if (Rvous) { n_rem = n; q_rem = q; } oi = q->stepnr[i]; for (m = n->rgt, j = 0; m && j < q->nflds; m = m->rgt, j++) { if (columns && !full) /* was columns == 1 */ continue; if ((verbose&8) && !Rvous && depth >= jumpsteps) { sr_talk(n, q->contents[i*q->nflds+j], (full && n->val < 2)?"Recv ":"[Recv] ", "<-", j, q); } if (!full) continue; /* test */ if (m && m->lft->ntyp != CONST && m->lft->ntyp != EVAL) { (void) setval(m->lft, q->contents[i*q->nflds+j]); typ_ck(q->fld_width[j], Sym_typ(m->lft), "recv"); } if (n->val < 2) /* not a poll */ for (k = i; k < q->qlen-1; k++) { q->contents[k*q->nflds+j] = q->contents[(k+1)*q->nflds+j]; if (j == 0) q->stepnr[k] = q->stepnr[k+1]; } } if ((!columns || full) && (verbose&8) && !Rvous && depth >= jumpsteps) for (i = j; i < q->nflds; i++) { sr_talk(n, 0, (full && n->val < 2)?"Recv ":"[Recv] ", "<-", i, q); } if (columns == 2 && full && !Rvous && depth >= jumpsteps) putarrow(oi, depth); if (full && n->val < 2) q->qlen--; return 1; } static int s_snd(Queue *q, Lextok *n) { Lextok *m; RunList *rX, *sX = X; /* rX=recvr, sX=sendr */ int i, j = 0; /* q field# */ for (m = n->rgt; m && j < q->nflds; m = m->rgt, j++) { q->contents[j] = cast_val(q->fld_width[j], eval(m->lft), 0); typ_ck(q->fld_width[j], Sym_typ(m->lft), "rv-send"); } q->qlen = 1; if (!complete_rendez()) { q->qlen = 0; return 0; } if (TstOnly) { q->qlen = 0; return 1; } q->stepnr[0] = depth; if ((verbose&16) && depth >= jumpsteps) { m = n->rgt; rX = X; X = sX; for (j = 0; m && j < q->nflds; m = m->rgt, j++) sr_talk(n, eval(m->lft), "Sent ", "->", j, q); for (i = j; i < q->nflds; i++) sr_talk(n, 0, "Sent ", "->", i, q); if (j < q->nflds) printf("%3d: warning: missing params in rv-send\n", depth); else if (m) printf("%3d: warning: too many params in rv-send\n", depth); X = rX; /* restore receiver's context */ if (!s_trail) { if (!n_rem || !q_rem) fatal("cannot happen, s_snd", (char *) 0); m = n_rem->rgt; for (j = 0; m && j < q->nflds; m = m->rgt, j++) { if (m->lft->ntyp != NAME || strcmp(m->lft->sym->name, "_") != 0) i = eval(m->lft); else i = 0; if (verbose&8) sr_talk(n_rem,i,"Recv ","<-",j,q_rem); } if (verbose&8) for (i = j; i < q->nflds; i++) sr_talk(n_rem, 0, "Recv ", "<-", j, q_rem); if (columns == 2) putarrow(depth, depth); } n_rem = (Lextok *) 0; q_rem = (Queue *) 0; } return 1; } void channm(Lextok *n) { char lbuf[512]; if (n->sym->type == CHAN) strcat(Buf, n->sym->name); else if (n->sym->type == NAME) strcat(Buf, lookup(n->sym->name)->name); else if (n->sym->type == STRUCT) { Symbol *r = n->sym; if (r->context) r = findloc(r); ini_struct(r); printf("%s", r->name); strcpy(lbuf, ""); struct_name(n->lft, r, 1, lbuf); strcat(Buf, lbuf); } else strcat(Buf, "-"); if (n->lft->lft) { sprintf(lbuf, "[%d]", eval(n->lft->lft)); strcat(Buf, lbuf); } } static void difcolumns(Lextok *n, char *tr, int v, int j, Queue *q) { extern int pno; if (j == 0) { Buf[0] = '\0'; channm(n); strcat(Buf, (strncmp(tr, "Sen", 3))?"?":"!"); } else strcat(Buf, ","); if (tr[0] == '[') strcat(Buf, "["); sr_buf(v, q->fld_width[j] == MTYPE); if (j == q->nflds - 1) { int cnr; if (s_trail) cnr = pno; else cnr = X?X->pid - Have_claim:0; if (tr[0] == '[') strcat(Buf, "]"); pstext(cnr, Buf); } } static void docolumns(Lextok *n, char *tr, int v, int j, Queue *q) { int i; if (firstrow) { printf("q\\p"); for (i = 0; i < nproc-nstop - Have_claim; i++) printf(" %3d", i); printf("\n"); firstrow = 0; } if (j == 0) { printf("%3d", q->qid); if (X) for (i = 0; i < X->pid - Have_claim; i++) printf(" ."); printf(" "); Buf[0] = '\0'; channm(n); printf("%s%c", Buf, (strncmp(tr, "Sen", 3))?'?':'!'); } else printf(","); if (tr[0] == '[') printf("["); sr_mesg(stdout, v, q->fld_width[j] == MTYPE); if (j == q->nflds - 1) { if (tr[0] == '[') printf("]"); printf("\n"); } } typedef struct QH { int n; struct QH *nxt; } QH; QH *qh; void qhide(int q) { QH *p = (QH *) emalloc(sizeof(QH)); p->n = q; p->nxt = qh; qh = p; } int qishidden(int q) { QH *p; for (p = qh; p; p = p->nxt) if (p->n == q) return 1; return 0; } static void sr_talk(Lextok *n, int v, char *tr, char *a, int j, Queue *q) { char s[64]; if (qishidden(eval(n->lft))) return; if (columns) { if (columns == 2) difcolumns(n, tr, v, j, q); else docolumns(n, tr, v, j, q); return; } if (xspin) { if ((verbose&4) && tr[0] != '[') sprintf(s, "(state -)\t[values: %d", eval(n->lft)); else sprintf(s, "(state -)\t[%d", eval(n->lft)); if (strncmp(tr, "Sen", 3) == 0) strcat(s, "!"); else strcat(s, "?"); } else { strcpy(s, tr); } if (j == 0) { whoruns(1); printf("line %3d %s %s", n->ln, n->fn->name, s); } else printf(","); sr_mesg(stdout, v, q->fld_width[j] == MTYPE); if (j == q->nflds - 1) { if (xspin) { printf("]\n"); if (!(verbose&4)) printf("\n"); return; } printf("\t%s queue %d (", a, eval(n->lft)); Buf[0] = '\0'; channm(n); printf("%s)\n", Buf); } fflush(stdout); } void sr_buf(int v, int j) { int cnt = 1; Lextok *n; char lbuf[512]; for (n = Mtype; n && j; n = n->rgt, cnt++) if (cnt == v) { if(strlen(n->lft->sym->name) >= sizeof(lbuf)) { non_fatal("mtype name %s too long", n->lft->sym->name); break; } sprintf(lbuf, "%s", n->lft->sym->name); strcat(Buf, lbuf); return; } sprintf(lbuf, "%d", v); strcat(Buf, lbuf); } void sr_mesg(FILE *fd, int v, int j) { Buf[0] ='\0'; sr_buf(v, j); fprintf(fd, Buf); } void doq(Symbol *s, int n, RunList *r) { Queue *q; int j, k; if (!s->val) /* uninitialized queue */ return; for (q = qtab; q; q = q->nxt) if (q->qid == s->val[n]) { if (xspin > 0 && (verbose&4) && q->setat < depth) continue; if (q->nslots == 0) continue; /* rv q always empty */ printf("\t\tqueue %d (", q->qid); if (r) printf("%s(%d):", r->n->name, r->pid - Have_claim); if (s->nel != 1) printf("%s[%d]): ", s->name, n); else printf("%s): ", s->name); for (k = 0; k < q->qlen; k++) { printf("["); for (j = 0; j < q->nflds; j++) { if (j > 0) printf(","); sr_mesg(stdout, q->contents[k*q->nflds+j], q->fld_width[j] == MTYPE); } printf("]"); } printf("\n"); break; } } void nochan_manip(Lextok *p, Lextok *n, int d) { int e = 1; if (d == 0 && p->sym && p->sym->type == CHAN) { setaccess(p->sym, ZS, 0, 'L'); if (n && n->ntyp == CONST) fatal("invalid asgn to chan", (char *) 0); if (n && n->sym && n->sym->type == CHAN) { setaccess(n->sym, ZS, 0, 'V'); return; } } if (!n || n->ntyp == LEN || n->ntyp == RUN) return; if (n->sym && n->sym->type == CHAN) { if (d == 1) fatal("invalid use of chan name", (char *) 0); else setaccess(n->sym, ZS, 0, 'V'); } if (n->ntyp == NAME || n->ntyp == '.') e = 0; /* array index or struct element */ nochan_manip(p, n->lft, e); nochan_manip(p, n->rgt, 1); } void no_internals(Lextok *n) { char *sp; if (!n->sym || !n->sym->name) return; sp = n->sym->name; if ((strlen(sp) == strlen("_nr_pr") && strcmp(sp, "_nr_pr") == 0) || (strlen(sp) == strlen("_p") && strcmp(sp, "_p") == 0)) { fatal("attempt to assign value to system variable %s", sp); } }