xref: /plan9/sys/src/cmd/spin/pangen6.h (revision 00d970127b9d44d2b22f4f656717a212dec1f1d2)
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 };
2841