pangen6.h

对软件进行可达性测试的软件

	"			}",
	"			wrapup(); /* incomplete stats, but at least something */",
	"		}",
	"		return;",
	"	} /* else: should rarely happen, take more drastic measures */",
	"",
	"	if (core_id == 0)	/* local root process */",
	"	{	for (i = 1; i < NCORE; i++)	/* not for 0 of course */",
	"		{",
	"#if defined(WIN32) || defined(WIN64)",
	"				DWORD dwExitCode = 0;",
	"				GetExitCodeProcess(worker_handles[i], &dwExitCode);",
	"				if (dwExitCode == STILL_ACTIVE)",
	"				{	TerminateProcess(worker_handles[i], 0);",
	"				}",
	"				printf(\"cpu0: terminate %%d %%d\\n\",",
	"					worker_pids[i], (dwExitCode == STILL_ACTIVE));",
	"#else",
	"				sprintf(b, \"kill -%%d %%d\", SIGKILL, worker_pids[i]);",
	"				system(b);	/* if this is a proxy: receive half */",
	"				printf(\"cpu0: %%s\\n\", b);",
	"#endif",
	"		}",
	"		issued_kill++;",
	"	} else",
	"	{	/* on WIN32/WIN64 -- these merely kills the root process... */",
	"		if (was_interrupted == 0)",	/* 2=SIGINT to root to trigger stop */
	"		{	sprintf(b, \"kill -%%d %%d\", SIGINT, worker_pids[0]);",
	"			system(b);	/* warn the root process */",
	"			printf(\"cpu%%d: %%s\\n\", core_id, b);",
	"			issued_kill++;",
	"	}	}",
	"}",
	"",
	"#define iam_alive()	is_alive[core_id]++",	/* for crash detection */
	"",
	"extern int crash_test(double);",
	"extern void crash_reset(void);",
	"",
	"int",
	"someone_crashed(int wait_type)",
	"{	static double last_value = 0.0;",
	"	static int count = 0;",
	"",
	"	if (search_terminated == NULL",
	"	|| *search_terminated != 0)",
	"	{",
	"		if (!(*search_terminated & (8|32|128|256)))",
	"		{	if (count++ < 100*NCORE)",
	"			{	return 0;",
	"		}	}",
	"		return 1;",
	"	}",
	"	/* check left neighbor only */",
	"	if (last_value == is_alive[(core_id + NCORE - 1) %% NCORE])",
	"	{	if (count++ >= 100)	/* to avoid unnecessary checks */",
	"		{	return 1;",
	"		}",
	"		return 0;",
	"	}",
	"	last_value = is_alive[(core_id + NCORE - 1) %% NCORE];",
	"	count = 0;",
	"	crash_reset();",
	"	return 0;",
	"}",
	"",
	"void",
	"sleep_report(void)",
	"{",
	"	if (verbose)",
	"	{	enter_critical(GLOBAL_LOCK);",
	"#ifdef NGQ",
	"		printf(\"cpu%%d: locks: global %%g\\tother %%g\\t\",",
	"			core_id, glock_wait[0], lock_wait - glock_wait[0]);",
	"#else",
	"		printf(\"cpu%%d: locks: GL %%g, RQ %%g, WQ %%g, HT %%g\\t\",",
	"			core_id, glock_wait[0], glock_wait[1], glock_wait[2],",
	"			lock_wait - glock_wait[0] - glock_wait[1] - glock_wait[2]);",
	"#endif",
	"		printf(\"waits: states %%g slots %%g\\n\", frame_wait, free_wait);",
	"#ifndef NGQ",
	"		printf(\"cpu%%d: gq [tries %%g, room %%g, noroom %%g]\\n\", core_id, gq_tries, gq_hasroom, gq_hasnoroom);",
	"		if (core_id == 0 && (*gr_readmiss >= 1.0 || *gr_readmiss >= 1.0 || *grcnt != 0))",
	"		printf(\"cpu0: gq [readmiss: %%g, writemiss: %%g cnt %%d]\\n\", *gr_readmiss, *gr_writemiss, *grcnt);",
	"#endif",
	"		leave_critical(GLOBAL_LOCK);",
	"	}",
	"	if (free_wait > 1000000.)",
	"	{	enter_critical(GLOBAL_LOCK);",
	"		printf(\"hint: this search may be faster with larger work-queues \");",
	"		printf(\"(-DSET_WQ_SIZE=...), and/or with -DUSE_DISK\\n\");",
	"		leave_critical(GLOBAL_LOCK);",
	"	}",
	"}",
	"",
	"#ifndef MAX_DSK_FILE",
	"	#define MAX_DSK_FILE	1000000	/* default is max 1M states per file */",
	"#endif",
	"",
	"void",
	"multi_usage(FILE *fd)",
	"{	static int warned = 0;",
	"	if (warned > 0) { return; } else { warned++; }",
	"	fprintf(fd, \"\\n\");",
	"#if !defined(WIN32) && !defined(WIN64)",
	"	fprintf(fd, \"Usage details for multi-core options on linux and cygwin:\\n\\n\");",
	"	fprintf(fd, \"     Shared memory usage on linux systems:\\n\");",
	"	fprintf(fd, \"       the max size of a shared memory segment is defined in /usr/include/linux/shm.h\\n\");",
	"	fprintf(fd, \"       the default size is 32Mb (as it is on cygwin)\\n\");",
	"	fprintf(fd, \"       the max value can be changed with the /sbin/sysctl command (as root):\\n\");",
	"	fprintf(fd, \"         $ /sbin/sysctl -a | grep shmmax   # check what the current value is\\n\");",
	"	fprintf(fd, \"         kernel.shmmax = 33554432          # the default value\\n\");",
	"	fprintf(fd, \"         $ sudo /sbin/sysctl kernel.shmmax=6442450944	#  set new limit of 6 Gb\\n\");",
	"	fprintf(fd, \"       or\\n\");",
	"	fprintf(fd, \"         $ sudo /sbin/sysctl kernel.shmmax=32212254720	#  set new limit of 30 Gb\\n\");",
	"	fprintf(fd, \"       for large settings, you should also increase the max nr of shared pages\\n\");",
	"	fprintf(fd, \"       to the same number divided by the pagesize (e.g., 4096), e.g.:\\n\");",
	"	fprintf(fd, \"         $ sudo /sbin/sysctl kernel.shmall=7864320	# 30G/4K\\n\");",
	"	fprintf(fd, \"\\n\");",
	"	fprintf(fd, \"     Shared memory usage on cygwin PCs:\\n\");",
	"	fprintf(fd, \"       edit the value of kern.ipc.shmmaxpgs in /etc/cygserver.conf\\n\");",
	"	fprintf(fd, \"       the default value is 8,192 -- the maximum is 32,767\\n\");",
	"	fprintf(fd, \"       multiply by the pagesize (4096) to get the max shared memory segment\\n\");",
	"	fprintf(fd, \"       that corresponds to this: 32Mb by default and 128Mb max\\n\\n\");",
	"	fprintf(fd, \"       if cygserver is not running, start it first\\n\");",
	"	fprintf(fd, \"         sh /usr/bin/cygserver-config  # very first time only\\n\");",
	"	fprintf(fd, \"         cygrunsrv -S cygserver        # once or repeat when it dies\\n\\n\");",
	"	fprintf(fd, \"       finally, always have shell variable CYGWIN=server set in your environment\\n\");",
	"	fprintf(fd, \"       you can tell if cygserver is running by executing:\\n\");",
	"	fprintf(fd, \"         ipcs   # print a list of all current shared memory uses\\n\");",
	"	fprintf(fd, \"         if this fails -- then cygserver is not running and must be (re)started\\n\");",
	"	fprintf(fd, \"\\n\");",
	"	fprintf(fd, \"     On both systems: use ipcs to see which shared memory segments are in use\\n\");",
	"	fprintf(fd, \"     and use ipcrm to remove an occassional stray segment after a crash of pan\\n\");",
	"	fprintf(fd, \"\\n\");",
	"#endif",
	"	fprintf(fd, \"Additional directives supported in multi-core mode:\\n\\n\");",
	"	fprintf(fd, \"        -DDUAL_CORE --> same as -DNCORE=2\\n\");",
	"	fprintf(fd, \"        -DNCORE=N   --> enables multi_core verification if N>1\\n\");",
	"	fprintf(fd, \"        -DSEP_STATE --> forces separate statespaces instead of a single shared state space\\n\");",
	"	fprintf(fd, \"        -DR_H       --> handoff state with probability 1 in N using -zN parameter\\n\");",
	"	fprintf(fd, \"        -DNUSE_DISK --> use disk for storing states when a work queue overflows\\n\");",
	"	fprintf(fd, \"        -DMAX_DSK_FILE --> max nr of states per diskfile (%%d)\\n\", MAX_DSK_FILE);",
	"	fprintf(fd, \"        -DT_ALERT   --> collect stats on crash alert timeouts\\n\");",
	"	fprintf(fd, \"        -DFULL_TRAIL --> support full error trails -- increases memory use\\n\");",
	"	fprintf(fd, \"\\n\");",
	"	fprintf(fd, \"     To increase the nr of states that can be stored in the shared queues:\\n\");",
	"	fprintf(fd, \"        -DVMAX=N    --> upperbound on statevector for handoffs (N=%%d)\\n\", VMAX);",
	"	fprintf(fd, \"        -DPMAX=N    --> upperbound on nr of procs (N=%%d)\\n\", PMAX);",
	"	fprintf(fd, \"        -DQMAX=N    --> upperbound on nr of channels (N=%%d)\\n\", QMAX);",
	"	fprintf(fd, \"\\n\");",
	"#if !defined(WIN32) && !defined(WIN64)",
	"	fprintf(fd, \"     To change the size of spin's individual shared memory segments for cygwin/linux:\\n\");",
	"	fprintf(fd, \"        -DSET_SEG_SIZE=N --> default %%g (Mbytes)\\n\", SEG_SIZE/(1024.*1024.));",
	"	fprintf(fd, \"\\n\");",
	"#endif",
	"	fprintf(fd, \"     To change the size of shared workqueues:\\n\");",
	"	fprintf(fd, \"        -DSET_WQ_SIZE=N --> default %%g (Mbytes)\\n\", WQ_SIZE/(1024.*1024.));",
	"	fprintf(fd, \"\\n\");",
	"	fprintf(fd, \"     To define a fct to initialize data before spawning processes (must be quoted):\\n\");",
	"	fprintf(fd, \"        \\\"-DC_INIT=fct()\\\"\\n\");",
	"	fprintf(fd, \"\\n\");",
	"	fprintf(fd, \"     Modifying timer settings for termination and crash detection:\\n\");",
	"	fprintf(fd, \"        -DSHORT_T --> (%%g)   --> short timeout for termination detection trigger\\n\", (double) SHORT_T);",
	"	fprintf(fd, \"        -DLONG_T  --> (%%g) --> long timeout for giving up on termination detection\\n\", (double) LONG_T);",
	"	fprintf(fd, \"\\n\");",
	"	fprintf(fd, \"     Should rarely need changing:\\n\");",
	"	fprintf(fd, \"        -DONESECOND --> (1<<29) --> timeout waiting for a free slot -- to check for crash\\n\");",
	"	fprintf(fd, \"\\n\");",
	"}",
	"#if NCORE>1 && defined(FULL_TRAIL)",
	"typedef struct Stack_Tree {",
	"	uchar	      pr;	/* process that made transition */",
	"	T_ID	    t_id;	/* id of transition */",
	"	volatile struct Stack_Tree *prv; /* backward link towards root */",
	"} Stack_Tree;",
	"",
	"struct H_el *grab_shared(int);",
	"volatile Stack_Tree **stack_last; /* in shared memory */",
	"char *stack_cache = NULL;	/* local */",
	"int  nr_cached = 0;		/* local */",
	"",
	"#ifndef CACHE_NR",
	"	#define CACHE_NR	1024",
	"#endif",
	"",
	"volatile Stack_Tree *",
	"stack_prefetch(void)",
	"{	volatile Stack_Tree *st;",
	"",
	"	if (nr_cached == 0)",
	"	{	stack_cache = (char *) grab_shared(CACHE_NR * sizeof(Stack_Tree));",
	"		nr_cached = CACHE_NR;",
	"	}",
	"	st = (volatile Stack_Tree *) stack_cache;",
	"	stack_cache += sizeof(Stack_Tree);",
	"	nr_cached--;",
	"	return st;",
	"}",
	"",
	"void",
	"Push_Stack_Tree(short II, T_ID t_id)",
	"{	volatile Stack_Tree *st;",
	"",
	"	st = (volatile Stack_Tree *) stack_prefetch();",
	"	st->pr = II;",
	"	st->t_id = t_id;",
	"	st->prv = (Stack_Tree *) stack_last[core_id];",
	"	stack_last[core_id] = st;",
	"}",
	"",
	"void",
	"Pop_Stack_Tree(void)",
	"{	volatile Stack_Tree *cf = stack_last[core_id];",
	"",
	"	if (cf)",
	"	{	stack_last[core_id] = cf->prv;",
	"	} else if (nr_handoffs * z_handoff + depth > 0)",
	"	{	printf(\"cpu%%d: error pop_stack_tree (depth %%d)\\n\",",
	"			core_id, depth);",
	"	}",
	"}",
	"#endif", /* NCORE>1 && FULL_TRAIL */
	"",
	"void",
	"e_critical(int which)",
	"{	double cnt_start;",
	"",
	"	if (readtrail || iamin[which] > 0)",
	"	{	if (!readtrail && verbose)",
	"		{	printf(\"cpu%%d: Double Lock on %%d (now %%d)\\n\",",
	"				core_id, which, iamin[which]+1);",
	"			fflush(stdout);",
	"		}",
	"		iamin[which]++;	/* local variable */",
	"		return;",
	"	}",
	"",
	"	cnt_start = lock_wait;",
	"",
	"	while (sh_lock != NULL)	/* as long as we have shared memory */",
	"	{	int r = tas(&sh_lock[which]);",
	"		if (r == 0)",
	"		{	iamin[which] = 1;",
	"			return;		/* locked */",
	"		}",
	"",
	"		lock_wait++;",
	"#ifndef NGQ",
	"		if (which < 3) { glock_wait[which]++; }",
	"#else",
	"		if (which == 0) { glock_wait[which]++; }",
	"#endif",
	"		iam_alive();",
	"",
	"		if (lock_wait - cnt_start > TenSeconds)",
	"		{	printf(\"cpu%%d: lock timeout on %%d\\n\", core_id, which);",
	"			cnt_start = lock_wait;",
	"			if (someone_crashed(1))",
	"			{	sudden_stop(\"lock timeout\");",
	"				pan_exit(1);",
	"	}	}	}",
	"}",
	"",
	"void",
	"x_critical(int which)",
	"{",
	"	if (iamin[which] != 1)",
	"	{	if (iamin[which] > 1)",
	"		{	iamin[which]--;	/* this is thread-local - no races on this one */",
	"			if (!readtrail && verbose)",
	"			{	printf(\"cpu%%d: Partial Unlock on %%d (%%d more needed)\\n\",",
	"					core_id, which, iamin[which]);",
	"				fflush(stdout);",
	"			}",
	"			return;",
	"		} else /* iamin[which] <= 0 */",
	"		{	if (!readtrail)",
	"			{	printf(\"cpu%%d: Invalid Unlock iamin[%%d] = %%d\\n\",",
	"					core_id, which, iamin[which]);",
	"				fflush(stdout);",
	"			}",
	"			return;",
	"	}	}",
	"",
	"	if (sh_lock != NULL)",
	"	{	iamin[which]   = 0;",
	"		sh_lock[which] = 0;	/* unlock */",
	"	}",
	"}",
	"",
	"#ifndef SEP_STATE",
	"	void enter_critical(int w) { e_critical(w); }",
	"	void leave_critical(int w) { x_critical(w); }",
	"#else",
	"	#ifdef NGQ",
	"	void enter_critical(int w) { if (w == 0) e_critical(w); }",
	"	void leave_critical(int w) { if (w == 0) x_critical(w); }",
	"	#else",
	"	void enter_critical(int w) { if (w < 3) e_critical(w); }",
	"	void leave_critical(int w) { if (w < 3) x_critical(w); }",
	"	#endif",
	"#endif",
	"",
	"void",
	"#if defined(WIN32) || defined(WIN64)",
	"start_proxy(char *s, DWORD r_pid)",
	"#else",
	"start_proxy(char *s, int r_pid)",
	"#endif",
	"{	char  Q_arg[16], Z_arg[16], Y_arg[16];",
	"	char *args[32], *ptr;",
	"	int   argcnt = 0;",
	"",
	"	sprintf(Q_arg, \"-Q%%d\", getpid());",
	"	sprintf(Y_arg, \"-Y%%d\", r_pid);",
	"	sprintf(Z_arg, \"-Z%%d\", proxy_pid /* core_id */);",
	"",
	"	args[argcnt++] = \"proxy\";",
	"	args[argcnt++] = s; /* -r or -s */",
	"	args[argcnt++] = Q_arg;",
	"	args[argcnt++] = Z_arg;",
	"	args[argcnt++] = Y_arg;",
	"",
	"	if (strlen(o_cmdline) > 0)",
	"	{	ptr = o_cmdline; /* assume args separated by spaces */",
	"		do {	args[argcnt++] = ptr++;",
	"			if ((ptr = strchr(ptr, ' ')) != NULL)",
	"			{	while (*ptr == ' ')",
	"				{	*ptr++ = '\\0';",
	"				}",
	"			} else",
	"			{	break;",
	"			}",
	"		} while (argcnt < 31);",
	"	}",
	"	args[argcnt] = NULL;",
	"#if defined(WIN32) || defined(WIN64)",
	"	execvp(\"pan_proxy\", args); /* no return */",
	"#else",
	"	execvp(\"./pan_proxy\", args); /* no return */",
	"#endif",
	"	Uerror(\"pan_proxy exec failed\");",
	"}",
	"/*** end of common code fragment ***/",
	"",
	"#if !defined(WIN32) && !defined(WIN64)",
	"void",
	"init_shm(void)		/* initialize shared work-queues - linux/cygwin */",
	"{	key_t	key[NR_QS];",
	"	int	n, m;",
	"	int	must_exit = 0;",
	"",
	"	if (core_id == 0 && verbose)",
	"	{	printf(\"cpu0: step 3: allocate shared workqueues %%g Mb\\n\",",
	"			2. * (double) WQ_SIZE / (1024.*1024.));",
	"	}",
	"	for (m = 0; m < NR_QS; m++)		/* last q is the global q */",
	"	{	key[m] = ftok(PanSource, m+1);", /* m must be nonzero, 1..NCORE */
	"		if (key[m] == -1)",
	"		{	perror(\"ftok shared queues\"); must_exit = 1; break;",
	"		}",
	"",
	"		if (core_id == 0)	/* root creates */",
	"		{	/* check for stale copy */",
	"			shmid[m] = shmget(key[m], (size_t) WQ_SIZE, 0600);",
	"			if (shmid[m] != -1)	/* yes there is one; remove it */",
	"			{	printf(\"cpu0: removing stale q%%d, status: %%d\\n\",",
	"					m, shmctl(shmid[m], IPC_RMID, NULL));",
	"			}",
	"			shmid[m] = shmget(key[m], (size_t) WQ_SIZE, 0600|IPC_CREAT|IPC_EXCL);",
	"		} else			/* workers attach */",
	"		{	shmid[m] = shmget(key[m], (size_t) WQ_SIZE, 0600);",
	"			/* never called, since we create shm *before* we fork */",
	"		}",
	"		if (shmid[m] == -1)",
	"		{	perror(\"shmget shared queues\"); must_exit = 1; break;",
	"		}",
	"",
	"		shared_mem[m] = (char *) shmat(shmid[m], (void *) 0, 0);	/* attach */",
	"		if (shared_mem[m] == (char *) -1)",
	"		{ fprintf(stderr, \"error: cannot attach shared wq %%d of %%d (%%d Mb)\\n\",",
	"				m+1, NCORE, WQ_SIZE/(1024*1024));",
	"		  perror(\"shmat shared queues\"); must_exit = 1; break;",
	"		}",
	"",
	"		memcnt += (double) WQ_SIZE;",
	"",
	"		m_workq[m] = (SM_frame *) shared_mem[m];",
	"		if (core_id == 0)",
	"		{	for (n = 0; n < N_FRAMES; n++)",
	"			{	m_workq[m][n].m_vsize = 0;",
	"				m_workq[m][n].m_boq = 0;",
	"	}	}	}",