1 /***** spin: run.c *****/
2
3 /*
4 * This file is part of the public release of Spin. It is subject to the
5 * terms in the LICENSE file that is included in this source directory.
6 * Tool documentation is available at http://spinroot.com
7 */
8
9 #include <stdlib.h>
10 #include "spin.h"
11 #include "y.tab.h"
12
13 extern RunList *X_lst, *run_lst;
14 extern Symbol *Fname;
15 extern Element *LastStep;
16 extern int Rvous, lineno, Tval, interactive, MadeChoice, Priority_Sum;
17 extern int TstOnly, verbose, s_trail, xspin, jumpsteps, depth;
18 extern int analyze, nproc, nstop, no_print, like_java, old_priority_rules;
19 extern short Have_claim;
20
21 static long Seed = 1;
22 static int E_Check = 0, Escape_Check = 0;
23
24 static int eval_sync(Element *);
25 static int pc_enabled(Lextok *n);
26 static int get_priority(Lextok *n);
27 static void set_priority(Lextok *n, Lextok *m);
28 extern void sr_buf(int, int, const char *);
29
30 void
Srand(unsigned int s)31 Srand(unsigned int s)
32 { Seed = s;
33 }
34
35 long
Rand(void)36 Rand(void)
37 { /* CACM 31(10), Oct 1988 */
38 Seed = 16807*(Seed%127773) - 2836*(Seed/127773);
39 if (Seed <= 0) Seed += 2147483647;
40 return Seed;
41 }
42
43 Element *
rev_escape(SeqList * e)44 rev_escape(SeqList *e)
45 { Element *r = (Element *) 0;
46
47 if (e)
48 { if ((r = rev_escape(e->nxt)) == ZE) /* reversed order */
49 { r = eval_sub(e->this->frst);
50 } }
51
52 return r;
53 }
54
55 Element *
eval_sub(Element * e)56 eval_sub(Element *e)
57 { Element *f, *g;
58 SeqList *z;
59 int i, j, k, only_pos;
60
61 if (!e || !e->n)
62 return ZE;
63 #ifdef DEBUG
64 printf("\n\teval_sub(%d %s: line %d) ",
65 e->Seqno, e->esc?"+esc":"", e->n?e->n->ln:0);
66 comment(stdout, e->n, 0);
67 printf("\n");
68 #endif
69 if (e->n->ntyp == GOTO)
70 { if (Rvous) return ZE;
71 LastStep = e;
72 f = get_lab(e->n, 1);
73 f = huntele(f, e->status, -1); /* 5.2.3: was missing */
74 cross_dsteps(e->n, f->n);
75 #ifdef DEBUG
76 printf("GOTO leads to %d\n", f->seqno);
77 #endif
78 return f;
79 }
80 if (e->n->ntyp == UNLESS)
81 { /* escapes were distributed into sequence */
82 return eval_sub(e->sub->this->frst);
83 } else if (e->sub) /* true for IF, DO, and UNLESS */
84 { Element *has_else = ZE;
85 Element *bas_else = ZE;
86 int nr_else = 0, nr_choices = 0;
87 only_pos = -1;
88
89 if (interactive
90 && !MadeChoice && !E_Check
91 && !Escape_Check
92 && !(e->status&(D_ATOM))
93 && depth >= jumpsteps)
94 { printf("Select stmnt (");
95 whoruns(0); printf(")\n");
96 if (nproc-nstop > 1)
97 { printf("\tchoice 0: other process\n");
98 nr_choices++;
99 only_pos = 0;
100 } }
101 for (z = e->sub, j=0; z; z = z->nxt)
102 { j++;
103 if (interactive
104 && !MadeChoice && !E_Check
105 && !Escape_Check
106 && !(e->status&(D_ATOM))
107 && depth >= jumpsteps
108 && z->this->frst
109 && (xspin || (verbose&32) || Enabled0(z->this->frst)))
110 { if (z->this->frst->n->ntyp == ELSE)
111 { has_else = (Rvous)?ZE:z->this->frst->nxt;
112 nr_else = j;
113 continue;
114 }
115 printf("\tchoice %d: ", j);
116 #if 0
117 if (z->this->frst->n)
118 printf("line %d, ", z->this->frst->n->ln);
119 #endif
120 if (!Enabled0(z->this->frst))
121 printf("unexecutable, ");
122 else
123 { nr_choices++;
124 only_pos = j;
125 }
126 comment(stdout, z->this->frst->n, 0);
127 printf("\n");
128 } }
129
130 if (nr_choices == 0 && has_else)
131 { printf("\tchoice %d: (else)\n", nr_else);
132 only_pos = nr_else;
133 }
134
135 if (nr_choices <= 1 && only_pos != -1 && !MadeChoice)
136 { MadeChoice = only_pos;
137 }
138
139 if (interactive && depth >= jumpsteps
140 && !Escape_Check
141 && !(e->status&(D_ATOM))
142 && !E_Check)
143 { if (!MadeChoice)
144 { char buf[256];
145 if (xspin)
146 printf("Make Selection %d\n\n", j);
147 else
148 printf("Select [0-%d]: ", j);
149 fflush(stdout);
150 if (scanf("%64s", buf) <= 0)
151 { printf("no input\n");
152 return ZE;
153 }
154 if (isdigit((int)buf[0]))
155 k = atoi(buf);
156 else
157 { if (buf[0] == 'q')
158 alldone(0);
159 k = -1;
160 }
161 } else
162 { k = MadeChoice;
163 MadeChoice = 0;
164 }
165 if (k < 1 || k > j)
166 { if (k != 0) printf("\tchoice outside range\n");
167 return ZE;
168 }
169 k--;
170 } else
171 { if (e->n && e->n->indstep >= 0)
172 k = 0; /* select 1st executable guard */
173 else
174 k = Rand()%j; /* nondeterminism */
175 }
176
177 has_else = ZE;
178 bas_else = ZE;
179 for (i = 0, z = e->sub; i < j+k; i++)
180 { if (z->this->frst
181 && z->this->frst->n->ntyp == ELSE)
182 { bas_else = z->this->frst;
183 has_else = (Rvous)?ZE:bas_else->nxt;
184 if (!interactive || depth < jumpsteps
185 || Escape_Check
186 || (e->status&(D_ATOM)))
187 { z = (z->nxt)?z->nxt:e->sub;
188 continue;
189 }
190 }
191 if (z->this->frst
192 && ((z->this->frst->n->ntyp == ATOMIC
193 || z->this->frst->n->ntyp == D_STEP)
194 && z->this->frst->n->sl->this->frst->n->ntyp == ELSE))
195 { bas_else = z->this->frst->n->sl->this->frst;
196 has_else = (Rvous)?ZE:bas_else->nxt;
197 if (!interactive || depth < jumpsteps
198 || Escape_Check
199 || (e->status&(D_ATOM)))
200 { z = (z->nxt)?z->nxt:e->sub;
201 continue;
202 }
203 }
204 if (i >= k)
205 { if ((f = eval_sub(z->this->frst)) != ZE)
206 return f;
207 else if (interactive && depth >= jumpsteps
208 && !(e->status&(D_ATOM)))
209 { if (!E_Check && !Escape_Check)
210 printf("\tunexecutable\n");
211 return ZE;
212 } }
213 z = (z->nxt)?z->nxt:e->sub;
214 }
215 LastStep = bas_else;
216 return has_else;
217 } else
218 { if (e->n->ntyp == ATOMIC
219 || e->n->ntyp == D_STEP)
220 { f = e->n->sl->this->frst;
221 g = e->n->sl->this->last;
222 g->nxt = e->nxt;
223 if (!(g = eval_sub(f))) /* atomic guard */
224 return ZE;
225 return g;
226 } else if (e->n->ntyp == NON_ATOMIC)
227 { f = e->n->sl->this->frst;
228 g = e->n->sl->this->last;
229 g->nxt = e->nxt; /* close it */
230 return eval_sub(f);
231 } else if (e->n->ntyp == '.')
232 { if (!Rvous) return e->nxt;
233 return eval_sub(e->nxt);
234 } else
235 { SeqList *x;
236 if (!(e->status & (D_ATOM))
237 && e->esc && (verbose&32))
238 { printf("Stmnt [");
239 comment(stdout, e->n, 0);
240 printf("] has escape(s): ");
241 for (x = e->esc; x; x = x->nxt)
242 { printf("[");
243 g = x->this->frst;
244 if (g->n->ntyp == ATOMIC
245 || g->n->ntyp == NON_ATOMIC)
246 g = g->n->sl->this->frst;
247 comment(stdout, g->n, 0);
248 printf("] ");
249 }
250 printf("\n");
251 }
252 #if 0
253 if (!(e->status & D_ATOM)) /* escapes don't reach inside d_steps */
254 /* 4.2.4: only the guard of a d_step can have an escape */
255 #endif
256 #if 1
257 if (!s_trail) /* trail determines selections, new 5.2.5 */
258 #endif
259 { Escape_Check++;
260 if (like_java)
261 { if ((g = rev_escape(e->esc)) != ZE)
262 { if (verbose&4)
263 { printf("\tEscape taken (-J) ");
264 if (g->n && g->n->fn)
265 printf("%s:%d", g->n->fn->name, g->n->ln);
266 printf("\n");
267 }
268 Escape_Check--;
269 return g;
270 }
271 } else
272 { for (x = e->esc; x; x = x->nxt)
273 { if ((g = eval_sub(x->this->frst)) != ZE)
274 { if (verbose&4)
275 { printf("\tEscape taken ");
276 if (g->n && g->n->fn)
277 printf("%s:%d", g->n->fn->name, g->n->ln);
278 printf("\n");
279 }
280 Escape_Check--;
281 return g;
282 } } }
283 Escape_Check--;
284 }
285 switch (e->n->ntyp) {
286 case ASGN:
287 if (check_track(e->n) == STRUCT) { break; }
288 /* else fall thru */
289 case TIMEOUT: case RUN:
290 case PRINT: case PRINTM:
291 case C_CODE: case C_EXPR:
292 case ASSERT:
293 case 's': case 'r': case 'c':
294 /* toplevel statements only */
295 LastStep = e;
296 default:
297 break;
298 }
299 if (Rvous)
300 {
301 return (eval_sync(e))?e->nxt:ZE;
302 }
303 return (eval(e->n))?e->nxt:ZE;
304 }
305 }
306 return ZE; /* not reached */
307 }
308
309 static int
eval_sync(Element * e)310 eval_sync(Element *e)
311 { /* allow only synchronous receives
312 and related node types */
313 Lextok *now = (e)?e->n:ZN;
314
315 if (!now
316 || now->ntyp != 'r'
317 || now->val >= 2 /* no rv with a poll */
318 || !q_is_sync(now))
319 {
320 return 0;
321 }
322
323 LastStep = e;
324 return eval(now);
325 }
326
327 static int
assign(Lextok * now)328 assign(Lextok *now)
329 { int t;
330
331 if (TstOnly) return 1;
332
333 switch (now->rgt->ntyp) {
334 case FULL: case NFULL:
335 case EMPTY: case NEMPTY:
336 case RUN: case LEN:
337 t = BYTE;
338 break;
339 default:
340 t = Sym_typ(now->rgt);
341 break;
342 }
343 typ_ck(Sym_typ(now->lft), t, "assignment");
344
345 return setval(now->lft, eval(now->rgt));
346 }
347
348 static int
nonprogress(void)349 nonprogress(void) /* np_ */
350 { RunList *r;
351
352 for (r = run_lst; r; r = r->nxt)
353 { if (has_lab(r->pc, 4)) /* 4=progress */
354 return 0;
355 }
356 return 1;
357 }
358
359 int
eval(Lextok * now)360 eval(Lextok *now)
361 { int temp;
362
363 if (now) {
364 lineno = now->ln;
365 Fname = now->fn;
366 #ifdef DEBUG
367 printf("eval ");
368 comment(stdout, now, 0);
369 printf("\n");
370 #endif
371 switch (now->ntyp) {
372 case CONST: return now->val;
373 case '!': return !eval(now->lft);
374 case UMIN: return -eval(now->lft);
375 case '~': return ~eval(now->lft);
376
377 case '/': temp = eval(now->rgt);
378 if (temp == 0)
379 { fatal("division by zero", (char *) 0);
380 }
381 return (eval(now->lft) / temp);
382 case '*': return (eval(now->lft) * eval(now->rgt));
383 case '-': return (eval(now->lft) - eval(now->rgt));
384 case '+': return (eval(now->lft) + eval(now->rgt));
385 case '%': temp = eval(now->rgt);
386 if (temp == 0)
387 { fatal("taking modulo of zero", (char *) 0);
388 }
389 return (eval(now->lft) % temp);
390 case LT: return (eval(now->lft) < eval(now->rgt));
391 case GT: return (eval(now->lft) > eval(now->rgt));
392 case '&': return (eval(now->lft) & eval(now->rgt));
393 case '^': return (eval(now->lft) ^ eval(now->rgt));
394 case '|': return (eval(now->lft) | eval(now->rgt));
395 case LE: return (eval(now->lft) <= eval(now->rgt));
396 case GE: return (eval(now->lft) >= eval(now->rgt));
397 case NE: return (eval(now->lft) != eval(now->rgt));
398 case EQ: return (eval(now->lft) == eval(now->rgt));
399 case OR: return (eval(now->lft) || eval(now->rgt));
400 case AND: return (eval(now->lft) && eval(now->rgt));
401 case LSHIFT: return (eval(now->lft) << eval(now->rgt));
402 case RSHIFT: return (eval(now->lft) >> eval(now->rgt));
403 case '?': return (eval(now->lft) ? eval(now->rgt->lft)
404 : eval(now->rgt->rgt));
405
406 case 'p': return remotevar(now); /* _p for remote reference */
407 case 'q': return remotelab(now);
408 case 'R': return qrecv(now, 0); /* test only */
409 case LEN: return qlen(now);
410 case FULL: return (qfull(now));
411 case EMPTY: return (qlen(now)==0);
412 case NFULL: return (!qfull(now));
413 case NEMPTY: return (qlen(now)>0);
414 case ENABLED: if (s_trail) return 1;
415 return pc_enabled(now->lft);
416
417 case GET_P: return get_priority(now->lft);
418 case SET_P: set_priority(now->lft->lft, now->lft->rgt); return 1;
419
420 case EVAL: if (now->lft->ntyp == ',')
421 { Lextok *fix = now->lft;
422 do { /* new */
423 if (eval(fix->lft) == 0) /* usertype6 */
424 { return 0;
425 }
426 fix = fix->rgt;
427 } while (fix && fix->ntyp == ',');
428 return 1;
429 }
430 return eval(now->lft);
431
432 case PC_VAL: return pc_value(now->lft);
433 case NONPROGRESS: return nonprogress();
434 case NAME: return getval(now);
435
436 case TIMEOUT: return Tval;
437 case RUN: return TstOnly?1:enable(now);
438
439 case 's': return qsend(now); /* send */
440 case 'r': return qrecv(now, 1); /* receive or poll */
441 case 'c': return eval(now->lft); /* condition */
442 case PRINT: return TstOnly?1:interprint(stdout, now);
443 case PRINTM: return TstOnly?1:printm(stdout, now);
444 case ASGN:
445 if (check_track(now) == STRUCT) { return 1; }
446 return assign(now);
447
448 case C_CODE: if (!analyze)
449 { printf("%s:\t", now->sym->name);
450 plunk_inline(stdout, now->sym->name, 0, 1);
451 }
452 return 1; /* uninterpreted */
453
454 case C_EXPR: if (!analyze)
455 { printf("%s:\t", now->sym->name);
456 plunk_expr(stdout, now->sym->name);
457 printf("\n");
458 }
459 return 1; /* uninterpreted */
460
461 case ASSERT: if (TstOnly || eval(now->lft)) return 1;
462 non_fatal("assertion violated", (char *) 0);
463 printf("spin: text of failed assertion: assert(");
464 comment(stdout, now->lft, 0);
465 printf(")\n");
466 if (s_trail && !xspin) return 1;
467 wrapup(1); /* doesn't return */
468
469 case IF: case DO: case BREAK: case UNLESS: /* compound */
470 case '.': return 1; /* return label for compound */
471 case '@': return 0; /* stop state */
472 case ELSE: return 1; /* only hit here in guided trails */
473
474 case ',': /* reached through option -A with array initializer */
475 case 0:
476 return 0; /* not great, but safe */
477
478 default : printf("spin: bad node type %d (run)\n", now->ntyp);
479 if (s_trail) printf("spin: trail file doesn't match spec?\n");
480 fatal("aborting", 0);
481 }}
482 return 0;
483 }
484
485 int
printm(FILE * fd,Lextok * n)486 printm(FILE *fd, Lextok *n)
487 { extern char GBuf[];
488 char *s = 0;
489 int j;
490
491 GBuf[0] = '\0';
492 if (!no_print)
493 if (!s_trail || depth >= jumpsteps)
494 {
495 if (n->lft->sym
496 && n->lft->sym->mtype_name)
497 { s = n->lft->sym->mtype_name->name;
498 }
499
500 if (n->lft->ismtyp)
501 { j = n->lft->val;
502 } else /* constant */
503 { j = eval(n->lft);
504 }
505 sr_buf(j, 1, s);
506 dotag(fd, GBuf);
507 }
508 return 1;
509 }
510
511 int
interprint(FILE * fd,Lextok * n)512 interprint(FILE *fd, Lextok *n)
513 { Lextok *tmp = n->lft;
514 char c, *s = n->sym->name, *t = 0;
515 int i, j; char lbuf[512]; /* matches value in sr_buf() */
516 extern char GBuf[]; /* global, size 4096 */
517 char tBuf[4096]; /* match size of global GBuf[] */
518
519 GBuf[0] = '\0';
520 if (!no_print)
521 if (!s_trail || depth >= jumpsteps) {
522 for (i = 0; i < (int) strlen(s); i++)
523 switch (s[i]) {
524 case '\"': break; /* ignore */
525 case '\\':
526 switch(s[++i]) {
527 case 't': strcat(GBuf, "\t"); break;
528 case 'n': strcat(GBuf, "\n"); break;
529 default: goto onechar;
530 }
531 break;
532 case '%':
533 if ((c = s[++i]) == '%')
534 { strcat(GBuf, "%"); /* literal */
535 break;
536 }
537 if (!tmp)
538 { non_fatal("too few print args %s", s);
539 break;
540 }
541 j = eval(tmp->lft);
542
543 if (c == 'e'
544 && tmp->lft
545 && tmp->lft->sym
546 && tmp->lft->sym->mtype_name)
547 { t = tmp->lft->sym->mtype_name->name;
548 }
549
550 tmp = tmp->rgt;
551 switch(c) {
552 case 'c': sprintf(lbuf, "%c", j); break;
553 case 'd': sprintf(lbuf, "%d", j); break;
554
555 case 'e': strcpy(tBuf, GBuf); /* event name */
556 GBuf[0] = '\0';
557
558 sr_buf(j, 1, t);
559
560 strcpy(lbuf, GBuf);
561 strcpy(GBuf, tBuf);
562 break;
563
564 case 'o': sprintf(lbuf, "%o", j); break;
565 case 'u': sprintf(lbuf, "%u", (unsigned) j); break;
566 case 'x': sprintf(lbuf, "%x", j); break;
567 default: non_fatal("bad print cmd: '%s'", &s[i-1]);
568 lbuf[0] = '\0'; break;
569 }
570 goto append;
571 default:
572 onechar: lbuf[0] = s[i]; lbuf[1] = '\0';
573 append: strcat(GBuf, lbuf);
574 break;
575 }
576 dotag(fd, GBuf);
577 }
578 if (strlen(GBuf) >= 4096) fatal("printf string too long", 0);
579 return 1;
580 }
581
582 static int
Enabled1(Lextok * n)583 Enabled1(Lextok *n)
584 { int i; int v = verbose;
585
586 if (n)
587 switch (n->ntyp) {
588 case 'c':
589 if (has_typ(n->lft, RUN))
590 return 1; /* conservative */
591 /* else fall through */
592 default: /* side-effect free */
593 verbose = 0;
594 E_Check++;
595 i = eval(n);
596 E_Check--;
597 verbose = v;
598 return i;
599
600 case SET_P:
601 case C_CODE: case C_EXPR:
602 case PRINT: case PRINTM:
603 case ASGN: case ASSERT:
604 return 1;
605
606 case 's':
607 if (q_is_sync(n))
608 { if (Rvous) return 0;
609 TstOnly = 1; verbose = 0;
610 E_Check++;
611 i = eval(n);
612 E_Check--;
613 TstOnly = 0; verbose = v;
614 return i;
615 }
616 return (!qfull(n));
617 case 'r':
618 if (q_is_sync(n))
619 return 0; /* it's never a user-choice */
620 n->ntyp = 'R'; verbose = 0;
621 E_Check++;
622 i = eval(n);
623 E_Check--;
624 n->ntyp = 'r'; verbose = v;
625 return i;
626 }
627 return 0;
628 }
629
630 int
Enabled0(Element * e)631 Enabled0(Element *e)
632 { SeqList *z;
633
634 if (!e || !e->n)
635 return 0;
636
637 switch (e->n->ntyp) {
638 case '@':
639 return X_lst->pid == (nproc-nstop-1);
640 case '.':
641 case SET_P:
642 return 1;
643 case GOTO:
644 if (Rvous) return 0;
645 return 1;
646 case UNLESS:
647 return Enabled0(e->sub->this->frst);
648 case ATOMIC:
649 case D_STEP:
650 case NON_ATOMIC:
651 return Enabled0(e->n->sl->this->frst);
652 }
653 if (e->sub) /* true for IF, DO, and UNLESS */
654 { for (z = e->sub; z; z = z->nxt)
655 if (Enabled0(z->this->frst))
656 return 1;
657 return 0;
658 }
659 for (z = e->esc; z; z = z->nxt)
660 { if (Enabled0(z->this->frst))
661 return 1;
662 }
663 #if 0
664 printf("enabled1 ");
665 comment(stdout, e->n, 0);
666 printf(" ==> %s\n", Enabled1(e->n)?"yes":"nope");
667 #endif
668 return Enabled1(e->n);
669 }
670
671 int
pc_enabled(Lextok * n)672 pc_enabled(Lextok *n)
673 { int i = nproc - nstop;
674 int pid = eval(n);
675 int result = 0;
676 RunList *Y, *oX;
677
678 if (pid == X_lst->pid)
679 fatal("used: enabled(pid=thisproc) [%s]", X_lst->n->name);
680
681 for (Y = run_lst; Y; Y = Y->nxt)
682 if (--i == pid)
683 { oX = X_lst; X_lst = Y;
684 result = Enabled0(X_lst->pc);
685 X_lst = oX;
686 break;
687 }
688 return result;
689 }
690
691 int
pc_highest(Lextok * n)692 pc_highest(Lextok *n)
693 { int i = nproc - nstop;
694 int pid = eval(n);
695 int target = 0, result = 1;
696 RunList *Y, *oX;
697
698 if (X_lst->prov && !eval(X_lst->prov))
699 { return 0; /* can't be highest unless fully enabled */
700 }
701
702 for (Y = run_lst; Y; Y = Y->nxt)
703 { if (--i == pid)
704 { target = Y->priority;
705 break;
706 } }
707 if (0) printf("highest for pid %d @ priority = %d\n", pid, target);
708
709 oX = X_lst;
710 i = nproc - nstop;
711 for (Y = run_lst; Y; Y = Y->nxt)
712 { i--;
713 if (0) printf(" pid %d @ priority %d\t", Y->pid, Y->priority);
714 if (Y->priority > target)
715 { X_lst = Y;
716 if (0) printf("enabled: %s\n", Enabled0(X_lst->pc)?"yes":"nope");
717 if (0) printf("provided: %s\n", eval(X_lst->prov)?"yes":"nope");
718 if (Enabled0(X_lst->pc) && (!X_lst->prov || eval(X_lst->prov)))
719 { result = 0;
720 break;
721 } }
722 else
723 if (0) printf("\n");
724 }
725 X_lst = oX;
726
727 return result;
728 }
729
730 int
get_priority(Lextok * n)731 get_priority(Lextok *n)
732 { int i = nproc - nstop;
733 int pid = eval(n);
734 RunList *Y;
735
736 if (old_priority_rules)
737 { return 1;
738 }
739
740 for (Y = run_lst; Y; Y = Y->nxt)
741 { if (--i == pid)
742 { return Y->priority;
743 } }
744 return 0;
745 }
746
747 void
set_priority(Lextok * n,Lextok * p)748 set_priority(Lextok *n, Lextok *p)
749 { int i = nproc - nstop - Have_claim;
750 int pid = eval(n);
751 RunList *Y;
752
753 if (old_priority_rules)
754 { return;
755 }
756 for (Y = run_lst; Y; Y = Y->nxt)
757 { if (--i == pid)
758 { Priority_Sum -= Y->priority;
759 Y->priority = eval(p);
760 Priority_Sum += Y->priority;
761 if (1)
762 { printf("%3d: setting priority of proc %d (%s) to %d\n",
763 depth, pid, Y->n->name, Y->priority);
764 } } }
765 if (verbose&32)
766 { printf("\tPid\tName\tPriority\n");
767 for (Y = run_lst; Y; Y = Y->nxt)
768 { printf("\t%d\t%s\t%d\n",
769 Y->pid,
770 Y->n->name,
771 Y->priority);
772 } }
773 }
774