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