projects / lttv.git / blob
? search:
summary | shortlog | log | commit | commitdiff | tree
blame | history | raw | HEAD
move everything out of trunk
[lttv.git] / verif / Spin / Src5.1.6 / pangen6.h
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 };
LTTng 2.x Viewer (LTTV)
This page took 0.139257 seconds and 4 git commands to generate.