0b55f123 |
1 | /***** spin: pangen6.h *****/ |
2 | |
3 | /* Copyright (c) 2006-2007 by the California Institute of Technology. */ |
4 | /* ALL RIGHTS RESERVED. United States Government Sponsorship acknowledged */ |
5 | /* Supporting routines for a multi-core extension of the SPIN software */ |
6 | /* Developed as part of Reliable Software Engineering Project ESAS/6G */ |
7 | /* Like all SPIN Software this software is for educational purposes only. */ |
8 | /* No guarantee whatsoever is expressed or implied by the distribution of */ |
9 | /* this code. Permission is given to distribute this code provided that */ |
10 | /* this introductory message is not removed and no monies are exchanged. */ |
11 | /* Any commercial use must be negotiated with the Office of Technology */ |
12 | /* Transfer at the California Institute of Technology. */ |
13 | /* Software written by Gerard J. Holzmann. For tool documentation see: */ |
14 | /* http://spinroot.com/ */ |
15 | /* Bug-reports and/or questions can be send to: bugs@spinroot.com */ |
16 | |
17 | static char *Code2c[] = { /* multi-core option - Spin 5.0 and later */ |
18 | "#if NCORE>1", |
19 | "#if defined(WIN32) || defined(WIN64)", |
20 | "#ifndef _CONSOLE", |
21 | " #define _CONSOLE", |
22 | "#endif", |
23 | " #ifdef WIN64", |
24 | "#undef long", |
25 | " #endif", |
26 | "#include <windows.h>", |
27 | "", |
28 | " #ifdef WIN64", |
29 | " #define long long long", |
30 | " #endif", |
31 | "#else", |
32 | "#include <sys/ipc.h>", |
33 | "#include <sys/sem.h>", |
34 | "#include <sys/shm.h>", |
35 | "#endif", |
36 | "", |
37 | "/* code common to cygwin/linux and win32/win64: */", |
38 | "", |
39 | "#ifdef VERBOSE", |
40 | " #define VVERBOSE (1)", |
41 | "#else", |
42 | " #define VVERBOSE (0)", |
43 | "#endif", |
44 | "", |
45 | "/* the following values must be larger than 256 and must fit in an int */", |
46 | "#define QUIT 1024 /* terminate now command */", |
47 | "#define QUERY 512 /* termination status query message */", |
48 | "#define QUERY_F 513 /* query failed, cannot quit */", |
49 | "", |
50 | "#define GN_FRAMES (int) (GWQ_SIZE / (double) sizeof(SM_frame))", |
51 | "#define LN_FRAMES (int) (LWQ_SIZE / (double) sizeof(SM_frame))", |
52 | "", |
53 | "#ifndef VMAX", |
54 | " #define VMAX VECTORSZ", |
55 | "#endif", |
56 | "#ifndef PMAX", |
57 | " #define PMAX 64", |
58 | "#endif", |
59 | "#ifndef QMAX", |
60 | " #define QMAX 64", |
61 | "#endif", |
62 | "", |
63 | "#if VECTORSZ>32000", |
64 | " #define OFFT int", |
65 | "#else", |
66 | " #define OFFT short", |
67 | "#endif", |
68 | "", |
69 | "#ifdef SET_SEG_SIZE", |
70 | " /* no longer usefule -- being recomputed for local heap size anyway */", |
71 | " double SEG_SIZE = (((double) SET_SEG_SIZE) * 1048576.);", |
72 | "#else", |
73 | " double SEG_SIZE = (1048576.*1024.); /* 1GB default shared memory pool segments */", |
74 | "#endif", |
75 | "", |
76 | "double LWQ_SIZE = 0.; /* initialized in main */", |
77 | "", |
78 | "#ifdef SET_WQ_SIZE", |
79 | " #ifdef NGQ", |
80 | " #warning SET_WQ_SIZE applies to global queue -- ignored", |
81 | " double GWQ_SIZE = 0.;", |
82 | " #else", |
83 | " double GWQ_SIZE = (((double) SET_WQ_SIZE) * 1048576.);", |
84 | " /* must match the value in pan_proxy.c, if used */", |
85 | " #endif", |
86 | "#else", |
87 | " #ifdef NGQ", |
88 | " double GWQ_SIZE = 0.;", |
89 | " #else", |
90 | " double GWQ_SIZE = (128.*1048576.); /* 128 MB default queue sizes */", |
91 | " #endif", |
92 | "#endif", |
93 | "", |
94 | "/* Crash Detection Parameters */", |
95 | "#ifndef ONESECOND", |
96 | " #define ONESECOND (1<<25)", /* name is somewhat of a misnomer */ |
97 | "#endif", |
98 | "#ifndef SHORT_T", |
99 | " #define SHORT_T (0.1)", |
100 | "#endif", |
101 | "#ifndef LONG_T", |
102 | " #define LONG_T (600)", |
103 | "#endif", |
104 | "", |
105 | "double OneSecond = (double) (ONESECOND); /* waiting for a free slot -- checks crash */", |
106 | "double TenSeconds = 10. * (ONESECOND); /* waiting for a lock -- check for a crash */", |
107 | "", |
108 | "/* Termination Detection Params -- waiting for new state input in Get_Full_Frame */", |
109 | "double Delay = ((double) SHORT_T) * (ONESECOND); /* termination detection trigger */", |
110 | "double OneHour = ((double) LONG_T) * (ONESECOND); /* timeout termination detection */", |
111 | "", |
112 | "typedef struct SM_frame SM_frame;", |
113 | "typedef struct SM_results SM_results;", |
114 | "typedef struct sh_Allocater sh_Allocater;", |
115 | "", |
116 | "struct SM_frame { /* about 6K per slot */", |
117 | " volatile int m_vsize; /* 0 means free slot */", |
118 | " volatile int m_boq; /* >500 is a control message */", |
119 | "#ifdef FULL_TRAIL", |
120 | " volatile struct Stack_Tree *m_stack; /* ptr to previous state */", |
121 | "#endif", |
122 | " volatile uchar m_tau;", |
123 | " volatile uchar m_o_pm;", |
124 | " volatile int nr_handoffs; /* to compute real_depth */", |
125 | " volatile char m_now [VMAX];", |
126 | " volatile char m_Mask [(VMAX + 7)/8];", |
127 | " volatile OFFT m_p_offset[PMAX];", |
128 | " volatile OFFT m_q_offset[QMAX];", |
129 | " volatile uchar m_p_skip [PMAX];", |
130 | " volatile uchar m_q_skip [QMAX];", |
131 | "#if defined(C_States) && (HAS_TRACK==1) && (HAS_STACK==1)", |
132 | " volatile uchar m_c_stack [StackSize];", |
133 | /* captures contents of c_stack[] for unmatched objects */ |
134 | "#endif", |
135 | "};", |
136 | "", |
137 | "int proxy_pid; /* id of proxy if nonzero -- receive half */", |
138 | "int store_proxy_pid;", |
139 | "short remote_party;", |
140 | "int proxy_pid_snd; /* id of proxy if nonzero -- send half */", |
141 | "char o_cmdline[512]; /* to pass options to children */", |
142 | "", |
143 | "int iamin[CS_NR+NCORE]; /* non-shared */", |
144 | "", |
145 | "#if defined(WIN32) || defined(WIN64)", |
146 | "int tas(volatile LONG *);", |
147 | "", |
148 | "HANDLE proxy_handle_snd; /* for Windows Create and Terminate */", |
149 | "", |
150 | "struct sh_Allocater { /* shared memory for states */", |
151 | " volatile char *dc_arena; /* to allocate states from */", |
152 | " volatile long pattern; /* to detect overruns */", |
153 | " volatile long dc_size; /* nr of bytes left */", |
154 | " volatile void *dc_start; /* where memory segment starts */", |
155 | " volatile void *dc_id; /* to attach, detach, remove shared memory segments */", |
156 | " volatile sh_Allocater *nxt; /* linked list of pools */", |
157 | "};", |
158 | "DWORD worker_pids[NCORE]; /* root mem of pids of all workers created */", |
159 | "HANDLE worker_handles[NCORE]; /* for windows Create and Terminate */", |
160 | "void * shmid [NR_QS]; /* return value from CreateFileMapping */", |
161 | "void * shmid_M; /* shared mem for state allocation in hashtable */", |
162 | "", |
163 | "#ifdef SEP_STATE", |
164 | " void *shmid_X;", |
165 | "#else", |
166 | " void *shmid_S; /* shared bitstate arena or hashtable */", |
167 | "#endif", |
168 | "#else", |
169 | "int tas(volatile int *);", |
170 | "", |
171 | "struct sh_Allocater { /* shared memory for states */", |
172 | " volatile char *dc_arena; /* to allocate states from */", |
173 | " volatile long pattern; /* to detect overruns */", |
174 | " volatile long dc_size; /* nr of bytes left */", |
175 | " volatile char *dc_start; /* where memory segment starts */", |
176 | " volatile int dc_id; /* to attach, detach, remove shared memory segments */", |
177 | " volatile sh_Allocater *nxt; /* linked list of pools */", |
178 | "};", |
179 | "", |
180 | "int worker_pids[NCORE]; /* root mem of pids of all workers created */", |
181 | "int shmid [NR_QS]; /* return value from shmget */", |
182 | "int nibis = 0; /* set after shared mem has been released */", |
183 | "int shmid_M; /* shared mem for state allocation in hashtable */", |
184 | "#ifdef SEP_STATE", |
185 | " long shmid_X;", |
186 | "#else", |
187 | " int shmid_S; /* shared bitstate arena or hashtable */", |
188 | " volatile sh_Allocater *first_pool; /* of shared state memory */", |
189 | " volatile sh_Allocater *last_pool;", |
190 | "#endif", /* SEP_STATE */ |
191 | "#endif", /* WIN32 || WIN64 */ |
192 | "", |
193 | "struct SM_results { /* for shuttling back final stats */", |
194 | " volatile int m_vsize; /* avoid conflicts with frames */", |
195 | " volatile int m_boq; /* these 2 fields are not written in record_info */", |
196 | " /* probably not all fields really need to be volatile */", |
197 | " volatile double m_memcnt;", |
198 | " volatile double m_nstates;", |
199 | " volatile double m_truncs;", |
200 | " volatile double m_truncs2;", |
201 | " volatile double m_nShadow;", |
202 | " volatile double m_nlinks;", |
203 | " volatile double m_ngrabs;", |
204 | " volatile double m_nlost;", |
205 | " volatile double m_hcmp;", |
206 | " volatile double m_frame_wait;", |
207 | " volatile int m_hmax;", |
208 | " volatile int m_svmax;", |
209 | " volatile int m_smax;", |
210 | " volatile int m_mreached;", |
211 | " volatile int m_errors;", |
212 | " volatile int m_VMAX;", |
213 | " volatile short m_PMAX;", |
214 | " volatile short m_QMAX;", |
215 | " volatile uchar m_R; /* reached info for all proctypes */", |
216 | "};", |
217 | "", |
218 | "int core_id = 0; /* internal process nr, to know which q to use */", |
219 | "unsigned long nstates_put = 0; /* statistics */", |
220 | "unsigned long nstates_get = 0;", |
221 | "int query_in_progress = 0; /* termination detection */", |
222 | "", |
223 | "double free_wait = 0.; /* waiting for a free frame */", |
224 | "double frame_wait = 0.; /* waiting for a full frame */", |
225 | "double lock_wait = 0.; /* waiting for access to cs */", |
226 | "double glock_wait[3]; /* waiting for access to global lock */", |
227 | "", |
228 | "char *sprefix = \"rst\";", |
229 | "uchar was_interrupted, issued_kill, writing_trail;", |
230 | "", |
231 | "static SM_frame cur_Root; /* current root, to be safe with error trails */", |
232 | "", |
233 | "SM_frame *m_workq [NR_QS]; /* per cpu work queues + global q */", |
234 | "char *shared_mem[NR_QS]; /* return value from shmat */", |
235 | "#ifdef SEP_HEAP", |
236 | "char *my_heap;", |
237 | "long my_size;", |
238 | "#endif", |
239 | "volatile sh_Allocater *dc_shared; /* assigned at initialization */", |
240 | "", |
241 | "static int vmax_seen, pmax_seen, qmax_seen;", |
242 | "static double gq_tries, gq_hasroom, gq_hasnoroom;", |
243 | "", |
244 | "volatile int *prfree;", /* [NCORE] */ |
245 | "volatile int *prfull;", /* [NCORE] */ |
246 | "volatile int *prcnt;", /* [NCORE] */ |
247 | "volatile int *prmax;", /* [NCORE] */ |
248 | "", |
249 | "volatile int *sh_lock; /* mutual exclusion locks - in shared memory */", |
250 | "volatile double *is_alive; /* to detect when processes crash */", |
251 | "volatile int *grfree, *grfull, *grcnt, *grmax; /* access to shared global q */", |
252 | "volatile double *gr_readmiss, *gr_writemiss;", |
253 | "static int lrfree; /* used for temporary recording of slot */", |
254 | "static int dfs_phase2;", |
255 | "", |
256 | "void mem_put(int); /* handoff state to other cpu */", |
257 | "void mem_put_acc(void); /* liveness mode */", |
258 | "void mem_get(void); /* get state from work queue */", |
259 | "void sudden_stop(char *);", |
260 | "#if 0", |
261 | "void enter_critical(int);", |
262 | "void leave_critical(int);", |
263 | "#endif", |
264 | "", |
265 | "void", |
266 | "record_info(SM_results *r)", |
267 | "{ int i;", |
268 | " uchar *ptr;", |
269 | "", |
270 | "#ifdef SEP_STATE", |
271 | " if (0)", |
272 | " { cpu_printf(\"nstates %%g nshadow %%g -- memory %%-6.3f Mb\\n\",", |
273 | " nstates, nShadow, memcnt/(1048576.));", |
274 | " }", |
275 | " r->m_memcnt = 0;", |
276 | "#else", |
277 | " #ifdef BITSTATE", |
278 | " r->m_memcnt = 0; /* it's shared */", |
279 | " #endif", |
280 | " r->m_memcnt = memcnt;", |
281 | "#endif", |
282 | " if (a_cycles && core_id == 1)", |
283 | " { r->m_nstates = nstates;", |
284 | " r->m_nShadow = nstates;", |
285 | " } else", |
286 | " { r->m_nstates = nstates;", |
287 | " r->m_nShadow = nShadow;", |
288 | " }", |
289 | " r->m_truncs = truncs;", |
290 | " r->m_truncs2 = truncs2;", |
291 | " r->m_nlinks = nlinks;", |
292 | " r->m_ngrabs = ngrabs;", |
293 | " r->m_nlost = nlost;", |
294 | " r->m_hcmp = hcmp;", |
295 | " r->m_frame_wait = frame_wait;", |
296 | " r->m_hmax = hmax;", |
297 | " r->m_svmax = svmax;", |
298 | " r->m_smax = smax;", |
299 | " r->m_mreached = mreached;", |
300 | " r->m_errors = errors;", |
301 | " r->m_VMAX = vmax_seen;", |
302 | " r->m_PMAX = (short) pmax_seen;", |
303 | " r->m_QMAX = (short) qmax_seen;", |
304 | " ptr = (uchar *) &(r->m_R);", |
305 | " for (i = 0; i <= _NP_; i++) /* all proctypes */", |
306 | " { memcpy(ptr, reached[i], NrStates[i]*sizeof(uchar));", |
307 | " ptr += NrStates[i]*sizeof(uchar);", |
308 | " }", |
309 | " if (verbose>1)", |
310 | " { cpu_printf(\"Put Results nstates %%g (sz %%d)\\n\", nstates, ptr - &(r->m_R));", |
311 | " }", |
312 | "}", |
313 | "", |
314 | "void snapshot(void);", |
315 | "", |
316 | "void", |
317 | "retrieve_info(SM_results *r)", |
318 | "{ int i, j;", |
319 | " volatile uchar *ptr;", |
320 | "", |
321 | " snapshot(); /* for a final report */", |
322 | "", |
323 | " enter_critical(GLOBAL_LOCK);", |
324 | "#ifdef SEP_HEAP", |
325 | " if (verbose)", |
326 | " { printf(\"cpu%%d: local heap-left %%ld KB (%%d MB)\\n\",", |
327 | " core_id, (int) (my_size/1024), (int) (my_size/1048576));", |
328 | " }", |
329 | "#endif", |
330 | " if (verbose && core_id == 0)", |
331 | " { printf(\"qmax: \");", |
332 | " for (i = 0; i < NCORE; i++)", |
333 | " { printf(\"%%d \", prmax[i]);", |
334 | " }", |
335 | "#ifndef NGQ", |
336 | " printf(\"G: %%d\", *grmax);", |
337 | "#endif", |
338 | " printf(\"\\n\");", |
339 | " }", |
340 | " leave_critical(GLOBAL_LOCK);", |
341 | "", |
342 | " memcnt += r->m_memcnt;", |
343 | " nstates += r->m_nstates;", |
344 | " nShadow += r->m_nShadow;", |
345 | " truncs += r->m_truncs;", |
346 | " truncs2 += r->m_truncs2;", |
347 | " nlinks += r->m_nlinks;", |
348 | " ngrabs += r->m_ngrabs;", |
349 | " nlost += r->m_nlost;", |
350 | " hcmp += r->m_hcmp;", |
351 | " /* frame_wait += r->m_frame_wait; */", |
352 | " errors += r->m_errors;", |
353 | "", |
354 | " if (hmax < r->m_hmax) hmax = r->m_hmax;", |
355 | " if (svmax < r->m_svmax) svmax = r->m_svmax;", |
356 | " if (smax < r->m_smax) smax = r->m_smax;", |
357 | " if (mreached < r->m_mreached) mreached = r->m_mreached;", |
358 | "", |
359 | " if (vmax_seen < r->m_VMAX) vmax_seen = r->m_VMAX;", |
360 | " if (pmax_seen < (int) r->m_PMAX) pmax_seen = (int) r->m_PMAX;", |
361 | " if (qmax_seen < (int) r->m_QMAX) qmax_seen = (int) r->m_QMAX;", |
362 | "", |
363 | " ptr = &(r->m_R);", |
364 | " for (i = 0; i <= _NP_; i++) /* all proctypes */", |
365 | " { for (j = 0; j < NrStates[i]; j++)", |
366 | " { if (*(ptr + j) != 0)", |
367 | " { reached[i][j] = 1;", |
368 | " } }", |
369 | " ptr += NrStates[i]*sizeof(uchar);", |
370 | " }", |
371 | " if (verbose>1)", |
372 | " { cpu_printf(\"Got Results (%%d)\\n\", ptr - &(r->m_R));", |
373 | " snapshot();", |
374 | " }", |
375 | "}", |
376 | "", |
377 | "#if !defined(WIN32) && !defined(WIN64)", |
378 | "static void", |
379 | "rm_shared_segments(void)", |
380 | "{ int m;", |
381 | " volatile sh_Allocater *nxt_pool;", |
382 | " /*", |
383 | " * mark all shared memory segments for removal ", |
384 | " * the actual removes wont happen intil last process dies or detaches", |
385 | " * the shmctl calls can return -1 if not all procs have detached yet", |
386 | " */", |
387 | " for (m = 0; m < NR_QS; m++) /* +1 for global q */", |
388 | " { if (shmid[m] != -1)", |
389 | " { (void) shmctl(shmid[m], IPC_RMID, NULL);", |
390 | " } }", |
391 | "#ifdef SEP_STATE", |
392 | " if (shmid_M != -1)", |
393 | " { (void) shmctl(shmid_M, IPC_RMID, NULL);", |
394 | " }", |
395 | "#else", |
396 | " if (shmid_S != -1)", |
397 | " { (void) shmctl(shmid_S, IPC_RMID, NULL);", |
398 | " }", |
399 | " for (last_pool = first_pool; last_pool != NULL; last_pool = nxt_pool)", |
400 | " { shmid_M = (int) (last_pool->dc_id);", |
401 | " nxt_pool = last_pool->nxt; /* as a pre-caution only */", |
402 | " if (shmid_M != -1)", |
403 | " { (void) shmctl(shmid_M, IPC_RMID, NULL);", |
404 | " } }", |
405 | "#endif", |
406 | "}", |
407 | "#endif", |
408 | "", |
409 | "void", |
410 | "sudden_stop(char *s)", |
411 | "{ char b[64];", |
412 | " int i;", |
413 | "", |
414 | " printf(\"cpu%%d: stop - %%s\\n\", core_id, s);", |
415 | "#if !defined(WIN32) && !defined(WIN64)", |
416 | " if (proxy_pid != 0)", |
417 | " { rm_shared_segments();", |
418 | " }", |
419 | "#endif", |
420 | " if (search_terminated != NULL)", |
421 | " { if (*search_terminated != 0)", |
422 | " { if (verbose)", |
423 | " { printf(\"cpu%%d: termination initiated (%%d)\\n\",", |
424 | " core_id, *search_terminated);", |
425 | " }", |
426 | " } else", |
427 | " { if (verbose)", |
428 | " { printf(\"cpu%%d: initiated termination\\n\", core_id);", |
429 | " }", |
430 | " *search_terminated |= 8; /* sudden_stop */", |
431 | " }", |
432 | " if (core_id == 0)", |
433 | " { if (((*search_terminated) & 4) /* uerror in one of the cpus */", |
434 | " && !((*search_terminated) & (8|32|128|256))) /* abnormal stop */", |
435 | " { if (errors == 0) errors++; /* we know there is at least 1 */", |
436 | " }", |
437 | " wrapup(); /* incomplete stats, but at least something */", |
438 | " }", |
439 | " return;", |
440 | " } /* else: should rarely happen, take more drastic measures */", |
441 | "", |
442 | " if (core_id == 0) /* local root process */", |
443 | " { for (i = 1; i < NCORE; i++) /* not for 0 of course */", |
444 | " {", |
445 | "#if defined(WIN32) || defined(WIN64)", |
446 | " DWORD dwExitCode = 0;", |
447 | " GetExitCodeProcess(worker_handles[i], &dwExitCode);", |
448 | " if (dwExitCode == STILL_ACTIVE)", |
449 | " { TerminateProcess(worker_handles[i], 0);", |
450 | " }", |
451 | " printf(\"cpu0: terminate %%d %%d\\n\",", |
452 | " worker_pids[i], (dwExitCode == STILL_ACTIVE));", |
453 | "#else", |
454 | " sprintf(b, \"kill -%%d %%d\", SIGKILL, worker_pids[i]);", |
455 | " system(b); /* if this is a proxy: receive half */", |
456 | " printf(\"cpu0: %%s\\n\", b);", |
457 | "#endif", |
458 | " }", |
459 | " issued_kill++;", |
460 | " } else", |
461 | " { /* on WIN32/WIN64 -- these merely kills the root process... */", |
462 | " if (was_interrupted == 0)", /* 2=SIGINT to root to trigger stop */ |
463 | " { sprintf(b, \"kill -%%d %%d\", SIGINT, worker_pids[0]);", |
464 | " system(b); /* warn the root process */", |
465 | " printf(\"cpu%%d: %%s\\n\", core_id, b);", |
466 | " issued_kill++;", |
467 | " } }", |
468 | "}", |
469 | "", |
470 | "#define iam_alive() is_alive[core_id]++", /* for crash detection */ |
471 | "", |
472 | "extern int crash_test(double);", |
473 | "extern void crash_reset(void);", |
474 | "", |
475 | "int", |
476 | "someone_crashed(int wait_type)", |
477 | "{ static double last_value = 0.0;", |
478 | " static int count = 0;", |
479 | "", |
480 | " if (search_terminated == NULL", |
481 | " || *search_terminated != 0)", |
482 | " {", |
483 | " if (!(*search_terminated & (8|32|128|256)))", |
484 | " { if (count++ < 100*NCORE)", |
485 | " { return 0;", |
486 | " } }", |
487 | " return 1;", |
488 | " }", |
489 | " /* check left neighbor only */", |
490 | " if (last_value == is_alive[(core_id + NCORE - 1) %% NCORE])", |
491 | " { if (count++ >= 100) /* to avoid unnecessary checks */", |
492 | " { return 1;", |
493 | " }", |
494 | " return 0;", |
495 | " }", |
496 | " last_value = is_alive[(core_id + NCORE - 1) %% NCORE];", |
497 | " count = 0;", |
498 | " crash_reset();", |
499 | " return 0;", |
500 | "}", |
501 | "", |
502 | "void", |
503 | "sleep_report(void)", |
504 | "{", |
505 | " enter_critical(GLOBAL_LOCK);", |
506 | " if (verbose)", |
507 | " {", |
508 | "#ifdef NGQ", |
509 | " printf(\"cpu%%d: locks: global %%g\\tother %%g\\t\",", |
510 | " core_id, glock_wait[0], lock_wait - glock_wait[0]);", |
511 | "#else", |
512 | " printf(\"cpu%%d: locks: GL %%g, RQ %%g, WQ %%g, HT %%g\\t\",", |
513 | " core_id, glock_wait[0], glock_wait[1], glock_wait[2],", |
514 | " lock_wait - glock_wait[0] - glock_wait[1] - glock_wait[2]);", |
515 | "#endif", |
516 | " printf(\"waits: states %%g slots %%g\\n\", frame_wait, free_wait);", |
517 | "#ifndef NGQ", |
518 | " printf(\"cpu%%d: gq [tries %%g, room %%g, noroom %%g]\\n\", core_id, gq_tries, gq_hasroom, gq_hasnoroom);", |
519 | " if (core_id == 0 && (*gr_readmiss >= 1.0 || *gr_readmiss >= 1.0 || *grcnt != 0))", |
520 | " printf(\"cpu0: gq [readmiss: %%g, writemiss: %%g cnt %%d]\\n\", *gr_readmiss, *gr_writemiss, *grcnt);", |
521 | "#endif", |
522 | " }", |
523 | " if (free_wait > 1000000.)", |
524 | " #ifndef NGQ", |
525 | " if (!a_cycles)", |
526 | " { printf(\"hint: this search may be faster with a larger work-queue\\n\");", |
527 | " printf(\" (-DSET_WQ_SIZE=N with N>%%g), and/or with -DUSE_DISK\\n\",", |
528 | " GWQ_SIZE/sizeof(SM_frame));", |
529 | " printf(\" or with a larger value for -zN (N>%%d)\\n\", z_handoff);", |
530 | " #else", |
531 | " { printf(\"hint: this search may be faster if compiled without -DNGQ, with -DUSE_DISK, \");", |
532 | " printf(\"or with a larger -zN (N>%%d)\\n\", z_handoff);", |
533 | " #endif", |
534 | " }", |
535 | " leave_critical(GLOBAL_LOCK);", |
536 | "}", |
537 | "", |
538 | "#ifndef MAX_DSK_FILE", |
539 | " #define MAX_DSK_FILE 1000000 /* default is max 1M states per file */", |
540 | "#endif", |
541 | "", |
542 | "void", |
543 | "multi_usage(FILE *fd)", |
544 | "{ static int warned = 0;", |
545 | " if (warned > 0) { return; } else { warned++; }", |
546 | " fprintf(fd, \"\\n\");", |
547 | " fprintf(fd, \"Defining multi-core mode:\\n\\n\");", |
548 | " fprintf(fd, \" -DDUAL_CORE --> same as -DNCORE=2\\n\");", |
549 | " fprintf(fd, \" -DQUAD_CORE --> same as -DNCORE=4\\n\");", |
550 | " fprintf(fd, \" -DNCORE=N --> enables multi_core verification if N>1\\n\");", |
551 | " fprintf(fd, \"\\n\");", |
552 | " fprintf(fd, \"Additional directives supported in multi-core mode:\\n\\n\");", |
553 | " fprintf(fd, \" -DSEP_STATE --> forces separate statespaces instead of a single shared state space\\n\");", |
554 | " fprintf(fd, \" -DNUSE_DISK --> use disk for storing states when a work queue overflows\\n\");", |
555 | " fprintf(fd, \" -DMAX_DSK_FILE --> max nr of states per diskfile (%%d)\\n\", MAX_DSK_FILE);", |
556 | " fprintf(fd, \" -DFULL_TRAIL --> support full error trails (increases memory use)\\n\");", |
557 | " fprintf(fd, \"\\n\");", |
558 | " fprintf(fd, \"More advanced use (should rarely need changing):\\n\\n\");", |
559 | " fprintf(fd, \" To change the nr of states that can be stored in the global queue\\n\");", |
560 | " fprintf(fd, \" (lower numbers allow for more states to be stored, prefer multiples of 8):\\n\");", |
561 | " fprintf(fd, \" -DVMAX=N --> upperbound on statevector for handoffs (N=%%d)\\n\", VMAX);", |
562 | " fprintf(fd, \" -DPMAX=N --> upperbound on nr of procs (default: N=%%d)\\n\", PMAX);", |
563 | " fprintf(fd, \" -DQMAX=N --> upperbound on nr of channels (default: N=%%d)\\n\", QMAX);", |
564 | " fprintf(fd, \"\\n\");", |
565 | #if 0 |
566 | "#if !defined(WIN32) && !defined(WIN64)", |
567 | " fprintf(fd, \" To change the size of spin's individual shared memory segments for cygwin/linux:\\n\");", |
568 | " fprintf(fd, \" -DSET_SEG_SIZE=N --> default %%g (Mbytes)\\n\", SEG_SIZE/(1048576.));", |
569 | " fprintf(fd, \"\\n\");", |
570 | "#endif", |
571 | #endif |
572 | " fprintf(fd, \" To set the total amount of memory reserved for the global workqueue:\\n\");", |
573 | " fprintf(fd, \" -DSET_WQ_SIZE=N --> default: N=128 (defined in MBytes)\\n\\n\");", |
574 | #if 0 |
575 | " fprintf(fd, \" To omit the global workqueue completely (bad idea):\\n\");", |
576 | " fprintf(fd, \" -DNGQ\\n\\n\");", |
577 | #endif |
578 | " fprintf(fd, \" To force the use of a single global heap, instead of separate heaps:\\n\");", |
579 | " fprintf(fd, \" -DGLOB_HEAP\\n\");", |
580 | " fprintf(fd, \"\\n\");", |
581 | " fprintf(fd, \" To define a fct to initialize data before spawning processes (use quotes):\\n\");", |
582 | " fprintf(fd, \" \\\"-DC_INIT=fct()\\\"\\n\");", |
583 | " fprintf(fd, \"\\n\");", |
584 | " fprintf(fd, \" Timer settings for termination and crash detection:\\n\");", |
585 | " fprintf(fd, \" -DSHORT_T=N --> timeout for termination detection trigger (N=%%g)\\n\", (double) SHORT_T);", |
586 | " fprintf(fd, \" -DLONG_T=N --> timeout for giving up on termination detection (N=%%g)\\n\", (double) LONG_T);", |
587 | " fprintf(fd, \" -DONESECOND --> (1<<29) --> timeout waiting for a free slot -- to check for crash\\n\");", |
588 | " fprintf(fd, \" -DT_ALERT --> collect stats on crash alert timeouts\\n\\n\");", |
589 | " fprintf(fd, \"Help with Linux/Windows/Cygwin configuration for multi-core:\\n\");", |
590 | " fprintf(fd, \" http://spinroot.com/spin/multicore/V5_Readme.html\\n\");", |
591 | " fprintf(fd, \"\\n\");", |
592 | "}", |
593 | "#if NCORE>1 && defined(FULL_TRAIL)", |
594 | "typedef struct Stack_Tree {", |
595 | " uchar pr; /* process that made transition */", |
596 | " T_ID t_id; /* id of transition */", |
597 | " volatile struct Stack_Tree *prv; /* backward link towards root */", |
598 | "} Stack_Tree;", |
599 | "", |
600 | "struct H_el *grab_shared(int);", |
601 | "volatile Stack_Tree **stack_last; /* in shared memory */", |
602 | "char *stack_cache = NULL; /* local */", |
603 | "int nr_cached = 0; /* local */", |
604 | "", |
605 | "#ifndef CACHE_NR", |
606 | " #define CACHE_NR 1024", |
607 | "#endif", |
608 | "", |
609 | "volatile Stack_Tree *", |
610 | "stack_prefetch(void)", |
611 | "{ volatile Stack_Tree *st;", |
612 | "", |
613 | " if (nr_cached == 0)", |
614 | " { stack_cache = (char *) grab_shared(CACHE_NR * sizeof(Stack_Tree));", |
615 | " nr_cached = CACHE_NR;", |
616 | " }", |
617 | " st = (volatile Stack_Tree *) stack_cache;", |
618 | " stack_cache += sizeof(Stack_Tree);", |
619 | " nr_cached--;", |
620 | " return st;", |
621 | "}", |
622 | "", |
623 | "void", |
624 | "Push_Stack_Tree(short II, T_ID t_id)", |
625 | "{ volatile Stack_Tree *st;", |
626 | "", |
627 | " st = (volatile Stack_Tree *) stack_prefetch();", |
628 | " st->pr = II;", |
629 | " st->t_id = t_id;", |
630 | " st->prv = (Stack_Tree *) stack_last[core_id];", |
631 | " stack_last[core_id] = st;", |
632 | "}", |
633 | "", |
634 | "void", |
635 | "Pop_Stack_Tree(void)", |
636 | "{ volatile Stack_Tree *cf = stack_last[core_id];", |
637 | "", |
638 | " if (cf)", |
639 | " { stack_last[core_id] = cf->prv;", |
640 | " } else if (nr_handoffs * z_handoff + depth > 0)", |
641 | " { printf(\"cpu%%d: error pop_stack_tree (depth %%d)\\n\",", |
642 | " core_id, depth);", |
643 | " }", |
644 | "}", |
645 | "#endif", /* NCORE>1 && FULL_TRAIL */ |
646 | "", |
647 | "void", |
648 | "e_critical(int which)", |
649 | "{ double cnt_start;", |
650 | "", |
651 | " if (readtrail || iamin[which] > 0)", |
652 | " { if (!readtrail && verbose)", |
653 | " { printf(\"cpu%%d: Double Lock on %%d (now %%d)\\n\",", |
654 | " core_id, which, iamin[which]+1);", |
655 | " fflush(stdout);", |
656 | " }", |
657 | " iamin[which]++; /* local variable */", |
658 | " return;", |
659 | " }", |
660 | "", |
661 | " cnt_start = lock_wait;", |
662 | "", |
663 | " while (sh_lock != NULL) /* as long as we have shared memory */", |
664 | " { int r = tas(&sh_lock[which]);", |
665 | " if (r == 0)", |
666 | " { iamin[which] = 1;", |
667 | " return; /* locked */", |
668 | " }", |
669 | "", |
670 | " lock_wait++;", |
671 | "#ifndef NGQ", |
672 | " if (which < 3) { glock_wait[which]++; }", |
673 | "#else", |
674 | " if (which == 0) { glock_wait[which]++; }", |
675 | "#endif", |
676 | " iam_alive();", |
677 | "", |
678 | " if (lock_wait - cnt_start > TenSeconds)", |
679 | " { printf(\"cpu%%d: lock timeout on %%d\\n\", core_id, which);", |
680 | " cnt_start = lock_wait;", |
681 | " if (someone_crashed(1))", |
682 | " { sudden_stop(\"lock timeout\");", |
683 | " pan_exit(1);", |
684 | " } } }", |
685 | "}", |
686 | "", |
687 | "void", |
688 | "x_critical(int which)", |
689 | "{", |
690 | " if (iamin[which] != 1)", |
691 | " { if (iamin[which] > 1)", |
692 | " { iamin[which]--; /* this is thread-local - no races on this one */", |
693 | " if (!readtrail && verbose)", |
694 | " { printf(\"cpu%%d: Partial Unlock on %%d (%%d more needed)\\n\",", |
695 | " core_id, which, iamin[which]);", |
696 | " fflush(stdout);", |
697 | " }", |
698 | " return;", |
699 | " } else /* iamin[which] <= 0 */", |
700 | " { if (!readtrail)", |
701 | " { printf(\"cpu%%d: Invalid Unlock iamin[%%d] = %%d\\n\",", |
702 | " core_id, which, iamin[which]);", |
703 | " fflush(stdout);", |
704 | " }", |
705 | " return;", |
706 | " } }", |
707 | "", |
708 | " if (sh_lock != NULL)", |
709 | " { iamin[which] = 0;", |
710 | " sh_lock[which] = 0; /* unlock */", |
711 | " }", |
712 | "}", |
713 | "", |
714 | "void", |
715 | "#if defined(WIN32) || defined(WIN64)", |
716 | "start_proxy(char *s, DWORD r_pid)", |
717 | "#else", |
718 | "start_proxy(char *s, int r_pid)", |
719 | "#endif", |
720 | "{ char Q_arg[16], Z_arg[16], Y_arg[16];", |
721 | " char *args[32], *ptr;", |
722 | " int argcnt = 0;", |
723 | "", |
724 | " sprintf(Q_arg, \"-Q%%d\", getpid());", |
725 | " sprintf(Y_arg, \"-Y%%d\", r_pid);", |
726 | " sprintf(Z_arg, \"-Z%%d\", proxy_pid /* core_id */);", |
727 | "", |
728 | " args[argcnt++] = \"proxy\";", |
729 | " args[argcnt++] = s; /* -r or -s */", |
730 | " args[argcnt++] = Q_arg;", |
731 | " args[argcnt++] = Z_arg;", |
732 | " args[argcnt++] = Y_arg;", |
733 | "", |
734 | " if (strlen(o_cmdline) > 0)", |
735 | " { ptr = o_cmdline; /* assume args separated by spaces */", |
736 | " do { args[argcnt++] = ptr++;", |
737 | " if ((ptr = strchr(ptr, ' ')) != NULL)", |
738 | " { while (*ptr == ' ')", |
739 | " { *ptr++ = '\\0';", |
740 | " }", |
741 | " } else", |
742 | " { break;", |
743 | " }", |
744 | " } while (argcnt < 31);", |
745 | " }", |
746 | " args[argcnt] = NULL;", |
747 | "#if defined(WIN32) || defined(WIN64)", |
748 | " execvp(\"pan_proxy\", args); /* no return */", |
749 | "#else", |
750 | " execvp(\"./pan_proxy\", args); /* no return */", |
751 | "#endif", |
752 | " Uerror(\"pan_proxy exec failed\");", |
753 | "}", |
754 | "/*** end of common code fragment ***/", |
755 | "", |
756 | "#if !defined(WIN32) && !defined(WIN64)", |
757 | "void", |
758 | "init_shm(void) /* initialize shared work-queues - linux/cygwin */", |
759 | "{ key_t key[NR_QS];", |
760 | " int n, m;", |
761 | " int must_exit = 0;", |
762 | "", |
763 | " if (core_id == 0 && verbose)", |
764 | " { printf(\"cpu0: step 3: allocate shared workqueues %%g MB\\n\",", |
765 | " ((double) NCORE * LWQ_SIZE + GWQ_SIZE) / (1048576.) );", |
766 | " }", |
767 | " for (m = 0; m < NR_QS; m++) /* last q is the global q */", |
768 | " { double qsize = (m == NCORE) ? GWQ_SIZE : LWQ_SIZE;", |
769 | " key[m] = ftok(PanSource, m+1);", /* m must be nonzero, 1..NCORE */ |
770 | " if (key[m] == -1)", |
771 | " { perror(\"ftok shared queues\"); must_exit = 1; break;", |
772 | " }", |
773 | "", |
774 | " if (core_id == 0) /* root creates */", |
775 | " { /* check for stale copy */", |
776 | " shmid[m] = shmget(key[m], (size_t) qsize, 0600);", |
777 | " if (shmid[m] != -1) /* yes there is one; remove it */", |
778 | " { printf(\"cpu0: removing stale q%%d, status: %%d\\n\",", |
779 | " m, shmctl(shmid[m], IPC_RMID, NULL));", |
780 | " }", |
781 | " shmid[m] = shmget(key[m], (size_t) qsize, 0600|IPC_CREAT|IPC_EXCL);", |
782 | " memcnt += qsize;", |
783 | " } else /* workers attach */", |
784 | " { shmid[m] = shmget(key[m], (size_t) qsize, 0600);", |
785 | " /* never called, since we create shm *before* we fork */", |
786 | " }", |
787 | " if (shmid[m] == -1)", |
788 | " { perror(\"shmget shared queues\"); must_exit = 1; break;", |
789 | " }", |
790 | "", |
791 | " shared_mem[m] = (char *) shmat(shmid[m], (void *) 0, 0); /* attach */", |
792 | " if (shared_mem[m] == (char *) -1)", |
793 | " { fprintf(stderr, \"error: cannot attach shared wq %%d (%%d Mb)\\n\",", |
794 | " m+1, (int) (qsize/(1048576.)));", |
795 | " perror(\"shmat shared queues\"); must_exit = 1; break;", |
796 | " }", |
797 | "", |
798 | " m_workq[m] = (SM_frame *) shared_mem[m];", |
799 | " if (core_id == 0)", |
800 | " { int nframes = (m == NCORE) ? GN_FRAMES : LN_FRAMES;", |
801 | " for (n = 0; n < nframes; n++)", |
802 | " { m_workq[m][n].m_vsize = 0;", |
803 | " m_workq[m][n].m_boq = 0;", |
804 | " } } }", |
805 | "", |
806 | " if (must_exit)", |
807 | " { rm_shared_segments();", |
808 | " fprintf(stderr, \"pan: check './pan --' for usage details\\n\");", |
809 | " pan_exit(1); /* calls cleanup_shm */", |
810 | " }", |
811 | "}", |
812 | "", |
813 | "static uchar *", |
814 | "prep_shmid_S(size_t n) /* either sets SS or H_tab, linux/cygwin */", |
815 | "{ char *rval;", |
816 | "#ifndef SEP_STATE", |
817 | " key_t key;", |
818 | "", |
819 | " if (verbose && core_id == 0)", |
820 | " {", |
821 | " #ifdef BITSTATE", |
822 | " printf(\"cpu0: step 1: allocate shared bitstate %%g Mb\\n\",", |
823 | " (double) n / (1048576.));", |
824 | " #else", |
825 | " printf(\"cpu0: step 1: allocate shared hastable %%g Mb\\n\",", |
826 | " (double) n / (1048576.));", |
827 | " #endif", |
828 | " }", |
829 | " #ifdef MEMLIM", /* memlim has a value */ |
830 | " if (memcnt + (double) n > memlim)", |
831 | " { printf(\"cpu0: S %%8g + %%d Kb exceeds memory limit of %%8g Mb\\n\",", |
832 | " memcnt/1024., n/1024, memlim/(1048576.));", |
833 | " printf(\"cpu0: insufficient memory -- aborting\\n\");", |
834 | " exit(1);", |
835 | " }", |
836 | " #endif", |
837 | "", |
838 | " key = ftok(PanSource, NCORE+2); /* different from queues */", |
839 | " if (key == -1)", |
840 | " { perror(\"ftok shared bitstate or hashtable\");", |
841 | " fprintf(stderr, \"pan: check './pan --' for usage details\\n\");", |
842 | " pan_exit(1);", |
843 | " }", |
844 | "", |
845 | " if (core_id == 0) /* root */", |
846 | " { shmid_S = shmget(key, n, 0600);", |
847 | " if (shmid_S != -1)", |
848 | " { printf(\"cpu0: removing stale segment, status: %%d\\n\",", |
849 | " shmctl(shmid_S, IPC_RMID, NULL));", |
850 | " }", |
851 | " shmid_S = shmget(key, n, 0600 | IPC_CREAT | IPC_EXCL);", |
852 | " memcnt += (double) n;", |
853 | " } else /* worker */", |
854 | " { shmid_S = shmget(key, n, 0600);", |
855 | " }", |
856 | " if (shmid_S == -1)", |
857 | " { perror(\"shmget shared bitstate or hashtable too large?\");", |
858 | " fprintf(stderr, \"pan: check './pan --' for usage details\\n\");", |
859 | " pan_exit(1);", |
860 | " }", |
861 | "", |
862 | " rval = (char *) shmat(shmid_S, (void *) 0, 0); /* attach */", |
863 | " if ((char *) rval == (char *) -1)", |
864 | " { perror(\"shmat shared bitstate or hashtable\");", |
865 | " fprintf(stderr, \"pan: check './pan --' for usage details\\n\");", |
866 | " pan_exit(1);", |
867 | " }", |
868 | "#else", |
869 | " rval = (char *) emalloc(n);", |
870 | "#endif", |
871 | " return (uchar *) rval;", |
872 | "}", |
873 | "", |
874 | "#define TRY_AGAIN 1", |
875 | "#define NOT_AGAIN 0", |
876 | "", |
877 | "static char shm_prep_result;", |
878 | "", |
879 | "static uchar *", |
880 | "prep_state_mem(size_t n) /* sets memory arena for states linux/cygwin */", |
881 | "{ char *rval;", |
882 | " key_t key;", |
883 | " static int cnt = 3; /* start larger than earlier ftok calls */", |
884 | "", |
885 | " shm_prep_result = NOT_AGAIN; /* default */", |
886 | " if (verbose && core_id == 0)", |
887 | " { printf(\"cpu0: step 2+: pre-allocate memory arena %%d of %%6.2g Mb\\n\",", |
888 | " cnt-3, (double) n / (1048576.));", |
889 | " }", |
890 | " #ifdef MEMLIM", |
891 | " if (memcnt + (double) n > memlim)", |
892 | " { printf(\"cpu0: error: M %%.0f + %%.0f Kb exceeds memory limit of %%.0f Mb\\n\",", |
893 | " memcnt/1024.0, (double) n/1024.0, memlim/(1048576.));", |
894 | " return NULL;", |
895 | " }", |
896 | " #endif", |
897 | "", |
898 | " key = ftok(PanSource, NCORE+cnt); cnt++;", /* starts at NCORE+3 */ |
899 | " if (key == -1)", |
900 | " { perror(\"ftok T\");", |
901 | " printf(\"pan: check './pan --' for usage details\\n\");", |
902 | " pan_exit(1);", |
903 | " }", |
904 | "", |
905 | " if (core_id == 0)", |
906 | " { shmid_M = shmget(key, n, 0600);", |
907 | " if (shmid_M != -1)", |
908 | " { printf(\"cpu0: removing stale memory segment %%d, status: %%d\\n\",", |
909 | " cnt-3, shmctl(shmid_M, IPC_RMID, NULL));", |
910 | " }", |
911 | " shmid_M = shmget(key, n, 0600 | IPC_CREAT | IPC_EXCL);", |
912 | " /* memcnt += (double) n; -- only amount actually used is counted */", |
913 | " } else", |
914 | " { shmid_M = shmget(key, n, 0600);", |
915 | " ", |
916 | " }", |
917 | " if (shmid_M == -1)", |
918 | " { if (verbose)", |
919 | " { printf(\"error: failed to get pool of shared memory %%d of %%.0f Mb\\n\",", |
920 | " cnt-3, ((double)n)/(1048576.));", |
921 | " perror(\"state mem\");", |
922 | " printf(\"pan: check './pan --' for usage details\\n\");", |
923 | " }", |
924 | " shm_prep_result = TRY_AGAIN;", |
925 | " return NULL;", |
926 | " }", |
927 | " rval = (char *) shmat(shmid_M, (void *) 0, 0); /* attach */", |
928 | "", |
929 | " if ((char *) rval == (char *) -1)", |
930 | " { printf(\"cpu%%d error: failed to attach pool of shared memory %%d of %%.0f Mb\\n\",", |
931 | " core_id, cnt-3, ((double)n)/(1048576.));", |
932 | " perror(\"state mem\");", |
933 | " return NULL;", |
934 | " }", |
935 | " return (uchar *) rval;", |
936 | "}", |
937 | "", |
938 | "void", |
939 | "init_HT(unsigned long n) /* cygwin/linux version */", |
940 | "{ volatile char *x;", |
941 | " double get_mem;", |
942 | "#ifndef SEP_STATE", |
943 | " volatile char *dc_mem_start;", |
944 | " double need_mem, got_mem = 0.;", |
945 | "#endif", |
946 | "", |
947 | "#ifdef SEP_STATE", |
948 | " #ifndef MEMLIM", |
949 | " if (verbose)", |
950 | " { printf(\"cpu0: steps 0,1: no -DMEMLIM set\\n\");", /* cannot happen */ |
951 | " }", |
952 | " #else", |
953 | " if (verbose)", |
954 | " { printf(\"cpu0: steps 0,1: -DMEMLIM=%%d Mb - (hashtable %%g Mb + workqueues %%g Mb)\\n\",", |
955 | " MEMLIM, ((double)n/(1048576.)), (((double) NCORE * LWQ_SIZE) + GWQ_SIZE) /(1048576.) );", |
956 | " }", |
957 | " #endif", |
958 | " get_mem = NCORE * sizeof(double) + (1 + CS_NR) * sizeof(void *) + 4*sizeof(void *) + 2*sizeof(double);", |
959 | " /* NCORE * is_alive + search_terminated + CS_NR * sh_lock + 6 gr vars */", |
960 | " get_mem += 4 * NCORE * sizeof(void *); /* prfree, prfull, prcnt, prmax */", |
961 | " #ifdef FULL_TRAIL", |
962 | " get_mem += (NCORE) * sizeof(Stack_Tree *); /* NCORE * stack_last */", |
963 | " #endif", |
964 | " x = (volatile char *) prep_state_mem((size_t) get_mem); /* work queues and basic structs */", |
965 | " shmid_X = (long) x;", |
966 | " if (x == NULL)", /* do not repeat for smaller sizes */ |
967 | " { printf(\"cpu0: could not allocate shared memory, see ./pan --\\n\");", |
968 | " exit(1);", |
969 | " }", |
970 | " search_terminated = (volatile unsigned int *) x; /* comes first */", |
971 | " x += sizeof(void *); /* maintain alignment */", |
972 | "", |
973 | " is_alive = (volatile double *) x;", |
974 | " x += NCORE * sizeof(double);", |
975 | "", |
976 | " sh_lock = (volatile int *) x;", |
977 | " x += CS_NR * sizeof(void *);", /* allow 1 word per entry */ |
978 | "", |
979 | " grfree = (volatile int *) x;", |
980 | " x += sizeof(void *);", |
981 | " grfull = (volatile int *) x;", |
982 | " x += sizeof(void *);", |
983 | " grcnt = (volatile int *) x;", |
984 | " x += sizeof(void *);", |
985 | " grmax = (volatile int *) x;", |
986 | " x += sizeof(void *);", |
987 | " prfree = (volatile int *) x;", |
988 | " x += NCORE * sizeof(void *);", |
989 | " prfull = (volatile int *) x;", |
990 | " x += NCORE * sizeof(void *);", |
991 | " prcnt = (volatile int *) x;", |
992 | " x += NCORE * sizeof(void *);", |
993 | " prmax = (volatile int *) x;", |
994 | " x += NCORE * sizeof(void *);", |
995 | " gr_readmiss = (volatile double *) x;", |
996 | " x += sizeof(double);", |
997 | " gr_writemiss = (volatile double *) x;", |
998 | " x += sizeof(double);", |
999 | "", |
1000 | " #ifdef FULL_TRAIL", |
1001 | " stack_last = (volatile Stack_Tree **) x;", |
1002 | " x += NCORE * sizeof(Stack_Tree *);", |
1003 | " #endif", |
1004 | "", |
1005 | " #ifndef BITSTATE", |
1006 | " H_tab = (struct H_el **) emalloc(n);", |
1007 | " #endif", |
1008 | "#else", |
1009 | " #ifndef MEMLIM", |
1010 | " #warning MEMLIM not set", /* cannot happen */ |
1011 | " #define MEMLIM (2048)", |
1012 | " #endif", |
1013 | "", |
1014 | " if (core_id == 0 && verbose)", |
1015 | " { printf(\"cpu0: step 0: -DMEMLIM=%%d Mb minus hashtable+workqs (%%g + %%g Mb) leaves %%g Mb\\n\",", |
1016 | " MEMLIM, ((double)n/(1048576.)), (NCORE * LWQ_SIZE + GWQ_SIZE)/(1048576.),", |
1017 | " (memlim - memcnt - (double) n - (NCORE * LWQ_SIZE + GWQ_SIZE))/(1048576.));", |
1018 | " }", |
1019 | " #ifndef BITSTATE", |
1020 | " H_tab = (struct H_el **) prep_shmid_S((size_t) n); /* hash_table */", |
1021 | " #endif", |
1022 | " need_mem = memlim - memcnt - ((double) NCORE * LWQ_SIZE) - GWQ_SIZE;", |
1023 | " if (need_mem <= 0.)", |
1024 | " { Uerror(\"internal error -- shared state memory\");", |
1025 | " }", |
1026 | "", |
1027 | " if (core_id == 0 && verbose)", |
1028 | " { printf(\"cpu0: step 2: pre-allocate shared state memory %%g Mb\\n\",", |
1029 | " need_mem/(1048576.));", |
1030 | " }", |
1031 | "#ifdef SEP_HEAP", |
1032 | " SEG_SIZE = need_mem / NCORE;", |
1033 | " if (verbose && core_id == 0)", |
1034 | " { printf(\"cpu0: setting segsize to %%6g MB\\n\",", |
1035 | " SEG_SIZE/(1048576.));", |
1036 | " }", |
1037 | " #if defined(CYGWIN) || defined(__CYGWIN__)", |
1038 | " if (SEG_SIZE > 512.*1024.*1024.)", |
1039 | " { printf(\"warning: reducing SEG_SIZE of %%g MB to 512MB (exceeds max for Cygwin)\\n\",", |
1040 | " SEG_SIZE/(1024.*1024.));", |
1041 | " SEG_SIZE = 512.*1024.*1024.;", |
1042 | " }", |
1043 | " #endif", |
1044 | "#endif", |
1045 | " mem_reserved = need_mem;", |
1046 | " while (need_mem > 1024.)", |
1047 | " { get_mem = need_mem;", |
1048 | "shm_more:", |
1049 | " if (get_mem > (double) SEG_SIZE)", |
1050 | " { get_mem = (double) SEG_SIZE;", |
1051 | " }", |
1052 | " if (get_mem <= 0.0) break;", |
1053 | "", |
1054 | " /* for allocating states: */", |
1055 | " x = dc_mem_start = (volatile char *) prep_state_mem((size_t) get_mem);", |
1056 | " if (x == NULL)", |
1057 | " { if (shm_prep_result == NOT_AGAIN", |
1058 | " || first_pool != NULL", |
1059 | " || SEG_SIZE < (16. * 1048576.))", |
1060 | " { break;", |
1061 | " }", |
1062 | " SEG_SIZE /= 2.;", |
1063 | " if (verbose)", |
1064 | " { printf(\"pan: lowered segsize to %f\\n\", SEG_SIZE);", |
1065 | " }", |
1066 | " if (SEG_SIZE >= 1024.)", |
1067 | " { goto shm_more;", /* always terminates */ |
1068 | " }", |
1069 | " break;", |
1070 | " }", |
1071 | "", |
1072 | " need_mem -= get_mem;", |
1073 | " got_mem += get_mem;", |
1074 | " if (first_pool == NULL)", |
1075 | " { search_terminated = (volatile unsigned int *) x; /* comes first */", |
1076 | " x += sizeof(void *); /* maintain alignment */", |
1077 | "", |
1078 | " is_alive = (volatile double *) x;", |
1079 | " x += NCORE * sizeof(double);", |
1080 | "", |
1081 | " sh_lock = (volatile int *) x;", |
1082 | " x += CS_NR * sizeof(void *);", /* allow 1 word per entry */ |
1083 | "", |
1084 | " grfree = (volatile int *) x;", |
1085 | " x += sizeof(void *);", |
1086 | " grfull = (volatile int *) x;", |
1087 | " x += sizeof(void *);", |
1088 | " grcnt = (volatile int *) x;", |
1089 | " x += sizeof(void *);", |
1090 | " grmax = (volatile int *) x;", |
1091 | " x += sizeof(void *);", |
1092 | " prfree = (volatile int *) x;", |
1093 | " x += NCORE * sizeof(void *);", |
1094 | " prfull = (volatile int *) x;", |
1095 | " x += NCORE * sizeof(void *);", |
1096 | " prcnt = (volatile int *) x;", |
1097 | " x += NCORE * sizeof(void *);", |
1098 | " prmax = (volatile int *) x;", |
1099 | " x += NCORE * sizeof(void *);", |
1100 | " gr_readmiss = (volatile double *) x;", |
1101 | " x += sizeof(double);", |
1102 | " gr_writemiss = (volatile double *) x;", |
1103 | " x += sizeof(double);", |
1104 | " #ifdef FULL_TRAIL", |
1105 | " stack_last = (volatile Stack_Tree **) x;", |
1106 | " x += NCORE * sizeof(Stack_Tree *);", |
1107 | " #endif", |
1108 | " if (((long)x)&(sizeof(void *)-1)) /* 64-bit word alignment */", |
1109 | " { x += sizeof(void *)-(((long)x)&(sizeof(void *)-1));", |
1110 | " }", |
1111 | "", |
1112 | " #ifdef COLLAPSE", |
1113 | " ncomps = (unsigned long *) x;", |
1114 | " x += (256+2) * sizeof(unsigned long);", |
1115 | " #endif", |
1116 | " }", |
1117 | "", |
1118 | " dc_shared = (sh_Allocater *) x; /* must be in shared memory */", |
1119 | " x += sizeof(sh_Allocater);", |
1120 | "", |
1121 | " if (core_id == 0) /* root only */", |
1122 | " { dc_shared->dc_id = shmid_M;", |
1123 | " dc_shared->dc_start = dc_mem_start;", |
1124 | " dc_shared->dc_arena = x;", |
1125 | " dc_shared->pattern = 1234567; /* protection */", |
1126 | " dc_shared->dc_size = (long) get_mem - (long) (x - dc_mem_start);", |
1127 | " dc_shared->nxt = (long) 0;", |
1128 | "", |
1129 | " if (last_pool == NULL)", |
1130 | " { first_pool = last_pool = dc_shared;", |
1131 | " } else", |
1132 | " { last_pool->nxt = dc_shared;", |
1133 | " last_pool = dc_shared;", |
1134 | " }", |
1135 | " } else if (first_pool == NULL)", |
1136 | " { first_pool = dc_shared;", |
1137 | " } }", |
1138 | "", |
1139 | " if (need_mem > 1024.)", |
1140 | " { printf(\"cpu0: could allocate only %%g Mb of shared memory (wanted %%g more)\\n\",", |
1141 | " got_mem/(1048576.), need_mem/(1048576.));", |
1142 | " }", |
1143 | "", |
1144 | " if (!first_pool)", |
1145 | " { printf(\"cpu0: insufficient memory -- aborting.\\n\");", |
1146 | " exit(1);", |
1147 | " }", |
1148 | " /* we are still single-threaded at this point, with core_id 0 */", |
1149 | " dc_shared = first_pool;", |
1150 | "", |
1151 | "#endif", /* !SEP_STATE */ |
1152 | "}", |
1153 | "", |
1154 | " /* Test and Set assembly code */", |
1155 | "", |
1156 | " #if defined(i386) || defined(__i386__) || defined(__x86_64__)", |
1157 | " int", |
1158 | " tas(volatile int *s) /* tested */", |
1159 | " { int r;", |
1160 | " __asm__ __volatile__(", |
1161 | " \"xchgl %%0, %%1 \\n\\t\"", |
1162 | " : \"=r\"(r), \"=m\"(*s)", |
1163 | " : \"0\"(1), \"m\"(*s)", |
1164 | " : \"memory\");", |
1165 | " ", |
1166 | " return r;", |
1167 | " }", |
1168 | " #elif defined(__arm__)", |
1169 | " int", |
1170 | " tas(volatile int *s) /* not tested */", |
1171 | " { int r = 1;", |
1172 | " __asm__ __volatile__(", |
1173 | " \"swpb %%0, %%0, [%%3] \\n\"", |
1174 | " : \"=r\"(r), \"=m\"(*s)", |
1175 | " : \"0\"(r), \"r\"(s));", |
1176 | "", |
1177 | " return r;", |
1178 | " }", |
1179 | " #elif defined(sparc) || defined(__sparc__)", |
1180 | " int", |
1181 | " tas(volatile int *s) /* not tested */", |
1182 | " { int r = 1;", |
1183 | " __asm__ __volatile__(", |
1184 | " \" ldstub [%%2], %%0 \\n\"", |
1185 | " : \"=r\"(r), \"=m\"(*s)", |
1186 | " : \"r\"(s));", |
1187 | "", |
1188 | " return r;", |
1189 | " }", |
1190 | " #elif defined(ia64) || defined(__ia64__)", |
1191 | " /* Intel Itanium */", |
1192 | " int", |
1193 | " tas(volatile int *s) /* tested */", |
1194 | " { long int r;", |
1195 | " __asm__ __volatile__(", |
1196 | " \" xchg4 %%0=%%1,%%2 \\n\"", |
1197 | " : \"=r\"(r), \"+m\"(*s)", |
1198 | " : \"r\"(1)", |
1199 | " : \"memory\");", |
1200 | " return (int) r;", |
1201 | " }", |
1202 | " #else", |
1203 | " #error missing definition of test and set operation for this platform", |
1204 | " #endif", |
1205 | "", |
1206 | "void", |
1207 | "cleanup_shm(int val)", |
1208 | "{ volatile sh_Allocater *nxt_pool;", |
1209 | " unsigned long cnt = 0;", |
1210 | " int m;", |
1211 | "", |
1212 | " if (nibis != 0)", |
1213 | " { printf(\"cpu%%d: Redundant call to cleanup_shm(%%d)\\n\", core_id, val);", |
1214 | " return;", |
1215 | " } else", |
1216 | " { nibis = 1;", |
1217 | " }", |
1218 | " if (search_terminated != NULL)", |
1219 | " { *search_terminated |= 16; /* cleanup_shm */", |
1220 | " }", |
1221 | "", |
1222 | " for (m = 0; m < NR_QS; m++)", |
1223 | " { if (shmdt((void *) shared_mem[m]) > 0)", |
1224 | " { perror(\"shmdt detaching from shared queues\");", |
1225 | " } }", |
1226 | "", |
1227 | "#ifdef SEP_STATE", |
1228 | " if (shmdt((void *) shmid_X) != 0)", |
1229 | " { perror(\"shmdt detaching from shared state memory\");", |
1230 | " }", |
1231 | "#else", |
1232 | " #ifdef BITSTATE", |
1233 | " if (SS > 0 && shmdt((void *) SS) != 0)", |
1234 | " { if (verbose)", |
1235 | " { perror(\"shmdt detaching from shared bitstate arena\");", |
1236 | " } }", |
1237 | " #else", |
1238 | " if (core_id == 0)", |
1239 | " { /* before detaching: */", |
1240 | " for (nxt_pool = dc_shared; nxt_pool != NULL; nxt_pool = nxt_pool->nxt)", |
1241 | " { cnt += nxt_pool->dc_size;", |
1242 | " }", |
1243 | " if (verbose)", |
1244 | " { printf(\"cpu0: done, %%ld Mb of shared state memory left\\n\",", |
1245 | " cnt / (long)(1048576));", |
1246 | " } }", |
1247 | "", |
1248 | " if (shmdt((void *) H_tab) != 0)", |
1249 | " { perror(\"shmdt detaching from shared hashtable\");", |
1250 | " }", |
1251 | "", |
1252 | " for (last_pool = first_pool; last_pool != NULL; last_pool = nxt_pool)", |
1253 | " { nxt_pool = last_pool->nxt;", |
1254 | " if (shmdt((void *) last_pool->dc_start) != 0)", |
1255 | " { perror(\"shmdt detaching from shared state memory\");", |
1256 | " } }", |
1257 | " first_pool = last_pool = NULL; /* precaution */", |
1258 | " #endif", |
1259 | "#endif", |
1260 | " /* detached from shared memory - so cannot use cpu_printf */", |
1261 | " if (verbose)", |
1262 | " { printf(\"cpu%%d: done -- got %%d states from queue\\n\",", |
1263 | " core_id, nstates_get);", |
1264 | " }", |
1265 | "}", |
1266 | "", |
1267 | "extern void give_up(int);", |
1268 | "extern void Read_Queue(int);", |
1269 | "", |
1270 | "void", |
1271 | "mem_get(void)", |
1272 | "{ SM_frame *f;", |
1273 | " int is_parent;", |
1274 | "", |
1275 | "#if defined(MA) && !defined(SEP_STATE)", |
1276 | " #error MA without SEP_STATE is not supported with multi-core", |
1277 | "#endif", |
1278 | "#ifdef BFS", |
1279 | " #error BFS is not supported with multi-core", |
1280 | "#endif", |
1281 | "#ifdef SC", |
1282 | " #error SC is not supported with multi-core", |
1283 | "#endif", |
1284 | " init_shm(); /* we are single threaded when this starts */", |
1285 | "", |
1286 | " if (core_id == 0 && verbose)", |
1287 | " { printf(\"cpu0: step 4: calling fork()\\n\");", |
1288 | " }", |
1289 | " fflush(stdout);", |
1290 | "", |
1291 | "/* if NCORE > 1 the child or the parent should fork N-1 more times", |
1292 | " * the parent is the only process with core_id == 0 and is_parent > 0", |
1293 | " * the workers have is_parent = 0 and core_id = 1..NCORE-1", |
1294 | " */", |
1295 | " if (core_id == 0)", |
1296 | " { worker_pids[0] = getpid(); /* for completeness */", |
1297 | " while (++core_id < NCORE) /* first worker sees core_id = 1 */", |
1298 | " { is_parent = fork();", |
1299 | " if (is_parent == -1)", |
1300 | " { Uerror(\"fork failed\");", |
1301 | " }", |
1302 | " if (is_parent == 0) /* this is a worker process */", |
1303 | " { if (proxy_pid == core_id) /* always non-zero */", |
1304 | " { start_proxy(\"-r\", 0); /* no return */", |
1305 | " }", |
1306 | " goto adapt; /* root process continues spawning */", |
1307 | " }", |
1308 | " worker_pids[core_id] = is_parent;", |
1309 | " }", |
1310 | " /* note that core_id is now NCORE */", |
1311 | " if (proxy_pid > 0 && proxy_pid < NCORE)", /* add send-half of proxy */ |
1312 | " { proxy_pid_snd = fork();", |
1313 | " if (proxy_pid_snd == -1)", |
1314 | " { Uerror(\"proxy fork failed\");", |
1315 | " }", |
1316 | " if (proxy_pid_snd == 0)", |
1317 | " { start_proxy(\"-s\", worker_pids[proxy_pid]); /* no return */", |
1318 | " } } /* else continue */", |
1319 | |
1320 | " if (is_parent > 0)", |
1321 | " { core_id = 0; /* reset core_id for root process */", |
1322 | " }", |
1323 | " } else /* worker */", |
1324 | " { static char db0[16]; /* good for up to 10^6 cores */", |
1325 | " static char db1[16];", |
1326 | "adapt: tprefix = db0; sprefix = db1;", |
1327 | " sprintf(tprefix, \"cpu%%d_trail\", core_id);", |
1328 | " sprintf(sprefix, \"cpu%%d_rst\", core_id);", |
1329 | " memcnt = 0; /* count only additionally allocated memory */", |
1330 | " }", |
1331 | " signal(SIGINT, give_up);", |
1332 | "", |
1333 | " if (proxy_pid == 0) /* not in a cluster setup, pan_proxy must attach */", |
1334 | " { rm_shared_segments(); /* mark all shared segments for removal on exit */", |
1335 | " }", /* doing it early means less chance of being unable to do this */ |
1336 | " if (verbose)", |
1337 | " { cpu_printf(\"starting core_id %%d -- pid %%d\\n\", core_id, getpid());", |
1338 | " }", |
1339 | |
1340 | "#if defined(SEP_HEAP) && !defined(SEP_STATE)", /* set my_heap and adjust dc_shared */ |
1341 | " { int i;", |
1342 | " volatile sh_Allocater *ptr;", |
1343 | " ptr = first_pool;", |
1344 | " for (i = 0; i < NCORE && ptr != NULL; i++)", |
1345 | " { if (i == core_id)", |
1346 | " { my_heap = (char *) ptr->dc_arena;", |
1347 | " my_size = (long) ptr->dc_size;", |
1348 | " if (verbose)", |
1349 | " cpu_printf(\"local heap %%ld MB\\n\", my_size/(1048576));", |
1350 | " break;", |
1351 | " }", |
1352 | " ptr = ptr->nxt; /* local */", |
1353 | " }", |
1354 | " if (my_heap == NULL)", |
1355 | " { printf(\"cpu%%d: no local heap\\n\", core_id);", |
1356 | " pan_exit(1);", |
1357 | " } /* else */", |
1358 | " #if defined(CYGWIN) || defined(__CYGWIN__)", |
1359 | " ptr = first_pool;", |
1360 | " for (i = 0; i < NCORE && ptr != NULL; i++)", |
1361 | " { ptr = ptr->nxt; /* local */", |
1362 | " }", |
1363 | " dc_shared = ptr; /* any remainder */", |
1364 | " #else", |
1365 | " dc_shared = NULL; /* used all mem for local heaps */", |
1366 | " #endif", |
1367 | " }", |
1368 | "#endif", |
1369 | |
1370 | " if (core_id == 0 && !remote_party)", |
1371 | " { new_state(); /* cpu0 explores root */", |
1372 | " if (verbose)", |
1373 | " cpu_printf(\"done with 1st dfs, nstates %%g (put %%d states), read q\\n\",", |
1374 | " nstates, nstates_put);", |
1375 | " dfs_phase2 = 1;", |
1376 | " }", |
1377 | " Read_Queue(core_id); /* all cores */", |
1378 | "", |
1379 | " if (verbose)", |
1380 | " { cpu_printf(\"put %%6d states into queue -- got %%6d\\n\",", |
1381 | " nstates_put, nstates_get);", |
1382 | " }", |
1383 | " if (proxy_pid != 0)", |
1384 | " { rm_shared_segments();", |
1385 | " }", |
1386 | " done = 1;", |
1387 | " wrapup();", |
1388 | " exit(0);", |
1389 | "}", |
1390 | "", |
1391 | "#else", |
1392 | "int unpack_state(SM_frame *, int);", |
1393 | "#endif", |
1394 | "", |
1395 | "struct H_el *", |
1396 | "grab_shared(int n)", |
1397 | "{", |
1398 | "#ifndef SEP_STATE", |
1399 | " char *rval = (char *) 0;", |
1400 | "", |
1401 | " if (n == 0)", |
1402 | " { printf(\"cpu%%d: grab shared zero\\n\", core_id); fflush(stdout);", |
1403 | " return (struct H_el *) rval;", |
1404 | " } else if (n&(sizeof(void *)-1))", |
1405 | " { n += sizeof(void *)-(n&(sizeof(void *)-1)); /* alignment */", |
1406 | " }", |
1407 | "", |
1408 | "#ifdef SEP_HEAP", |
1409 | " /* no locking */", |
1410 | " if (my_heap != NULL && my_size > n)", |
1411 | " { rval = my_heap;", |
1412 | " my_heap += n;", |
1413 | " my_size -= n;", |
1414 | " goto done;", |
1415 | " }", |
1416 | "#endif", |
1417 | "", |
1418 | " if (!dc_shared)", |
1419 | " { sudden_stop(\"pan: out of memory\");", |
1420 | " }", |
1421 | "", |
1422 | " /* another lock is always already in effect when this is called */", |
1423 | " /* but not always the same lock -- i.e., on different parts of the hashtable */", |
1424 | " enter_critical(GLOBAL_LOCK); /* this must be independently mutex */", |
1425 | "#if defined(SEP_HEAP) && !defined(WIN32) && !defined(WIN64)", |
1426 | " { static int noted = 0;", |
1427 | " if (!noted)", |
1428 | " { noted = 1;", |
1429 | " printf(\"cpu%%d: global heap has %%ld bytes left, needed %%d\\n\",", |
1430 | " core_id, dc_shared?dc_shared->dc_size:0, n);", |
1431 | " } }", |
1432 | "#endif", |
1433 | "#if 0", /* for debugging */ |
1434 | " if (dc_shared->pattern != 1234567)", |
1435 | " { leave_critical(GLOBAL_LOCK);", |
1436 | " Uerror(\"overrun -- memory corruption\");", |
1437 | " }", |
1438 | "#endif", |
1439 | " if (dc_shared->dc_size < n)", |
1440 | " { if (verbose)", |
1441 | " { printf(\"Next Pool %%g Mb + %%d\\n\", memcnt/(1048576.), n);", |
1442 | " }", |
1443 | " if (dc_shared->nxt == NULL", |
1444 | " || dc_shared->nxt->dc_arena == NULL", |
1445 | " || dc_shared->nxt->dc_size < n)", |
1446 | " { printf(\"cpu%%d: memcnt %%g Mb + wanted %%d bytes more\\n\",", |
1447 | " core_id, memcnt / (1048576.), n);", |
1448 | " leave_critical(GLOBAL_LOCK);", |
1449 | " sudden_stop(\"out of memory -- aborting\");", |
1450 | " wrapup(); /* exits */", |
1451 | " } else", |
1452 | " { dc_shared = (sh_Allocater *) dc_shared->nxt;", |
1453 | " } }", |
1454 | "", |
1455 | " rval = (char *) dc_shared->dc_arena;", |
1456 | " dc_shared->dc_arena += n;", |
1457 | " dc_shared->dc_size -= (long) n;", |
1458 | "#if 0", |
1459 | " if (VVERBOSE)", |
1460 | " printf(\"cpu%%d grab shared (%%d bytes) -- %%ld left\\n\",", |
1461 | " core_id, n, dc_shared->dc_size);", |
1462 | "#endif", |
1463 | " leave_critical(GLOBAL_LOCK);", |
1464 | "done:", |
1465 | " memset(rval, 0, n);", |
1466 | " memcnt += (double) n;", |
1467 | "", |
1468 | " return (struct H_el *) rval;", |
1469 | "#else", |
1470 | " return (struct H_el *) emalloc(n);", |
1471 | "#endif", |
1472 | "}", |
1473 | "", |
1474 | "SM_frame *", |
1475 | "Get_Full_Frame(int n)", |
1476 | "{ SM_frame *f;", |
1477 | " double cnt_start = frame_wait;", |
1478 | "", |
1479 | " f = &m_workq[n][prfull[n]];", |
1480 | " while (f->m_vsize == 0) /* await full slot LOCK : full frame */", |
1481 | " { iam_alive();", |
1482 | "#ifndef NGQ", |
1483 | " #ifndef SAFETY", |
1484 | " if (!a_cycles || core_id != 0)", |
1485 | " #endif", |
1486 | " if (*grcnt > 0) /* accessed outside lock, but safe even if wrong */", |
1487 | " { enter_critical(GQ_RD); /* gq - read access */", |
1488 | " if (*grcnt > 0) /* could have changed */", |
1489 | " { f = &m_workq[NCORE][*grfull]; /* global q */", |
1490 | " if (f->m_vsize == 0)", |
1491 | " { /* writer is still filling the slot */", |
1492 | " *gr_writemiss++;", |
1493 | " f = &m_workq[n][prfull[n]]; /* reset */", |
1494 | " } else", |
1495 | " { *grfull = (*grfull+1) %% (GN_FRAMES);", |
1496 | " enter_critical(GQ_WR);", |
1497 | " *grcnt = *grcnt - 1;", |
1498 | " leave_critical(GQ_WR);", |
1499 | " leave_critical(GQ_RD);", |
1500 | " return f;", |
1501 | " } }", |
1502 | " leave_critical(GQ_RD);", |
1503 | " }", |
1504 | "#endif", |
1505 | " if (frame_wait++ - cnt_start > Delay)", |
1506 | " { if (0)", /* too frequent to enable this one */ |
1507 | " { cpu_printf(\"timeout on q%%d -- %%u -- query %%d\\n\",", |
1508 | " n, f, query_in_progress);", |
1509 | " }", |
1510 | " return (SM_frame *) 0; /* timeout */", |
1511 | " } }", |
1512 | " iam_alive();", |
1513 | " if (VVERBOSE) cpu_printf(\"got frame from q%%d\\n\", n);", |
1514 | " prfull[n] = (prfull[n] + 1) %% (LN_FRAMES);", |
1515 | " enter_critical(QLOCK(n));", |
1516 | " prcnt[n]--; /* lock out increments */", |
1517 | " leave_critical(QLOCK(n));", |
1518 | " return f;", |
1519 | "}", |
1520 | "", |
1521 | "SM_frame *", |
1522 | "Get_Free_Frame(int n)", |
1523 | "{ SM_frame *f;", |
1524 | " double cnt_start = free_wait;", |
1525 | "", |
1526 | " if (VVERBOSE) { cpu_printf(\"get free frame from q%%d\\n\", n); }", |
1527 | "", |
1528 | " if (n == NCORE) /* global q */", |
1529 | " { f = &(m_workq[n][lrfree]);", |
1530 | " } else", |
1531 | " { f = &(m_workq[n][prfree[n]]);", |
1532 | " }", |
1533 | " while (f->m_vsize != 0) /* await free slot LOCK : free slot */", |
1534 | " { iam_alive();", |
1535 | " if (free_wait++ - cnt_start > OneSecond)", |
1536 | " { if (verbose)", |
1537 | " { cpu_printf(\"timeout waiting for free slot q%%d\\n\", n);", |
1538 | " }", |
1539 | " cnt_start = free_wait;", |
1540 | " if (someone_crashed(1))", |
1541 | " { printf(\"cpu%%d: search terminated\\n\", core_id);", |
1542 | " sudden_stop(\"get free frame\");", |
1543 | " pan_exit(1);", |
1544 | " } } }", |
1545 | " if (n != NCORE)", |
1546 | " { prfree[n] = (prfree[n] + 1) %% (LN_FRAMES);", |
1547 | " enter_critical(QLOCK(n));", |
1548 | " prcnt[n]++; /* lock out decrements */", |
1549 | " if (prmax[n] < prcnt[n])", |
1550 | " { prmax[n] = prcnt[n];", |
1551 | " }", |
1552 | " leave_critical(QLOCK(n));", |
1553 | " }", |
1554 | " return f;", |
1555 | "}", |
1556 | "" |
1557 | "#ifndef NGQ", |
1558 | "int", |
1559 | "GlobalQ_HasRoom(void)", |
1560 | "{ int rval = 0;", |
1561 | "", |
1562 | " gq_tries++;", |
1563 | " if (*grcnt < GN_FRAMES) /* there seems to be room */", |
1564 | " { enter_critical(GQ_WR); /* gq write access */", |
1565 | " if (*grcnt < GN_FRAMES)", |
1566 | " { if (m_workq[NCORE][*grfree].m_vsize != 0)", |
1567 | " { /* can happen if reader is slow emptying slot */", |
1568 | " *gr_readmiss++;", |
1569 | " goto out; /* dont wait: release lock and return */", |
1570 | " }", |
1571 | " lrfree = *grfree; /* Get_Free_Frame use lrfree in this mode */", |
1572 | " *grfree = (*grfree + 1) %% GN_FRAMES;", /* next process looks at next slot */ |
1573 | " *grcnt = *grcnt + 1; /* count nr of slots filled -- no additional lock needed */", |
1574 | " if (*grmax < *grcnt) *grmax = *grcnt;", |
1575 | " leave_critical(GQ_WR); /* for short lock duration */", |
1576 | " gq_hasroom++;", |
1577 | " mem_put(NCORE); /* copy state into reserved slot */", |
1578 | " rval = 1; /* successfull handoff */", |
1579 | " } else", |
1580 | " { gq_hasnoroom++;", |
1581 | "out: leave_critical(GQ_WR);", /* should be rare */ |
1582 | " } }", |
1583 | " return rval;", |
1584 | "}", |
1585 | "#endif", |
1586 | "", |
1587 | "int", |
1588 | "unpack_state(SM_frame *f, int from_q)", |
1589 | "{ int i, j;", |
1590 | " static struct H_el D_State;", |
1591 | "", |
1592 | " if (f->m_vsize > 0)", |
1593 | " { boq = f->m_boq;", |
1594 | " if (boq > 256)", |
1595 | " { cpu_printf(\"saw control %%d, expected state\\n\", boq);", |
1596 | " return 0;", |
1597 | " }", |
1598 | " vsize = f->m_vsize;", |
1599 | "correct:", |
1600 | " memcpy((uchar *) &now, (uchar *) f->m_now, vsize);", |
1601 | " for (i = j = 0; i < VMAX; i++, j = (j+1)%%8)", |
1602 | " { Mask[i] = (f->m_Mask[i/8] & (1<<j)) ? 1 : 0;", |
1603 | " }", |
1604 | " if (now._nr_pr > 0)", |
1605 | " { memcpy((uchar *) proc_offset, (uchar *) f->m_p_offset, now._nr_pr * sizeof(OFFT));", |
1606 | " memcpy((uchar *) proc_skip, (uchar *) f->m_p_skip, now._nr_pr * sizeof(uchar));", |
1607 | " }", |
1608 | " if (now._nr_qs > 0)", |
1609 | " { memcpy((uchar *) q_offset, (uchar *) f->m_q_offset, now._nr_qs * sizeof(OFFT));", |
1610 | " memcpy((uchar *) q_skip, (uchar *) f->m_q_skip, now._nr_qs * sizeof(uchar));", |
1611 | " }", |
1612 | "#ifndef NOVSZ", |
1613 | " if (vsize != now._vsz)", |
1614 | " { cpu_printf(\"vsize %%d != now._vsz %%d (type %%d) %%d\\n\",", |
1615 | " vsize, now._vsz, f->m_boq, f->m_vsize);", |
1616 | " vsize = now._vsz;", |
1617 | " goto correct; /* rare event: a race */", |
1618 | " }", |
1619 | "#endif", |
1620 | " hmax = max(hmax, vsize);", |
1621 | "", |
1622 | " if (f != &cur_Root)", |
1623 | " { memcpy((uchar *) &cur_Root, (uchar *) f, sizeof(SM_frame));", |
1624 | " }", |
1625 | "", |
1626 | " if (((now._a_t) & 1) == 1) /* i.e., when starting nested DFS */", |
1627 | " { A_depth = depthfound = 0;", |
1628 | " memcpy((uchar *)&A_Root, (uchar *)&now, vsize);", |
1629 | " }", |
1630 | " nr_handoffs = f->nr_handoffs;", |
1631 | " } else", |
1632 | " { cpu_printf(\"pan: state empty\\n\");", |
1633 | " }", |
1634 | "", |
1635 | " depth = 0;", |
1636 | " trpt = &trail[1];", |
1637 | " trpt->tau = f->m_tau;", |
1638 | " trpt->o_pm = f->m_o_pm;", |
1639 | "", |
1640 | " (trpt-1)->ostate = &D_State; /* stub */", |
1641 | " trpt->ostate = &D_State;", |
1642 | "", |
1643 | "#ifdef FULL_TRAIL", |
1644 | " if (upto > 0)", |
1645 | " { stack_last[core_id] = (Stack_Tree *) f->m_stack;", |
1646 | " }", |
1647 | " #if defined(VERBOSE)", |
1648 | " if (stack_last[core_id])", |
1649 | " { cpu_printf(\"%%d: UNPACK -- SET m_stack %%u (%%d,%%d)\\n\",", |
1650 | " depth, stack_last[core_id], stack_last[core_id]->pr,", |
1651 | " stack_last[core_id]->t_id);", |
1652 | " }", |
1653 | " #endif", |
1654 | "#endif", |
1655 | "", |
1656 | " if (!trpt->o_t)", |
1657 | " { static Trans D_Trans;", |
1658 | " trpt->o_t = &D_Trans;", |
1659 | " }", |
1660 | "", |
1661 | " #ifdef VERI", |
1662 | " if ((trpt->tau & 4) != 4)", |
1663 | " { trpt->tau |= 4; /* the claim moves first */", |
1664 | " cpu_printf(\"warning: trpt was not up to date\\n\");", |
1665 | " }", |
1666 | " #endif", |
1667 | "", |
1668 | " for (i = 0; i < (int) now._nr_pr; i++)", |
1669 | " { P0 *ptr = (P0 *) pptr(i);", |
1670 | " #ifndef NP", |
1671 | " if (accpstate[ptr->_t][ptr->_p])", |
1672 | " { trpt->o_pm |= 2;", |
1673 | " }", |
1674 | " #else", |
1675 | " if (progstate[ptr->_t][ptr->_p])", |
1676 | " { trpt->o_pm |= 4;", |
1677 | " }", |
1678 | " #endif", |
1679 | " }", |
1680 | "", |
1681 | " #ifdef EVENT_TRACE", |
1682 | " #ifndef NP", |
1683 | " if (accpstate[EVENT_TRACE][now._event])", |
1684 | " { trpt->o_pm |= 2;", |
1685 | " }", |
1686 | " #else", |
1687 | " if (progstate[EVENT_TRACE][now._event])", |
1688 | " { trpt->o_pm |= 4;", |
1689 | " }", |
1690 | " #endif", |
1691 | " #endif", |
1692 | "", |
1693 | " #if defined(C_States) && (HAS_TRACK==1)", |
1694 | " /* restore state of tracked C objects */", |
1695 | " c_revert((uchar *) &(now.c_state[0]));", |
1696 | " #if (HAS_STACK==1)", |
1697 | " c_unstack((uchar *) f->m_c_stack); /* unmatched tracked data */", |
1698 | " #endif", |
1699 | " #endif", |
1700 | " return 1;", |
1701 | "}", |
1702 | "", |
1703 | "void", |
1704 | "write_root(void) /* for trail file */", |
1705 | "{ int fd;", |
1706 | "", |
1707 | " if (iterative == 0 && Nr_Trails > 1)", |
1708 | " sprintf(fnm, \"%%s%%d.%%s\", TrailFile, Nr_Trails-1, sprefix);", |
1709 | " else", |
1710 | " sprintf(fnm, \"%%s.%%s\", TrailFile, sprefix);", |
1711 | "", |
1712 | " if (cur_Root.m_vsize == 0)", |
1713 | " { (void) unlink(fnm); /* remove possible old copy */", |
1714 | " return; /* its the default initial state */", |
1715 | " }", |
1716 | "", |
1717 | " if ((fd = creat(fnm, TMODE)) < 0)", |
1718 | " { char *q;", |
1719 | " if ((q = strchr(TrailFile, \'.\')))", |
1720 | " { *q = \'\\0\'; /* strip .pml */", |
1721 | " if (iterative == 0 && Nr_Trails-1 > 0)", |
1722 | " sprintf(fnm, \"%%s%%d.%%s\", TrailFile, Nr_Trails-1, sprefix);", |
1723 | " else", |
1724 | " sprintf(fnm, \"%%s.%%s\", TrailFile, sprefix);", |
1725 | " *q = \'.\';", |
1726 | " fd = creat(fnm, TMODE);", |
1727 | " }", |
1728 | " if (fd < 0)", |
1729 | " { cpu_printf(\"pan: cannot create %%s\\n\", fnm);", |
1730 | " perror(\"cause\");", |
1731 | " return;", |
1732 | " } }", |
1733 | "", |
1734 | " if (write(fd, &cur_Root, sizeof(SM_frame)) != sizeof(SM_frame))", |
1735 | " { cpu_printf(\"pan: error writing %%s\\n\", fnm);", |
1736 | " } else", |
1737 | " { cpu_printf(\"pan: wrote %%s\\n\", fnm);", |
1738 | " }", |
1739 | " close(fd);", |
1740 | "}", |
1741 | "", |
1742 | "void", |
1743 | "set_root(void)", |
1744 | "{ int fd;", |
1745 | " char *q;", |
1746 | " char MyFile[512];", /* enough to hold a reasonable pathname */ |
1747 | " char MySuffix[16];", |
1748 | " char *ssuffix = \"rst\";", |
1749 | " int try_core = 1;", |
1750 | "", |
1751 | " strcpy(MyFile, TrailFile);", |
1752 | "try_again:", |
1753 | " if (whichtrail > 0)", |
1754 | " { sprintf(fnm, \"%%s%%d.%%s\", MyFile, whichtrail, ssuffix);", |
1755 | " fd = open(fnm, O_RDONLY, 0);", |
1756 | " if (fd < 0 && (q = strchr(MyFile, \'.\')))", |
1757 | " { *q = \'\\0\'; /* strip .pml */", |
1758 | " sprintf(fnm, \"%%s%%d.%%s\", MyFile, whichtrail, ssuffix);", |
1759 | " *q = \'.\';", |
1760 | " fd = open(fnm, O_RDONLY, 0);", |
1761 | " }", |
1762 | " } else", |
1763 | " { sprintf(fnm, \"%%s.%%s\", MyFile, ssuffix);", |
1764 | " fd = open(fnm, O_RDONLY, 0);", |
1765 | " if (fd < 0 && (q = strchr(MyFile, \'.\')))", |
1766 | " { *q = \'\\0\'; /* strip .pml */", |
1767 | " sprintf(fnm, \"%%s.%%s\", MyFile, ssuffix);", |
1768 | " *q = \'.\';", |
1769 | " fd = open(fnm, O_RDONLY, 0);", |
1770 | " } }", |
1771 | "", |
1772 | " if (fd < 0)", |
1773 | " { if (try_core < NCORE)", |
1774 | " { ssuffix = MySuffix;", |
1775 | " sprintf(ssuffix, \"cpu%%d_rst\", try_core++);", |
1776 | " goto try_again;", |
1777 | " }", |
1778 | " cpu_printf(\"no file '%%s.rst' or '%%s' (not an error)\\n\", MyFile, fnm);", |
1779 | " } else", |
1780 | " { if (read(fd, &cur_Root, sizeof(SM_frame)) != sizeof(SM_frame))", |
1781 | " { cpu_printf(\"read error %%s\\n\", fnm);", |
1782 | " close(fd);", |
1783 | " pan_exit(1);", |
1784 | " }", |
1785 | " close(fd);", |
1786 | " (void) unpack_state(&cur_Root, -2);", |
1787 | "#ifdef SEP_STATE", |
1788 | " cpu_printf(\"partial trail -- last few steps only\\n\");", |
1789 | "#endif", |
1790 | " cpu_printf(\"restored root from '%%s'\\n\", fnm);", |
1791 | " printf(\"=====State:=====\\n\");", |
1792 | " { int i, j; P0 *z;", |
1793 | " for (i = 0; i < now._nr_pr; i++)", |
1794 | " { z = (P0 *)pptr(i);", |
1795 | " printf(\"proc %%2d (%%s) \", i, procname[z->_t]);", |
1796 | |
1797 | " for (j = 0; src_all[j].src; j++)", |
1798 | " if (src_all[j].tp == (int) z->_t)", |
1799 | " { printf(\" line %%3d \\\"%%s\\\" \",", |
1800 | " src_all[j].src[z->_p], PanSource);", |
1801 | " break;", |
1802 | " }", |
1803 | " printf(\"(state %%d)\\n\", z->_p);", |
1804 | " c_locals(i, z->_t);", |
1805 | " }", |
1806 | " c_globals();", |
1807 | " }", |
1808 | " printf(\"================\\n\");", |
1809 | " }", |
1810 | "}", |
1811 | "", |
1812 | "#ifdef USE_DISK", |
1813 | "unsigned long dsk_written, dsk_drained;", |
1814 | "void mem_drain(void);", |
1815 | "#endif", |
1816 | "", |
1817 | "void", |
1818 | "m_clear_frame(SM_frame *f)", /* clear room for stats */ |
1819 | "{ int i, clr_sz = sizeof(SM_results);", |
1820 | "", |
1821 | " for (i = 0; i <= _NP_; i++) /* all proctypes */", |
1822 | " { clr_sz += NrStates[i]*sizeof(uchar);", |
1823 | " }", |
1824 | " memset(f, 0, clr_sz);", |
1825 | " /* caution if sizeof(SM_results) > sizeof(SM_frame) */", |
1826 | "}", |
1827 | "", |
1828 | "#define TargetQ_Full(n) (m_workq[n][prfree[n]].m_vsize != 0)", /* no free slot */ |
1829 | "#define TargetQ_NotFull(n) (m_workq[n][prfree[n]].m_vsize == 0)", /* avoiding prcnt */ |
1830 | "", |
1831 | "int", |
1832 | "AllQueuesEmpty(void)", |
1833 | "{ int q;", |
1834 | "#ifndef NGQ", |
1835 | " if (*grcnt != 0)", |
1836 | " { return 0;", |
1837 | " }", |
1838 | "#endif", |
1839 | " for (q = 0; q < NCORE; q++)", |
1840 | " { if (prcnt[q] != 0)", /* not locked, ok if race */ |
1841 | " { return 0;", |
1842 | " } }", |
1843 | " return 1;", |
1844 | "}", |
1845 | "", |
1846 | "void", |
1847 | "Read_Queue(int q)", |
1848 | "{ SM_frame *f, *of;", |
1849 | " int remember, target_q;", |
1850 | " SM_results *r;", |
1851 | " double patience = 0.0;", |
1852 | "", |
1853 | " target_q = (q + 1) %% NCORE;", |
1854 | "", |
1855 | " for (;;)", |
1856 | " { f = Get_Full_Frame(q);", |
1857 | " if (!f) /* 1 second timeout -- and trigger for Query */", |
1858 | " { if (someone_crashed(2))", |
1859 | " { printf(\"cpu%%d: search terminated [code %%d]\\n\",", |
1860 | " core_id, search_terminated?*search_terminated:-1);", |
1861 | " sudden_stop(\"\");", |
1862 | " pan_exit(1);", |
1863 | " }", |
1864 | "#ifdef TESTING", |
1865 | " /* to profile with cc -pg and gprof pan.exe -- set handoff depth beyond maxdepth */", |
1866 | " exit(0);", |
1867 | "#endif", |
1868 | " remember = *grfree;", |
1869 | " if (core_id == 0 /* root can initiate termination */", |
1870 | " && remote_party == 0 /* and only the original root */", |
1871 | " && query_in_progress == 0 /* unless its already in progress */", |
1872 | " && AllQueuesEmpty())", |
1873 | " { f = Get_Free_Frame(target_q);", |
1874 | " query_in_progress = 1; /* only root process can do this */", |
1875 | " if (!f) { Uerror(\"Fatal1: no free slot\"); }", |
1876 | " f->m_boq = QUERY; /* initiate Query */", |
1877 | " if (verbose)", |
1878 | " { cpu_printf(\"snd QUERY to q%%d (%%d) into slot %%d\\n\",", |
1879 | " target_q, nstates_get + 1, prfree[target_q]-1);", |
1880 | " }", |
1881 | " f->m_vsize = remember + 1;", |
1882 | " /* number will not change unless we receive more states */", |
1883 | " } else if (patience++ > OneHour) /* one hour watchdog timer */", |
1884 | " { cpu_printf(\"timeout -- giving up\\n\");", |
1885 | " sudden_stop(\"queue timeout\");", |
1886 | " pan_exit(1);", |
1887 | " }", |
1888 | " if (0) cpu_printf(\"timed out -- try again\\n\");", |
1889 | " continue; ", |
1890 | " }", |
1891 | " patience = 0.0; /* reset watchdog */", |
1892 | "", |
1893 | " if (f->m_boq == QUERY)", |
1894 | " { if (verbose)", |
1895 | " { cpu_printf(\"got QUERY on q%%d (%%d <> %%d) from slot %%d\\n\",", |
1896 | " q, f->m_vsize, nstates_put + 1, prfull[q]-1);", |
1897 | " snapshot();", |
1898 | " }", |
1899 | " remember = f->m_vsize;", |
1900 | " f->m_vsize = 0; /* release slot */", |
1901 | "", |
1902 | " if (core_id == 0 && remote_party == 0) /* original root cpu0 */", |
1903 | " { if (query_in_progress == 1 /* didn't send more states in the interim */", |
1904 | " && *grfree + 1 == remember) /* no action on global queue meanwhile */", |
1905 | " { if (verbose) cpu_printf(\"Termination detected\\n\");", |
1906 | " if (TargetQ_Full(target_q))", |
1907 | " { if (verbose)", |
1908 | " cpu_printf(\"warning: target q is full\\n\");", |
1909 | " }", |
1910 | " f = Get_Free_Frame(target_q);", |
1911 | " if (!f) { Uerror(\"Fatal2: no free slot\"); }", |
1912 | " m_clear_frame(f);", |
1913 | " f->m_boq = QUIT; /* send final Quit, collect stats */", |
1914 | " f->m_vsize = 111; /* anything non-zero will do */", |
1915 | " if (verbose)", |
1916 | " cpu_printf(\"put QUIT on q%%d\\n\", target_q);", |
1917 | " } else", |
1918 | " { if (verbose) cpu_printf(\"Stale Query\\n\");", |
1919 | "#ifdef USE_DISK", |
1920 | " mem_drain();", |
1921 | "#endif", |
1922 | " }", |
1923 | " query_in_progress = 0;", |
1924 | " } else", |
1925 | " { if (TargetQ_Full(target_q))", |
1926 | " { if (verbose)", |
1927 | " cpu_printf(\"warning: forward query - target q full\\n\");", |
1928 | " }", |
1929 | " f = Get_Free_Frame(target_q);", |
1930 | " if (verbose)", |
1931 | " cpu_printf(\"snd QUERY response to q%%d (%%d <> %%d) in slot %%d\\n\",", |
1932 | " target_q, remember, *grfree + 1, prfree[target_q]-1);", |
1933 | " if (!f) { Uerror(\"Fatal4: no free slot\"); }", |
1934 | "", |
1935 | " if (*grfree + 1 == remember) /* no action on global queue */", |
1936 | " { f->m_boq = QUERY; /* forward query, to root */", |
1937 | " f->m_vsize = remember;", |
1938 | " } else", |
1939 | " { f->m_boq = QUERY_F; /* no match -- busy */", |
1940 | " f->m_vsize = 112; /* anything non-zero */", |
1941 | "#ifdef USE_DISK", |
1942 | " if (dsk_written != dsk_drained)", |
1943 | " { mem_drain();", |
1944 | " }", |
1945 | "#endif", |
1946 | " } }", |
1947 | " continue;", |
1948 | " }", |
1949 | "", |
1950 | " if (f->m_boq == QUERY_F)", |
1951 | " { if (verbose)", |
1952 | " { cpu_printf(\"got QUERY_F on q%%d from slot %%d\\n\", q, prfull[q]-1);", |
1953 | " }", |
1954 | " f->m_vsize = 0; /* release slot */", |
1955 | "", |
1956 | " if (core_id == 0 && remote_party == 0) /* original root cpu0 */", |
1957 | " { if (verbose) cpu_printf(\"No Match on Query\\n\");", |
1958 | " query_in_progress = 0;", |
1959 | " } else", |
1960 | " { if (TargetQ_Full(target_q))", |
1961 | " { if (verbose) cpu_printf(\"warning: forwarding query_f, target queue full\\n\");", |
1962 | " }", |
1963 | " f = Get_Free_Frame(target_q);", |
1964 | " if (verbose) cpu_printf(\"forward QUERY_F to q%%d into slot %%d\\n\",", |
1965 | " target_q, prfree[target_q]-1);", |
1966 | " if (!f) { Uerror(\"Fatal5: no free slot\"); }", |
1967 | " f->m_boq = QUERY_F; /* cannot terminate yet */", |
1968 | " f->m_vsize = 113; /* anything non-zero */", |
1969 | " }", |
1970 | "#ifdef USE_DISK", |
1971 | " if (dsk_written != dsk_drained)", |
1972 | " { mem_drain();", |
1973 | " }", |
1974 | "#endif", |
1975 | " continue;", |
1976 | " }", |
1977 | "", |
1978 | " if (f->m_boq == QUIT)", |
1979 | " { if (0) cpu_printf(\"done -- local memcnt %%g Mb\\n\", memcnt/(1048576.));", |
1980 | " retrieve_info((SM_results *) f); /* collect and combine stats */", |
1981 | " if (verbose)", |
1982 | " { cpu_printf(\"received Quit\\n\");", |
1983 | " snapshot();", |
1984 | " }", |
1985 | " f->m_vsize = 0; /* release incoming slot */", |
1986 | " if (core_id != 0)", |
1987 | " { f = Get_Free_Frame(target_q); /* new outgoing slot */", |
1988 | " if (!f) { Uerror(\"Fatal6: no free slot\"); }", |
1989 | " m_clear_frame(f); /* start with zeroed stats */", |
1990 | " record_info((SM_results *) f);", |
1991 | " f->m_boq = QUIT; /* forward combined results */", |
1992 | " f->m_vsize = 114; /* anything non-zero */", |
1993 | " if (verbose>1)", |
1994 | " cpu_printf(\"fwd Results to q%%d\\n\", target_q);", |
1995 | " }", |
1996 | " break; /* successful termination */", |
1997 | " }", |
1998 | "", |
1999 | " /* else: 0<= boq <= 255, means STATE transfer */", |
2000 | " if (unpack_state(f, q) != 0)", |
2001 | " { nstates_get++;", |
2002 | " f->m_vsize = 0; /* release slot */", |
2003 | " if (VVERBOSE) cpu_printf(\"Got state\\n\");", |
2004 | "", |
2005 | " if (search_terminated != NULL", |
2006 | " && *search_terminated == 0)", |
2007 | " { new_state(); /* explore successors */", |
2008 | " memset((uchar *) &cur_Root, 0, sizeof(SM_frame)); /* avoid confusion */", |
2009 | " } else", |
2010 | " { pan_exit(0);", |
2011 | " }", |
2012 | " } else", |
2013 | " { pan_exit(0);", |
2014 | " } }", |
2015 | " if (verbose) cpu_printf(\"done got %%d put %%d\\n\", nstates_get, nstates_put);", |
2016 | " sleep_report();", |
2017 | "}", |
2018 | "", |
2019 | "void", |
2020 | "give_up(int unused_x)", |
2021 | "{", |
2022 | " if (search_terminated != NULL)", |
2023 | " { *search_terminated |= 32; /* give_up */", |
2024 | " }", |
2025 | " if (!writing_trail)", |
2026 | " { was_interrupted = 1;", |
2027 | " snapshot();", |
2028 | " cpu_printf(\"Give Up\\n\");", |
2029 | " sleep_report();", |
2030 | " pan_exit(1);", |
2031 | " } else /* we are already terminating */", |
2032 | " { cpu_printf(\"SIGINT\\n\");", |
2033 | " }", |
2034 | "}", |
2035 | "", |
2036 | "void", |
2037 | "check_overkill(void)", |
2038 | "{", |
2039 | " vmax_seen = (vmax_seen + 7)/ 8;", |
2040 | " vmax_seen *= 8; /* round up to a multiple of 8 */", |
2041 | "", |
2042 | " if (core_id == 0", |
2043 | " && !remote_party", |
2044 | " && nstates_put > 0", |
2045 | " && VMAX - vmax_seen > 8)", |
2046 | " {", |
2047 | "#ifdef BITSTATE", |
2048 | " printf(\"cpu0: max VMAX value seen in this run: \");", |
2049 | "#else", |
2050 | " printf(\"cpu0: recommend recompiling with \");", |
2051 | "#endif", |
2052 | " printf(\"-DVMAX=%%d\\n\", vmax_seen);", |
2053 | " }", |
2054 | "}", |
2055 | "", |
2056 | "void", |
2057 | "mem_put(int q) /* handoff state to other cpu, workq q */", |
2058 | "{ SM_frame *f;", |
2059 | " int i, j;", |
2060 | "", |
2061 | " if (vsize > VMAX)", |
2062 | " { vsize = (vsize + 7)/8; vsize *= 8; /* round up */", |
2063 | " printf(\"pan: recompile with -DVMAX=N with N >= %%d\\n\", vsize);", |
2064 | " Uerror(\"aborting\");", |
2065 | " }", |
2066 | " if (now._nr_pr > PMAX)", |
2067 | " { printf(\"pan: recompile with -DPMAX=N with N >= %%d\\n\", now._nr_pr);", |
2068 | " Uerror(\"aborting\");", |
2069 | " }", |
2070 | " if (now._nr_qs > QMAX)", |
2071 | " { printf(\"pan: recompile with -DQMAX=N with N >= %%d\\n\", now._nr_qs);", |
2072 | " Uerror(\"aborting\");", |
2073 | " }", |
2074 | " if (vsize > vmax_seen) vmax_seen = vsize;", |
2075 | " if (now._nr_pr > pmax_seen) pmax_seen = now._nr_pr;", |
2076 | " if (now._nr_qs > qmax_seen) qmax_seen = now._nr_qs;", |
2077 | "", |
2078 | " f = Get_Free_Frame(q); /* not called in likely deadlock states */", |
2079 | " if (!f) { Uerror(\"Fatal3: no free slot\"); }", |
2080 | "", |
2081 | " if (VVERBOSE) cpu_printf(\"putting state into q%%d\\n\", q);", |
2082 | "", |
2083 | " memcpy((uchar *) f->m_now, (uchar *) &now, vsize);", |
2084 | " memset((uchar *) f->m_Mask, 0, (VMAX+7)/8 * sizeof(char));", |
2085 | " for (i = j = 0; i < VMAX; i++, j = (j+1)%%8)", |
2086 | " { if (Mask[i])", |
2087 | " { f->m_Mask[i/8] |= (1<<j);", |
2088 | " } }", |
2089 | "", |
2090 | " if (now._nr_pr > 0)", |
2091 | " { memcpy((uchar *) f->m_p_offset, (uchar *) proc_offset, now._nr_pr * sizeof(OFFT));", |
2092 | " memcpy((uchar *) f->m_p_skip, (uchar *) proc_skip, now._nr_pr * sizeof(uchar));", |
2093 | " }", |
2094 | " if (now._nr_qs > 0)", |
2095 | " { memcpy((uchar *) f->m_q_offset, (uchar *) q_offset, now._nr_qs * sizeof(OFFT));", |
2096 | " memcpy((uchar *) f->m_q_skip, (uchar *) q_skip, now._nr_qs * sizeof(uchar));", |
2097 | " }", |
2098 | "#if defined(C_States) && (HAS_TRACK==1) && (HAS_STACK==1)", |
2099 | " c_stack((uchar *) f->m_c_stack); /* save unmatched tracked data */", |
2100 | "#endif", |
2101 | "#ifdef FULL_TRAIL", |
2102 | " f->m_stack = stack_last[core_id];", |
2103 | "#endif", |
2104 | " f->nr_handoffs = nr_handoffs+1;", |
2105 | " f->m_tau = trpt->tau;", |
2106 | " f->m_o_pm = trpt->o_pm;", |
2107 | " f->m_boq = boq;", |
2108 | " f->m_vsize = vsize; /* must come last - now the other cpu can see it */", |
2109 | "", |
2110 | " if (query_in_progress == 1)", |
2111 | " query_in_progress = 2; /* make sure we know, if a query makes the rounds */", |
2112 | " nstates_put++;", |
2113 | "}", |
2114 | "", |
2115 | "#ifdef USE_DISK", |
2116 | "int Dsk_W_Nr, Dsk_R_Nr;", |
2117 | "int dsk_file = -1, dsk_read = -1;", |
2118 | "unsigned long dsk_written, dsk_drained;", |
2119 | "char dsk_name[512];", |
2120 | "", |
2121 | "#ifndef BFS_DISK", |
2122 | "#if defined(WIN32) || defined(WIN64)", |
2123 | " #define RFLAGS (O_RDONLY|O_BINARY)", |
2124 | " #define WFLAGS (O_CREAT|O_WRONLY|O_TRUNC|O_BINARY)", |
2125 | "#else", |
2126 | " #define RFLAGS (O_RDONLY)", |
2127 | " #define WFLAGS (O_CREAT|O_WRONLY|O_TRUNC)", |
2128 | "#endif", |
2129 | "#endif", |
2130 | "", |
2131 | "void", |
2132 | "dsk_stats(void)", |
2133 | "{ int i;", |
2134 | "", |
2135 | " if (dsk_written > 0)", |
2136 | " { cpu_printf(\"dsk_written %%d states in %%d files\\ncpu%%d: dsk_drained %%6d states\\n\",", |
2137 | " dsk_written, Dsk_W_Nr, core_id, dsk_drained);", |
2138 | " close(dsk_read);", |
2139 | " close(dsk_file);", |
2140 | " for (i = 0; i < Dsk_W_Nr; i++)", |
2141 | " { sprintf(dsk_name, \"Q%%.3d_%%.3d.tmp\", i, core_id);", |
2142 | " unlink(dsk_name);", |
2143 | " } }", |
2144 | "}", |
2145 | "", |
2146 | "void", |
2147 | "mem_drain(void)", |
2148 | "{ SM_frame *f, g;", |
2149 | " int q = (core_id + 1) %% NCORE; /* target q */", |
2150 | " int sz;", |
2151 | "", |
2152 | " if (dsk_read < 0", |
2153 | " || dsk_written <= dsk_drained)", |
2154 | " { return;", |
2155 | " }", |
2156 | "", |
2157 | " while (dsk_written > dsk_drained", |
2158 | " && TargetQ_NotFull(q))", |
2159 | " { f = Get_Free_Frame(q);", |
2160 | " if (!f) { Uerror(\"Fatal: unhandled condition\"); }", |
2161 | "", |
2162 | " if ((dsk_drained+1)%%MAX_DSK_FILE == 0) /* 100K states max per file */", |
2163 | " { (void) close(dsk_read); /* close current read handle */", |
2164 | " sprintf(dsk_name, \"Q%%.3d_%%.3d.tmp\", Dsk_R_Nr++, core_id);", |
2165 | " (void) unlink(dsk_name); /* remove current file */", |
2166 | " sprintf(dsk_name, \"Q%%.3d_%%.3d.tmp\", Dsk_R_Nr, core_id);", |
2167 | " cpu_printf(\"reading %%s\\n\", dsk_name);", |
2168 | " dsk_read = open(dsk_name, RFLAGS); /* open next file */", |
2169 | " if (dsk_read < 0)", |
2170 | " { Uerror(\"could not open dsk file\");", |
2171 | " } }", |
2172 | " if (read(dsk_read, &g, sizeof(SM_frame)) != sizeof(SM_frame))", |
2173 | " { Uerror(\"bad dsk file read\");", |
2174 | " }", |
2175 | " sz = g.m_vsize;", |
2176 | " g.m_vsize = 0;", |
2177 | " memcpy(f, &g, sizeof(SM_frame));", |
2178 | " f->m_vsize = sz; /* last */", |
2179 | "", |
2180 | " dsk_drained++;", |
2181 | " }", |
2182 | "}", |
2183 | "", |
2184 | "void", |
2185 | "mem_file(void)", |
2186 | "{ SM_frame f;", |
2187 | " int i, j, q = (core_id + 1) %% NCORE; /* target q */", |
2188 | "", |
2189 | " if (vsize > VMAX)", |
2190 | " { printf(\"pan: recompile with -DVMAX=N with N >= %%d\\n\", vsize);", |
2191 | " Uerror(\"aborting\");", |
2192 | " }", |
2193 | " if (now._nr_pr > PMAX)", |
2194 | " { printf(\"pan: recompile with -DPMAX=N with N >= %%d\\n\", now._nr_pr);", |
2195 | " Uerror(\"aborting\");", |
2196 | " }", |
2197 | " if (now._nr_qs > QMAX)", |
2198 | " { printf(\"pan: recompile with -DQMAX=N with N >= %%d\\n\", now._nr_qs);", |
2199 | " Uerror(\"aborting\");", |
2200 | " }", |
2201 | "", |
2202 | " if (VVERBOSE) cpu_printf(\"filing state for q%%d\\n\", q);", |
2203 | "", |
2204 | " memcpy((uchar *) f.m_now, (uchar *) &now, vsize);", |
2205 | " memset((uchar *) f.m_Mask, 0, (VMAX+7)/8 * sizeof(char));", |
2206 | " for (i = j = 0; i < VMAX; i++, j = (j+1)%%8)", |
2207 | " { if (Mask[i])", |
2208 | " { f.m_Mask[i/8] |= (1<<j);", |
2209 | " } }", |
2210 | "", |
2211 | " if (now._nr_pr > 0)", |
2212 | " { memcpy((uchar *)f.m_p_offset, (uchar *)proc_offset, now._nr_pr*sizeof(OFFT));", |
2213 | " memcpy((uchar *)f.m_p_skip, (uchar *)proc_skip, now._nr_pr*sizeof(uchar));", |
2214 | " }", |
2215 | " if (now._nr_qs > 0)", |
2216 | " { memcpy((uchar *) f.m_q_offset, (uchar *) q_offset, now._nr_qs*sizeof(OFFT));", |
2217 | " memcpy((uchar *) f.m_q_skip, (uchar *) q_skip, now._nr_qs*sizeof(uchar));", |
2218 | " }", |
2219 | "#if defined(C_States) && (HAS_TRACK==1) && (HAS_STACK==1)", |
2220 | " c_stack((uchar *) f.m_c_stack); /* save unmatched tracked data */", |
2221 | "#endif", |
2222 | "#ifdef FULL_TRAIL", |
2223 | " f.m_stack = stack_last[core_id];", |
2224 | "#endif", |
2225 | " f.nr_handoffs = nr_handoffs+1;", |
2226 | " f.m_tau = trpt->tau;", |
2227 | " f.m_o_pm = trpt->o_pm;", |
2228 | " f.m_boq = boq;", |
2229 | " f.m_vsize = vsize;", |
2230 | "", |
2231 | " if (query_in_progress == 1)", |
2232 | " { query_in_progress = 2;", |
2233 | " }", |
2234 | " if (dsk_file < 0)", |
2235 | " { sprintf(dsk_name, \"Q%%.3d_%%.3d.tmp\", Dsk_W_Nr, core_id);", |
2236 | " dsk_file = open(dsk_name, WFLAGS, 0644);", |
2237 | " dsk_read = open(dsk_name, RFLAGS);", |
2238 | " if (dsk_file < 0 || dsk_read < 0)", |
2239 | " { cpu_printf(\"File: <%%s>\\n\", dsk_name);", |
2240 | " Uerror(\"cannot open diskfile\");", |
2241 | " }", |
2242 | " Dsk_W_Nr++; /* nr of next file to open */", |
2243 | " cpu_printf(\"created temporary diskfile %%s\\n\", dsk_name);", |
2244 | " } else if ((dsk_written+1)%%MAX_DSK_FILE == 0)", |
2245 | " { close(dsk_file); /* close write handle */", |
2246 | " sprintf(dsk_name, \"Q%%.3d_%%.3d.tmp\", Dsk_W_Nr++, core_id);", |
2247 | " dsk_file = open(dsk_name, WFLAGS, 0644);", |
2248 | " if (dsk_file < 0)", |
2249 | " { cpu_printf(\"File: <%%s>\\n\", dsk_name);", |
2250 | " Uerror(\"aborting: cannot open new diskfile\");", |
2251 | " }", |
2252 | " cpu_printf(\"created temporary diskfile %%s\\n\", dsk_name);", |
2253 | " }", |
2254 | " if (write(dsk_file, &f, sizeof(SM_frame)) != sizeof(SM_frame))", |
2255 | " { Uerror(\"aborting -- disk write failed (disk full?)\");", |
2256 | " }", |
2257 | " nstates_put++;", |
2258 | " dsk_written++;", |
2259 | "}", |
2260 | "#endif", |
2261 | "", |
2262 | "int", |
2263 | "mem_hand_off(void)", |
2264 | "{", |
2265 | " if (search_terminated == NULL", |
2266 | " || *search_terminated != 0) /* not a full crash check */", |
2267 | " { pan_exit(0);", |
2268 | " }", |
2269 | " iam_alive(); /* on every transition of Down */", |
2270 | "#ifdef USE_DISK", |
2271 | " mem_drain(); /* maybe call this also on every Up */", |
2272 | "#endif", |
2273 | " if (depth > z_handoff /* above handoff limit */", |
2274 | "#ifndef SAFETY", |
2275 | " && !a_cycles /* not in liveness mode */", |
2276 | "#endif", |
2277 | "#if SYNC", |
2278 | " && boq == -1 /* not mid-rv */", |
2279 | "#endif", |
2280 | "#ifdef VERI", |
2281 | " && (trpt->tau&4) /* claim moves first */", |
2282 | " && !((trpt-1)->tau&128) /* not a stutter move */", |
2283 | "#endif", |
2284 | " && !(trpt->tau&8)) /* not an atomic move */", |
2285 | " { int q = (core_id + 1) %% NCORE; /* circular handoff */", |
2286 | " #ifdef GENEROUS", |
2287 | " if (prcnt[q] < LN_FRAMES)", /* not the best strategy */ |
2288 | " #else", |
2289 | " if (TargetQ_NotFull(q)", |
2290 | " && (dfs_phase2 == 0 || prcnt[core_id] > 0))", /* not locked, ok if race */ |
2291 | " #endif", |
2292 | " { mem_put(q);", /* only 1 writer: lock-free */ |
2293 | " return 1;", |
2294 | " }", |
2295 | " { int rval;", |
2296 | " #ifndef NGQ", |
2297 | " rval = GlobalQ_HasRoom();", |
2298 | " #else", |
2299 | " rval = 0;", |
2300 | " #endif", |
2301 | " #ifdef USE_DISK", |
2302 | " if (rval == 0)", |
2303 | " { void mem_file(void);", |
2304 | " mem_file();", |
2305 | " rval = 1;", |
2306 | " }", |
2307 | " #endif", |
2308 | " return rval;", |
2309 | " }", |
2310 | " }", |
2311 | " return 0; /* i.e., no handoff */", |
2312 | "}", |
2313 | "", |
2314 | "void", |
2315 | "mem_put_acc(void) /* liveness mode */", |
2316 | "{ int q = (core_id + 1) %% NCORE;", |
2317 | "", |
2318 | " if (search_terminated == NULL", |
2319 | " || *search_terminated != 0)", |
2320 | " { pan_exit(0);", |
2321 | " }", |
2322 | "#ifdef USE_DISK", |
2323 | " mem_drain();", |
2324 | "#endif", |
2325 | " /* some tortured use of preprocessing: */", |
2326 | "#if !defined(NGQ) || defined(USE_DISK)", |
2327 | " if (TargetQ_Full(q))", |
2328 | " {", |
2329 | "#endif", |
2330 | "#ifndef NGQ", |
2331 | " if (GlobalQ_HasRoom())", |
2332 | " { return;", |
2333 | " }", |
2334 | "#endif", |
2335 | "#ifdef USE_DISK", |
2336 | " mem_file();", |
2337 | " } else", |
2338 | "#else", |
2339 | " #if !defined(NGQ) || defined(USE_DISK)", |
2340 | " }", |
2341 | " #endif", |
2342 | "#endif", |
2343 | " { mem_put(q);", |
2344 | " }", |
2345 | "}", |
2346 | "", |
2347 | "#if defined(WIN32) || defined(WIN64)", /* visual studio */ |
2348 | "void", |
2349 | "init_shm(void) /* initialize shared work-queues */", |
2350 | "{ char key[512];", |
2351 | " int n, m;", |
2352 | " int must_exit = 0;", |
2353 | "", |
2354 | " if (core_id == 0 && verbose)", |
2355 | " { printf(\"cpu0: step 3: allocate shared work-queues %%g Mb\\n\",", |
2356 | " ((double) NCORE * LWQ_SIZE + GWQ_SIZE) / (1048576.));", |
2357 | " }", |
2358 | " for (m = 0; m < NR_QS; m++) /* last q is global 1 */", |
2359 | " { double qsize = (m == NCORE) ? GWQ_SIZE : LWQ_SIZE;", |
2360 | " sprintf(key, \"Global\\\\pan_%%s_%%.3d\", PanSource, m);", |
2361 | " if (core_id == 0)", /* root process creates shared memory segments */ |
2362 | " { shmid[m] = CreateFileMapping(", |
2363 | " INVALID_HANDLE_VALUE, /* use paging file */", |
2364 | " NULL, /* default security */", |
2365 | " PAGE_READWRITE, /* access permissions */", |
2366 | " 0, /* high-order 4 bytes */", |
2367 | " qsize, /* low-order bytes, size in bytes */", |
2368 | " key); /* name */", |
2369 | " } else /* worker nodes just open these segments */", |
2370 | " { shmid[m] = OpenFileMapping(", |
2371 | " FILE_MAP_ALL_ACCESS, /* read/write access */", |
2372 | " FALSE, /* children do not inherit handle */", |
2373 | " key);", |
2374 | " }", |
2375 | " if (shmid[m] == NULL)", |
2376 | " { fprintf(stderr, \"cpu%%d: could not create or open shared queues\\n\",", |
2377 | " core_id);", |
2378 | " must_exit = 1;", |
2379 | " break;", |
2380 | " }", |
2381 | " /* attach: */", |
2382 | " shared_mem[m] = (char *) MapViewOfFile(shmid[m], FILE_MAP_ALL_ACCESS, 0, 0, 0);", |
2383 | " if (shared_mem[m] == NULL)", |
2384 | " { fprintf(stderr, \"cpu%%d: cannot attach shared q%%d (%%d Mb)\\n\",", |
2385 | " core_id, m+1, (int) (qsize/(1048576.)));", |
2386 | " must_exit = 1;", |
2387 | " break;", |
2388 | " }", |
2389 | "", |
2390 | " memcnt += qsize;", |
2391 | "", |
2392 | " m_workq[m] = (SM_frame *) shared_mem[m];", |
2393 | " if (core_id == 0)", |
2394 | " { int nframes = (m == NCORE) ? GN_FRAMES : LN_FRAMES;", |
2395 | " for (n = 0; n < nframes; n++)", |
2396 | " { m_workq[m][n].m_vsize = 0;", |
2397 | " m_workq[m][n].m_boq = 0;", |
2398 | " } } }", |
2399 | "", |
2400 | " if (must_exit)", |
2401 | " { fprintf(stderr, \"pan: check './pan --' for usage details\\n\");", |
2402 | " pan_exit(1); /* calls cleanup_shm */", |
2403 | " }", |
2404 | "}", |
2405 | "", |
2406 | "static uchar *", |
2407 | "prep_shmid_S(size_t n) /* either sets SS or H_tab, WIN32/WIN64 */", |
2408 | "{ char *rval;", |
2409 | "#ifndef SEP_STATE", |
2410 | " char key[512];", |
2411 | "", |
2412 | " if (verbose && core_id == 0)", |
2413 | " {", |
2414 | " #ifdef BITSTATE", |
2415 | " printf(\"cpu0: step 1: allocate shared bitstate %%g Mb\\n\",", |
2416 | " (double) n / (1048576.));", |
2417 | " #else", |
2418 | " printf(\"cpu0: step 1: allocate shared hastable %%g Mb\\n\",", |
2419 | " (double) n / (1048576.));", |
2420 | " #endif", |
2421 | " }", |
2422 | " #ifdef MEMLIM", |
2423 | " if (memcnt + (double) n > memlim)", |
2424 | " { printf(\"cpu%%d: S %%8g + %%d Kb exceeds memory limit of %%8g Mb\\n\",", |
2425 | " core_id, memcnt/1024., n/1024, memlim/(1048576.));", |
2426 | " printf(\"cpu%%d: insufficient memory -- aborting\\n\", core_id);", |
2427 | " exit(1);", |
2428 | " }", |
2429 | " #endif", |
2430 | "", |
2431 | " /* make key different from queues: */", |
2432 | " sprintf(key, \"Global\\\\pan_%%s_%%.3d\", PanSource, NCORE+2); /* different from qs */", |
2433 | "", |
2434 | " if (core_id == 0) /* root */", |
2435 | " { shmid_S = CreateFileMapping(INVALID_HANDLE_VALUE, NULL,", |
2436 | "#ifdef WIN64", |
2437 | " PAGE_READWRITE, (n>>32), (n & 0xffffffff), key);", |
2438 | "#else", |
2439 | " PAGE_READWRITE, 0, n, key);", |
2440 | "#endif", |
2441 | " memcnt += (double) n;", |
2442 | " } else /* worker */", |
2443 | " { shmid_S = OpenFileMapping(FILE_MAP_ALL_ACCESS, FALSE, key);", |
2444 | " }", |
2445 | |
2446 | " if (shmid_S == NULL)", |
2447 | " {", |
2448 | " #ifdef BITSTATE", |
2449 | " fprintf(stderr, \"cpu%%d: cannot %%s shared bitstate\",", |
2450 | " core_id, core_id?\"open\":\"create\");", |
2451 | " #else", |
2452 | " fprintf(stderr, \"cpu%%d: cannot %%s shared hashtable\",", |
2453 | " core_id, core_id?\"open\":\"create\");", |
2454 | " #endif", |
2455 | " fprintf(stderr, \"pan: check './pan --' for usage details\\n\");", |
2456 | " pan_exit(1);", |
2457 | " }", |
2458 | "", |
2459 | " rval = (char *) MapViewOfFile(shmid_S, FILE_MAP_ALL_ACCESS, 0, 0, 0); /* attach */", |
2460 | " if ((char *) rval == NULL)", |
2461 | " { fprintf(stderr, \"cpu%%d: cannot attach shared bitstate or hashtable\\n\", core_id);", |
2462 | " fprintf(stderr, \"pan: check './pan --' for usage details\\n\");", |
2463 | " pan_exit(1);", |
2464 | " }", |
2465 | "#else", |
2466 | " rval = (char *) emalloc(n);", |
2467 | "#endif", |
2468 | " return (uchar *) rval;", |
2469 | "}", |
2470 | "", |
2471 | "static uchar *", |
2472 | "prep_state_mem(size_t n) /* WIN32/WIN64 sets memory arena for states */", |
2473 | "{ char *rval;", |
2474 | " char key[512];", |
2475 | " static int cnt = 3; /* start larger than earlier ftok calls */", |
2476 | "", |
2477 | " if (verbose && core_id == 0)", |
2478 | " { printf(\"cpu0: step 2+: pre-allocate memory arena %%d of %%g Mb\\n\",", |
2479 | " cnt-3, (double) n / (1048576.));", |
2480 | " }", |
2481 | " #ifdef MEMLIM", |
2482 | " if (memcnt + (double) n > memlim)", |
2483 | " { printf(\"cpu%%d: error: M %%.0f + %%.0f exceeds memory limit of %%.0f Kb\\n\",", |
2484 | " core_id, memcnt/1024.0, (double) n/1024.0, memlim/1024.0);", |
2485 | " return NULL;", |
2486 | " }", |
2487 | " #endif", |
2488 | "", |
2489 | " sprintf(key, \"Global\\\\pan_%%s_%%.3d\", PanSource, NCORE+cnt); cnt++;", |
2490 | "", |
2491 | " if (core_id == 0)", |
2492 | " { shmid_M = CreateFileMapping(INVALID_HANDLE_VALUE, NULL,", |
2493 | "#ifdef WIN64", |
2494 | " PAGE_READWRITE, (n>>32), (n & 0xffffffff), key);", |
2495 | "#else", |
2496 | " PAGE_READWRITE, 0, n, key);", |
2497 | "#endif", |
2498 | " } else", |
2499 | " { shmid_M = OpenFileMapping(FILE_MAP_ALL_ACCESS, FALSE, key);", |
2500 | " }", |
2501 | " if (shmid_M == NULL)", |
2502 | " { printf(\"cpu%%d: failed to get pool of shared memory nr %%d of size %%d\\n\",", |
2503 | " core_id, cnt-3, n);", |
2504 | " printf(\"pan: check './pan --' for usage details\\n\");", |
2505 | " return NULL;", |
2506 | " }", |
2507 | " rval = (char *) MapViewOfFile(shmid_M, FILE_MAP_ALL_ACCESS, 0, 0, 0); /* attach */", |
2508 | "", |
2509 | " if (rval == NULL)", |
2510 | " { printf(\"cpu%%d: failed to attach pool of shared memory nr %%d of size %%d\\n\",", |
2511 | " core_id, cnt-3, n);", |
2512 | " return NULL;", |
2513 | " }", |
2514 | " return (uchar *) rval;", |
2515 | "}", |
2516 | "", |
2517 | "void", |
2518 | "init_HT(unsigned long n) /* WIN32/WIN64 version */", |
2519 | "{ volatile char *x;", |
2520 | " double get_mem;", |
2521 | "#ifndef SEP_STATE", |
2522 | " char *dc_mem_start;", |
2523 | "#endif", |
2524 | " if (verbose) printf(\"cpu%%d: initialization for Windows\\n\", core_id);", |
2525 | "", |
2526 | "#ifdef SEP_STATE", |
2527 | " #ifndef MEMLIM", |
2528 | " if (verbose)", |
2529 | " { printf(\"cpu0: steps 0,1: no -DMEMLIM set\\n\");", |
2530 | " }", |
2531 | " #else", |
2532 | " if (verbose)", |
2533 | " printf(\"cpu0: steps 0,1: -DMEMLIM=%%d Mb - (hashtable %%g Mb + workqueues %%g Mb)\\n\",", |
2534 | " MEMLIM, ((double)n/(1048576.)), ((double) NCORE * LWQ_SIZE + GWQ_SIZE)/(1048576.));", |
2535 | "#endif", |
2536 | " get_mem = NCORE * sizeof(double) + (1 + CS_NR) * sizeof(void *)+ 4*sizeof(void *) + 2*sizeof(double);", |
2537 | " /* NCORE * is_alive + search_terminated + CS_NR * sh_lock + 6 gr vars */", |
2538 | " get_mem += 4 * NCORE * sizeof(void *);", /* prfree, prfull, prcnt, prmax */ |
2539 | " #ifdef FULL_TRAIL", |
2540 | " get_mem += (NCORE) * sizeof(Stack_Tree *);", |
2541 | " /* NCORE * stack_last */", |
2542 | " #endif", |
2543 | " x = (volatile char *) prep_state_mem((size_t) get_mem);", |
2544 | " shmid_X = (void *) x;", |
2545 | " if (x == NULL)", |
2546 | " { printf(\"cpu0: could not allocate shared memory, see ./pan --\\n\");", |
2547 | " exit(1);", |
2548 | " }", |
2549 | " search_terminated = (volatile unsigned int *) x; /* comes first */", |
2550 | " x += sizeof(void *); /* maintain alignment */", |
2551 | "", |
2552 | " is_alive = (volatile double *) x;", |
2553 | " x += NCORE * sizeof(double);", |
2554 | "", |
2555 | " sh_lock = (volatile int *) x;", |
2556 | " x += CS_NR * sizeof(void *); /* allow 1 word per entry */", |
2557 | "", |
2558 | " grfree = (volatile int *) x;", |
2559 | " x += sizeof(void *);", |
2560 | " grfull = (volatile int *) x;", |
2561 | " x += sizeof(void *);", |
2562 | " grcnt = (volatile int *) x;", |
2563 | " x += sizeof(void *);", |
2564 | " grmax = (volatile int *) x;", |
2565 | " x += sizeof(void *);", |
2566 | " prfree = (volatile int *) x;", |
2567 | " x += NCORE * sizeof(void *);", |
2568 | " prfull = (volatile int *) x;", |
2569 | " x += NCORE * sizeof(void *);", |
2570 | " prcnt = (volatile int *) x;", |
2571 | " x += NCORE * sizeof(void *);", |
2572 | " prmax = (volatile int *) x;", |
2573 | " x += NCORE * sizeof(void *);", |
2574 | " gr_readmiss = (volatile double *) x;", |
2575 | " x += sizeof(double);", |
2576 | " gr_writemiss = (volatile double *) x;", |
2577 | " x += sizeof(double);", |
2578 | "", |
2579 | " #ifdef FULL_TRAIL", |
2580 | " stack_last = (volatile Stack_Tree **) x;", |
2581 | " x += NCORE * sizeof(Stack_Tree *);", |
2582 | " #endif", |
2583 | "", |
2584 | " #ifndef BITSTATE", |
2585 | " H_tab = (struct H_el **) emalloc(n);", |
2586 | " #endif", |
2587 | "#else", |
2588 | " #ifndef MEMLIM", |
2589 | " #warning MEMLIM not set", /* cannot happen */ |
2590 | " #define MEMLIM (2048)", |
2591 | " #endif", |
2592 | "", |
2593 | " if (core_id == 0 && verbose)", |
2594 | " printf(\"cpu0: step 0: -DMEMLIM=%%d Mb - (hashtable %%g Mb + workqueues %%g Mb) = %%g Mb for state storage\\n\",", |
2595 | " MEMLIM, ((double)n/(1048576.)), ((double) NCORE * LWQ_SIZE + GWQ_SIZE)/(1048576.),", |
2596 | " (memlim - memcnt - (double) n - ((double) NCORE * LWQ_SIZE + GWQ_SIZE))/(1048576.));", |
2597 | " #ifndef BITSTATE", |
2598 | " H_tab = (struct H_el **) prep_shmid_S((size_t) n); /* hash_table */", |
2599 | " #endif", |
2600 | " get_mem = memlim - memcnt - ((double) NCORE) * LWQ_SIZE - GWQ_SIZE;", |
2601 | " if (get_mem <= 0)", |
2602 | " { Uerror(\"internal error -- shared state memory\");", |
2603 | " }", |
2604 | "", |
2605 | " if (core_id == 0 && verbose)", |
2606 | " { printf(\"cpu0: step 2: shared state memory %%g Mb\\n\",", |
2607 | " get_mem/(1048576.));", |
2608 | " }", |
2609 | " x = dc_mem_start = (char *) prep_state_mem((size_t) get_mem); /* for states */", |
2610 | " if (x == NULL)", |
2611 | " { printf(\"cpu%%d: insufficient memory -- aborting\\n\", core_id);", |
2612 | " exit(1);", |
2613 | " }", |
2614 | "", |
2615 | " search_terminated = (volatile unsigned int *) x; /* comes first */", |
2616 | " x += sizeof(void *); /* maintain alignment */", |
2617 | "", |
2618 | " is_alive = (volatile double *) x;", |
2619 | " x += NCORE * sizeof(double);", |
2620 | "", |
2621 | " sh_lock = (volatile int *) x;", |
2622 | " x += CS_NR * sizeof(int);", |
2623 | "", |
2624 | " grfree = (volatile int *) x;", |
2625 | " x += sizeof(void *);", |
2626 | " grfull = (volatile int *) x;", |
2627 | " x += sizeof(void *);", |
2628 | " grcnt = (volatile int *) x;", |
2629 | " x += sizeof(void *);", |
2630 | " grmax = (volatile int *) x;", |
2631 | " x += sizeof(void *);", |
2632 | " prfree = (volatile int *) x;", |
2633 | " x += NCORE * sizeof(void *);", |
2634 | " prfull = (volatile int *) x;", |
2635 | " x += NCORE * sizeof(void *);", |
2636 | " prcnt = (volatile int *) x;", |
2637 | " x += NCORE * sizeof(void *);", |
2638 | " prmax = (volatile int *) x;", |
2639 | " x += NCORE * sizeof(void *);", |
2640 | " gr_readmiss = (volatile double *) x;", |
2641 | " x += sizeof(double);", |
2642 | " gr_writemiss = (volatile double *) x;", |
2643 | " x += sizeof(double);", |
2644 | "", |
2645 | " #ifdef FULL_TRAIL", |
2646 | " stack_last = (volatile Stack_Tree **) x;", |
2647 | " x += NCORE * sizeof(Stack_Tree *);", |
2648 | " #endif", |
2649 | " if (((long)x)&(sizeof(void *)-1)) /* word alignment */", |
2650 | " { x += sizeof(void *)-(((long)x)&(sizeof(void *)-1)); /* 64-bit align */", |
2651 | " }", |
2652 | "", |
2653 | " #ifdef COLLAPSE", |
2654 | " ncomps = (unsigned long *) x;", |
2655 | " x += (256+2) * sizeof(unsigned long);", |
2656 | " #endif", |
2657 | "", |
2658 | " dc_shared = (sh_Allocater *) x; /* in shared memory */", |
2659 | " x += sizeof(sh_Allocater);", |
2660 | "", |
2661 | " if (core_id == 0) /* root only */", |
2662 | " { dc_shared->dc_id = shmid_M;", |
2663 | " dc_shared->dc_start = (void *) dc_mem_start;", |
2664 | " dc_shared->dc_arena = x;", |
2665 | " dc_shared->pattern = 1234567;", |
2666 | " dc_shared->dc_size = (long) get_mem - (long) (x - dc_mem_start);", |
2667 | " dc_shared->nxt = NULL;", |
2668 | " }", |
2669 | "#endif", |
2670 | "}", |
2671 | "", |
2672 | "#if defined(WIN32) || defined(WIN64) || defined(__i386__) || defined(__x86_64__)", |
2673 | "extern BOOLEAN InterlockedBitTestAndSet(LONG volatile* Base, LONG Bit);", |
2674 | "int", |
2675 | "tas(volatile LONG *s)", /* atomic test and set */ |
2676 | "{ return InterlockedBitTestAndSet(s, 1);", |
2677 | "}", |
2678 | "#else", |
2679 | " #error missing definition of test and set operation for this platform", |
2680 | "#endif", |
2681 | "", |
2682 | "void", |
2683 | "cleanup_shm(int val)", |
2684 | "{ int m;", |
2685 | " static int nibis = 0;", |
2686 | "", |
2687 | " if (nibis != 0)", |
2688 | " { printf(\"cpu%%d: Redundant call to cleanup_shm(%%d)\\n\", core_id, val);", |
2689 | " return;", |
2690 | " } else", |
2691 | " { nibis = 1;", |
2692 | " }", |
2693 | " if (search_terminated != NULL)", |
2694 | " { *search_terminated |= 16; /* cleanup_shm */", |
2695 | " }", |
2696 | "", |
2697 | " for (m = 0; m < NR_QS; m++)", |
2698 | " { if (shmid[m] != NULL)", |
2699 | " { UnmapViewOfFile((char *) shared_mem[m]);", |
2700 | " CloseHandle(shmid[m]);", |
2701 | " } }", |
2702 | "#ifdef SEP_STATE", |
2703 | " UnmapViewOfFile((void *) shmid_X);", |
2704 | " CloseHandle((void *) shmid_M);", |
2705 | "#else", |
2706 | " #ifdef BITSTATE", |
2707 | " if (shmid_S != NULL)", |
2708 | " { UnmapViewOfFile(SS);", |
2709 | " CloseHandle(shmid_S);", |
2710 | " }", |
2711 | " #else", |
2712 | " if (core_id == 0 && verbose)", |
2713 | " { printf(\"cpu0: done, %%ld Mb of shared state memory left\\n\",", |
2714 | " dc_shared->dc_size / (long)(1048576));", |
2715 | " }", |
2716 | " if (shmid_S != NULL)", |
2717 | " { UnmapViewOfFile(H_tab);", |
2718 | " CloseHandle(shmid_S);", |
2719 | " }", |
2720 | " shmid_M = (void *) (dc_shared->dc_id);", |
2721 | " UnmapViewOfFile((char *) dc_shared->dc_start);", |
2722 | " CloseHandle(shmid_M);", |
2723 | " #endif", |
2724 | "#endif", |
2725 | " /* detached from shared memory - so cannot use cpu_printf */", |
2726 | " if (verbose)", |
2727 | " { printf(\"cpu%%d: done -- got %%d states from queue\\n\",", |
2728 | " core_id, nstates_get);", |
2729 | " }", |
2730 | "}", |
2731 | "", |
2732 | "void", |
2733 | "mem_get(void)", |
2734 | "{ SM_frame *f;", |
2735 | " int is_parent;", |
2736 | "", |
2737 | "#if defined(MA) && !defined(SEP_STATE)", |
2738 | " #error MA requires SEP_STATE in multi-core mode", |
2739 | "#endif", |
2740 | "#ifdef BFS", |
2741 | " #error BFS is not supported in multi-core mode", |
2742 | "#endif", |
2743 | "#ifdef SC", |
2744 | " #error SC is not supported in multi-core mode", |
2745 | "#endif", |
2746 | " init_shm(); /* we are single threaded when this starts */", |
2747 | " signal(SIGINT, give_up); /* windows control-c interrupt */", |
2748 | "", |
2749 | " if (core_id == 0 && verbose)", |
2750 | " { printf(\"cpu0: step 4: creating additional workers (proxy %%d)\\n\",", |
2751 | " proxy_pid);", |
2752 | " }", |
2753 | "#if 0", |
2754 | " if NCORE > 1 the child or the parent should fork N-1 more times", |
2755 | " the parent is the only process with core_id == 0 and is_parent > 0", |
2756 | " the others (workers) have is_parent = 0 and core_id = 1..NCORE-1", |
2757 | "#endif", |
2758 | " if (core_id == 0) /* root starts up the workers */", |
2759 | " { worker_pids[0] = (DWORD) getpid(); /* for completeness */", |
2760 | " while (++core_id < NCORE) /* first worker sees core_id = 1 */", |
2761 | " { char cmdline[64];", |
2762 | " STARTUPINFO si = { sizeof(si) };", |
2763 | " PROCESS_INFORMATION pi;", |
2764 | "", |
2765 | " if (proxy_pid == core_id) /* always non-zero */", |
2766 | " { sprintf(cmdline, \"pan_proxy.exe -r %%s-Q%%d -Z%%d\",", |
2767 | " o_cmdline, getpid(), core_id);", |
2768 | " } else", |
2769 | " { sprintf(cmdline, \"pan.exe %%s-Q%%d -Z%%d\",", |
2770 | " o_cmdline, getpid(), core_id);", |
2771 | " }", |
2772 | " if (verbose) printf(\"cpu%%d: spawn %%s\\n\", core_id, cmdline);", |
2773 | "", |
2774 | " is_parent = CreateProcess(0, cmdline, 0, 0, FALSE, 0, 0, 0, &si, &pi);", |
2775 | " if (is_parent == 0)", |
2776 | " { Uerror(\"fork failed\");", |
2777 | " }", |
2778 | " worker_pids[core_id] = pi.dwProcessId;", |
2779 | " worker_handles[core_id] = pi.hProcess;", |
2780 | " if (verbose)", |
2781 | " { cpu_printf(\"created core %%d, pid %%d\\n\",", |
2782 | " core_id, pi.dwProcessId);", |
2783 | " }", |
2784 | " if (proxy_pid == core_id) /* we just created the receive half */", |
2785 | " { /* add proxy send, store pid in proxy_pid_snd */", |
2786 | " sprintf(cmdline, \"pan_proxy.exe -s %%s-Q%%d -Z%%d -Y%%d\",", |
2787 | " o_cmdline, getpid(), core_id, worker_pids[proxy_pid]);", |
2788 | " if (verbose) printf(\"cpu%%d: spawn %%s\\n\", core_id, cmdline);", |
2789 | " is_parent = CreateProcess(0, cmdline, 0,0, FALSE, 0,0,0, &si, &pi);", |
2790 | " if (is_parent == 0)", |
2791 | " { Uerror(\"fork failed\");", |
2792 | " }", |
2793 | " proxy_pid_snd = pi.dwProcessId;", |
2794 | " proxy_handle_snd = pi.hProcess;", |
2795 | " if (verbose)", |
2796 | " { cpu_printf(\"created core %%d, pid %%d (send proxy)\\n\",", |
2797 | " core_id, pi.dwProcessId);", |
2798 | " } } }", |
2799 | " core_id = 0; /* reset core_id for root process */", |
2800 | " } else /* worker */", |
2801 | " { static char db0[16]; /* good for up to 10^6 cores */", |
2802 | " static char db1[16];", |
2803 | " tprefix = db0; sprefix = db1;", |
2804 | " sprintf(tprefix, \"cpu%%d_trail\", core_id); /* avoid conflicts on file access */", |
2805 | " sprintf(sprefix, \"cpu%%d_rst\", core_id);", |
2806 | " memcnt = 0; /* count only additionally allocated memory */", |
2807 | " }", |
2808 | " if (verbose)", |
2809 | " { cpu_printf(\"starting core_id %%d -- pid %%d\\n\", core_id, getpid());", |
2810 | " }", |
2811 | " if (core_id == 0 && !remote_party)", |
2812 | " { new_state(); /* root starts the search */", |
2813 | " if (verbose)", |
2814 | " cpu_printf(\"done with 1st dfs, nstates %%g (put %%d states), start reading q\\n\",", |
2815 | " nstates, nstates_put);", |
2816 | " dfs_phase2 = 1;", |
2817 | " }", |
2818 | " Read_Queue(core_id); /* all cores */", |
2819 | "", |
2820 | " if (verbose)", |
2821 | " { cpu_printf(\"put %%6d states into queue -- got %%6d\\n\",", |
2822 | " nstates_put, nstates_get);", |
2823 | " }", |
2824 | " done = 1;", |
2825 | " wrapup();", |
2826 | " exit(0);", |
2827 | "}", |
2828 | "#endif", /* WIN32 || WIN64 */ |
2829 | "", |
2830 | "#ifdef BITSTATE", |
2831 | "void", |
2832 | "init_SS(unsigned long n)", |
2833 | "{", |
2834 | " SS = (uchar *) prep_shmid_S((size_t) n);", |
2835 | " init_HT(0L);", /* locks and shared memory for Stack_Tree allocations */ |
2836 | "}", |
2837 | "#endif", /* BITSTATE */ |
2838 | "", |
2839 | "#endif", /* NCORE>1 */ |
2840 | 0, |
2841 | }; |