Subversion Repositories planix.SVN

Rev

Rev 2 | Blame | Compare with Previous | Last modification | View Log | RSS feed

/***** 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, (long) (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\", (int) (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>%%ld)\\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., (int) (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\",",
        "                               (int) 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 %%ld 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(\" %%s:%%d \",",
        "                                               PanSource, src_all[j].src[z->_p]);",
        "                                       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\", (int) 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,
};