pangen6.h

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

	"	if (shmdt((void *) shmid_X) != 0)",
	"	{	perror(\"shmdt detaching from shared state memory\");",
	"	}",
	"#else",
	"	#ifdef BITSTATE",
	"		if (SS > 0 && shmdt((void *) SS) != 0)",
	"		{	if (verbose)",
	"			{	perror(\"shmdt detaching from shared bitstate arena\");",
	"		}	}",
	"	#else",
	"		if (core_id == 0)",
	"		{	/* before detaching: */",
	"			for (nxt_pool = dc_shared; nxt_pool != NULL; nxt_pool = nxt_pool->nxt)",
	"			{	cnt += nxt_pool->dc_size;",
	"			}",
	"			if (verbose)",
	"			{	printf(\"cpu0: done, %%ld Mb of shared state memory left\\n\",",
	"					cnt / (long)(1024*1024));",
	"		}	}",
	"",
	"		if (shmdt((void *) H_tab) != 0)",
	"		{	perror(\"shmdt detaching from shared hashtable\");",
	"		}",
	"",
	"		for (last_pool = first_pool; last_pool != NULL; last_pool = nxt_pool)",
	"		{	nxt_pool = last_pool->nxt;",
	"			if (shmdt((void *) last_pool->dc_start) != 0)",
	"			{	perror(\"shmdt detaching from shared state memory\");",
	"		}	}",
	"		first_pool = last_pool = NULL;	/* precaution */",
	"	#endif",
	"#endif",
	"	/* detached from shared memory - so cannot use cpu_printf */",
	"	if (verbose)",
	"	{	printf(\"cpu%%d: done -- got %%d states from queue\\n\",",
	"			core_id, nstates_get);",
	"	}",
	"}",
	"",
	"extern void give_up(int);",
	"extern void Read_Queue(int);",
	"",
	"void",
	"mem_get(void)",
	"{	SM_frame   *f;",
	"	int is_parent;",
	"",
	"#if defined(MA) && !defined(SEP_STATE)",
	"	#error MA without SEP_STATE is not supported with multi-core",
	"#endif",
	"#ifdef BFS",
	"	#error BFS is not supported with multi-core",
	"#endif",
	"#ifdef SC",
	"	#error SC is not supported with multi-core",
	"#endif",
	"	init_shm();	/* we are single threaded when this starts */",
	"",
	"	if (core_id == 0 && verbose)",
	"	{	printf(\"cpu0: step 4: calling fork()\\n\");",
	"	}",
	"",
	"/*	if NCORE > 1 the child or the parent should fork N-1 more times",
	" *	the parent is the only process with core_id == 0 and is_parent > 0",
	" *	the workers have is_parent = 0 and core_id = 1..NCORE-1",
	" */",
	"	if (core_id == 0)",
	"	{	worker_pids[0] = getpid();	/* for completeness */",
	"		while (++core_id < NCORE)	/* first worker sees core_id = 1 */",
	"		{	is_parent = fork();",
	"			if (is_parent == -1)",
	"			{	Uerror(\"fork failed\");",
	"			}",
	"			if (is_parent == 0)	/* this is a worker process */",
	"			{	if (proxy_pid == core_id)	/* always non-zero */",
	"				{	start_proxy(\"-r\", 0);	/* no return */",
	"				}",
	"				goto adapt;	/* root process continues spawning */",
	"			}",
	"			worker_pids[core_id] = is_parent;",
	"		}",
	"		/* note that core_id is now NCORE */",
	"		if (proxy_pid > 0 && proxy_pid < NCORE)", /* add send-half of proxy */
	"		{	proxy_pid_snd = fork();",
	"			if (proxy_pid_snd == -1)",
	"			{	Uerror(\"proxy fork failed\");",
	"			}",
	"			if (proxy_pid_snd == 0)",
	"			{	start_proxy(\"-s\", worker_pids[proxy_pid]); /* no return */",
	"		}	} /* else continue */",

	"		if (is_parent > 0)",
	"		{	core_id = 0;	/* reset core_id for root process */",
	"		}",
	"	} else	/* worker */",
	"	{	static char db0[16];	/* good for up to 10^6 cores */",
	"		static char db1[16];",
	"adapt:		tprefix = db0; sprefix = db1;",
	"		sprintf(tprefix, \"cpu%%d_trail\", core_id);",
	"		sprintf(sprefix, \"cpu%%d_rst\", core_id);",
	"		memcnt = 0;	/* count only additionally allocated memory */",
	"	}",
	"	signal(SIGINT, give_up);",
	"",
	"	if (proxy_pid == 0)		/* not in a cluster setup, pan_proxy must attach */",
	"	{	rm_shared_segments();	/* mark all shared segments for removal on exit */",
	"	}", /* doing it early means less chance of being unable to do this */
	"	if (verbose)",
	"	{	cpu_printf(\"starting core_id %%d -- pid %%d\\n\", core_id, getpid());",
	"	}",
	"	if (core_id == 0 && !remote_party)",
	"	{	new_state();		/* cpu0 explores root */",
	"		if (verbose)",
	"		cpu_printf(\"done with 1st dfs, nstates %%g (put %%d states), read q\\n\",",
	"			nstates, nstates_put);",
	"		dfs_phase2 = 1;",
	"	}",
	"	Read_Queue(core_id);	/* all cores */",
	"",
	"	if (verbose)",
	"	{	cpu_printf(\"put %%6d states into queue -- got %%6d -- %%6d slots in q\\n\",",
	"		nstates_put, nstates_get, N_FRAMES);",
	"	}",
	"	if (proxy_pid != 0)",
	"	{	rm_shared_segments();",
	"	}",
	"	done = 1;",
	"	wrapup();",
	"	exit(0);",
	"}",
	"",
	"#else",
	"int unpack_state(SM_frame *, int);",
	"#endif",
	"",
	"struct H_el *",
	"grab_shared(int n)",
	"{",
	"#ifndef SEP_STATE",
	"	char *rval = (char *) 0;",
	"",
	"	if (n == 0)",
	"	{	printf(\"cpu%%d: grab shared zero\\n\", core_id); fflush(stdout);",
	"		return (struct H_el *) rval;",
	"	} else if (n&(sizeof(void *)-1))",
	"	{	n += sizeof(void *)-(n&(sizeof(void *)-1)); /* alignment */",
	"	}",
	"",
	"	if (!dc_shared)",
	"	{	sudden_stop(\"pan: no shared memory segment\");",
	"	}",
	"",
	"	/* critical -- a lock is always in set when this is called */",
	"	/* but not always the same lock -- i.e., on different parts of the hashtable */",
	"	enter_critical(GLOBAL_LOCK);	/* make this part independently mutex */",
	"	cnt_shared++;",
	"		if (dc_shared->pattern != 1234567)",
	"		{	leave_critical(GLOBAL_LOCK);",
	"			Uerror(\"overrun -- memory corruption\");",
	"		}",
	"		if (dc_shared->dc_size < n)",
	"		{	if (verbose)",
	"			{ printf(\"Next Pool %%g Mb + %%d\\n\", memcnt/(1024.*1024.), n);",
	"			}",
	"			if (dc_shared->nxt == NULL",
	"			||  dc_shared->nxt->dc_arena == NULL",
	"			||  dc_shared->nxt->dc_size < n)",
	"			{	printf(\"cpu%%d: memcnt %%g Mb + wanted %%d bytes more\\n\",",
	"					core_id, memcnt / (1024. * 1024.), n);",
	"				leave_critical(GLOBAL_LOCK);",
	"				sudden_stop(\"out of memory -- aborting\");",
	"				wrapup();	/* exits */",
	"			} else",
	"			{	dc_shared = (sh_Allocater *) dc_shared->nxt;",
	"		}	}",
	"",
	"		rval = (char *) dc_shared->dc_arena;",
	"		dc_shared->dc_arena += n;",
	"		dc_shared->dc_size  -= (long) n;",
	"",
	"		if (VVERBOSE)",
	"		printf(\"cpu%%d grab shared (%%d bytes) -- %%ld left\\n\",",
	"			core_id, n, dc_shared->dc_size);",
	"",
	"	leave_critical(GLOBAL_LOCK);",
	"",
	"	memset(rval, 0, n);",
	"	memcnt += (double) n;",
	"",
	"	return (struct H_el *) rval;",
	"#else",
	"	return (struct H_el *) emalloc(n);",
	"#endif",
	"}",
	"",
	"SM_frame *",
	"Get_Full_Frame(int n)",
	"{	SM_frame *f;",
	"	double cnt_start = frame_wait;",
	"",
	"	f = &m_workq[n][prfull[n]];",
	"	while (f->m_vsize == 0)	/* await full slot LOCK : full frame */",
	"	{	iam_alive();",
	"#ifndef NGQ",
	"		if (*grcnt > 0)	/* accessed outside lock, but safe even if wrong */",
	"		{	enter_critical(GQ_RD);	/* gq - read access */",
	"			if (*grcnt > 0)		/* could have changed */",
	"			{	f = &m_workq[NCORE][*grfull];	/* global q */",
	"				if (f->m_vsize == 0)",
	"				{	/* writer is still filling the slot */",
	"					*gr_writemiss++;",
	"					f = &m_workq[n][prfull[n]]; /* reset */",
	"				} else",
	"				{	*grfull = (*grfull+1) %% (N_FRAMES);",
	"						enter_critical(GQ_WR);",
	"						*grcnt = *grcnt - 1;",
	"						leave_critical(GQ_WR);",
	"					leave_critical(GQ_RD);",
	"					return f;",
	"			}	}",
	"			leave_critical(GQ_RD);",
	"		}",
	"#endif",
	"		if (frame_wait++ - cnt_start > Delay)",
	"		{	if (0)", /* too frequent to enable this one */
	"			{	cpu_printf(\"timeout on q%%d -- %%u -- query %%d\\n\",",
	"					n, f, query_in_progress);",
	"			}",
	"			return (SM_frame *) 0;	/* timeout */",
	"	}	}",
	"	iam_alive();",
	"	if (VVERBOSE) cpu_printf(\"got frame from q%%d\\n\", n);",
	"	prfull[n] = (prfull[n] + 1) %% (N_FRAMES);",
	"	return f;",
	"}",
	"",
	"SM_frame *",
	"Get_Free_Frame(int n)",
	"{	SM_frame *f;",
	"	double cnt_start = free_wait;",
	"",
	"	if (VVERBOSE) { cpu_printf(\"get free frame from q%%d\\n\", n); }",
	"",
	"	if (n == NCORE)	/* global q */",
	"	{	f = &(m_workq[n][lrfree]);",
	"	} else",
	"	{	f = &(m_workq[n][prfree[n]]);",
	"	}",
	"	while (f->m_vsize != 0)	/* await free slot LOCK : free slot */",
	"	{	iam_alive();",
	"		if (free_wait++ - cnt_start > OneSecond)",
	"		{	if (verbose)",
	"			{	cpu_printf(\"timeout waiting for free slot q%%d\\n\", n);",
	"			}",
	"			cnt_start = free_wait;",
	"			if (someone_crashed(1))",
	"			{	printf(\"cpu%%d: search terminated\\n\", core_id);",
	"				sudden_stop(\"get free frame\");",
	"				pan_exit(1);",
	"	}	}	}",
	"	if (n != NCORE)",
	"	{	prfree[n] = (prfree[n] + 1) %% (N_FRAMES);",
	"	}",
	"	return f;",
	"}",
	"",
	"#define TargetQ_NotFull(n)	(m_workq[n][prfree[n]].m_vsize == 0)",
	"#define TargetQ_Empty(n)	(m_workq[n][prfull[n]].m_vsize == 0)",
	""
	"#ifndef NGQ",
	"int",
	"GlobalQ_HasRoom(void)",
	"{	int rval = 0;",
	"",
	"	gq_tries++;",
	"	if (*grcnt < N_FRAMES) /* there seems to be room -- ok if wrong */",
	"	{	enter_critical(GQ_WR);	/* gq write access */",
	"		if (*grcnt < N_FRAMES)",
	"		{	if (m_workq[NCORE][*grfree].m_vsize != 0)",
	"			{	/* can happen if reader is slow emptying slot */",
	"				*gr_readmiss++;",
	"				goto out; /* dont wait: release lock and return */",
	"			}",
	"			lrfree = *grfree;	/* Get_Free_Frame use lrfree in this mode */",
	"			*grfree = (*grfree + 1) %% N_FRAMES;",	/* next process looks at next slot */
	"			*grcnt = *grcnt + 1;	/* count nr of slots filled -- no additional lock needed */",
	"			leave_critical(GQ_WR);	/* for short lock duration */",
	"			gq_hasroom++;",
	"			mem_put(NCORE);		/* copy state into reserved slot */",
	"			rval = 1;		/* successfull handoff */",
	"		} else",
	"		{	gq_hasnoroom++;",
	"out:			leave_critical(GQ_WR);",	/* should be rare */
	"	}	}",
	"	return rval;",
	"}",
	"#endif",
	"",
	"int",
	"Likely_Deadlock(void)",
	"{	int q = (core_id + 1) %% NCORE;	/* target q */",
	"	return (m_workq[q][prfree[q]].m_vsize != 0);",
	"}",
	"",
	"int",
	"unpack_state(SM_frame *f, int from_q)",
	"{	int i, j;",
	"	static struct H_el D_State;",
	"",
	"	if (f->m_vsize > 0)",
	"	{	boq   = f->m_boq;",
	"		if (boq > 256)",
	"		{	cpu_printf(\"saw control %%d, expected state\\n\", boq);",
	"			return 0;",
	"		}",
	"		vsize = f->m_vsize;",
	"correct:",
	"		memcpy((uchar *) &now, (uchar *) f->m_now, vsize);",
	"		for (i = j = 0; i < VMAX; i++, j = (j+1)%%8)",
	"		{	Mask[i] = (f->m_Mask[i/8] & (1<<j)) ? 1 : 0;",
	"		}",
	"		if (now._nr_pr > 0)",
	"		{	memcpy((uchar *) proc_offset, (uchar *) f->m_p_offset, now._nr_pr * sizeof(OFFT));",
	"			memcpy((uchar *) proc_skip,   (uchar *) f->m_p_skip,   now._nr_pr * sizeof(uchar));",
	"		}",
	"		if (now._nr_qs > 0)",
	"		{	memcpy((uchar *) q_offset,    (uchar *) f->m_q_offset, now._nr_qs * sizeof(OFFT));",
	"			memcpy((uchar *) q_skip,      (uchar *) f->m_q_skip,   now._nr_qs * sizeof(uchar));",
	"		}",
	"#ifndef NOVSZ",
	"		if (vsize != now._vsz)",
	"		{	cpu_printf(\"vsize %%d != now._vsz %%d (type %%d) %%d\\n\",",
	"				vsize, now._vsz, f->m_boq, f->m_vsize);",
	"			vsize = now._vsz;",
	"			goto correct;	/* rare event: a race */",
	"		}",
	"#endif",
	"		hmax = max(hmax, vsize);",
	"",
	"		if (f != &cur_Root)",
	"		{	memcpy((uchar *) &cur_Root, (uchar *) f, sizeof(SM_frame));",
	"		}",
	"",
	"		if (((now._a_t) & 1) == 1)	/* i.e., when starting nested DFS */",
	"		{	A_depth = depthfound = 0;",
	"			memcpy((uchar *)&A_Root, (uchar *)&now, vsize);",
	"		}",
	"		nr_handoffs = f->nr_handoffs;",
	"	} else",
	"	{	cpu_printf(\"pan: state empty\\n\");",
	"	}",
	"",
	"	depth = 0;",
	"	trpt = &trail[1];",
	"	trpt->tau    = f->m_tau;",
	"	trpt->o_pm   = f->m_o_pm;",
	"",
	"	(trpt-1)->ostate = &D_State; /* stub */",
	"	trpt->ostate = &D_State;",
	"",
	"#ifdef FULL_TRAIL",
	"	if (upto > 0)",
	"	{	stack_last[core_id] = (Stack_Tree *) f->m_stack;",
	"	}",
	"	#if defined(VERBOSE)",
	"	if (stack_last[core_id])",
	"	{	cpu_printf(\"%%d: UNPACK -- SET m_stack %%u (%%d,%%d)\\n\",",
	"			depth, stack_last[core_id], stack_last[core_id]->pr,",
	"			stack_last[core_id]->t_id);",
	"	}",
	"	#endif",
	"#endif",
	"",
	"	if (!trpt->o_t)",
	"	{	static Trans D_Trans;",
	"		trpt->o_t = &D_Trans;",
	"	}",
	"",
	"	#ifdef VERI",
	"	if ((trpt->tau & 4) != 4)",
	"	{	trpt->tau |= 4;	/* the claim moves first */",
	"		cpu_printf(\"warning: trpt was not up to date\\n\");",
	"	}",
	"	#endif",
	"",
	"	for (i = 0; i < (int) now._nr_pr; i++)",
	"	{	P0 *ptr = (P0 *) pptr(i);",
	"	#ifndef NP",
	"		if (accpstate[ptr->_t][ptr->_p])",
	"		{	trpt->o_pm |= 2;",
	"		}",
	"	#else",
	"		if (progstate[ptr->_t][ptr->_p])",
	"		{	trpt->o_pm |= 4;",