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
];
191 break; /* inner loop */
192 goto found
; /* New < Old */
195 for (j
= q
->qlen
-1; j
>= i
; j
--)
196 for (k
= 0; k
< q
->nflds
; k
++)
197 { q
->contents
[(j
+1)*q
->nflds
+k
] =
198 q
->contents
[j
*q
->nflds
+k
]; /* shift up */
200 q
->stepnr
[j
+1] = q
->stepnr
[j
];
202 return i
*q
->nflds
; /* new q offset */
206 typ_ck(int ft
, int at
, char *s
)
208 if ((verbose
&32) && ft
!= at
209 && (ft
== CHAN
|| at
== CHAN
))
210 { char buf
[128], tag1
[64], tag2
[64];
211 (void) sputtype(tag1
, ft
);
212 (void) sputtype(tag2
, at
);
213 sprintf(buf
, "type-clash in %s, (%s<-> %s)", s
, tag1
, tag2
);
214 non_fatal("%s", buf
);
219 a_snd(Queue
*q
, Lextok
*n
)
221 int i
= q
->qlen
*q
->nflds
; /* q offset */
222 int j
= 0; /* q field# */
224 if (q
->nslots
> 0 && q
->qlen
>= q
->nslots
)
225 return m_loss
; /* q is full */
227 if (TstOnly
) return 1;
229 if (n
->val
) i
= sa_snd(q
, n
); /* sorted insert */
231 q
->stepnr
[i
/q
->nflds
] = depth
;
233 for (m
= n
->rgt
; m
&& j
< q
->nflds
; m
= m
->rgt
, j
++)
234 { int New
= eval(m
->lft
);
235 q
->contents
[i
+j
] = cast_val(q
->fld_width
[j
], New
, 0);
236 if ((verbose
&16) && depth
>= jumpsteps
)
237 sr_talk(n
, New
, "Send ", "->", j
, q
);
238 typ_ck(q
->fld_width
[j
], Sym_typ(m
->lft
), "send");
240 if ((verbose
&16) && depth
>= jumpsteps
)
241 { for (i
= j
; i
< q
->nflds
; i
++)
242 sr_talk(n
, 0, "Send ", "->", i
, q
);
244 printf("%3d: warning: missing params in send\n",
247 printf("%3d: warning: too many params in send\n",
255 a_rcv(Queue
*q
, Lextok
*n
, int full
)
261 return 0; /* q is empty */
263 /* test executability */
264 for (m
= n
->rgt
, j
=0; m
&& j
< q
->nflds
; m
= m
->rgt
, j
++)
265 if ((m
->lft
->ntyp
== CONST
266 && q
->contents
[i
*q
->nflds
+j
] != m
->lft
->val
)
267 || (m
->lft
->ntyp
== EVAL
268 && q
->contents
[i
*q
->nflds
+j
] != eval(m
->lft
->lft
)))
269 { if (n
->val
== 0 /* fifo recv */
270 || n
->val
== 2 /* fifo poll */
271 || ++i
>= q
->qlen
) /* last slot */
272 return 0; /* no match */
275 if (TstOnly
) return 1;
279 printf("%3d: warning: missing params in next recv\n",
282 printf("%3d: warning: too many params in next recv\n",
293 for (m
= n
->rgt
, j
= 0; m
&& j
< q
->nflds
; m
= m
->rgt
, j
++)
294 { if (columns
&& !full
) /* was columns == 1 */
296 if ((verbose
&8) && !Rvous
&& depth
>= jumpsteps
)
297 { sr_talk(n
, q
->contents
[i
*q
->nflds
+j
],
298 (full
&& n
->val
< 2)?"Recv ":"[Recv] ", "<-", j
, q
);
302 if (m
&& m
->lft
->ntyp
!= CONST
&& m
->lft
->ntyp
!= EVAL
)
303 { (void) setval(m
->lft
, q
->contents
[i
*q
->nflds
+j
]);
304 typ_ck(q
->fld_width
[j
], Sym_typ(m
->lft
), "recv");
306 if (n
->val
< 2) /* not a poll */
307 for (k
= i
; k
< q
->qlen
-1; k
++)
308 { q
->contents
[k
*q
->nflds
+j
] =
309 q
->contents
[(k
+1)*q
->nflds
+j
];
311 q
->stepnr
[k
] = q
->stepnr
[k
+1];
315 if ((!columns
|| full
)
316 && (verbose
&8) && !Rvous
&& depth
>= jumpsteps
)
317 for (i
= j
; i
< q
->nflds
; i
++)
319 (full
&& n
->val
< 2)?"Recv ":"[Recv] ", "<-", i
, q
);
321 if (columns
== 2 && full
&& !Rvous
&& depth
>= jumpsteps
)
324 if (full
&& n
->val
< 2)
330 s_snd(Queue
*q
, Lextok
*n
)
332 RunList
*rX
, *sX
= X
; /* rX=recvr, sX=sendr */
333 int i
, j
= 0; /* q field# */
335 for (m
= n
->rgt
; m
&& j
< q
->nflds
; m
= m
->rgt
, j
++)
336 { q
->contents
[j
] = cast_val(q
->fld_width
[j
], eval(m
->lft
), 0);
337 typ_ck(q
->fld_width
[j
], Sym_typ(m
->lft
), "rv-send");
340 if (!complete_rendez())
348 q
->stepnr
[0] = depth
;
349 if ((verbose
&16) && depth
>= jumpsteps
)
352 for (j
= 0; m
&& j
< q
->nflds
; m
= m
->rgt
, j
++)
353 sr_talk(n
, eval(m
->lft
), "Sent ", "->", j
, q
);
354 for (i
= j
; i
< q
->nflds
; i
++)
355 sr_talk(n
, 0, "Sent ", "->", i
, q
);
357 printf("%3d: warning: missing params in rv-send\n",
360 printf("%3d: warning: too many params in rv-send\n",
362 X
= rX
; /* restore receiver's context */
364 { if (!n_rem
|| !q_rem
)
365 fatal("cannot happen, s_snd", (char *) 0);
367 for (j
= 0; m
&& j
< q
->nflds
; m
= m
->rgt
, j
++)
368 { if (m
->lft
->ntyp
!= NAME
369 || strcmp(m
->lft
->sym
->name
, "_") != 0)
374 sr_talk(n_rem
,i
,"Recv ","<-",j
,q_rem
);
377 for (i
= j
; i
< q
->nflds
; i
++)
378 sr_talk(n_rem
, 0, "Recv ", "<-", j
, q_rem
);
380 putarrow(depth
, depth
);
382 n_rem
= (Lextok
*) 0;
392 if (n
->sym
->type
== CHAN
)
393 strcat(Buf
, n
->sym
->name
);
394 else if (n
->sym
->type
== NAME
)
395 strcat(Buf
, lookup(n
->sym
->name
)->name
);
396 else if (n
->sym
->type
== STRUCT
)
397 { Symbol
*r
= n
->sym
;
401 { strcat(Buf
, "*?*");
405 printf("%s", r
->name
);
407 struct_name(n
->lft
, r
, 1, lbuf
);
412 { sprintf(lbuf
, "[%d]", eval(n
->lft
->lft
));
418 difcolumns(Lextok
*n
, char *tr
, int v
, int j
, Queue
*q
)
424 strcat(Buf
, (strncmp(tr
, "Sen", 3))?"?":"!");
427 if (tr
[0] == '[') strcat(Buf
, "[");
428 sr_buf(v
, q
->fld_width
[j
] == MTYPE
);
429 if (j
== q
->nflds
- 1)
431 if (s_trail
) cnr
= pno
; else cnr
= X
?X
->pid
- Have_claim
:0;
432 if (tr
[0] == '[') strcat(Buf
, "]");
438 docolumns(Lextok
*n
, char *tr
, int v
, int j
, Queue
*q
)
443 for (i
= 0; i
< nproc
-nstop
- Have_claim
; i
++)
449 { printf("%3d", q
->qid
);
451 for (i
= 0; i
< X
->pid
- Have_claim
; i
++)
456 printf("%s%c", Buf
, (strncmp(tr
, "Sen", 3))?'?':'!');
459 if (tr
[0] == '[') printf("[");
460 sr_mesg(stdout
, v
, q
->fld_width
[j
] == MTYPE
);
461 if (j
== q
->nflds
- 1)
462 { if (tr
[0] == '[') printf("]");
475 { QH
*p
= (QH
*) emalloc(sizeof(QH
));
484 for (p
= qh
; p
; p
= p
->nxt
)
491 sr_talk(Lextok
*n
, int v
, char *tr
, char *a
, int j
, Queue
*q
)
494 if (qishidden(eval(n
->lft
)))
499 difcolumns(n
, tr
, v
, j
, q
);
501 docolumns(n
, tr
, v
, j
, q
);
505 { if ((verbose
&4) && tr
[0] != '[')
506 sprintf(s
, "(state -)\t[values: %d",
509 sprintf(s
, "(state -)\t[%d", eval(n
->lft
));
510 if (strncmp(tr
, "Sen", 3) == 0)
520 printf("line %3d %s %s",
521 n
->ln
, n
->fn
->name
, s
);
524 sr_mesg(stdout
, v
, q
->fld_width
[j
] == MTYPE
);
526 if (j
== q
->nflds
- 1)
529 if (!(verbose
&4)) printf("\n");
532 printf("\t%s queue %d (", a
, eval(n
->lft
));
535 printf("%s)\n", Buf
);
542 { int cnt
= 1; Lextok
*n
;
545 for (n
= Mtype
; n
&& j
; n
= n
->rgt
, cnt
++)
547 { if(strlen(n
->lft
->sym
->name
) >= sizeof(lbuf
))
548 { non_fatal("mtype name %s too long", n
->lft
->sym
->name
);
551 sprintf(lbuf
, "%s", n
->lft
->sym
->name
);
555 sprintf(lbuf
, "%d", v
);
560 sr_mesg(FILE *fd
, int v
, int j
)
567 doq(Symbol
*s
, int n
, RunList
*r
)
571 if (!s
->val
) /* uninitialized queue */
573 for (q
= qtab
; q
; q
= q
->nxt
)
574 if (q
->qid
== s
->val
[n
])
580 continue; /* rv q always empty */
581 printf("\t\tqueue %d (", q
->qid
);
583 printf("%s(%d):", r
->n
->name
, r
->pid
- Have_claim
);
585 printf("%s[%d]): ", s
->name
, n
);
587 printf("%s): ", s
->name
);
588 for (k
= 0; k
< q
->qlen
; k
++)
590 for (j
= 0; j
< q
->nflds
; j
++)
591 { if (j
> 0) printf(",");
592 sr_mesg(stdout
, q
->contents
[k
*q
->nflds
+j
],
593 q
->fld_width
[j
] == MTYPE
);
603 nochan_manip(Lextok
*p
, Lextok
*n
, int d
)
606 if (d
== 0 && p
->sym
&& p
->sym
->type
== CHAN
)
607 { setaccess(p
->sym
, ZS
, 0, 'L');
609 if (n
&& n
->ntyp
== CONST
)
610 fatal("invalid asgn to chan", (char *) 0);
612 if (n
&& n
->sym
&& n
->sym
->type
== CHAN
)
613 { setaccess(n
->sym
, ZS
, 0, 'V');
618 if (!n
|| n
->ntyp
== LEN
|| n
->ntyp
== RUN
)
621 if (n
->sym
&& n
->sym
->type
== CHAN
)
623 fatal("invalid use of chan name", (char *) 0);
625 setaccess(n
->sym
, ZS
, 0, 'V');
630 e
= 0; /* array index or struct element */
632 nochan_manip(p
, n
->lft
, e
);
633 nochan_manip(p
, n
->rgt
, 1);
637 no_internals(Lextok
*n
)
646 if ((strlen(sp
) == strlen("_nr_pr") && strcmp(sp
, "_nr_pr") == 0)
647 || (strlen(sp
) == strlen("_p") && strcmp(sp
, "_p") == 0))
648 { fatal("attempt to assign value to system variable %s", sp
);
This page took 0.044203 seconds and 4 git commands to generate.