1 /***** spin: mesg.c *****/
3 /* Copyright (c) 1989-2003 by Lucent Technologies, Bell Laboratories. */
4 /* All Rights Reserved. This software is for educational purposes only. */
5 /* No guarantee whatsoever is expressed or implied by the distribution of */
6 /* this code. Permission is given to distribute this code provided that */
7 /* this introductory message is not removed and no monies are exchanged. */
8 /* Software written by Gerard J. Holzmann. For tool documentation see: */
9 /* http://spinroot.com/ */
10 /* Send all bug-reports and/or questions to: bugs@spinroot.com */
16 #define MAXQ 2500 /* default max # queues */
22 extern int verbose, TstOnly, s_trail, analyze, columns;
23 extern int lineno, depth, xspin, m_loss, jumpsteps;
24 extern int nproc, nstop;
25 extern short Have_claim;
27 Queue *qtab = (Queue *) 0; /* linked list of queues */
28 Queue *ltab[MAXQ]; /* linear list of queues */
29 int nqs = 0, firstrow = 1;
32 static Lextok *n_rem = (Lextok *) 0;
33 static Queue *q_rem = (Queue *) 0;
35 static int a_rcv(Queue *, Lextok *, int);
36 static int a_snd(Queue *, Lextok *);
37 static int sa_snd(Queue *, Lextok *);
38 static int s_snd(Queue *, Lextok *);
39 extern void sr_buf(int, int);
40 extern void sr_mesg(FILE *, int, int);
41 extern void putarrow(int, int);
42 static void sr_talk(Lextok *, int, char *, char *, int, Queue *);
49 for (m = n; m; m = m->rgt)
64 { lineno = s->ini->ln;
66 fatal("too many queues (%s)", s->name);
68 if (analyze && nqs >= 255)
69 { fatal("too many channel types", (char *)0);
72 if (s->ini->ntyp != CHAN)
75 q = (Queue *) emalloc(sizeof(Queue));
77 q->nslots = s->ini->val;
78 q->nflds = cnt_mpars(s->ini->rgt);
81 i = max(1, q->nslots); /* 0-slot qs get 1 slot minimum */
83 q->contents = (int *) emalloc(q->nflds*i*sizeof(int));
84 q->fld_width = (int *) emalloc(q->nflds*sizeof(int));
85 q->stepnr = (int *) emalloc(i*sizeof(int));
87 for (m = s->ini->rgt, i = 0; m; m = m->rgt)
88 { if (m->sym && m->ntyp == STRUCT)
89 i = Width_set(q->fld_width, i, getuname(m->sym));
91 q->fld_width[i++] = m->ntyp;
102 { int whichq = eval(n->lft)-1;
104 if (whichq < MAXQ && whichq >= 0 && ltab[whichq])
105 return (ltab[whichq]->qlen >= ltab[whichq]->nslots);
111 { int whichq = eval(n->lft)-1;
113 if (whichq < MAXQ && whichq >= 0 && ltab[whichq])
114 return ltab[whichq]->qlen;
120 { int whichq = eval(n->lft)-1;
122 if (whichq < MAXQ && whichq >= 0 && ltab[whichq])
123 return (ltab[whichq]->nslots == 0);
129 { int whichq = eval(n->lft)-1;
132 { printf("Error: sending to an uninitialized chan\n");
136 if (whichq < MAXQ && whichq >= 0 && ltab[whichq])
137 { ltab[whichq]->setat = depth;
138 if (ltab[whichq]->nslots > 0)
139 return a_snd(ltab[whichq], n);
141 return s_snd(ltab[whichq], n);
147 qrecv(Lextok *n, int full)
148 { int whichq = eval(n->lft)-1;
151 { if (n->sym && !strcmp(n->sym->name, "STDIN"))
154 if (TstOnly) return 1;
156 for (m = n->rgt; m; m = m->rgt)
157 if (m->lft->ntyp != CONST && m->lft->ntyp != EVAL)
159 (void) setval(m->lft, c);
161 fatal("invalid use of STDIN", (char *)0);
166 printf("Error: receiving from an uninitialized chan %s\n",
167 n->sym?n->sym->name:"");
171 if (whichq < MAXQ && whichq >= 0 && ltab[whichq])
172 { ltab[whichq]->setat = depth;
173 return a_rcv(ltab[whichq], n, full);
179 sa_snd(Queue *q, Lextok *n) /* sorted asynchronous */
184 for (i = 0; i < q->qlen; i++)
185 for (j = 0, m = n->rgt; m && j < q->nflds; m = m->rgt, j++)
186 { New = cast_val(q->fld_width[j], eval(m->lft), 0);
187 Old = q->contents[i*q->nflds+j];
188 if (New == Old) continue;
189 if (New > Old) break; /* inner loop */
190 if (New < Old) goto found;
193 for (j = q->qlen-1; j >= i; j--)
194 for (k = 0; k < q->nflds; k++)
195 { q->contents[(j+1)*q->nflds+k] =
196 q->contents[j*q->nflds+k]; /* shift up */
198 q->stepnr[j+1] = q->stepnr[j];
200 return i*q->nflds; /* new q offset */
204 typ_ck(int ft, int at, char *s)
206 if ((verbose&32) && ft != at
207 && (ft == CHAN || at == CHAN))
208 { char buf[128], tag1[64], tag2[64];
209 (void) sputtype(tag1, ft);
210 (void) sputtype(tag2, at);
211 sprintf(buf, "type-clash in %s, (%s<-> %s)", s, tag1, tag2);
212 non_fatal("%s", buf);
217 a_snd(Queue *q, Lextok *n)
219 int i = q->qlen*q->nflds; /* q offset */
220 int j = 0; /* q field# */
222 if (q->nslots > 0 && q->qlen >= q->nslots)
223 return m_loss; /* q is full */
225 if (TstOnly) return 1;
227 if (n->val) i = sa_snd(q, n); /* sorted insert */
229 q->stepnr[i/q->nflds] = depth;
231 for (m = n->rgt; m && j < q->nflds; m = m->rgt, j++)
232 { int New = eval(m->lft);
233 q->contents[i+j] = cast_val(q->fld_width[j], New, 0);
234 if ((verbose&16) && depth >= jumpsteps)
235 sr_talk(n, New, "Send ", "->", j, q);
236 typ_ck(q->fld_width[j], Sym_typ(m->lft), "send");
238 if ((verbose&16) && depth >= jumpsteps)
239 { for (i = j; i < q->nflds; i++)
240 sr_talk(n, 0, "Send ", "->", i, q);
242 printf("%3d: warning: missing params in send\n",
245 printf("%3d: warning: too many params in send\n",
253 a_rcv(Queue *q, Lextok *n, int full)
259 return 0; /* q is empty */
261 /* test executability */
262 for (m = n->rgt, j=0; m && j < q->nflds; m = m->rgt, j++)
263 if ((m->lft->ntyp == CONST
264 && q->contents[i*q->nflds+j] != m->lft->val)
265 || (m->lft->ntyp == EVAL
266 && q->contents[i*q->nflds+j] != eval(m->lft->lft)))
267 { if (n->val == 0 /* fifo recv */
268 || n->val == 2 /* fifo poll */
269 || ++i >= q->qlen) /* last slot */
270 return 0; /* no match */
273 if (TstOnly) return 1;
277 printf("%3d: warning: missing params in next recv\n",
280 printf("%3d: warning: too many params in next recv\n",
291 for (m = n->rgt, j = 0; m && j < q->nflds; m = m->rgt, j++)
292 { if (columns && !full) /* was columns == 1 */
294 if ((verbose&8) && !Rvous && depth >= jumpsteps)
295 { sr_talk(n, q->contents[i*q->nflds+j],
296 (full && n->val < 2)?"Recv ":"[Recv] ", "<-", j, q);
300 if (m && m->lft->ntyp != CONST && m->lft->ntyp != EVAL)
301 { (void) setval(m->lft, q->contents[i*q->nflds+j]);
302 typ_ck(q->fld_width[j], Sym_typ(m->lft), "recv");
304 if (n->val < 2) /* not a poll */
305 for (k = i; k < q->qlen-1; k++)
306 { q->contents[k*q->nflds+j] =
307 q->contents[(k+1)*q->nflds+j];
309 q->stepnr[k] = q->stepnr[k+1];
313 if ((!columns || full)
314 && (verbose&8) && !Rvous && depth >= jumpsteps)
315 for (i = j; i < q->nflds; i++)
317 (full && n->val < 2)?"Recv ":"[Recv] ", "<-", i, q);
319 if (columns == 2 && full && !Rvous && depth >= jumpsteps)
322 if (full && n->val < 2)
328 s_snd(Queue *q, Lextok *n)
330 RunList *rX, *sX = X; /* rX=recvr, sX=sendr */
331 int i, j = 0; /* q field# */
333 for (m = n->rgt; m && j < q->nflds; m = m->rgt, j++)
334 { q->contents[j] = cast_val(q->fld_width[j], eval(m->lft), 0);
335 typ_ck(q->fld_width[j], Sym_typ(m->lft), "rv-send");
338 if (!complete_rendez())
346 q->stepnr[0] = depth;
347 if ((verbose&16) && depth >= jumpsteps)
350 for (j = 0; m && j < q->nflds; m = m->rgt, j++)
351 sr_talk(n, eval(m->lft), "Sent ", "->", j, q);
352 for (i = j; i < q->nflds; i++)
353 sr_talk(n, 0, "Sent ", "->", i, q);
355 printf("%3d: warning: missing params in rv-send\n",
358 printf("%3d: warning: too many params in rv-send\n",
360 X = rX; /* restore receiver's context */
362 { if (!n_rem || !q_rem)
363 fatal("cannot happen, s_snd", (char *) 0);
365 for (j = 0; m && j < q->nflds; m = m->rgt, j++)
366 { if (m->lft->ntyp != NAME
367 || strcmp(m->lft->sym->name, "_") != 0)
372 sr_talk(n_rem,i,"Recv ","<-",j,q_rem);
375 for (i = j; i < q->nflds; i++)
376 sr_talk(n_rem, 0, "Recv ", "<-", j, q_rem);
378 putarrow(depth, depth);
380 n_rem = (Lextok *) 0;
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;
399 printf("%s", r->name);
401 struct_name(n->lft, r, 1, lbuf);
406 { sprintf(lbuf, "[%d]", eval(n->lft->lft));
412 difcolumns(Lextok *n, char *tr, int v, int j, Queue *q)
418 strcat(Buf, (strncmp(tr, "Sen", 3))?"?":"!");
421 if (tr[0] == '[') strcat(Buf, "[");
422 sr_buf(v, q->fld_width[j] == MTYPE);
423 if (j == q->nflds - 1)
425 if (s_trail) cnr = pno; else cnr = X?X->pid - Have_claim:0;
426 if (tr[0] == '[') strcat(Buf, "]");
432 docolumns(Lextok *n, char *tr, int v, int j, Queue *q)
437 for (i = 0; i < nproc-nstop - Have_claim; i++)
443 { printf("%3d", q->qid);
445 for (i = 0; i < X->pid - Have_claim; i++)
450 printf("%s%c", Buf, (strncmp(tr, "Sen", 3))?'?':'!');
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("]");
469 { QH *p = (QH *) emalloc(sizeof(QH));
478 for (p = qh; p; p = p->nxt)
485 sr_talk(Lextok *n, int v, char *tr, char *a, int j, Queue *q)
488 if (qishidden(eval(n->lft)))
493 difcolumns(n, tr, v, j, q);
495 docolumns(n, tr, v, j, q);
499 { if ((verbose&4) && tr[0] != '[')
500 sprintf(s, "(state -)\t[values: %d",
503 sprintf(s, "(state -)\t[%d", eval(n->lft));
504 if (strncmp(tr, "Sen", 3) == 0)
514 printf("line %3d %s %s",
515 n->ln, n->fn->name, s);
518 sr_mesg(stdout, v, q->fld_width[j] == MTYPE);
520 if (j == q->nflds - 1)
523 if (!(verbose&4)) printf("\n");
526 printf("\t%s queue %d (", a, eval(n->lft));
529 printf("%s)\n", Buf);
536 { int cnt = 1; Lextok *n;
539 for (n = Mtype; n && j; n = n->rgt, cnt++)
541 { if(strlen(n->lft->sym->name) >= sizeof(lbuf))
542 { non_fatal("mtype name %s too long", n->lft->sym->name);
545 sprintf(lbuf, "%s", n->lft->sym->name);
549 sprintf(lbuf, "%d", v);
554 sr_mesg(FILE *fd, int v, int j)
561 doq(Symbol *s, int n, RunList *r)
565 if (!s->val) /* uninitialized queue */
567 for (q = qtab; q; q = q->nxt)
568 if (q->qid == s->val[n])
574 continue; /* rv q always empty */
575 printf("\t\tqueue %d (", q->qid);
577 printf("%s(%d):", r->n->name, r->pid - Have_claim);
579 printf("%s[%d]): ", s->name, n);
581 printf("%s): ", s->name);
582 for (k = 0; k < q->qlen; k++)
584 for (j = 0; j < q->nflds; j++)
585 { if (j > 0) printf(",");
586 sr_mesg(stdout, q->contents[k*q->nflds+j],
587 q->fld_width[j] == MTYPE);
597 nochan_manip(Lextok *p, Lextok *n, int d)
600 if (d == 0 && p->sym && p->sym->type == CHAN)
601 { setaccess(p->sym, ZS, 0, 'L');
603 if (n && n->ntyp == CONST)
604 fatal("invalid asgn to chan", (char *) 0);
606 if (n && n->sym && n->sym->type == CHAN)
607 { setaccess(n->sym, ZS, 0, 'V');
612 if (!n || n->ntyp == LEN || n->ntyp == RUN)
615 if (n->sym && n->sym->type == CHAN)
617 fatal("invalid use of chan name", (char *) 0);
619 setaccess(n->sym, ZS, 0, 'V');
624 e = 0; /* array index or struct element */
626 nochan_manip(p, n->lft, e);
627 nochan_manip(p, n->rgt, 1);
631 no_internals(Lextok *n)
640 if ((strlen(sp) == strlen("_nr_pr") && strcmp(sp, "_nr_pr") == 0)
641 || (strlen(sp) == strlen("_p") && strcmp(sp, "_p") == 0))
642 { fatal("attempt to assign value to system variable %s", sp);