1 /***** spin: sched.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 extern int verbose
, s_trail
, analyze
, no_wrapup
;
17 extern char *claimproc
, *eventmap
, Buf
[];
18 extern Ordered
*all_names
;
19 extern Symbol
*Fname
, *context
;
20 extern int lineno
, nr_errs
, dumptab
, xspin
, jumpsteps
, columns
;
21 extern int u_sync
, Elcnt
, interactive
, TstOnly
, cutoff
;
22 extern short has_enabled
;
23 extern int limited_vis
;
25 RunList
*X
= (RunList
*) 0;
26 RunList
*run
= (RunList
*) 0;
27 RunList
*LastX
= (RunList
*) 0; /* previous executing proc */
28 ProcList
*rdy
= (ProcList
*) 0;
29 Element
*LastStep
= ZE
;
30 int nproc
=0, nstop
=0, Tval
=0;
31 int Rvous
=0, depth
=0, nrRdy
=0, MadeChoice
;
32 short Have_claim
=0, Skip_claim
=0;
34 static int Priority_Sum
= 0;
35 static void setlocals(RunList
*);
36 static void setparams(RunList
*, ProcList
*, Lextok
*);
37 static void talk(RunList
*);
40 runnable(ProcList
*p
, int weight
, int noparams
)
41 { RunList
*r
= (RunList
*) emalloc(sizeof(RunList
));
45 r
->pid
= nproc
++ - nstop
+ Skip_claim
;
47 if ((verbose
&4) || (verbose
&32))
48 printf("Starting %s with pid %d\n",
49 p
->n
?p
->n
->name
:"--", r
->pid
);
52 fatal("parsing error, no sequence %s",
53 p
->n
?p
->n
->name
:"--");
55 r
->pc
= huntele(p
->s
->frst
, p
->s
->frst
->status
, -1);
59 p
->s
->last
->status
|= ENDSTATE
; /* normal end state */
64 if (noparams
) setlocals(r
);
65 Priority_Sum
+= weight
;
70 ready(Symbol
*n
, Lextok
*p
, Sequence
*s
, int det
, Lextok
*prov
)
71 /* n=name, p=formals, s=body det=deterministic prov=provided */
72 { ProcList
*r
= (ProcList
*) emalloc(sizeof(ProcList
));
73 Lextok
*fp
, *fpt
; int j
; extern int Npars
;
80 if (det
!= 0 && det
!= 1)
81 { fprintf(stderr
, "spin: bad value for det (cannot happen)\n");
87 for (fp
= p
, j
= 0; fp
; fp
= fp
->rgt
)
88 for (fpt
= fp
->lft
; fpt
; fpt
= fpt
->rgt
)
89 j
++; /* count # of parameters */
90 Npars
= max(Npars
, j
);
99 for (p
= rdy
; p
; p
= p
->nxt
)
101 return p
->s
->maxel
++;
111 for (p
= rdy
; p
; p
= p
->nxt
)
112 { if (!p
->p
) continue;
114 for (f
= p
->p
; f
; f
= f
->rgt
) /* types */
115 for (t
= f
->lft
; t
; t
= t
->rgt
) /* formals */
116 { if (t
->ntyp
!= ',')
117 t
->sym
->Nid
= cnt
--; /* overload Nid */
119 t
->lft
->sym
->Nid
= cnt
--;
132 { sprintf(Buf
, "%d:%s",
133 run
->pid
- Have_claim
, run
->n
->name
);
134 pstext(run
->pid
- Have_claim
, Buf
);
136 printf("proc %d = %s\n",
137 run
->pid
- Have_claim
, run
->n
->name
);
148 printf(" 0: proc - (%s) ", w
);
151 printf("creates proc %2d (%s)",
152 run
->pid
- Have_claim
,
154 if (run
->priority
> 1)
155 printf(" priority %d", run
->priority
);
160 #define MAXP 255 /* matches max nr of processes in verifier */
166 Symbol
*s
= m
->sym
; /* proctype name */
167 Lextok
*n
= m
->lft
; /* actual parameters */
169 if (m
->val
< 1) m
->val
= 1; /* minimum priority */
170 for (p
= rdy
; p
; p
= p
->nxt
)
171 if (strcmp(s
->name
, p
->n
->name
) == 0)
172 { if (nproc
-nstop
>= MAXP
)
173 { printf("spin: too many processes (%d max)\n", MAXP
);
176 runnable(p
, m
->val
, 0);
177 announce((char *) 0);
178 setparams(run
, p
, n
);
179 setlocals(run
); /* after setparams */
180 return run
->pid
- Have_claim
+ Skip_claim
; /* effective simu pid */
182 return 0; /* process not found */
186 check_param_count(int i
, Lextok
*m
)
188 Symbol
*s
= m
->sym
; /* proctype name */
189 Lextok
*f
, *t
; /* formal pars */
192 for (p
= rdy
; p
; p
= p
->nxt
)
193 { if (strcmp(s
->name
, p
->n
->name
) == 0)
194 { if (m
->lft
) /* actual param list */
195 { lineno
= m
->lft
->ln
;
198 for (f
= p
->p
; f
; f
= f
->rgt
) /* one type at a time */
199 for (t
= f
->lft
; t
; t
= t
->rgt
) /* count formal params */
203 { printf("spin: saw %d parameters, expected %d\n", i
, cnt
);
204 non_fatal("wrong number of parameters", "");
213 RunList
*r
, *q
= (RunList
*) 0;
215 for (p
= rdy
; p
; p
= p
->nxt
)
217 && strcmp(p
->n
->name
, ":never:") == 0)
221 printf("spin: couldn't find claim (ignored)\n");
225 /* move claim to far end of runlist, and reassign it pid 0 */
228 pstext(0, "0::never:");
229 for (r
= run
; r
; r
= r
->nxt
)
230 { if (!strcmp(r
->n
->name
, ":never:"))
232 sprintf(Buf
, "%d:%s",
233 r
->pid
+1, r
->n
->name
);
234 pstext(r
->pid
+1, Buf
);
237 if (run
->pid
== 0) return; /* it is the first process started */
239 q
= run
; run
= run
->nxt
;
240 q
->pid
= 0; q
->nxt
= (RunList
*) 0; /* remove */
243 for (r
= run
; r
; r
= r
->nxt
)
244 { r
->pid
= r
->pid
+Have_claim
; /* adjust */
256 for (r
= run
; r
; r
= r
->nxt
)
257 if (strcmp(n
, r
->n
->name
) == 0)
259 { printf("spin: remote ref to proctype %s, ", n
);
260 printf("has more than one match: %d and %d\n",
273 { extern void putpostlude(void);
274 if (columns
== 2) putpostlude();
276 printf("-------------\nfinal state:\n-------------\n");
282 printf("#processes: %d\n", nproc
-nstop
- Have_claim
+ Skip_claim
);
286 verbose
&= ~1; /* no more globals */
287 verbose
|= 32; /* add process states */
288 for (X
= run
; X
; X
= X
->nxt
)
290 verbose
= ov
; /* restore */
292 printf("%d process%s created\n",
293 nproc
- Have_claim
+ Skip_claim
,
294 (xspin
|| nproc
!=1)?"es":"");
296 if (xspin
) alldone(0); /* avoid an abort from xspin */
297 if (fini
) alldone(1);
300 static char is_blocked
[256];
306 is_blocked
[p
%256] = 1;
307 for (i
= j
= 0; i
< nproc
- nstop
; i
++)
309 if (j
>= nproc
- nstop
)
310 { memset(is_blocked
, 0, 256);
317 silent_moves(Element
*e
)
321 switch (e
->n
->ntyp
) {
324 f
= get_lab(e
->n
, 1);
325 cross_dsteps(e
->n
, f
->n
);
326 return f
; /* guard against goto cycles */
328 return silent_moves(e
->sub
->this->frst
);
332 e
->n
->sl
->this->last
->nxt
= e
->nxt
;
333 return silent_moves(e
->n
->sl
->this->frst
);
335 return silent_moves(e
->nxt
);
342 { SeqList
*z
; Element
*has_else
;
344 int j
, k
, nr_else
= 0;
346 if (nproc
<= nstop
+1)
350 if (!interactive
|| depth
< jumpsteps
)
351 { /* was: j = (int) Rand()%(nproc-nstop); */
352 if (Priority_Sum
< nproc
-nstop
)
353 fatal("cannot happen - weights", (char *)0);
354 j
= (int) Rand()%Priority_Sum
;
356 while (j
- X
->priority
>= 0)
360 if (!X
) { Y
= NULL
; X
= run
; }
363 { int only_choice
= -1;
364 int no_choice
= 0, proc_no_ch
, proc_k
;
366 Tval
= 0; /* new 4.2.6 */
367 try_again
: printf("Select a statement\n");
368 try_more
: for (X
= run
, k
= 1; X
; X
= X
->nxt
)
369 { if (X
->pid
> 255) break;
371 Choices
[X
->pid
] = (short) k
;
374 || (X
->prov
&& !eval(X
->prov
)))
379 X
->pc
= silent_moves(X
->pc
);
380 if (!X
->pc
->sub
&& X
->pc
->n
)
382 unex
= !Enabled0(X
->pc
);
387 if (!xspin
&& unex
&& !(verbose
&32))
391 printf("\tchoice %d: ", k
++);
394 printf(" unexecutable,");
396 comment(stdout
, X
->pc
->n
, 0);
397 if (X
->pc
->esc
) printf(" + Escape");
401 proc_no_ch
= no_choice
;
403 for (z
= X
->pc
->sub
, j
=0; z
; z
= z
->nxt
)
404 { Element
*y
= silent_moves(z
->this->frst
);
408 if (y
->n
->ntyp
== ELSE
)
409 { has_else
= (Rvous
)?ZE
:y
;
419 if (!xspin
&& unex
&& !(verbose
&32))
423 printf("\tchoice %d: ", k
++);
426 printf(" unexecutable,");
428 comment(stdout
, y
->n
, 0);
432 { if (no_choice
-proc_no_ch
>= (k
-proc_k
)-1)
433 { only_choice
= nr_else
;
434 printf("\tchoice %d: ", nr_else
);
439 printf("\tchoice %d: ", nr_else
);
441 printf(" unexecutable, [else]\n");
445 if (k
- no_choice
< 2 && Tval
== 0)
447 no_choice
= 0; only_choice
= -1;
451 printf("Make Selection %d\n\n", k
-1);
453 { if (k
- no_choice
< 2)
454 { printf("no executable choices\n");
457 printf("Select [1-%d]: ", k
-1);
459 if (!xspin
&& k
- no_choice
== 2)
460 { printf("%d\n", only_choice
);
474 { printf("\tchoice is outside range\n");
479 for (X
= run
; X
; Y
= X
, X
= X
->nxt
)
482 || j
< Choices
[X
->nxt
->pid
])
484 MadeChoice
= 1+j
-Choices
[X
->pid
];
494 RunList
*Y
= NULL
; /* previous process in run queue */
496 int go
, notbeyond
= 0;
507 if (has_enabled
&& u_sync
> 0)
508 { printf("spin: error, cannot use 'enabled()' in ");
509 printf("models with synchronous channels.\n");
520 printf("warning: never claim not used in random simulation\n");
522 printf("warning: trace assertion not used in random simulation\n");
529 if (X
->pc
&& X
->pc
->n
)
530 { lineno
= X
->pc
->n
->ln
;
531 Fname
= X
->pc
->n
->fn
;
533 if (cutoff
> 0 && depth
>= cutoff
)
534 { printf("-------------\n");
535 printf("depth-limit (-u%d steps) reached\n", cutoff
);
539 if (xspin
&& !interactive
&& --bufmax
<= 0)
540 { int c
; /* avoid buffer overflow on pc's */
541 printf("spin: type return to proceed\n");
544 if (c
== 'q') wrapup(0);
548 depth
++; LastStep
= ZE
;
549 oX
= X
; /* a rendezvous could change it */
552 && !(X
->pc
->status
& D_ATOM
)
554 { if (!xspin
&& ((verbose
&32) || (verbose
&4)))
556 printf("\t<<Not Enabled>>\n");
560 if (go
&& (e
= eval_sub(X
->pc
)))
561 { if (depth
>= jumpsteps
562 && ((verbose
&32) || (verbose
&4)))
564 if (!(e
->status
& D_ATOM
) || (verbose
&32)) /* no talking in d_steps */
567 if (!LastStep
) LastStep
= X
->pc
;
568 comment(stdout
, LastStep
->n
, 0);
571 if (verbose
&1) dumpglobals();
572 if (verbose
&2) dumplocal(X
);
574 if (!(e
->status
& D_ATOM
))
579 || (X
->pc
->status
& (ATOM
|D_ATOM
))) /* new 5.0 */
580 { e
= silent_moves(e
);
583 oX
->pc
= e
; LastX
= X
;
585 if (!interactive
) Tval
= 0;
586 memset(is_blocked
, 0, 256);
588 if (X
->pc
&& (X
->pc
->status
& (ATOM
|L_ATOM
))
589 && (notbeyond
== 0 || oX
!= X
))
590 { if ((X
->pc
->status
& L_ATOM
))
592 continue; /* no process switch */
596 if (oX
->pc
&& (oX
->pc
->status
& D_ATOM
))
597 { non_fatal("stmnt in d_step blocks", (char *)0);
601 && X
->pc
->n
->ntyp
== '@'
602 && X
->pid
== (nproc
-nstop
-1))
603 { if (X
!= run
&& Y
!= NULL
)
608 Priority_Sum
-= X
->priority
;
611 dotag(stdout
, "terminates\n");
614 if (!interactive
) Tval
= 0;
615 if (nproc
== nstop
) break;
616 memset(is_blocked
, 0, 256);
617 /* proc X is no longer in runlist */
618 X
= (X
->nxt
) ? X
->nxt
: run
;
620 { if (p_blocked(X
->pid
))
623 if (depth
>= jumpsteps
)
625 X
= (RunList
*) 0; /* to suppress indent */
626 dotag(stdout
, "timeout\n");
630 if (!run
|| !X
) break; /* new 5.0 */
640 complete_rendez(void)
641 { RunList
*orun
= X
, *tmp
;
642 Element
*s_was
= LastStep
;
644 int j
, ointer
= interactive
;
648 if (orun
->pc
->status
& D_ATOM
)
649 fatal("rv-attempt in d_step sequence", (char *)0);
653 j
= (int) Rand()%Priority_Sum
; /* randomize start point */
655 while (j
- X
->priority
>= 0)
660 for (j
= nproc
- nstop
; j
> 0; j
--)
662 && (!X
->prov
|| eval(X
->prov
))
663 && (e
= eval_sub(X
->pc
)))
669 if ((verbose
&32) || (verbose
&4))
670 { tmp
= orun
; orun
= X
; X
= tmp
;
671 if (!s_was
) s_was
= X
->pc
;
674 comment(stdout
, s_was
->n
, 0);
676 tmp
= orun
; orun
= X
; X
= tmp
;
677 if (!LastStep
) LastStep
= X
->pc
;
680 comment(stdout
, LastStep
->n
, 0);
683 Rvous
= 0; /* before silent_moves */
684 X
->pc
= silent_moves(e
);
685 out
: interactive
= ointer
;
694 interactive
= ointer
;
698 /***** Runtime - Local Variables *****/
701 addsymbol(RunList
*r
, Symbol
*s
)
705 for (t
= r
->symtab
; t
; t
= t
->next
)
706 if (strcmp(t
->name
, s
->name
) == 0)
707 return; /* it's already there */
709 t
= (Symbol
*) emalloc(sizeof(Symbol
));
712 t
->hidden
= s
->hidden
;
718 if (s
->type
!= STRUCT
)
719 { if (s
->val
) /* if already initialized, copy info */
720 { t
->val
= (int *) emalloc(s
->nel
*sizeof(int));
721 for (i
= 0; i
< s
->nel
; i
++)
722 t
->val
[i
] = s
->val
[i
];
724 (void) checkvar(t
, 0); /* initialize it */
727 fatal("saw preinitialized struct %s", s
->name
);
731 /* t->context = r->n; */
733 t
->next
= r
->symtab
; /* add it */
738 setlocals(RunList
*r
)
744 for (walk
= all_names
; walk
; walk
= walk
->next
)
748 && strcmp(sp
->context
->name
, r
->n
->name
) == 0
750 && (sp
->type
== UNSIGNED
757 || sp
->type
== STRUCT
))
759 non_fatal("setlocals: cannot happen '%s'",
767 oneparam(RunList
*r
, Lextok
*t
, Lextok
*a
, ProcList
*p
)
772 fatal("missing actual parameters: '%s'", p
->n
->name
);
773 if (t
->sym
->nel
!= 1)
774 fatal("array in parameter list, %s", t
->sym
->name
);
777 at
= Sym_typ(a
->lft
);
778 X
= r
; /* switch context */
781 if (at
!= ft
&& (at
== CHAN
|| ft
== CHAN
))
782 { char buf
[256], tag1
[64], tag2
[64];
783 (void) sputtype(tag1
, ft
);
784 (void) sputtype(tag2
, at
);
785 sprintf(buf
, "type-clash in params of %s(..), (%s<-> %s)",
786 p
->n
->name
, tag1
, tag2
);
787 non_fatal("%s", buf
);
790 addsymbol(r
, t
->sym
);
797 setparams(RunList
*r
, ProcList
*p
, Lextok
*q
)
798 { Lextok
*f
, *a
; /* formal and actual pars */
799 Lextok
*t
; /* list of pars of 1 type */
805 for (f
= p
->p
, a
= q
; f
; f
= f
->rgt
) /* one type at a time */
806 for (t
= f
->lft
; t
; t
= t
->rgt
, a
= (a
)?a
->rgt
:a
)
807 { if (t
->ntyp
!= ',')
808 oneparam(r
, t
, a
, p
); /* plain var */
810 oneparam(r
, t
->lft
, a
, p
); /* expanded struct */
819 { /* fatal("error, cannot eval '%s' (no proc)", s->name); */
822 for (r
= X
->symtab
; r
; r
= r
->next
)
823 if (strcmp(r
->name
, s
->name
) == 0)
833 in_bound(Symbol
*r
, int n
)
837 if (n
>= r
->nel
|| n
< 0)
838 { printf("spin: indexing %s[%d] - size is %d\n",
840 non_fatal("indexing array \'%s\'", r
->name
);
848 { Symbol
*r
, *s
= sn
->sym
;
849 int n
= eval(sn
->lft
);
852 if (r
&& r
->type
== STRUCT
)
853 return Rval_struct(sn
, r
, 1); /* 1 = check init */
855 return cast_val(r
->type
, r
->val
[n
], r
->nbits
);
860 setlocal(Lextok
*p
, int m
)
861 { Symbol
*r
= findloc(p
->sym
);
862 int n
= eval(p
->lft
);
865 { if (r
->type
== STRUCT
)
866 (void) Lval_struct(p
, r
, 1, m
); /* 1 = check init */
871 m
= (m
& ((1<<r
->nbits
)-1));
874 r
->val
[n
] = cast_val(r
->type
, m
, r
->nbits
);
886 if (lnr
) printf("%3d: ", depth
);
888 if (Have_claim
&& X
->pid
== 0)
891 printf("%2d", X
->pid
- Have_claim
);
892 printf(" (%s) ", X
->n
->name
);
898 if ((verbose
&32) || (verbose
&4))
901 if (verbose
&1) dumpglobals();
902 if (verbose
&2) dumplocal(r
);
907 p_talk(Element
*e
, int lnr
)
908 { static int lastnever
= -1;
914 if (Have_claim
&& X
&& X
->pid
== 0
915 && lastnever
!= newnever
&& e
)
917 { printf("MSC: ~G line %d\n", newnever
);
919 printf("%3d: proc - (NEVER) line %d \"never\" ",
921 printf("(state 0)\t[printf('MSC: never\\\\n')]\n");
923 { printf("%3d: proc - (NEVER) line %d \"never\"\n",
927 lastnever
= newnever
;
932 { printf("line %3d %s (state %d)",
934 e
->n
?e
->n
->fn
->name
:"-",
937 && ((e
->status
&ENDSTATE
) || has_lab(e
, 2))) /* 2=end */
938 { printf(" <valid end state>");
949 if (n
->sym
->type
!= 0 && n
->sym
->type
!= LABEL
)
950 { printf("spin: error, type: %d\n", n
->sym
->type
);
951 fatal("not a labelname: '%s'", n
->sym
->name
);
954 { fatal("remote ref to label '%s' inside d_step",
957 if ((i
= find_lab(n
->sym
, n
->lft
->sym
, 1)) == 0)
958 fatal("unknown labelname: %s", n
->sym
->name
);
964 { int prno
, i
, added
=0;
973 prno
= f_pid(n
->lft
->sym
->name
);
975 { prno
= eval(n
->lft
->lft
); /* pid - can cause recursive call */
977 if (n
->lft
->lft
->ntyp
== CONST
) /* user-guessed pid */
979 { prno
+= Have_claim
;
984 return 0; /* non-existing process */
987 for (Y
= run
; Y
; Y
= Y
->nxt
)
989 printf(" %s: i=%d, prno=%d, ->pid=%d\n", Y
->n
->name
, i
, prno
, Y
->pid
);
993 for (Y
= run
; Y
; Y
= Y
->nxt
)
995 { if (strcmp(Y
->n
->name
, n
->lft
->sym
->name
) != 0)
996 { printf("spin: remote reference error on '%s[%d]'\n",
997 n
->lft
->sym
->name
, prno
-added
);
998 non_fatal("refers to wrong proctype '%s'", Y
->n
->name
);
1000 if (strcmp(n
->sym
->name
, "_p") == 0)
1002 return Y
->pc
->seqno
;
1003 /* harmless, can only happen with -t */
1007 /* new 4.0 allow remote variables */
1015 n
->sym
= findloc(n
->sym
);
1027 printf("remote ref: %s[%d] ", n
->lft
->sym
->name
, prno
-added
);
1028 non_fatal("%s not found", n
->sym
->name
);
1029 printf("have only:\n");
1030 i
= nproc
- nstop
- 1;
1031 for (Y
= run
; Y
; Y
= Y
->nxt
, i
--)
1032 if (!strcmp(Y
->n
->name
, n
->lft
->sym
->name
))
1033 printf("\t%d\t%s\n", i
, Y
->n
->name
);
This page took 0.079479 seconds and 4 git commands to generate.