pangen6.h

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

/***** spin: pangen6a.h *****/

/* Copyright (c) 2006-2007 by the California Institute of Technology.     */
/* ALL RIGHTS RESERVED. United States Government Sponsorship acknowledged */
/* Supporting routines for a multi-core extension of the SPIN software    */
/* Developed as part of Reliable Software Engineering Project ESAS/6G     */
/* Like all SPIN Software this software is for educational purposes only. */
/* No guarantee whatsoever is expressed or implied by the distribution of */
/* this code.  Permission is given to distribute this code provided that  */
/* this introductory message is not removed and no monies are exchanged.  */
/* Any commercial use must be negotiated with the Office of Technology    */
/* Transfer at the California Institute of Technology.                    */
/* Software written by Gerard J. Holzmann.  For tool documentation see:   */
/*             http://spinroot.com/                                       */
/* Bug-reports and/or questions can be send to: [e-mail]         */

static char *Code2c[] = { /* multi-core option - Spin 5.0 and later */
	"#if NCORE>1",
	"#if defined(WIN32) || defined(WIN64)",
		"#ifndef _CONSOLE",
		"	#define _CONSOLE",
		"#endif",
		"	#ifdef WIN64",
			"#undef long",
		"	#endif",
		"#include <windows.h>",
		"",
		"	#ifdef WIN64",
		"	#define long	long long",
		"	#endif",
	"#else",
		"#include <sys/ipc.h>",
		"#include <sys/sem.h>",
		"#include <sys/shm.h>",
	"#endif",
	"",
	"/* code common to cygwin/linux and win32/win64: */",
	"",
	"#ifdef VERBOSE",
	"	#define VVERBOSE	(1)",
	"#else",
	"	#define VVERBOSE	(0)",
	"#endif",
	"",
	"/* the following values must be larger than 256 and must fit in an int */",
	"#define QUIT		1024	/* terminate now command */",
	"#define QUERY		 512	/* termination status query message */",
	"#define QUERY_F	 513	/* query failed, cannot quit */",
	"",
	"#define N_FRAMES	(int) (WQ_SIZE / (double) sizeof(SM_frame))",
	"",
	"#ifndef VMAX",
	"	#define VMAX		 256",
	"#endif",
	"#ifndef PMAX",
	"	#define PMAX		  16",
	"#endif",
	"#ifndef QMAX",
	"	#define QMAX		  16",
	"#endif",
	"",
	"#if VECTORSZ>32000",
	"	#define OFFT	int",
	"#else",
	"	#define OFFT	short",
	"#endif",
	"",
	"#ifdef SET_SEG_SIZE",
	"	double SEG_SIZE = (((double) SET_SEG_SIZE) * 1024. * 1024.);",
	"#else",
	"	double SEG_SIZE = (1024.*1024.*1024.);	/* default for cygwin/linux */",
	"#endif",

	"#ifdef SET_WQ_SIZE",
		"double WQ_SIZE  = (((double) SET_WQ_SIZE) * 1024. * 1024.);",
		"/* value set here must match value in pan_proxy.c, if used */",
	"#else",
		"double WQ_SIZE  = (64.*1024.*1024.);",
	"#endif",
	"",
	"/* Crash Detection Parameters */",
	"#ifndef ONESECOND",
	"	#define ONESECOND	(1<<25)", /* name is somewhat of a misnomer */
	"#endif",
	"#ifndef SHORT_T",
	"	#define SHORT_T	(0.1)",
	"#endif",
	"#ifndef LONG_T",
	"	#define LONG_T	(600)",
	"#endif",
	"",
	"double OneSecond   = (double) (ONESECOND); /* waiting for a free slot -- checks crash */",
	"double TenSeconds  = 10. * (ONESECOND);    /* waiting for a lock -- check for a crash */",
	"",
	"/* Termination Detection Params -- waiting for new state input in Get_Full_Frame */",
	"double Delay       = ((double) SHORT_T) * (ONESECOND);	/* termination detection trigger */",
	"double OneHour     = ((double) LONG_T) * (ONESECOND);	/* timeout termination detection */",
	"",
	"typedef struct SM_frame     SM_frame;",
	"typedef struct SM_results   SM_results;",
	"typedef struct sh_Allocater sh_Allocater;",
	"",
	"struct SM_frame {			/* about 6K per slot */",
	"	volatile int	m_vsize;	/* 0 means free slot */",
	"	volatile int	m_boq;		/* >500 is a control message */",
	"#ifdef FULL_TRAIL",
	"	volatile struct Stack_Tree *m_stack;	/* ptr to previous state */",
	"#endif",
	"	volatile uchar	m_tau;",
	"	volatile uchar	m_o_pm;",
	"	volatile int	nr_handoffs;	/* to compute real_depth */",
	"	volatile char	m_now     [VMAX];",
	"	volatile char	m_Mask    [(VMAX + 7)/8];",
	"	volatile OFFT	m_p_offset[PMAX];",
	"	volatile OFFT	m_q_offset[QMAX];",
	"	volatile uchar	m_p_skip  [PMAX];",
	"	volatile uchar	m_q_skip  [QMAX];",
	"#if defined(C_States) && (HAS_TRACK==1) && (HAS_STACK==1)",
	"	volatile uchar	m_c_stack [StackSize];",
		 /* captures contents of c_stack[] for unmatched objects */
	"#endif",
	"};",
	"",
	"int	proxy_pid;		/* id of proxy if nonzero -- receive half */",
	"int	store_proxy_pid;",
	"short	remote_party;",
	"int	proxy_pid_snd;		/* id of proxy if nonzero -- send half */",
	"char	o_cmdline[512];		/* to pass options to children */",
	"",
	"int	iamin[CS_NR+NCORE];		/* non-shared */",
	"",
"#if defined(WIN32) || defined(WIN64)",
	"int tas(volatile LONG *);",
	"",
	"HANDLE		proxy_handle_snd;	/* for Windows Create and Terminate */",
	"",
	"struct sh_Allocater {			/* shared memory for states */",
	"	volatile char	*dc_arena;	/* to allocate states from */",
	"	volatile long	 pattern;	/* to detect overruns */",
	"	volatile long	 dc_size;	/* nr of bytes left */",
	"	volatile void	*dc_start;	/* where memory segment starts */",
	"	volatile void	*dc_id;		/* to attach, detach, remove shared memory segments */",
	"	volatile sh_Allocater *nxt;	/* linked list of pools */",
	"};",
	"DWORD		worker_pids[NCORE];	/* root mem of pids of all workers created */",
	"HANDLE		worker_handles[NCORE];	/* for windows Create and Terminate */",
	"void *		shmid      [NR_QS];	/* return value from CreateFileMapping */",
	"void *		shmid_M;		/* shared mem for state allocation in hashtable */",
	"",
	"#ifdef SEP_STATE",
	"	void *shmid_X;",
	"#else",
	"	void *shmid_S;			/* shared bitstate arena or hashtable */",
	"#endif",
"#else",
	"int tas(volatile int *);",
	"",
	"struct sh_Allocater {			/* shared memory for states */",
	"	volatile char	*dc_arena;	/* to allocate states from */",
	"	volatile long	 pattern;	/* to detect overruns */",
	"	volatile long	 dc_size;	/* nr of bytes left */",
	"	volatile char	*dc_start;	/* where memory segment starts */",
	"	volatile int	dc_id;		/* to attach, detach, remove shared memory segments */",
	"	volatile sh_Allocater *nxt;	/* linked list of pools */",
	"};",
	"",
	"int	worker_pids[NCORE];	/* root mem of pids of all workers created */",
	"int	shmid      [NR_QS];	/* return value from shmget */",
	"int	nibis = 0;		/* set after shared mem has been released */",
	"int	shmid_M;		/* shared mem for state allocation in hashtable */",
	"#ifdef SEP_STATE",
	"	long	shmid_X;",
	"#else",
	"	int	shmid_S;	/* shared bitstate arena or hashtable */",
	"	volatile sh_Allocater	*first_pool;	/* of shared state memory */",
	"	volatile sh_Allocater	*last_pool;",
	"#endif", /* SEP_STATE */
"#endif", /* WIN32 || WIN64 */
	"",
	"struct SM_results {			/* for shuttling back final stats */",
	"	volatile int	m_vsize;	/* avoid conflicts with frames */",
	"	volatile int	m_boq;		/* these 2 fields are not written in record_info */",
	"	/* probably not all fields really need to be volatile */",
	"	volatile double	m_memcnt;",
	"	volatile double	m_nstates;",
	"	volatile double	m_truncs;",
	"	volatile double	m_truncs2;",
	"	volatile double	m_nShadow;",
	"	volatile double	m_nlinks;",
	"	volatile double	m_ngrabs;",
	"	volatile double	m_nlost;",
	"	volatile double	m_hcmp;",
	"	volatile double	m_frame_wait;",
	"	volatile int	m_hmax;",
	"	volatile int	m_svmax;",
	"	volatile int	m_smax;",
	"	volatile int	m_mreached;",
	"	volatile int	m_errors;",
	"	volatile int	m_VMAX;",
	"	volatile short	m_PMAX;",
	"	volatile short	m_QMAX;",
	"	volatile uchar	m_R;		/* reached info for all proctypes */",
	"};",
	"",
	"int		core_id = 0;		/* internal process nr, to know which q to use */",
	"unsigned long	nstates_put = 0;	/* statistics */",
	"unsigned long	nstates_get = 0;",
	"int		query_in_progress = 0;	/* termination detection */",
	"",
	"double		free_wait  = 0.;	/* waiting for a free frame */",
	"double		frame_wait = 0.;	/* waiting for a full frame */",
	"double		lock_wait  = 0.;	/* waiting for access to cs */",
	"double		glock_wait[3];	/* waiting for access to global lock */",
	"",
	"char		*sprefix = \"rst\";",
	"uchar		was_interrupted, issued_kill, writing_trail;",
	"",
	"static SM_frame cur_Root;		/* current root, to be safe with error trails */",
	"",
	"SM_frame	*m_workq   [NR_QS];	/* per cpu work queues + global q */",
	"char		*shared_mem[NR_QS];	/* return value from shmat */",
	"volatile sh_Allocater	*dc_shared;	/* assigned at initialization */",
	"",
	"static int	vmax_seen, pmax_seen, qmax_seen;",
	"static double	gq_tries, gq_hasroom, gq_hasnoroom;",
	"",
	"volatile int *prfree;",	/* [NCORE] independent of presence of global q */
	"volatile int *prfull;",	/* [NCORE] independent of presence of global q */
	"",
	"volatile int	*sh_lock;	/* mutual exclusion locks - in shared memory */",
	"volatile double *is_alive;	/* to detect when processes crash */",
	"volatile int    *grfree, *grfull, *grcnt;	/* access to shared global q */",
	"volatile double *gr_readmiss, *gr_writemiss;",
	"static   int	lrfree;		/* used for temporary recording of slot */",
	"static   int dfs_phase2;",
	"",
	"void mem_put(int);		/* handoff state to other cpu */",
	"void mem_put_wrap(void);	/* liveness mode */",
	"void mem_get(void);		/* get state from work queue  */",
	"void sudden_stop(char *);",
	"void enter_critical(int);",
	"void leave_critical(int);",
	"",
	"void",
	"record_info(SM_results *r)",
	"{	int i;",
	"	uchar *ptr;",
	"",
	"#ifdef SEP_STATE",
	"	if (0)",
	"	{	cpu_printf(\"nstates %%g nshadow %%g -- memory %%-6.3f Mb\\n\",",
	"			nstates, nShadow, memcnt/(1024. * 1024.));",
	"	}",
	"	r->m_memcnt = 0;",
	"#else",
	"	#ifdef BITSTATE",
		"	r->m_memcnt = 0; /* it's shared */",
	"	#endif",
	"	r->m_memcnt = memcnt;",
	"#endif",
	"	if (a_cycles && core_id == 1)",
	"	{	r->m_nstates  = nstates;",
	"		r->m_nShadow  = nstates;",
	"	} else",
	"	{	r->m_nstates  = nstates;",
	"		r->m_nShadow  = nShadow;",
	"	}",
	"	r->m_truncs   = truncs;",
	"	r->m_truncs2  = truncs2;",
	"	r->m_nlinks   = nlinks;",
	"	r->m_ngrabs   = ngrabs;",
	"	r->m_nlost    = nlost;",
	"	r->m_hcmp     = hcmp;",
	"	r->m_frame_wait = frame_wait;",
	"	r->m_hmax     = hmax;",
	"	r->m_svmax    = svmax;",
	"	r->m_smax     = smax;",
	"	r->m_mreached = mreached;",
	"	r->m_errors   = errors;",
	"	r->m_VMAX     = vmax_seen;",
	"	r->m_PMAX     = (short) pmax_seen;",
	"	r->m_QMAX     = (short) qmax_seen;",
	"	ptr = (uchar *) &(r->m_R);",
	"	for (i = 0; i <= _NP_; i++)	/* all proctypes */",
	"	{	memcpy(ptr, reached[i], NrStates[i]*sizeof(uchar));",
	"		ptr += NrStates[i]*sizeof(uchar);",
	"	}",
	"	if (verbose>1)",
	"	{	cpu_printf(\"Put Results nstates %%g (sz %%d)\\n\", nstates, ptr - &(r->m_R));",
	"	}",
	"}",
	"",
	"void snapshot(void);",
	"",
	"void",
	"retrieve_info(SM_results *r)",
	"{	int i, j;",
	"	volatile uchar *ptr;",
	"",
	"	snapshot();	/* for a final report */",
	"	memcnt  += r->m_memcnt;",
	"	nstates += r->m_nstates;",
	"	nShadow += r->m_nShadow;",
	"	truncs  += r->m_truncs;",
	"	truncs2 += r->m_truncs2;",
	"	nlinks  += r->m_nlinks;",
	"	ngrabs  += r->m_ngrabs;",
	"	nlost   += r->m_nlost;",
	"	hcmp    += r->m_hcmp;",
	"	/* frame_wait += r->m_frame_wait; */",
	"	errors  += r->m_errors;",
	"",
	"	if (hmax  < r->m_hmax)  hmax  = r->m_hmax;",
	"	if (svmax < r->m_svmax) svmax = r->m_svmax;",
	"	if (smax  < r->m_smax)  smax  = r->m_smax;",
	"	if (mreached < r->m_mreached) mreached = r->m_mreached;",
	"",
	"	if (vmax_seen < r->m_VMAX) vmax_seen = r->m_VMAX;",
	"	if (pmax_seen < (int) r->m_PMAX) pmax_seen = (int) r->m_PMAX;",
	"	if (qmax_seen < (int) r->m_QMAX) qmax_seen = (int) r->m_QMAX;",
	"",
	"	ptr = &(r->m_R);",
	"	for (i = 0; i <= _NP_; i++)	/* all proctypes */",
	"	{	for (j = 0; j < NrStates[i]; j++)",
	"		{	if (*(ptr + j) != 0)",
	"			{	reached[i][j] = 1;",
	"		}	}",
	"		ptr += NrStates[i]*sizeof(uchar);",
	"	}",
	"	if (verbose>1)",
	"	{	cpu_printf(\"Got Results (%%d)\\n\", ptr - &(r->m_R));",
	"		snapshot();",
	"	}",
	"}",
	"",
	"#if !defined(WIN32) && !defined(WIN64)",
	"static void",
	"rm_shared_segments(void)",
	"{	int m;",
	"	volatile sh_Allocater *nxt_pool;",
	"	/*",
	"	 * mark all shared memory segments for removal ",
	"	 * the actual removes wont happen intil last process dies or detaches",
	"	 * the shmctl calls can return -1 if not all procs have detached yet",
	"	 */",
	"	for (m = 0; m < NR_QS; m++)	/* +1 for global q */",
	"	{	if (shmid[m] != -1)",
	"		{	(void) shmctl(shmid[m], IPC_RMID, NULL);",
	"	}	}",
	"#ifdef SEP_STATE",
	"	if (shmid_M != -1)",
	"	{	(void) shmctl(shmid_M, IPC_RMID, NULL);",
	"	}",
	"#else",
	"	if (shmid_S != -1)",
	"	{	(void) shmctl(shmid_S, IPC_RMID, NULL);",
	"	}",
	"	for (last_pool = first_pool; last_pool != NULL; last_pool = nxt_pool)",
	"	{	shmid_M = (int) (last_pool->dc_id);",
	"		nxt_pool = last_pool->nxt;	/* as a pre-caution only */",
	"		if (shmid_M != -1)",
	"		{	(void) shmctl(shmid_M, IPC_RMID, NULL);",
	"	}	}",
	"#endif",
	"}",
	"#endif",
	"",
	"void",
	"sudden_stop(char *s)",
	"{	char b[64];",
	"	int i;",
	"",
	"	printf(\"cpu%%d: stop - %%s\\n\", core_id, s);",
	"#if !defined(WIN32) && !defined(WIN64)",
	"	if (proxy_pid != 0)",
	"	{	rm_shared_segments();",
	"	}",
	"#endif",
	"	if (search_terminated != NULL)",
	"	{	if (*search_terminated != 0)",
	"		{	if (verbose)",
	"			{	printf(\"cpu%%d: termination initiated (%%d)\\n\",",
	"					core_id, *search_terminated);",
	"			}",
	"		} else",
	"		{	if (verbose)",
	"			{	printf(\"cpu%%d: initiated termination\\n\", core_id);",
	"			}",
	"			*search_terminated |= 8;	/* sudden_stop */",
	"		}",
	"		if (core_id == 0)",
	"		{	if (((*search_terminated) & 4)	/* uerror in one of the cpus */",
	"			&& !((*search_terminated) & (8|32|128|256))) /* abnormal stop */",
	"			{	if (errors == 0) errors++; /* we know there is at least 1 */",