3 pcc -DSAFETY -DREACH -DMEMLIM'='500 -o pan pan.c
20 atomic { x == 0; x = 1 }
31 assert !sleeping[_pid];
35 :: atomic { else -> sleeping[_pid] = 1 } ->
47 :: sleeping[id] == 1 -> sleeping[id] = 0
77 :: (i < N && j > 0) ->
79 :: onlist[i] && waiting[i] ->
80 atomic { printf("kicked %d\n", i);
89 /* reset i and j to reduce state space */
97 atomic { value = value+n; printf("release %d\n", n); };
103 atomic { value > 0 -> value--; };
107 #define semawoke() !waiting[_pid]
109 inline semacquire(block)
112 :: atomic { canacquire() -> printf("easy acquire\n"); } ->
117 :: !block -> goto out
126 :: atomic { canacquire() -> printf("hard acquire\n"); } ->
133 printf("%d interrupted\n", _pid);
145 assert (!block || interrupted || acquired[_pid]);
146 assert !(interrupted && acquired[_pid]);
147 assert !waiting[_pid];
148 printf("%d done\n", _pid);
151 active[N] proctype acquire()
156 printf("%d finished\n", _pid);
160 active proctype release()
175 * If this guy, the highest-numbered proc, sticks
176 * around, then everyone else sticks around.
177 * This makes sure that we get a state line for
178 * everyone in a proc dump.
180 active proctype dummy()