+++ /dev/null
-/***** spin: pangen6.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: bugs@spinroot.com */
-
-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 GN_FRAMES (int) (GWQ_SIZE / (double) sizeof(SM_frame))",
- "#define LN_FRAMES (int) (LWQ_SIZE / (double) sizeof(SM_frame))",
- "",
- "#ifndef VMAX",
- " #define VMAX VECTORSZ",
- "#endif",
- "#ifndef PMAX",
- " #define PMAX 64",
- "#endif",
- "#ifndef QMAX",
- " #define QMAX 64",
- "#endif",
- "",
- "#if VECTORSZ>32000",
- " #define OFFT int",
- "#else",
- " #define OFFT short",
- "#endif",
- "",
- "#ifdef SET_SEG_SIZE",
- " /* no longer usefule -- being recomputed for local heap size anyway */",
- " double SEG_SIZE = (((double) SET_SEG_SIZE) * 1048576.);",
- "#else",
- " double SEG_SIZE = (1048576.*1024.); /* 1GB default shared memory pool segments */",
- "#endif",
- "",
- "double LWQ_SIZE = 0.; /* initialized in main */",
- "",
- "#ifdef SET_WQ_SIZE",
- " #ifdef NGQ",
- " #warning SET_WQ_SIZE applies to global queue -- ignored",
- " double GWQ_SIZE = 0.;",
- " #else",
- " double GWQ_SIZE = (((double) SET_WQ_SIZE) * 1048576.);",
- " /* must match the value in pan_proxy.c, if used */",
- " #endif",
- "#else",
- " #ifdef NGQ",
- " double GWQ_SIZE = 0.;",
- " #else",
- " double GWQ_SIZE = (128.*1048576.); /* 128 MB default queue sizes */",
- " #endif",
- "#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 */",
- "#ifdef SEP_HEAP",
- "char *my_heap;",
- "long my_size;",
- "#endif",
- "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] */
- "volatile int *prfull;", /* [NCORE] */
- "volatile int *prcnt;", /* [NCORE] */
- "volatile int *prmax;", /* [NCORE] */
- "",
- "volatile int *sh_lock; /* mutual exclusion locks - in shared memory */",
- "volatile double *is_alive; /* to detect when processes crash */",
- "volatile int *grfree, *grfull, *grcnt, *grmax; /* 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_acc(void); /* liveness mode */",
- "void mem_get(void); /* get state from work queue */",
- "void sudden_stop(char *);",
- "#if 0",
- "void enter_critical(int);",
- "void leave_critical(int);",
- "#endif",
- "",
- "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/(1048576.));",
- " }",
- " 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 */",
- "",
- " enter_critical(GLOBAL_LOCK);",
- "#ifdef SEP_HEAP",
- " if (verbose)",
- " { printf(\"cpu%%d: local heap-left %%ld KB (%%d MB)\\n\",",
- " core_id, (int) (my_size/1024), (int) (my_size/1048576));",
- " }",
- "#endif",
- " if (verbose && core_id == 0)",
- " { printf(\"qmax: \");",
- " for (i = 0; i < NCORE; i++)",
- " { printf(\"%%d \", prmax[i]);",
- " }",
- "#ifndef NGQ",
- " printf(\"G: %%d\", *grmax);",
- "#endif",
- " printf(\"\\n\");",
- " }",
- " leave_critical(GLOBAL_LOCK);",
- "",
- " 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 */",
- " }",
- " 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)",
- "{",
- " enter_critical(GLOBAL_LOCK);",
- " if (verbose)",
- " {",
- "#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",
- " }",
- " if (free_wait > 1000000.)",
- " #ifndef NGQ",
- " if (!a_cycles)",
- " { printf(\"hint: this search may be faster with a larger work-queue\\n\");",
- " printf(\" (-DSET_WQ_SIZE=N with N>%%g), and/or with -DUSE_DISK\\n\",",
- " GWQ_SIZE/sizeof(SM_frame));",
- " printf(\" or with a larger value for -zN (N>%%d)\\n\", z_handoff);",
- " #else",
- " { printf(\"hint: this search may be faster if compiled without -DNGQ, with -DUSE_DISK, \");",
- " printf(\"or with a larger -zN (N>%%d)\\n\", z_handoff);",
- " #endif",
- " }",
- " 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\");",
- " fprintf(fd, \"Defining multi-core mode:\\n\\n\");",
- " fprintf(fd, \" -DDUAL_CORE --> same as -DNCORE=2\\n\");",
- " fprintf(fd, \" -DQUAD_CORE --> same as -DNCORE=4\\n\");",
- " fprintf(fd, \" -DNCORE=N --> enables multi_core verification if N>1\\n\");",
- " fprintf(fd, \"\\n\");",
- " fprintf(fd, \"Additional directives supported in multi-core mode:\\n\\n\");",
- " fprintf(fd, \" -DSEP_STATE --> forces separate statespaces instead of a single shared state space\\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, \" -DFULL_TRAIL --> support full error trails (increases memory use)\\n\");",
- " fprintf(fd, \"\\n\");",
- " fprintf(fd, \"More advanced use (should rarely need changing):\\n\\n\");",
- " fprintf(fd, \" To change the nr of states that can be stored in the global queue\\n\");",
- " fprintf(fd, \" (lower numbers allow for more states to be stored, prefer multiples of 8):\\n\");",
- " fprintf(fd, \" -DVMAX=N --> upperbound on statevector for handoffs (N=%%d)\\n\", VMAX);",
- " fprintf(fd, \" -DPMAX=N --> upperbound on nr of procs (default: N=%%d)\\n\", PMAX);",
- " fprintf(fd, \" -DQMAX=N --> upperbound on nr of channels (default: N=%%d)\\n\", QMAX);",
- " fprintf(fd, \"\\n\");",
-#if 0
- "#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/(1048576.));",
- " fprintf(fd, \"\\n\");",
- "#endif",
-#endif
- " fprintf(fd, \" To set the total amount of memory reserved for the global workqueue:\\n\");",
- " fprintf(fd, \" -DSET_WQ_SIZE=N --> default: N=128 (defined in MBytes)\\n\\n\");",
-#if 0
- " fprintf(fd, \" To omit the global workqueue completely (bad idea):\\n\");",
- " fprintf(fd, \" -DNGQ\\n\\n\");",
-#endif
- " fprintf(fd, \" To force the use of a single global heap, instead of separate heaps:\\n\");",
- " fprintf(fd, \" -DGLOB_HEAP\\n\");",
- " fprintf(fd, \"\\n\");",
- " fprintf(fd, \" To define a fct to initialize data before spawning processes (use quotes):\\n\");",
- " fprintf(fd, \" \\\"-DC_INIT=fct()\\\"\\n\");",
- " fprintf(fd, \"\\n\");",
- " fprintf(fd, \" Timer settings for termination and crash detection:\\n\");",
- " fprintf(fd, \" -DSHORT_T=N --> timeout for termination detection trigger (N=%%g)\\n\", (double) SHORT_T);",
- " fprintf(fd, \" -DLONG_T=N --> timeout for giving up on termination detection (N=%%g)\\n\", (double) LONG_T);",
- " fprintf(fd, \" -DONESECOND --> (1<<29) --> timeout waiting for a free slot -- to check for crash\\n\");",
- " fprintf(fd, \" -DT_ALERT --> collect stats on crash alert timeouts\\n\\n\");",
- " fprintf(fd, \"Help with Linux/Windows/Cygwin configuration for multi-core:\\n\");",
- " fprintf(fd, \" http://spinroot.com/spin/multicore/V5_Readme.html\\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 */",
- " }",
- "}",
- "",
- "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\",",
- " ((double) NCORE * LWQ_SIZE + GWQ_SIZE) / (1048576.) );",
- " }",
- " for (m = 0; m < NR_QS; m++) /* last q is the global q */",
- " { double qsize = (m == NCORE) ? GWQ_SIZE : LWQ_SIZE;",
- " 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) qsize, 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) qsize, 0600|IPC_CREAT|IPC_EXCL);",
- " memcnt += qsize;",
- " } else /* workers attach */",
- " { shmid[m] = shmget(key[m], (size_t) qsize, 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 (%%d Mb)\\n\",",
- " m+1, (int) (qsize/(1048576.)));",
- " perror(\"shmat shared queues\"); must_exit = 1; break;",
- " }",
- "",
- " m_workq[m] = (SM_frame *) shared_mem[m];",
- " if (core_id == 0)",
- " { int nframes = (m == NCORE) ? GN_FRAMES : LN_FRAMES;",
- " for (n = 0; n < nframes; n++)",
- " { m_workq[m][n].m_vsize = 0;",
- " m_workq[m][n].m_boq = 0;",
- " } } }",
- "",
- " if (must_exit)",
- " { rm_shared_segments();",
- " fprintf(stderr, \"pan: check './pan --' for usage details\\n\");",
- " pan_exit(1); /* calls cleanup_shm */",
- " }",
- "}",
- "",
- "static uchar *",
- "prep_shmid_S(size_t n) /* either sets SS or H_tab, linux/cygwin */",
- "{ char *rval;",
- "#ifndef SEP_STATE",
- " key_t key;",
- "",
- " if (verbose && core_id == 0)",
- " {",
- " #ifdef BITSTATE",
- " printf(\"cpu0: step 1: allocate shared bitstate %%g Mb\\n\",",
- " (double) n / (1048576.));",
- " #else",
- " printf(\"cpu0: step 1: allocate shared hastable %%g Mb\\n\",",
- " (double) n / (1048576.));",
- " #endif",
- " }",
- " #ifdef MEMLIM", /* memlim has a value */
- " if (memcnt + (double) n > memlim)",
- " { printf(\"cpu0: S %%8g + %%d Kb exceeds memory limit of %%8g Mb\\n\",",
- " memcnt/1024., n/1024, memlim/(1048576.));",
- " printf(\"cpu0: insufficient memory -- aborting\\n\");",
- " exit(1);",
- " }",
- " #endif",
- "",
- " key = ftok(PanSource, NCORE+2); /* different from queues */",
- " if (key == -1)",
- " { perror(\"ftok shared bitstate or hashtable\");",
- " fprintf(stderr, \"pan: check './pan --' for usage details\\n\");",
- " pan_exit(1);",
- " }",
- "",
- " if (core_id == 0) /* root */",
- " { shmid_S = shmget(key, n, 0600);",
- " if (shmid_S != -1)",
- " { printf(\"cpu0: removing stale segment, status: %%d\\n\",",
- " shmctl(shmid_S, IPC_RMID, NULL));",
- " }",
- " shmid_S = shmget(key, n, 0600 | IPC_CREAT | IPC_EXCL);",
- " memcnt += (double) n;",
- " } else /* worker */",
- " { shmid_S = shmget(key, n, 0600);",
- " }",
- " if (shmid_S == -1)",
- " { perror(\"shmget shared bitstate or hashtable too large?\");",
- " fprintf(stderr, \"pan: check './pan --' for usage details\\n\");",
- " pan_exit(1);",
- " }",
- "",
- " rval = (char *) shmat(shmid_S, (void *) 0, 0); /* attach */",
- " if ((char *) rval == (char *) -1)",
- " { perror(\"shmat shared bitstate or hashtable\");",
- " fprintf(stderr, \"pan: check './pan --' for usage details\\n\");",
- " pan_exit(1);",
- " }",
- "#else",
- " rval = (char *) emalloc(n);",
- "#endif",
- " return (uchar *) rval;",
- "}",
- "",
- "#define TRY_AGAIN 1",
- "#define NOT_AGAIN 0",
- "",
- "static char shm_prep_result;",
- "",
- "static uchar *",
- "prep_state_mem(size_t n) /* sets memory arena for states linux/cygwin */",
- "{ char *rval;",
- " key_t key;",
- " static int cnt = 3; /* start larger than earlier ftok calls */",
- "",
- " shm_prep_result = NOT_AGAIN; /* default */",
- " if (verbose && core_id == 0)",
- " { printf(\"cpu0: step 2+: pre-allocate memory arena %%d of %%6.2g Mb\\n\",",
- " cnt-3, (double) n / (1048576.));",
- " }",
- " #ifdef MEMLIM",
- " if (memcnt + (double) n > memlim)",
- " { printf(\"cpu0: error: M %%.0f + %%.0f Kb exceeds memory limit of %%.0f Mb\\n\",",
- " memcnt/1024.0, (double) n/1024.0, memlim/(1048576.));",
- " return NULL;",
- " }",
- " #endif",
- "",
- " key = ftok(PanSource, NCORE+cnt); cnt++;", /* starts at NCORE+3 */
- " if (key == -1)",
- " { perror(\"ftok T\");",
- " printf(\"pan: check './pan --' for usage details\\n\");",
- " pan_exit(1);",
- " }",
- "",
- " if (core_id == 0)",
- " { shmid_M = shmget(key, n, 0600);",
- " if (shmid_M != -1)",
- " { printf(\"cpu0: removing stale memory segment %%d, status: %%d\\n\",",
- " cnt-3, shmctl(shmid_M, IPC_RMID, NULL));",
- " }",
- " shmid_M = shmget(key, n, 0600 | IPC_CREAT | IPC_EXCL);",
- " /* memcnt += (double) n; -- only amount actually used is counted */",
- " } else",
- " { shmid_M = shmget(key, n, 0600);",
- " ",
- " }",
- " if (shmid_M == -1)",
- " { if (verbose)",
- " { printf(\"error: failed to get pool of shared memory %%d of %%.0f Mb\\n\",",
- " cnt-3, ((double)n)/(1048576.));",
- " perror(\"state mem\");",
- " printf(\"pan: check './pan --' for usage details\\n\");",
- " }",
- " shm_prep_result = TRY_AGAIN;",
- " return NULL;",
- " }",
- " rval = (char *) shmat(shmid_M, (void *) 0, 0); /* attach */",
- "",
- " if ((char *) rval == (char *) -1)",
- " { printf(\"cpu%%d error: failed to attach pool of shared memory %%d of %%.0f Mb\\n\",",
- " core_id, cnt-3, ((double)n)/(1048576.));",
- " perror(\"state mem\");",
- " return NULL;",
- " }",
- " return (uchar *) rval;",
- "}",
- "",
- "void",
- "init_HT(unsigned long n) /* cygwin/linux version */",
- "{ volatile char *x;",
- " double get_mem;",
- "#ifndef SEP_STATE",
- " volatile char *dc_mem_start;",
- " double need_mem, got_mem = 0.;",
- "#endif",
- "",
-"#ifdef SEP_STATE",
- " #ifndef MEMLIM",
- " if (verbose)",
- " { printf(\"cpu0: steps 0,1: no -DMEMLIM set\\n\");", /* cannot happen */
- " }",
- " #else",
- " if (verbose)",
- " { printf(\"cpu0: steps 0,1: -DMEMLIM=%%d Mb - (hashtable %%g Mb + workqueues %%g Mb)\\n\",",
- " MEMLIM, ((double)n/(1048576.)), (((double) NCORE * LWQ_SIZE) + GWQ_SIZE) /(1048576.) );",
- " }",
- " #endif",
- " get_mem = NCORE * sizeof(double) + (1 + CS_NR) * sizeof(void *) + 4*sizeof(void *) + 2*sizeof(double);",
- " /* NCORE * is_alive + search_terminated + CS_NR * sh_lock + 6 gr vars */",
- " get_mem += 4 * NCORE * sizeof(void *); /* prfree, prfull, prcnt, prmax */",
- " #ifdef FULL_TRAIL",
- " get_mem += (NCORE) * sizeof(Stack_Tree *); /* NCORE * stack_last */",
- " #endif",
- " x = (volatile char *) prep_state_mem((size_t) get_mem); /* work queues and basic structs */",
- " shmid_X = (long) x;",
- " if (x == NULL)", /* do not repeat for smaller sizes */
- " { printf(\"cpu0: could not allocate shared memory, see ./pan --\\n\");",
- " exit(1);",
- " }",
- " search_terminated = (volatile unsigned int *) x; /* comes first */",
- " x += sizeof(void *); /* maintain alignment */",
- "",
- " is_alive = (volatile double *) x;",
- " x += NCORE * sizeof(double);",
- "",
- " sh_lock = (volatile int *) x;",
- " x += CS_NR * sizeof(void *);", /* allow 1 word per entry */
- "",
- " grfree = (volatile int *) x;",
- " x += sizeof(void *);",
- " grfull = (volatile int *) x;",
- " x += sizeof(void *);",
- " grcnt = (volatile int *) x;",
- " x += sizeof(void *);",
- " grmax = (volatile int *) x;",
- " x += sizeof(void *);",
- " prfree = (volatile int *) x;",
- " x += NCORE * sizeof(void *);",
- " prfull = (volatile int *) x;",
- " x += NCORE * sizeof(void *);",
- " prcnt = (volatile int *) x;",
- " x += NCORE * sizeof(void *);",
- " prmax = (volatile int *) x;",
- " x += NCORE * sizeof(void *);",
- " gr_readmiss = (volatile double *) x;",
- " x += sizeof(double);",
- " gr_writemiss = (volatile double *) x;",
- " x += sizeof(double);",
- "",
- " #ifdef FULL_TRAIL",
- " stack_last = (volatile Stack_Tree **) x;",
- " x += NCORE * sizeof(Stack_Tree *);",
- " #endif",
- "",
- " #ifndef BITSTATE",
- " H_tab = (struct H_el **) emalloc(n);",
- " #endif",
-"#else",
- " #ifndef MEMLIM",
- " #warning MEMLIM not set", /* cannot happen */
- " #define MEMLIM (2048)",
- " #endif",
- "",
- " if (core_id == 0 && verbose)",
- " { printf(\"cpu0: step 0: -DMEMLIM=%%d Mb minus hashtable+workqs (%%g + %%g Mb) leaves %%g Mb\\n\",",
- " MEMLIM, ((double)n/(1048576.)), (NCORE * LWQ_SIZE + GWQ_SIZE)/(1048576.),",
- " (memlim - memcnt - (double) n - (NCORE * LWQ_SIZE + GWQ_SIZE))/(1048576.));",
- " }",
- " #ifndef BITSTATE",
- " H_tab = (struct H_el **) prep_shmid_S((size_t) n); /* hash_table */",
- " #endif",
- " need_mem = memlim - memcnt - ((double) NCORE * LWQ_SIZE) - GWQ_SIZE;",
- " if (need_mem <= 0.)",
- " { Uerror(\"internal error -- shared state memory\");",
- " }",
- "",
- " if (core_id == 0 && verbose)",
- " { printf(\"cpu0: step 2: pre-allocate shared state memory %%g Mb\\n\",",
- " need_mem/(1048576.));",
- " }",
- "#ifdef SEP_HEAP",
- " SEG_SIZE = need_mem / NCORE;",
- " if (verbose && core_id == 0)",
- " { printf(\"cpu0: setting segsize to %%6g MB\\n\",",
- " SEG_SIZE/(1048576.));",
- " }",
- " #if defined(CYGWIN) || defined(__CYGWIN__)",
- " if (SEG_SIZE > 512.*1024.*1024.)",
- " { printf(\"warning: reducing SEG_SIZE of %%g MB to 512MB (exceeds max for Cygwin)\\n\",",
- " SEG_SIZE/(1024.*1024.));",
- " SEG_SIZE = 512.*1024.*1024.;",
- " }",
- " #endif",
- "#endif",
- " mem_reserved = need_mem;",
- " while (need_mem > 1024.)",
- " { get_mem = need_mem;",
- "shm_more:",
- " if (get_mem > (double) SEG_SIZE)",
- " { get_mem = (double) SEG_SIZE;",
- " }",
- " if (get_mem <= 0.0) break;",
- "",
- " /* for allocating states: */",
- " x = dc_mem_start = (volatile char *) prep_state_mem((size_t) get_mem);",
- " if (x == NULL)",
- " { if (shm_prep_result == NOT_AGAIN",
- " || first_pool != NULL",
- " || SEG_SIZE < (16. * 1048576.))",
- " { break;",
- " }",
- " SEG_SIZE /= 2.;",
- " if (verbose)",
- " { printf(\"pan: lowered segsize to %f\\n\", SEG_SIZE);",
- " }",
- " if (SEG_SIZE >= 1024.)",
- " { goto shm_more;", /* always terminates */
- " }",
- " break;",
- " }",
- "",
- " need_mem -= get_mem;",
- " got_mem += get_mem;",
- " if (first_pool == NULL)",
- " { search_terminated = (volatile unsigned int *) x; /* comes first */",
- " x += sizeof(void *); /* maintain alignment */",
- "",
- " is_alive = (volatile double *) x;",
- " x += NCORE * sizeof(double);",
- "",
- " sh_lock = (volatile int *) x;",
- " x += CS_NR * sizeof(void *);", /* allow 1 word per entry */
- "",
- " grfree = (volatile int *) x;",
- " x += sizeof(void *);",
- " grfull = (volatile int *) x;",
- " x += sizeof(void *);",
- " grcnt = (volatile int *) x;",
- " x += sizeof(void *);",
- " grmax = (volatile int *) x;",
- " x += sizeof(void *);",
- " prfree = (volatile int *) x;",
- " x += NCORE * sizeof(void *);",
- " prfull = (volatile int *) x;",
- " x += NCORE * sizeof(void *);",
- " prcnt = (volatile int *) x;",
- " x += NCORE * sizeof(void *);",
- " prmax = (volatile int *) x;",
- " x += NCORE * sizeof(void *);",
- " gr_readmiss = (volatile double *) x;",
- " x += sizeof(double);",
- " gr_writemiss = (volatile double *) x;",
- " x += sizeof(double);",
- " #ifdef FULL_TRAIL",
- " stack_last = (volatile Stack_Tree **) x;",
- " x += NCORE * sizeof(Stack_Tree *);",
- " #endif",
- " if (((long)x)&(sizeof(void *)-1)) /* 64-bit word alignment */",
- " { x += sizeof(void *)-(((long)x)&(sizeof(void *)-1));",
- " }",
- "",
- " #ifdef COLLAPSE",
- " ncomps = (unsigned long *) x;",
- " x += (256+2) * sizeof(unsigned long);",
- " #endif",
- " }",
- "",
- " dc_shared = (sh_Allocater *) x; /* must be in shared memory */",
- " x += sizeof(sh_Allocater);",
- "",
- " if (core_id == 0) /* root only */",
- " { dc_shared->dc_id = shmid_M;",
- " dc_shared->dc_start = dc_mem_start;",
- " dc_shared->dc_arena = x;",
- " dc_shared->pattern = 1234567; /* protection */",
- " dc_shared->dc_size = (long) get_mem - (long) (x - dc_mem_start);",
- " dc_shared->nxt = (long) 0;",
- "",
- " if (last_pool == NULL)",
- " { first_pool = last_pool = dc_shared;",
- " } else",
- " { last_pool->nxt = dc_shared;",
- " last_pool = dc_shared;",
- " }",
- " } else if (first_pool == NULL)",
- " { first_pool = dc_shared;",
- " } }",
- "",
- " if (need_mem > 1024.)",
- " { printf(\"cpu0: could allocate only %%g Mb of shared memory (wanted %%g more)\\n\",",
- " got_mem/(1048576.), need_mem/(1048576.));",
- " }",
- "",
- " if (!first_pool)",
- " { printf(\"cpu0: insufficient memory -- aborting.\\n\");",
- " exit(1);",
- " }",
- " /* we are still single-threaded at this point, with core_id 0 */",
- " dc_shared = first_pool;",
- "",
-"#endif", /* !SEP_STATE */
- "}",
- "",
- " /* Test and Set assembly code */",
- "",
- " #if defined(i386) || defined(__i386__) || defined(__x86_64__)",
- " int",
- " tas(volatile int *s) /* tested */",
- " { int r;",
- " __asm__ __volatile__(",
- " \"xchgl %%0, %%1 \\n\\t\"",
- " : \"=r\"(r), \"=m\"(*s)",
- " : \"0\"(1), \"m\"(*s)",
- " : \"memory\");",
- " ",
- " return r;",
- " }",
- " #elif defined(__arm__)",
- " int",
- " tas(volatile int *s) /* not tested */",
- " { int r = 1;",
- " __asm__ __volatile__(",
- " \"swpb %%0, %%0, [%%3] \\n\"",
- " : \"=r\"(r), \"=m\"(*s)",
- " : \"0\"(r), \"r\"(s));",
- "",
- " return r;",
- " }",
- " #elif defined(sparc) || defined(__sparc__)",
- " int",
- " tas(volatile int *s) /* not tested */",
- " { int r = 1;",
- " __asm__ __volatile__(",
- " \" ldstub [%%2], %%0 \\n\"",
- " : \"=r\"(r), \"=m\"(*s)",
- " : \"r\"(s));",
- "",
- " return r;",
- " }",
- " #elif defined(ia64) || defined(__ia64__)",
- " /* Intel Itanium */",
- " int",
- " tas(volatile int *s) /* tested */",
- " { long int r;",
- " __asm__ __volatile__(",
- " \" xchg4 %%0=%%1,%%2 \\n\"",
- " : \"=r\"(r), \"+m\"(*s)",
- " : \"r\"(1)",
- " : \"memory\");",
- " return (int) r;",
- " }",
- " #else",
- " #error missing definition of test and set operation for this platform",
- " #endif",
- "",
- "void",
- "cleanup_shm(int val)",
- "{ volatile sh_Allocater *nxt_pool;",
- " unsigned long cnt = 0;",
- " int m;",
- "",
- " if (nibis != 0)",
- " { printf(\"cpu%%d: Redundant call to cleanup_shm(%%d)\\n\", core_id, val);",
- " return;",
- " } else",
- " { nibis = 1;",
- " }",
- " if (search_terminated != NULL)",
- " { *search_terminated |= 16; /* cleanup_shm */",
- " }",
- "",
- " for (m = 0; m < NR_QS; m++)",
- " { if (shmdt((void *) shared_mem[m]) > 0)",
- " { perror(\"shmdt detaching from shared queues\");",
- " } }",
- "",
- "#ifdef SEP_STATE",
- " 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)(1048576));",
- " } }",
- "",
- " 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\");",
- " }",
- " fflush(stdout);",
- "",
- "/* 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 defined(SEP_HEAP) && !defined(SEP_STATE)", /* set my_heap and adjust dc_shared */
- " { int i;",
- " volatile sh_Allocater *ptr;",
- " ptr = first_pool;",
- " for (i = 0; i < NCORE && ptr != NULL; i++)",
- " { if (i == core_id)",
- " { my_heap = (char *) ptr->dc_arena;",
- " my_size = (long) ptr->dc_size;",
- " if (verbose)",
- " cpu_printf(\"local heap %%ld MB\\n\", my_size/(1048576));",
- " break;",
- " }",
- " ptr = ptr->nxt; /* local */",
- " }",
- " if (my_heap == NULL)",
- " { printf(\"cpu%%d: no local heap\\n\", core_id);",
- " pan_exit(1);",
- " } /* else */",
- " #if defined(CYGWIN) || defined(__CYGWIN__)",
- " ptr = first_pool;",
- " for (i = 0; i < NCORE && ptr != NULL; i++)",
- " { ptr = ptr->nxt; /* local */",
- " }",
- " dc_shared = ptr; /* any remainder */",
- " #else",
- " dc_shared = NULL; /* used all mem for local heaps */",
- " #endif",
- " }",
- "#endif",
-
- " 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\\n\",",
- " nstates_put, nstates_get);",
- " }",
- " 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 */",
- " }",
- "",
- "#ifdef SEP_HEAP",
- " /* no locking */",
- " if (my_heap != NULL && my_size > n)",
- " { rval = my_heap;",
- " my_heap += n;",
- " my_size -= n;",
- " goto done;",
- " }",
- "#endif",
- "",
- " if (!dc_shared)",
- " { sudden_stop(\"pan: out of memory\");",
- " }",
- "",
- " /* another lock is always already in effect when this is called */",
- " /* but not always the same lock -- i.e., on different parts of the hashtable */",
- " enter_critical(GLOBAL_LOCK); /* this must be independently mutex */",
- "#if defined(SEP_HEAP) && !defined(WIN32) && !defined(WIN64)",
- " { static int noted = 0;",
- " if (!noted)",
- " { noted = 1;",
- " printf(\"cpu%%d: global heap has %%ld bytes left, needed %%d\\n\",",
- " core_id, dc_shared?dc_shared->dc_size:0, n);",
- " } }",
- "#endif",
- "#if 0", /* for debugging */
- " if (dc_shared->pattern != 1234567)",
- " { leave_critical(GLOBAL_LOCK);",
- " Uerror(\"overrun -- memory corruption\");",
- " }",
- "#endif",
- " if (dc_shared->dc_size < n)",
- " { if (verbose)",
- " { printf(\"Next Pool %%g Mb + %%d\\n\", memcnt/(1048576.), 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 / (1048576.), 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 0",
- " if (VVERBOSE)",
- " printf(\"cpu%%d grab shared (%%d bytes) -- %%ld left\\n\",",
- " core_id, n, dc_shared->dc_size);",
- "#endif",
- " leave_critical(GLOBAL_LOCK);",
- "done:",
- " 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",
- " #ifndef SAFETY",
- " if (!a_cycles || core_id != 0)",
- " #endif",
- " 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) %% (GN_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) %% (LN_FRAMES);",
- " enter_critical(QLOCK(n));",
- " prcnt[n]--; /* lock out increments */",
- " leave_critical(QLOCK(n));",
- " 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) %% (LN_FRAMES);",
- " enter_critical(QLOCK(n));",
- " prcnt[n]++; /* lock out decrements */",
- " if (prmax[n] < prcnt[n])",
- " { prmax[n] = prcnt[n];",
- " }",
- " leave_critical(QLOCK(n));",
- " }",
- " return f;",
- "}",
- ""
- "#ifndef NGQ",
- "int",
- "GlobalQ_HasRoom(void)",
- "{ int rval = 0;",
- "",
- " gq_tries++;",
- " if (*grcnt < GN_FRAMES) /* there seems to be room */",
- " { enter_critical(GQ_WR); /* gq write access */",
- " if (*grcnt < GN_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) %% GN_FRAMES;", /* next process looks at next slot */
- " *grcnt = *grcnt + 1; /* count nr of slots filled -- no additional lock needed */",
- " if (*grmax < *grcnt) *grmax = *grcnt;",
- " 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",
- "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;",
- " }",
- " #endif",
- " }",
- "",
- " #ifdef EVENT_TRACE",
- " #ifndef NP",
- " if (accpstate[EVENT_TRACE][now._event])",
- " { trpt->o_pm |= 2;",
- " }",
- " #else",
- " if (progstate[EVENT_TRACE][now._event])",
- " { trpt->o_pm |= 4;",
- " }",
- " #endif",
- " #endif",
- "",
- " #if defined(C_States) && (HAS_TRACK==1)",
- " /* restore state of tracked C objects */",
- " c_revert((uchar *) &(now.c_state[0]));",
- " #if (HAS_STACK==1)",
- " c_unstack((uchar *) f->m_c_stack); /* unmatched tracked data */",
- " #endif",
- " #endif",
- " return 1;",
- "}",
- "",
- "void",
- "write_root(void) /* for trail file */",
- "{ int fd;",
- "",
- " if (iterative == 0 && Nr_Trails > 1)",
- " sprintf(fnm, \"%%s%%d.%%s\", TrailFile, Nr_Trails-1, sprefix);",
- " else",
- " sprintf(fnm, \"%%s.%%s\", TrailFile, sprefix);",
- "",
- " if (cur_Root.m_vsize == 0)",
- " { (void) unlink(fnm); /* remove possible old copy */",
- " return; /* its the default initial state */",
- " }",
- "",
- " if ((fd = creat(fnm, TMODE)) < 0)",
- " { char *q;",
- " if ((q = strchr(TrailFile, \'.\')))",
- " { *q = \'\\0\'; /* strip .pml */",
- " if (iterative == 0 && Nr_Trails-1 > 0)",
- " sprintf(fnm, \"%%s%%d.%%s\", TrailFile, Nr_Trails-1, sprefix);",
- " else",
- " sprintf(fnm, \"%%s.%%s\", TrailFile, sprefix);",
- " *q = \'.\';",
- " fd = creat(fnm, TMODE);",
- " }",
- " if (fd < 0)",
- " { cpu_printf(\"pan: cannot create %%s\\n\", fnm);",
- " perror(\"cause\");",
- " return;",
- " } }",
- "",
- " if (write(fd, &cur_Root, sizeof(SM_frame)) != sizeof(SM_frame))",
- " { cpu_printf(\"pan: error writing %%s\\n\", fnm);",
- " } else",
- " { cpu_printf(\"pan: wrote %%s\\n\", fnm);",
- " }",
- " close(fd);",
- "}",
- "",
- "void",
- "set_root(void)",
- "{ int fd;",
- " char *q;",
- " char MyFile[512];", /* enough to hold a reasonable pathname */
- " char MySuffix[16];",
- " char *ssuffix = \"rst\";",
- " int try_core = 1;",
- "",
- " strcpy(MyFile, TrailFile);",
- "try_again:",
- " if (whichtrail > 0)",
- " { sprintf(fnm, \"%%s%%d.%%s\", MyFile, whichtrail, ssuffix);",
- " fd = open(fnm, O_RDONLY, 0);",
- " if (fd < 0 && (q = strchr(MyFile, \'.\')))",
- " { *q = \'\\0\'; /* strip .pml */",
- " sprintf(fnm, \"%%s%%d.%%s\", MyFile, whichtrail, ssuffix);",
- " *q = \'.\';",
- " fd = open(fnm, O_RDONLY, 0);",
- " }",
- " } else",
- " { sprintf(fnm, \"%%s.%%s\", MyFile, ssuffix);",
- " fd = open(fnm, O_RDONLY, 0);",
- " if (fd < 0 && (q = strchr(MyFile, \'.\')))",
- " { *q = \'\\0\'; /* strip .pml */",
- " sprintf(fnm, \"%%s.%%s\", MyFile, ssuffix);",
- " *q = \'.\';",
- " fd = open(fnm, O_RDONLY, 0);",
- " } }",
- "",
- " if (fd < 0)",
- " { if (try_core < NCORE)",
- " { ssuffix = MySuffix;",
- " sprintf(ssuffix, \"cpu%%d_rst\", try_core++);",
- " goto try_again;",
- " }",
- " cpu_printf(\"no file '%%s.rst' or '%%s' (not an error)\\n\", MyFile, fnm);",
- " } else",
- " { if (read(fd, &cur_Root, sizeof(SM_frame)) != sizeof(SM_frame))",
- " { cpu_printf(\"read error %%s\\n\", fnm);",
- " close(fd);",
- " pan_exit(1);",
- " }",
- " close(fd);",
- " (void) unpack_state(&cur_Root, -2);",
- "#ifdef SEP_STATE",
- " cpu_printf(\"partial trail -- last few steps only\\n\");",
- "#endif",
- " cpu_printf(\"restored root from '%%s'\\n\", fnm);",
- " printf(\"=====State:=====\\n\");",
- " { int i, j; P0 *z;",
- " for (i = 0; i < now._nr_pr; i++)",
- " { z = (P0 *)pptr(i);",
- " printf(\"proc %%2d (%%s) \", i, procname[z->_t]);",
-
- " for (j = 0; src_all[j].src; j++)",
- " if (src_all[j].tp == (int) z->_t)",
- " { printf(\" line %%3d \\\"%%s\\\" \",",
- " src_all[j].src[z->_p], PanSource);",
- " break;",
- " }",
- " printf(\"(state %%d)\\n\", z->_p);",
- " c_locals(i, z->_t);",
- " }",
- " c_globals();",
- " }",
- " printf(\"================\\n\");",
- " }",
- "}",
- "",
- "#ifdef USE_DISK",
- "unsigned long dsk_written, dsk_drained;",
- "void mem_drain(void);",
- "#endif",
- "",
- "void",
- "m_clear_frame(SM_frame *f)", /* clear room for stats */
- "{ int i, clr_sz = sizeof(SM_results);",
- "",
- " for (i = 0; i <= _NP_; i++) /* all proctypes */",
- " { clr_sz += NrStates[i]*sizeof(uchar);",
- " }",
- " memset(f, 0, clr_sz);",
- " /* caution if sizeof(SM_results) > sizeof(SM_frame) */",
- "}",
- "",
- "#define TargetQ_Full(n) (m_workq[n][prfree[n]].m_vsize != 0)", /* no free slot */
- "#define TargetQ_NotFull(n) (m_workq[n][prfree[n]].m_vsize == 0)", /* avoiding prcnt */
- "",
- "int",
- "AllQueuesEmpty(void)",
- "{ int q;",
- "#ifndef NGQ",
- " if (*grcnt != 0)",
- " { return 0;",
- " }",
- "#endif",
- " for (q = 0; q < NCORE; q++)",
- " { if (prcnt[q] != 0)", /* not locked, ok if race */
- " { return 0;",
- " } }",
- " return 1;",
- "}",
- "",
- "void",
- "Read_Queue(int q)",
- "{ SM_frame *f, *of;",
- " int remember, target_q;",
- " SM_results *r;",
- " double patience = 0.0;",
- "",
- " target_q = (q + 1) %% NCORE;",
- "",
- " for (;;)",
- " { f = Get_Full_Frame(q);",
- " if (!f) /* 1 second timeout -- and trigger for Query */",
- " { if (someone_crashed(2))",
- " { printf(\"cpu%%d: search terminated [code %%d]\\n\",",
- " core_id, search_terminated?*search_terminated:-1);",
- " sudden_stop(\"\");",
- " pan_exit(1);",
- " }",
- "#ifdef TESTING",
- " /* to profile with cc -pg and gprof pan.exe -- set handoff depth beyond maxdepth */",
- " exit(0);",
- "#endif",
- " remember = *grfree;",
- " if (core_id == 0 /* root can initiate termination */",
- " && remote_party == 0 /* and only the original root */",
- " && query_in_progress == 0 /* unless its already in progress */",
- " && AllQueuesEmpty())",
- " { f = Get_Free_Frame(target_q);",
- " query_in_progress = 1; /* only root process can do this */",
- " if (!f) { Uerror(\"Fatal1: no free slot\"); }",
- " f->m_boq = QUERY; /* initiate Query */",
- " if (verbose)",
- " { cpu_printf(\"snd QUERY to q%%d (%%d) into slot %%d\\n\",",
- " target_q, nstates_get + 1, prfree[target_q]-1);",
- " }",
- " f->m_vsize = remember + 1;",
- " /* number will not change unless we receive more states */",
- " } else if (patience++ > OneHour) /* one hour watchdog timer */",
- " { cpu_printf(\"timeout -- giving up\\n\");",
- " sudden_stop(\"queue timeout\");",
- " pan_exit(1);",
- " }",
- " if (0) cpu_printf(\"timed out -- try again\\n\");",
- " continue; ",
- " }",
- " patience = 0.0; /* reset watchdog */",
- "",
- " if (f->m_boq == QUERY)",
- " { if (verbose)",
- " { cpu_printf(\"got QUERY on q%%d (%%d <> %%d) from slot %%d\\n\",",
- " q, f->m_vsize, nstates_put + 1, prfull[q]-1);",
- " snapshot();",
- " }",
- " remember = f->m_vsize;",
- " f->m_vsize = 0; /* release slot */",
- "",
- " if (core_id == 0 && remote_party == 0) /* original root cpu0 */",
- " { if (query_in_progress == 1 /* didn't send more states in the interim */",
- " && *grfree + 1 == remember) /* no action on global queue meanwhile */",
- " { if (verbose) cpu_printf(\"Termination detected\\n\");",
- " if (TargetQ_Full(target_q))",
- " { if (verbose)",
- " cpu_printf(\"warning: target q is full\\n\");",
- " }",
- " f = Get_Free_Frame(target_q);",
- " if (!f) { Uerror(\"Fatal2: no free slot\"); }",
- " m_clear_frame(f);",
- " f->m_boq = QUIT; /* send final Quit, collect stats */",
- " f->m_vsize = 111; /* anything non-zero will do */",
- " if (verbose)",
- " cpu_printf(\"put QUIT on q%%d\\n\", target_q);",
- " } else",
- " { if (verbose) cpu_printf(\"Stale Query\\n\");",
- "#ifdef USE_DISK",
- " mem_drain();",
- "#endif",
- " }",
- " query_in_progress = 0;",
- " } else",
- " { if (TargetQ_Full(target_q))",
- " { if (verbose)",
- " cpu_printf(\"warning: forward query - target q full\\n\");",
- " }",
- " f = Get_Free_Frame(target_q);",
- " if (verbose)",
- " cpu_printf(\"snd QUERY response to q%%d (%%d <> %%d) in slot %%d\\n\",",
- " target_q, remember, *grfree + 1, prfree[target_q]-1);",
- " if (!f) { Uerror(\"Fatal4: no free slot\"); }",
- "",
- " if (*grfree + 1 == remember) /* no action on global queue */",
- " { f->m_boq = QUERY; /* forward query, to root */",
- " f->m_vsize = remember;",
- " } else",
- " { f->m_boq = QUERY_F; /* no match -- busy */",
- " f->m_vsize = 112; /* anything non-zero */",
- "#ifdef USE_DISK",
- " if (dsk_written != dsk_drained)",
- " { mem_drain();",
- " }",
- "#endif",
- " } }",
- " continue;",
- " }",
- "",
- " if (f->m_boq == QUERY_F)",
- " { if (verbose)",
- " { cpu_printf(\"got QUERY_F on q%%d from slot %%d\\n\", q, prfull[q]-1);",
- " }",
- " f->m_vsize = 0; /* release slot */",
- "",
- " if (core_id == 0 && remote_party == 0) /* original root cpu0 */",
- " { if (verbose) cpu_printf(\"No Match on Query\\n\");",
- " query_in_progress = 0;",
- " } else",
- " { if (TargetQ_Full(target_q))",
- " { if (verbose) cpu_printf(\"warning: forwarding query_f, target queue full\\n\");",
- " }",
- " f = Get_Free_Frame(target_q);",
- " if (verbose) cpu_printf(\"forward QUERY_F to q%%d into slot %%d\\n\",",
- " target_q, prfree[target_q]-1);",
- " if (!f) { Uerror(\"Fatal5: no free slot\"); }",
- " f->m_boq = QUERY_F; /* cannot terminate yet */",
- " f->m_vsize = 113; /* anything non-zero */",
- " }",
- "#ifdef USE_DISK",
- " if (dsk_written != dsk_drained)",
- " { mem_drain();",
- " }",
- "#endif",
- " continue;",
- " }",
- "",
- " if (f->m_boq == QUIT)",
- " { if (0) cpu_printf(\"done -- local memcnt %%g Mb\\n\", memcnt/(1048576.));",
- " retrieve_info((SM_results *) f); /* collect and combine stats */",
- " if (verbose)",
- " { cpu_printf(\"received Quit\\n\");",
- " snapshot();",
- " }",
- " f->m_vsize = 0; /* release incoming slot */",
- " if (core_id != 0)",
- " { f = Get_Free_Frame(target_q); /* new outgoing slot */",
- " if (!f) { Uerror(\"Fatal6: no free slot\"); }",
- " m_clear_frame(f); /* start with zeroed stats */",
- " record_info((SM_results *) f);",
- " f->m_boq = QUIT; /* forward combined results */",
- " f->m_vsize = 114; /* anything non-zero */",
- " if (verbose>1)",
- " cpu_printf(\"fwd Results to q%%d\\n\", target_q);",
- " }",
- " break; /* successful termination */",
- " }",
- "",
- " /* else: 0<= boq <= 255, means STATE transfer */",
- " if (unpack_state(f, q) != 0)",
- " { nstates_get++;",
- " f->m_vsize = 0; /* release slot */",
- " if (VVERBOSE) cpu_printf(\"Got state\\n\");",
- "",
- " if (search_terminated != NULL",
- " && *search_terminated == 0)",
- " { new_state(); /* explore successors */",
- " memset((uchar *) &cur_Root, 0, sizeof(SM_frame)); /* avoid confusion */",
- " } else",
- " { pan_exit(0);",
- " }",
- " } else",
- " { pan_exit(0);",
- " } }",
- " if (verbose) cpu_printf(\"done got %%d put %%d\\n\", nstates_get, nstates_put);",
- " sleep_report();",
- "}",
- "",
- "void",
- "give_up(int unused_x)",
- "{",
- " if (search_terminated != NULL)",
- " { *search_terminated |= 32; /* give_up */",
- " }",
- " if (!writing_trail)",
- " { was_interrupted = 1;",
- " snapshot();",
- " cpu_printf(\"Give Up\\n\");",
- " sleep_report();",
- " pan_exit(1);",
- " } else /* we are already terminating */",
- " { cpu_printf(\"SIGINT\\n\");",
- " }",
- "}",
- "",
- "void",
- "check_overkill(void)",
- "{",
- " vmax_seen = (vmax_seen + 7)/ 8;",
- " vmax_seen *= 8; /* round up to a multiple of 8 */",
- "",
- " if (core_id == 0",
- " && !remote_party",
- " && nstates_put > 0",
- " && VMAX - vmax_seen > 8)",
- " {",
- "#ifdef BITSTATE",
- " printf(\"cpu0: max VMAX value seen in this run: \");",
- "#else",
- " printf(\"cpu0: recommend recompiling with \");",
- "#endif",
- " printf(\"-DVMAX=%%d\\n\", vmax_seen);",
- " }",
- "}",
- "",
- "void",
- "mem_put(int q) /* handoff state to other cpu, workq q */",
- "{ SM_frame *f;",
- " int i, j;",
- "",
- " if (vsize > VMAX)",
- " { vsize = (vsize + 7)/8; vsize *= 8; /* round up */",
- " printf(\"pan: recompile with -DVMAX=N with N >= %%d\\n\", vsize);",
- " Uerror(\"aborting\");",
- " }",
- " if (now._nr_pr > PMAX)",
- " { printf(\"pan: recompile with -DPMAX=N with N >= %%d\\n\", now._nr_pr);",
- " Uerror(\"aborting\");",
- " }",
- " if (now._nr_qs > QMAX)",
- " { printf(\"pan: recompile with -DQMAX=N with N >= %%d\\n\", now._nr_qs);",
- " Uerror(\"aborting\");",
- " }",
- " if (vsize > vmax_seen) vmax_seen = vsize;",
- " if (now._nr_pr > pmax_seen) pmax_seen = now._nr_pr;",
- " if (now._nr_qs > qmax_seen) qmax_seen = now._nr_qs;",
- "",
- " f = Get_Free_Frame(q); /* not called in likely deadlock states */",
- " if (!f) { Uerror(\"Fatal3: no free slot\"); }",
- "",
- " if (VVERBOSE) cpu_printf(\"putting state into q%%d\\n\", q);",
- "",
- " memcpy((uchar *) f->m_now, (uchar *) &now, vsize);",
- " memset((uchar *) f->m_Mask, 0, (VMAX+7)/8 * sizeof(char));",
- " for (i = j = 0; i < VMAX; i++, j = (j+1)%%8)",
- " { if (Mask[i])",
- " { f->m_Mask[i/8] |= (1<<j);",
- " } }",
- "",
- " if (now._nr_pr > 0)",
- " { memcpy((uchar *) f->m_p_offset, (uchar *) proc_offset, now._nr_pr * sizeof(OFFT));",
- " memcpy((uchar *) f->m_p_skip, (uchar *) proc_skip, now._nr_pr * sizeof(uchar));",
- " }",
- " if (now._nr_qs > 0)",
- " { memcpy((uchar *) f->m_q_offset, (uchar *) q_offset, now._nr_qs * sizeof(OFFT));",
- " memcpy((uchar *) f->m_q_skip, (uchar *) q_skip, now._nr_qs * sizeof(uchar));",
- " }",
- "#if defined(C_States) && (HAS_TRACK==1) && (HAS_STACK==1)",
- " c_stack((uchar *) f->m_c_stack); /* save unmatched tracked data */",
- "#endif",
- "#ifdef FULL_TRAIL",
- " f->m_stack = stack_last[core_id];",
- "#endif",
- " f->nr_handoffs = nr_handoffs+1;",
- " f->m_tau = trpt->tau;",
- " f->m_o_pm = trpt->o_pm;",
- " f->m_boq = boq;",
- " f->m_vsize = vsize; /* must come last - now the other cpu can see it */",
- "",
- " if (query_in_progress == 1)",
- " query_in_progress = 2; /* make sure we know, if a query makes the rounds */",
- " nstates_put++;",
- "}",
- "",
- "#ifdef USE_DISK",
- "int Dsk_W_Nr, Dsk_R_Nr;",
- "int dsk_file = -1, dsk_read = -1;",
- "unsigned long dsk_written, dsk_drained;",
- "char dsk_name[512];",
- "",
- "#ifndef BFS_DISK",
- "#if defined(WIN32) || defined(WIN64)",
- " #define RFLAGS (O_RDONLY|O_BINARY)",
- " #define WFLAGS (O_CREAT|O_WRONLY|O_TRUNC|O_BINARY)",
- "#else",
- " #define RFLAGS (O_RDONLY)",
- " #define WFLAGS (O_CREAT|O_WRONLY|O_TRUNC)",
- "#endif",
- "#endif",
- "",
- "void",
- "dsk_stats(void)",
- "{ int i;",
- "",
- " if (dsk_written > 0)",
- " { cpu_printf(\"dsk_written %%d states in %%d files\\ncpu%%d: dsk_drained %%6d states\\n\",",
- " dsk_written, Dsk_W_Nr, core_id, dsk_drained);",
- " close(dsk_read);",
- " close(dsk_file);",
- " for (i = 0; i < Dsk_W_Nr; i++)",
- " { sprintf(dsk_name, \"Q%%.3d_%%.3d.tmp\", i, core_id);",
- " unlink(dsk_name);",
- " } }",
- "}",
- "",
- "void",
- "mem_drain(void)",
- "{ SM_frame *f, g;",
- " int q = (core_id + 1) %% NCORE; /* target q */",
- " int sz;",
- "",
- " if (dsk_read < 0",
- " || dsk_written <= dsk_drained)",
- " { return;",
- " }",
- "",
- " while (dsk_written > dsk_drained",
- " && TargetQ_NotFull(q))",
- " { f = Get_Free_Frame(q);",
- " if (!f) { Uerror(\"Fatal: unhandled condition\"); }",
- "",
- " if ((dsk_drained+1)%%MAX_DSK_FILE == 0) /* 100K states max per file */",
- " { (void) close(dsk_read); /* close current read handle */",
- " sprintf(dsk_name, \"Q%%.3d_%%.3d.tmp\", Dsk_R_Nr++, core_id);",
- " (void) unlink(dsk_name); /* remove current file */",
- " sprintf(dsk_name, \"Q%%.3d_%%.3d.tmp\", Dsk_R_Nr, core_id);",
- " cpu_printf(\"reading %%s\\n\", dsk_name);",
- " dsk_read = open(dsk_name, RFLAGS); /* open next file */",
- " if (dsk_read < 0)",
- " { Uerror(\"could not open dsk file\");",
- " } }",
- " if (read(dsk_read, &g, sizeof(SM_frame)) != sizeof(SM_frame))",
- " { Uerror(\"bad dsk file read\");",
- " }",
- " sz = g.m_vsize;",
- " g.m_vsize = 0;",
- " memcpy(f, &g, sizeof(SM_frame));",
- " f->m_vsize = sz; /* last */",
- "",
- " dsk_drained++;",
- " }",
- "}",
- "",
- "void",
- "mem_file(void)",
- "{ SM_frame f;",
- " int i, j, q = (core_id + 1) %% NCORE; /* target q */",
- "",
- " if (vsize > VMAX)",
- " { printf(\"pan: recompile with -DVMAX=N with N >= %%d\\n\", vsize);",
- " Uerror(\"aborting\");",
- " }",
- " if (now._nr_pr > PMAX)",
- " { printf(\"pan: recompile with -DPMAX=N with N >= %%d\\n\", now._nr_pr);",
- " Uerror(\"aborting\");",
- " }",
- " if (now._nr_qs > QMAX)",
- " { printf(\"pan: recompile with -DQMAX=N with N >= %%d\\n\", now._nr_qs);",
- " Uerror(\"aborting\");",
- " }",
- "",
- " if (VVERBOSE) cpu_printf(\"filing state for q%%d\\n\", q);",
- "",
- " memcpy((uchar *) f.m_now, (uchar *) &now, vsize);",
- " memset((uchar *) f.m_Mask, 0, (VMAX+7)/8 * sizeof(char));",
- " for (i = j = 0; i < VMAX; i++, j = (j+1)%%8)",
- " { if (Mask[i])",
- " { f.m_Mask[i/8] |= (1<<j);",
- " } }",
- "",
- " if (now._nr_pr > 0)",
- " { memcpy((uchar *)f.m_p_offset, (uchar *)proc_offset, now._nr_pr*sizeof(OFFT));",
- " memcpy((uchar *)f.m_p_skip, (uchar *)proc_skip, now._nr_pr*sizeof(uchar));",
- " }",
- " if (now._nr_qs > 0)",
- " { memcpy((uchar *) f.m_q_offset, (uchar *) q_offset, now._nr_qs*sizeof(OFFT));",
- " memcpy((uchar *) f.m_q_skip, (uchar *) q_skip, now._nr_qs*sizeof(uchar));",
- " }",
- "#if defined(C_States) && (HAS_TRACK==1) && (HAS_STACK==1)",
- " c_stack((uchar *) f.m_c_stack); /* save unmatched tracked data */",
- "#endif",
- "#ifdef FULL_TRAIL",
- " f.m_stack = stack_last[core_id];",
- "#endif",
- " f.nr_handoffs = nr_handoffs+1;",
- " f.m_tau = trpt->tau;",
- " f.m_o_pm = trpt->o_pm;",
- " f.m_boq = boq;",
- " f.m_vsize = vsize;",
- "",
- " if (query_in_progress == 1)",
- " { query_in_progress = 2;",
- " }",
- " if (dsk_file < 0)",
- " { sprintf(dsk_name, \"Q%%.3d_%%.3d.tmp\", Dsk_W_Nr, core_id);",
- " dsk_file = open(dsk_name, WFLAGS, 0644);",
- " dsk_read = open(dsk_name, RFLAGS);",
- " if (dsk_file < 0 || dsk_read < 0)",
- " { cpu_printf(\"File: <%%s>\\n\", dsk_name);",
- " Uerror(\"cannot open diskfile\");",
- " }",
- " Dsk_W_Nr++; /* nr of next file to open */",
- " cpu_printf(\"created temporary diskfile %%s\\n\", dsk_name);",
- " } else if ((dsk_written+1)%%MAX_DSK_FILE == 0)",
- " { close(dsk_file); /* close write handle */",
- " sprintf(dsk_name, \"Q%%.3d_%%.3d.tmp\", Dsk_W_Nr++, core_id);",
- " dsk_file = open(dsk_name, WFLAGS, 0644);",
- " if (dsk_file < 0)",
- " { cpu_printf(\"File: <%%s>\\n\", dsk_name);",
- " Uerror(\"aborting: cannot open new diskfile\");",
- " }",
- " cpu_printf(\"created temporary diskfile %%s\\n\", dsk_name);",
- " }",
- " if (write(dsk_file, &f, sizeof(SM_frame)) != sizeof(SM_frame))",
- " { Uerror(\"aborting -- disk write failed (disk full?)\");",
- " }",
- " nstates_put++;",
- " dsk_written++;",
- "}",
- "#endif",
- "",
- "int",
- "mem_hand_off(void)",
- "{",
- " if (search_terminated == NULL",
- " || *search_terminated != 0) /* not a full crash check */",
- " { pan_exit(0);",
- " }",
- " iam_alive(); /* on every transition of Down */",
- "#ifdef USE_DISK",
- " mem_drain(); /* maybe call this also on every Up */",
- "#endif",
- " if (depth > z_handoff /* above handoff limit */",
- "#ifndef SAFETY",
- " && !a_cycles /* not in liveness mode */",
- "#endif",
- "#if SYNC",
- " && boq == -1 /* not mid-rv */",
- "#endif",
- "#ifdef VERI",
- " && (trpt->tau&4) /* claim moves first */",
- " && !((trpt-1)->tau&128) /* not a stutter move */",
- "#endif",
- " && !(trpt->tau&8)) /* not an atomic move */",
- " { int q = (core_id + 1) %% NCORE; /* circular handoff */",
- " #ifdef GENEROUS",
- " if (prcnt[q] < LN_FRAMES)", /* not the best strategy */
- " #else",
- " if (TargetQ_NotFull(q)",
- " && (dfs_phase2 == 0 || prcnt[core_id] > 0))", /* not locked, ok if race */
- " #endif",
- " { mem_put(q);", /* only 1 writer: lock-free */
- " return 1;",
- " }",
- " { int rval;",
- " #ifndef NGQ",
- " rval = GlobalQ_HasRoom();",
- " #else",
- " rval = 0;",
- " #endif",
- " #ifdef USE_DISK",
- " if (rval == 0)",
- " { void mem_file(void);",
- " mem_file();",
- " rval = 1;",
- " }",
- " #endif",
- " return rval;",
- " }",
- " }",
- " return 0; /* i.e., no handoff */",
- "}",
- "",
- "void",
- "mem_put_acc(void) /* liveness mode */",
- "{ int q = (core_id + 1) %% NCORE;",
- "",
- " if (search_terminated == NULL",
- " || *search_terminated != 0)",
- " { pan_exit(0);",
- " }",
- "#ifdef USE_DISK",
- " mem_drain();",
- "#endif",
- " /* some tortured use of preprocessing: */",
- "#if !defined(NGQ) || defined(USE_DISK)",
- " if (TargetQ_Full(q))",
- " {",
- "#endif",
- "#ifndef NGQ",
- " if (GlobalQ_HasRoom())",
- " { return;",
- " }",
- "#endif",
- "#ifdef USE_DISK",
- " mem_file();",
- " } else",
- "#else",
- " #if !defined(NGQ) || defined(USE_DISK)",
- " }",
- " #endif",
- "#endif",
- " { mem_put(q);",
- " }",
- "}",
- "",
- "#if defined(WIN32) || defined(WIN64)", /* visual studio */
- "void",
- "init_shm(void) /* initialize shared work-queues */",
- "{ char key[512];",
- " int n, m;",
- " int must_exit = 0;",
- "",
- " if (core_id == 0 && verbose)",
- " { printf(\"cpu0: step 3: allocate shared work-queues %%g Mb\\n\",",
- " ((double) NCORE * LWQ_SIZE + GWQ_SIZE) / (1048576.));",
- " }",
- " for (m = 0; m < NR_QS; m++) /* last q is global 1 */",
- " { double qsize = (m == NCORE) ? GWQ_SIZE : LWQ_SIZE;",
- " sprintf(key, \"Global\\\\pan_%%s_%%.3d\", PanSource, m);",
- " if (core_id == 0)", /* root process creates shared memory segments */
- " { shmid[m] = CreateFileMapping(",
- " INVALID_HANDLE_VALUE, /* use paging file */",
- " NULL, /* default security */",
- " PAGE_READWRITE, /* access permissions */",
- " 0, /* high-order 4 bytes */",
- " qsize, /* low-order bytes, size in bytes */",
- " key); /* name */",
- " } else /* worker nodes just open these segments */",
- " { shmid[m] = OpenFileMapping(",
- " FILE_MAP_ALL_ACCESS, /* read/write access */",
- " FALSE, /* children do not inherit handle */",
- " key);",
- " }",
- " if (shmid[m] == NULL)",
- " { fprintf(stderr, \"cpu%%d: could not create or open shared queues\\n\",",
- " core_id);",
- " must_exit = 1;",
- " break;",
- " }",
- " /* attach: */",
- " shared_mem[m] = (char *) MapViewOfFile(shmid[m], FILE_MAP_ALL_ACCESS, 0, 0, 0);",
- " if (shared_mem[m] == NULL)",
- " { fprintf(stderr, \"cpu%%d: cannot attach shared q%%d (%%d Mb)\\n\",",
- " core_id, m+1, (int) (qsize/(1048576.)));",
- " must_exit = 1;",
- " break;",
- " }",
- "",
- " memcnt += qsize;",
- "",
- " m_workq[m] = (SM_frame *) shared_mem[m];",
- " if (core_id == 0)",
- " { int nframes = (m == NCORE) ? GN_FRAMES : LN_FRAMES;",
- " for (n = 0; n < nframes; n++)",
- " { m_workq[m][n].m_vsize = 0;",
- " m_workq[m][n].m_boq = 0;",
- " } } }",
- "",
- " if (must_exit)",
- " { fprintf(stderr, \"pan: check './pan --' for usage details\\n\");",
- " pan_exit(1); /* calls cleanup_shm */",
- " }",
- "}",
- "",
- "static uchar *",
- "prep_shmid_S(size_t n) /* either sets SS or H_tab, WIN32/WIN64 */",
- "{ char *rval;",
- "#ifndef SEP_STATE",
- " char key[512];",
- "",
- " if (verbose && core_id == 0)",
- " {",
- " #ifdef BITSTATE",
- " printf(\"cpu0: step 1: allocate shared bitstate %%g Mb\\n\",",
- " (double) n / (1048576.));",
- " #else",
- " printf(\"cpu0: step 1: allocate shared hastable %%g Mb\\n\",",
- " (double) n / (1048576.));",
- " #endif",
- " }",
- " #ifdef MEMLIM",
- " if (memcnt + (double) n > memlim)",
- " { printf(\"cpu%%d: S %%8g + %%d Kb exceeds memory limit of %%8g Mb\\n\",",
- " core_id, memcnt/1024., n/1024, memlim/(1048576.));",
- " printf(\"cpu%%d: insufficient memory -- aborting\\n\", core_id);",
- " exit(1);",
- " }",
- " #endif",
- "",
- " /* make key different from queues: */",
- " sprintf(key, \"Global\\\\pan_%%s_%%.3d\", PanSource, NCORE+2); /* different from qs */",
- "",
- " if (core_id == 0) /* root */",
- " { shmid_S = CreateFileMapping(INVALID_HANDLE_VALUE, NULL,",
- "#ifdef WIN64",
- " PAGE_READWRITE, (n>>32), (n & 0xffffffff), key);",
- "#else",
- " PAGE_READWRITE, 0, n, key);",
- "#endif",
- " memcnt += (double) n;",
- " } else /* worker */",
- " { shmid_S = OpenFileMapping(FILE_MAP_ALL_ACCESS, FALSE, key);",
- " }",
-
- " if (shmid_S == NULL)",
- " {",
- " #ifdef BITSTATE",
- " fprintf(stderr, \"cpu%%d: cannot %%s shared bitstate\",",
- " core_id, core_id?\"open\":\"create\");",
- " #else",
- " fprintf(stderr, \"cpu%%d: cannot %%s shared hashtable\",",
- " core_id, core_id?\"open\":\"create\");",
- " #endif",
- " fprintf(stderr, \"pan: check './pan --' for usage details\\n\");",
- " pan_exit(1);",
- " }",
- "",
- " rval = (char *) MapViewOfFile(shmid_S, FILE_MAP_ALL_ACCESS, 0, 0, 0); /* attach */",
- " if ((char *) rval == NULL)",
- " { fprintf(stderr, \"cpu%%d: cannot attach shared bitstate or hashtable\\n\", core_id);",
- " fprintf(stderr, \"pan: check './pan --' for usage details\\n\");",
- " pan_exit(1);",
- " }",
- "#else",
- " rval = (char *) emalloc(n);",
- "#endif",
- " return (uchar *) rval;",
- "}",
- "",
- "static uchar *",
- "prep_state_mem(size_t n) /* WIN32/WIN64 sets memory arena for states */",
- "{ char *rval;",
- " char key[512];",
- " static int cnt = 3; /* start larger than earlier ftok calls */",
- "",
- " if (verbose && core_id == 0)",
- " { printf(\"cpu0: step 2+: pre-allocate memory arena %%d of %%g Mb\\n\",",
- " cnt-3, (double) n / (1048576.));",
- " }",
- " #ifdef MEMLIM",
- " if (memcnt + (double) n > memlim)",
- " { printf(\"cpu%%d: error: M %%.0f + %%.0f exceeds memory limit of %%.0f Kb\\n\",",
- " core_id, memcnt/1024.0, (double) n/1024.0, memlim/1024.0);",
- " return NULL;",
- " }",
- " #endif",
- "",
- " sprintf(key, \"Global\\\\pan_%%s_%%.3d\", PanSource, NCORE+cnt); cnt++;",
- "",
- " if (core_id == 0)",
- " { shmid_M = CreateFileMapping(INVALID_HANDLE_VALUE, NULL,",
- "#ifdef WIN64",
- " PAGE_READWRITE, (n>>32), (n & 0xffffffff), key);",
- "#else",
- " PAGE_READWRITE, 0, n, key);",
- "#endif",
- " } else",
- " { shmid_M = OpenFileMapping(FILE_MAP_ALL_ACCESS, FALSE, key);",
- " }",
- " if (shmid_M == NULL)",
- " { printf(\"cpu%%d: failed to get pool of shared memory nr %%d of size %%d\\n\",",
- " core_id, cnt-3, n);",
- " printf(\"pan: check './pan --' for usage details\\n\");",
- " return NULL;",
- " }",
- " rval = (char *) MapViewOfFile(shmid_M, FILE_MAP_ALL_ACCESS, 0, 0, 0); /* attach */",
- "",
- " if (rval == NULL)",
- " { printf(\"cpu%%d: failed to attach pool of shared memory nr %%d of size %%d\\n\",",
- " core_id, cnt-3, n);",
- " return NULL;",
- " }",
- " return (uchar *) rval;",
- "}",
- "",
- "void",
- "init_HT(unsigned long n) /* WIN32/WIN64 version */",
- "{ volatile char *x;",
- " double get_mem;",
- "#ifndef SEP_STATE",
- " char *dc_mem_start;",
- "#endif",
- " if (verbose) printf(\"cpu%%d: initialization for Windows\\n\", core_id);",
- "",
-"#ifdef SEP_STATE",
- " #ifndef MEMLIM",
- " if (verbose)",
- " { printf(\"cpu0: steps 0,1: no -DMEMLIM set\\n\");",
- " }",
- " #else",
- " if (verbose)",
- " printf(\"cpu0: steps 0,1: -DMEMLIM=%%d Mb - (hashtable %%g Mb + workqueues %%g Mb)\\n\",",
- " MEMLIM, ((double)n/(1048576.)), ((double) NCORE * LWQ_SIZE + GWQ_SIZE)/(1048576.));",
- "#endif",
- " get_mem = NCORE * sizeof(double) + (1 + CS_NR) * sizeof(void *)+ 4*sizeof(void *) + 2*sizeof(double);",
- " /* NCORE * is_alive + search_terminated + CS_NR * sh_lock + 6 gr vars */",
- " get_mem += 4 * NCORE * sizeof(void *);", /* prfree, prfull, prcnt, prmax */
- " #ifdef FULL_TRAIL",
- " get_mem += (NCORE) * sizeof(Stack_Tree *);",
- " /* NCORE * stack_last */",
- " #endif",
- " x = (volatile char *) prep_state_mem((size_t) get_mem);",
- " shmid_X = (void *) x;",
- " if (x == NULL)",
- " { printf(\"cpu0: could not allocate shared memory, see ./pan --\\n\");",
- " exit(1);",
- " }",
- " search_terminated = (volatile unsigned int *) x; /* comes first */",
- " x += sizeof(void *); /* maintain alignment */",
- "",
- " is_alive = (volatile double *) x;",
- " x += NCORE * sizeof(double);",
- "",
- " sh_lock = (volatile int *) x;",
- " x += CS_NR * sizeof(void *); /* allow 1 word per entry */",
- "",
- " grfree = (volatile int *) x;",
- " x += sizeof(void *);",
- " grfull = (volatile int *) x;",
- " x += sizeof(void *);",
- " grcnt = (volatile int *) x;",
- " x += sizeof(void *);",
- " grmax = (volatile int *) x;",
- " x += sizeof(void *);",
- " prfree = (volatile int *) x;",
- " x += NCORE * sizeof(void *);",
- " prfull = (volatile int *) x;",
- " x += NCORE * sizeof(void *);",
- " prcnt = (volatile int *) x;",
- " x += NCORE * sizeof(void *);",
- " prmax = (volatile int *) x;",
- " x += NCORE * sizeof(void *);",
- " gr_readmiss = (volatile double *) x;",
- " x += sizeof(double);",
- " gr_writemiss = (volatile double *) x;",
- " x += sizeof(double);",
- "",
- " #ifdef FULL_TRAIL",
- " stack_last = (volatile Stack_Tree **) x;",
- " x += NCORE * sizeof(Stack_Tree *);",
- " #endif",
- "",
- " #ifndef BITSTATE",
- " H_tab = (struct H_el **) emalloc(n);",
- " #endif",
-"#else",
- " #ifndef MEMLIM",
- " #warning MEMLIM not set", /* cannot happen */
- " #define MEMLIM (2048)",
- " #endif",
- "",
- " if (core_id == 0 && verbose)",
- " printf(\"cpu0: step 0: -DMEMLIM=%%d Mb - (hashtable %%g Mb + workqueues %%g Mb) = %%g Mb for state storage\\n\",",
- " MEMLIM, ((double)n/(1048576.)), ((double) NCORE * LWQ_SIZE + GWQ_SIZE)/(1048576.),",
- " (memlim - memcnt - (double) n - ((double) NCORE * LWQ_SIZE + GWQ_SIZE))/(1048576.));",
- " #ifndef BITSTATE",
- " H_tab = (struct H_el **) prep_shmid_S((size_t) n); /* hash_table */",
- " #endif",
- " get_mem = memlim - memcnt - ((double) NCORE) * LWQ_SIZE - GWQ_SIZE;",
- " if (get_mem <= 0)",
- " { Uerror(\"internal error -- shared state memory\");",
- " }",
- "",
- " if (core_id == 0 && verbose)",
- " { printf(\"cpu0: step 2: shared state memory %%g Mb\\n\",",
- " get_mem/(1048576.));",
- " }",
- " x = dc_mem_start = (char *) prep_state_mem((size_t) get_mem); /* for states */",
- " if (x == NULL)",
- " { printf(\"cpu%%d: insufficient memory -- aborting\\n\", core_id);",
- " exit(1);",
- " }",
- "",
- " search_terminated = (volatile unsigned int *) x; /* comes first */",
- " x += sizeof(void *); /* maintain alignment */",
- "",
- " is_alive = (volatile double *) x;",
- " x += NCORE * sizeof(double);",
- "",
- " sh_lock = (volatile int *) x;",
- " x += CS_NR * sizeof(int);",
- "",
- " grfree = (volatile int *) x;",
- " x += sizeof(void *);",
- " grfull = (volatile int *) x;",
- " x += sizeof(void *);",
- " grcnt = (volatile int *) x;",
- " x += sizeof(void *);",
- " grmax = (volatile int *) x;",
- " x += sizeof(void *);",
- " prfree = (volatile int *) x;",
- " x += NCORE * sizeof(void *);",
- " prfull = (volatile int *) x;",
- " x += NCORE * sizeof(void *);",
- " prcnt = (volatile int *) x;",
- " x += NCORE * sizeof(void *);",
- " prmax = (volatile int *) x;",
- " x += NCORE * sizeof(void *);",
- " gr_readmiss = (volatile double *) x;",
- " x += sizeof(double);",
- " gr_writemiss = (volatile double *) x;",
- " x += sizeof(double);",
- "",
- " #ifdef FULL_TRAIL",
- " stack_last = (volatile Stack_Tree **) x;",
- " x += NCORE * sizeof(Stack_Tree *);",
- " #endif",
- " if (((long)x)&(sizeof(void *)-1)) /* word alignment */",
- " { x += sizeof(void *)-(((long)x)&(sizeof(void *)-1)); /* 64-bit align */",
- " }",
- "",
- " #ifdef COLLAPSE",
- " ncomps = (unsigned long *) x;",
- " x += (256+2) * sizeof(unsigned long);",
- " #endif",
- "",
- " dc_shared = (sh_Allocater *) x; /* in shared memory */",
- " x += sizeof(sh_Allocater);",
- "",
- " if (core_id == 0) /* root only */",
- " { dc_shared->dc_id = shmid_M;",
- " dc_shared->dc_start = (void *) dc_mem_start;",
- " dc_shared->dc_arena = x;",
- " dc_shared->pattern = 1234567;",
- " dc_shared->dc_size = (long) get_mem - (long) (x - dc_mem_start);",
- " dc_shared->nxt = NULL;",
- " }",
-"#endif",
- "}",
- "",
- "#if defined(WIN32) || defined(WIN64) || defined(__i386__) || defined(__x86_64__)",
- "extern BOOLEAN InterlockedBitTestAndSet(LONG volatile* Base, LONG Bit);",
- "int",
- "tas(volatile LONG *s)", /* atomic test and set */
- "{ return InterlockedBitTestAndSet(s, 1);",
- "}",
- "#else",
- " #error missing definition of test and set operation for this platform",
- "#endif",
- "",
- "void",
- "cleanup_shm(int val)",
- "{ int m;",
- " static int nibis = 0;",
- "",
- " if (nibis != 0)",
- " { printf(\"cpu%%d: Redundant call to cleanup_shm(%%d)\\n\", core_id, val);",
- " return;",
- " } else",
- " { nibis = 1;",
- " }",
- " if (search_terminated != NULL)",
- " { *search_terminated |= 16; /* cleanup_shm */",
- " }",
- "",
- " for (m = 0; m < NR_QS; m++)",
- " { if (shmid[m] != NULL)",
- " { UnmapViewOfFile((char *) shared_mem[m]);",
- " CloseHandle(shmid[m]);",
- " } }",
- "#ifdef SEP_STATE",
- " UnmapViewOfFile((void *) shmid_X);",
- " CloseHandle((void *) shmid_M);",
- "#else",
- " #ifdef BITSTATE",
- " if (shmid_S != NULL)",
- " { UnmapViewOfFile(SS);",
- " CloseHandle(shmid_S);",
- " }",
- " #else",
- " if (core_id == 0 && verbose)",
- " { printf(\"cpu0: done, %%ld Mb of shared state memory left\\n\",",
- " dc_shared->dc_size / (long)(1048576));",
- " }",
- " if (shmid_S != NULL)",
- " { UnmapViewOfFile(H_tab);",
- " CloseHandle(shmid_S);",
- " }",
- " shmid_M = (void *) (dc_shared->dc_id);",
- " UnmapViewOfFile((char *) dc_shared->dc_start);",
- " CloseHandle(shmid_M);",
- " #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);",
- " }",
- "}",
- "",
- "void",
- "mem_get(void)",
- "{ SM_frame *f;",
- " int is_parent;",
- "",
- "#if defined(MA) && !defined(SEP_STATE)",
- " #error MA requires SEP_STATE in multi-core mode",
- "#endif",
- "#ifdef BFS",
- " #error BFS is not supported in multi-core mode",
- "#endif",
- "#ifdef SC",
- " #error SC is not supported in multi-core mode",
- "#endif",
- " init_shm(); /* we are single threaded when this starts */",
- " signal(SIGINT, give_up); /* windows control-c interrupt */",
- "",
- " if (core_id == 0 && verbose)",
- " { printf(\"cpu0: step 4: creating additional workers (proxy %%d)\\n\",",
- " proxy_pid);",
- " }",
- "#if 0",
- " 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 others (workers) have is_parent = 0 and core_id = 1..NCORE-1",
- "#endif",
- " if (core_id == 0) /* root starts up the workers */",
- " { worker_pids[0] = (DWORD) getpid(); /* for completeness */",
- " while (++core_id < NCORE) /* first worker sees core_id = 1 */",
- " { char cmdline[64];",
- " STARTUPINFO si = { sizeof(si) };",
- " PROCESS_INFORMATION pi;",
- "",
- " if (proxy_pid == core_id) /* always non-zero */",
- " { sprintf(cmdline, \"pan_proxy.exe -r %%s-Q%%d -Z%%d\",",
- " o_cmdline, getpid(), core_id);",
- " } else",
- " { sprintf(cmdline, \"pan.exe %%s-Q%%d -Z%%d\",",
- " o_cmdline, getpid(), core_id);",
- " }",
- " if (verbose) printf(\"cpu%%d: spawn %%s\\n\", core_id, cmdline);",
- "",
- " is_parent = CreateProcess(0, cmdline, 0, 0, FALSE, 0, 0, 0, &si, &pi);",
- " if (is_parent == 0)",
- " { Uerror(\"fork failed\");",
- " }",
- " worker_pids[core_id] = pi.dwProcessId;",
- " worker_handles[core_id] = pi.hProcess;",
- " if (verbose)",
- " { cpu_printf(\"created core %%d, pid %%d\\n\",",
- " core_id, pi.dwProcessId);",
- " }",
- " if (proxy_pid == core_id) /* we just created the receive half */",
- " { /* add proxy send, store pid in proxy_pid_snd */",
- " sprintf(cmdline, \"pan_proxy.exe -s %%s-Q%%d -Z%%d -Y%%d\",",
- " o_cmdline, getpid(), core_id, worker_pids[proxy_pid]);",
- " if (verbose) printf(\"cpu%%d: spawn %%s\\n\", core_id, cmdline);",
- " is_parent = CreateProcess(0, cmdline, 0,0, FALSE, 0,0,0, &si, &pi);",
- " if (is_parent == 0)",
- " { Uerror(\"fork failed\");",
- " }",
- " proxy_pid_snd = pi.dwProcessId;",
- " proxy_handle_snd = pi.hProcess;",
- " if (verbose)",
- " { cpu_printf(\"created core %%d, pid %%d (send proxy)\\n\",",
- " core_id, pi.dwProcessId);",
- " } } }",
- " 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];",
- " tprefix = db0; sprefix = db1;",
- " sprintf(tprefix, \"cpu%%d_trail\", core_id); /* avoid conflicts on file access */",
- " sprintf(sprefix, \"cpu%%d_rst\", core_id);",
- " memcnt = 0; /* count only additionally allocated memory */",
- " }",
- " if (verbose)",
- " { cpu_printf(\"starting core_id %%d -- pid %%d\\n\", core_id, getpid());",
- " }",
- " if (core_id == 0 && !remote_party)",
- " { new_state(); /* root starts the search */",
- " if (verbose)",
- " cpu_printf(\"done with 1st dfs, nstates %%g (put %%d states), start reading 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\\n\",",
- " nstates_put, nstates_get);",
- " }",
- " done = 1;",
- " wrapup();",
- " exit(0);",
- "}",
- "#endif", /* WIN32 || WIN64 */
- "",
- "#ifdef BITSTATE",
- "void",
- "init_SS(unsigned long n)",
- "{",
- " SS = (uchar *) prep_shmid_S((size_t) n);",
- " init_HT(0L);", /* locks and shared memory for Stack_Tree allocations */
- "}",
- "#endif", /* BITSTATE */
- "",
- "#endif", /* NCORE>1 */
- 0,
-};
projects / lttv.git / blobdiff