sys/src/cmd/spin/pangen6.h

   1 /***** spin: pangen6.h *****/
   2
   3 /*
   4  * This file is part of the public release of Spin. It is subject to the
   5  * terms in the LICENSE file that is included in this source directory.
   6  * Tool documentation is available at http://spinroot.com
   7  */
   8
   9 static const char *Code2e[] = {
  10         "#if (NCORE>1 || defined(BFS_PAR)) && !defined(WIN32) && !defined(WIN64)",
  11         "       /* Test and Set assembly code */",
  12         "       #if defined(i386) || defined(__i386__) || defined(__x86_64__)",
  13         "               int",
  14         "               tas(volatile int *s)    /* tested */",
  15         "               {       int r;",
  16         "                       __asm__ __volatile__(",
  17         "                               \"xchgl %%0, %%1 \\n\\t\"",
  18         "                               : \"=r\"(r), \"=m\"(*s)",
  19         "                               : \"0\"(1), \"m\"(*s)",
  20         "                               : \"memory\");",
  21         "               ",
  22         "                       return r;",
  23         "               }",
  24         "       #elif defined(__arm__)",
  25         "               int",
  26         "               tas(volatile int *s)    /* not tested */",
  27         "               {       int r = 1;",
  28         "                       __asm__ __volatile__(",
  29         "                               \"swpb %%0, %%0, [%%3] \\n\"",
  30         "                               : \"=r\"(r), \"=m\"(*s)",
  31         "                               : \"0\"(r), \"r\"(s));",
  32         "",
  33         "                       return r;",
  34         "               }",
  35         "       #elif defined(sparc) || defined(__sparc__)",
  36         "               int",
  37         "               tas(volatile int *s)    /* not tested */",
  38         "               {       int r = 1;",
  39         "                       __asm__ __volatile__(",
  40         "                               \" ldstub [%%2], %%0 \\n\"",
  41         "                               : \"=r\"(r), \"=m\"(*s)",
  42         "                               : \"r\"(s));",
  43         "",
  44         "                       return r;",
  45         "               }",
  46         "       #elif defined(ia64) || defined(__ia64__)",
  47         "               /* Intel Itanium */",
  48         "               int",
  49         "               tas(volatile int *s)    /* tested */",
  50         "               {       long int r;",
  51         "                       __asm__ __volatile__(",
  52         "                               \"      xchg4   %%0=%%1,%%2     \\n\"",
  53         "               :               \"=r\"(r), \"+m\"(*s)",
  54         "               :               \"r\"(1)",
  55         "               :               \"memory\");",
  56         "                       return (int) r;",
  57         "               }",
  58         "       #elif defined(__powerpc64__)",
  59         "               int",
  60         "               tas(volatile int *s)    /* courtesy srirajpaul */",
  61         "               {       int r;",
  62         " #if 1",
  63         "                       r = __sync_lock_test_and_set();",
  64         " #else",
  65         "                       /* xlc compiler only */",
  66         "                       r = __fetch_and_or(s, 1);",
  67         "                       __isync();",
  68         " #endif",
  69         "                       return r;",
  70         "               }",
  71         "       #else",
  72         "               #error missing definition of test and set operation for this platform",
  73         "       #endif",
  74         "",
  75         "       #ifndef NO_CAS", /* linux, windows */
  76         "               #define cas(a,b,c) __sync_bool_compare_and_swap(a,b,c)",
  77         "       #else",
  78         "       int", /* workaround if the above is not available */
  79         "       cas(volatile uint32_t *a, uint32_t b, uint32_t c)",
  80         "       {       static volatile int cas_lock;",
  81         "               while (tas(&cas_lock) != 0) { ; }",
  82         "               if (*a == b)",
  83         "               {       *a = c;",
  84         "                       cas_lock = 0;",
  85         "                       return 1;",
  86         "               }",
  87         "               cas_lock = 0;",
  88         "               return 0;",
  89         "       }",
  90         "       #endif",
  91         "#endif",
  92         0,
  93 };
  94
  95 static const char *Code2c[] = { /* multi-core option - Spin 5.0 and later */
  96         "#if NCORE>1",
  97         "#if defined(WIN32) || defined(WIN64)",
  98         "       #ifndef _CONSOLE",
  99         "               #define _CONSOLE",
 100         "       #endif",
 101         "       #ifdef WIN64",
 102         "               #undef long",
 103         "       #endif",
 104         "       #include <windows.h>",
 105         "/*",
 106         "       #ifdef WIN64",
 107         "               #define long    long long",
 108         "       #endif",
 109         "*/",
 110         "#else",
 111         "       #include <sys/ipc.h>",
 112         "       #include <sys/sem.h>",
 113         "       #include <sys/shm.h>",
 114         "#endif",
 115         "",
 116         "/* code common to cygwin/linux and win32/win64: */",
 117         "",
 118         "#ifdef VERBOSE",
 119         "       #define VVERBOSE        (1)",
 120         "#else",
 121         "       #define VVERBOSE        (0)",
 122         "#endif",
 123         "",
 124         "/* the following values must be larger than 256 and must fit in an int */",
 125         "#define QUIT           1024    /* terminate now command */",
 126         "#define QUERY           512    /* termination status query message */",
 127         "#define QUERY_F         513    /* query failed, cannot quit */",
 128         "",
 129         "#define GN_FRAMES      (int) (GWQ_SIZE / (double) sizeof(SM_frame))",
 130         "#define LN_FRAMES      (int) (LWQ_SIZE / (double) sizeof(SM_frame))",
 131         "",
 132         "#ifndef VMAX",
 133         "       #define VMAX    VECTORSZ",
 134         "#endif",
 135         "#ifndef PMAX",
 136         "       #define PMAX    64",
 137         "#endif",
 138         "#ifndef QMAX",
 139         "       #define QMAX    64",
 140         "#endif",
 141         "",
 142         "#if VECTORSZ>32000",
 143         "       #define OFFT    int",
 144         "#else",
 145         "       #define OFFT    short",
 146         "#endif",
 147         "",
 148         "#ifdef SET_SEG_SIZE",
 149         "       /* no longer useful -- being recomputed for local heap size anyway */",
 150         "       double SEG_SIZE = (((double) SET_SEG_SIZE) * 1048576.);",
 151         "#else",
 152         "       double SEG_SIZE = (1048576.*1024.);     /* 1GB default shared memory pool segments */",
 153         "#endif",
 154         "",
 155         "double LWQ_SIZE = 0.; /* initialized in main */",
 156         "",
 157         "#ifdef SET_WQ_SIZE",
 158         "       #ifdef NGQ",
 159         "       #warning SET_WQ_SIZE applies to global queue -- ignored",
 160         "       double GWQ_SIZE = 0.;",
 161         "       #else",
 162         "       double GWQ_SIZE = (((double) SET_WQ_SIZE) * 1048576.);",
 163         "       /* must match the value in pan_proxy.c, if used */",
 164         "       #endif",
 165         "#else",
 166         "       #ifdef NGQ",
 167         "       double GWQ_SIZE = 0.;",
 168         "       #else",
 169         "       double GWQ_SIZE = (128.*1048576.);      /* 128 MB default queue sizes */",
 170         "       #endif",
 171         "#endif",
 172         "",
 173         "/* Crash Detection Parameters */",
 174         "#ifndef ONESECOND",
 175         "       #define ONESECOND       (1<<25)", /* name is somewhat of a misnomer */
 176         "#endif",
 177         "#ifndef SHORT_T",
 178         "       #define SHORT_T (0.1)",
 179         "#endif",
 180         "#ifndef LONG_T",
 181         "       #define LONG_T  (600)",
 182         "#endif",
 183         "",
 184         "double OneSecond   = (double) (ONESECOND); /* waiting for a free slot -- checks crash */",
 185         "double TenSeconds  = 10. * (ONESECOND);    /* waiting for a lock -- check for a crash */",
 186         "",
 187         "/* Termination Detection Params -- waiting for new state input in Get_Full_Frame */",
 188         "double Delay       = ((double) SHORT_T) * (ONESECOND); /* termination detection trigger */",
 189         "double OneHour     = ((double) LONG_T) * (ONESECOND);  /* timeout termination detection */",
 190         "",
 191         "typedef struct SM_frame     SM_frame;",
 192         "typedef struct SM_results   SM_results;",
 193         "typedef struct sh_Allocater sh_Allocater;",
 194         "",
 195         "struct SM_frame {                      /* about 6K per slot */",
 196         "       volatile int    m_vsize;        /* 0 means free slot */",
 197         "       volatile int    m_boq;          /* >500 is a control message */",
 198         "#ifdef FULL_TRAIL",
 199         "       volatile struct Stack_Tree *m_stack;    /* ptr to previous state */",
 200         "#endif",
 201         "       volatile uchar  m_tau;",
 202         "       volatile uchar  m_o_pm;",
 203         "       volatile int    nr_handoffs;    /* to compute real_depth */",
 204         "       volatile char   m_now     [VMAX];",
 205         "#if !defined(NOCOMP) && !defined(HC)",
 206         "       volatile char   m_mask    [(VMAX + 7)/8];",
 207         "#endif",
 208         "       volatile OFFT   m_p_offset[PMAX];",
 209         "       volatile OFFT   m_q_offset[QMAX];",
 210         "       volatile uchar  m_p_skip  [PMAX];",
 211         "       volatile uchar  m_q_skip  [QMAX];",
 212         "#if defined(C_States) && (HAS_TRACK==1) && (HAS_STACK==1)",
 213         "       volatile uchar  m_c_stack [StackSize];",
 214                  /* captures contents of c_stack[] for unmatched objects */
 215         "#endif",
 216         "};",
 217         "",
 218         "int    proxy_pid;              /* id of proxy if nonzero -- receive half */",
 219         "int    store_proxy_pid;",
 220         "short  remote_party;",
 221         "int    proxy_pid_snd;          /* id of proxy if nonzero -- send half */",
 222         "char   o_cmdline[512];         /* to pass options to children */",
 223         "",
 224         "int    iamin[CS_NR+NCORE];             /* non-shared */",
 225         "",
 226 "#if defined(WIN32) || defined(WIN64)",
 227         "int tas(volatile LONG *);",
 228         "",
 229         "HANDLE         proxy_handle_snd;       /* for Windows Create and Terminate */",
 230         "",
 231         "struct sh_Allocater {                  /* shared memory for states */",
 232         "       volatile char   *dc_arena;      /* to allocate states from */",
 233         "       volatile long    pattern;       /* to detect overruns */",
 234         "       volatile long    dc_size;       /* nr of bytes left */",
 235         "       volatile void   *dc_start;      /* where memory segment starts */",
 236         "       volatile void   *dc_id;         /* to attach, detach, remove shared memory segments */",
 237         "       volatile sh_Allocater *nxt;     /* linked list of pools */",
 238         "};",
 239         "DWORD          worker_pids[NCORE];     /* root mem of pids of all workers created */",
 240         "HANDLE         worker_handles[NCORE];  /* for windows Create and Terminate */",
 241         "void *         shmid      [NR_QS];     /* return value from CreateFileMapping */",
 242         "void *         shmid_M;                /* shared mem for state allocation in hashtable */",
 243         "",
 244         "#ifdef SEP_STATE",
 245         "       void *shmid_X;",
 246         "#else",
 247         "       void *shmid_S;                  /* shared bitstate arena or hashtable */",
 248         "#endif",
 249 "#else",
 250         "int tas(volatile int *);",
 251         "",
 252         "struct sh_Allocater {                  /* shared memory for states */",
 253         "       volatile char   *dc_arena;      /* to allocate states from */",
 254         "       volatile long    pattern;       /* to detect overruns */",
 255         "       volatile long    dc_size;       /* nr of bytes left */",
 256         "       volatile char   *dc_start;      /* where memory segment starts */",
 257         "       volatile int    dc_id;          /* to attach, detach, remove shared memory segments */",
 258         "       volatile sh_Allocater *nxt;     /* linked list of pools */",
 259         "};",
 260         "",
 261         "int    worker_pids[NCORE];     /* root mem of pids of all workers created */",
 262         "int    shmid      [NR_QS];     /* return value from shmget */",
 263         "int    nibis = 0;              /* set after shared mem has been released */",
 264         "int    shmid_M;                /* shared mem for state allocation in hashtable */",
 265         "#ifdef SEP_STATE",
 266         "       long    shmid_X;",
 267         "#else",
 268         "       int     shmid_S;        /* shared bitstate arena or hashtable */",
 269         "       volatile sh_Allocater   *first_pool;    /* of shared state memory */",
 270         "       volatile sh_Allocater   *last_pool;",
 271         "#endif", /* SEP_STATE */
 272 "#endif", /* WIN32 || WIN64 */
 273         "",
 274         "struct SM_results {                    /* for shuttling back final stats */",
 275         "       volatile int    m_vsize;        /* avoid conflicts with frames */",
 276         "       volatile int    m_boq;          /* these 2 fields are not written in record_info */",
 277         "       /* probably not all fields really need to be volatile */",
 278         "       volatile double m_memcnt;",
 279         "       volatile double m_nstates;",
 280         "       volatile double m_truncs;",
 281         "       volatile double m_truncs2;",
 282         "       volatile double m_nShadow;",
 283         "       volatile double m_nlinks;",
 284         "       volatile double m_ngrabs;",
 285         "       volatile double m_nlost;",
 286         "       volatile double m_hcmp;",
 287         "       volatile double m_frame_wait;",
 288         "       volatile int    m_hmax;",
 289         "       volatile int    m_svmax;",
 290         "       volatile int    m_smax;",
 291         "       volatile int    m_mreached;",
 292         "       volatile int    m_errors;",
 293         "       volatile int    m_VMAX;",
 294         "       volatile short  m_PMAX;",
 295         "       volatile short  m_QMAX;",
 296         "       volatile uchar  m_R;            /* reached info for all proctypes */",
 297         "};",
 298         "",
 299         "int            core_id = 0;            /* internal process nr, to know which q to use */",
 300         "unsigned long  nstates_put = 0;        /* statistics */",
 301         "unsigned long  nstates_get = 0;",
 302         "int            query_in_progress = 0;  /* termination detection */",
 303         "",
 304         "double         free_wait  = 0.;        /* waiting for a free frame */",
 305         "double         frame_wait = 0.;        /* waiting for a full frame */",
 306         "double         lock_wait  = 0.;        /* waiting for access to cs */",
 307         "double         glock_wait[3];  /* waiting for access to global lock */",
 308         "",
 309         "char           *sprefix = \"rst\";",
 310         "uchar          was_interrupted, issued_kill, writing_trail;",
 311         "",
 312         "static SM_frame cur_Root;              /* current root, to be safe with error trails */",
 313         "",
 314         "SM_frame       *m_workq   [NR_QS];     /* per cpu work queues + global q */",
 315         "char           *shared_mem[NR_QS];     /* return value from shmat */",
 316         "#ifdef SEP_HEAP",
 317         "char           *my_heap;",
 318         "long            my_size;",
 319         "#endif",
 320         "volatile sh_Allocater  *dc_shared;     /* assigned at initialization */",
 321         "",
 322         "static int     vmax_seen, pmax_seen, qmax_seen;",
 323         "static double  gq_tries, gq_hasroom, gq_hasnoroom;",
 324         "",
 325         "volatile int *prfree;",        /* [NCORE] */
 326         "volatile int *prfull;",        /* [NCORE] */
 327         "volatile int *prcnt;",         /* [NCORE] */
 328         "volatile int *prmax;",         /* [NCORE] */
 329         "",
 330         "volatile int   *sh_lock;       /* mutual exclusion locks - in shared memory */",
 331         "volatile double *is_alive;     /* to detect when processes crash */",
 332         "volatile int    *grfree, *grfull, *grcnt, *grmax;      /* access to shared global q */",
 333         "volatile double *gr_readmiss, *gr_writemiss;",
 334         "static   int   lrfree;         /* used for temporary recording of slot */",
 335         "static   int dfs_phase2;",
 336         "",
 337         "void mem_put(int);             /* handoff state to other cpu */",
 338         "void mem_put_acc(void);        /* liveness mode */",
 339         "void mem_get(void);            /* get state from work queue  */",
 340         "void sudden_stop(char *);",
 341         "",
 342         "void",
 343         "record_info(SM_results *r)",
 344         "{      int i;",
 345         "       uchar *ptr;",
 346         "",
 347         "#ifdef SEP_STATE",
 348         "       if (0)",
 349         "       {       cpu_printf(\"nstates %%g nshadow %%g -- memory %%-6.3f Mb\\n\",",
 350         "                       nstates, nShadow, memcnt/(1048576.));",
 351         "       }",
 352         "       r->m_memcnt = 0;",
 353         "#else",
 354         "       #ifdef BITSTATE",
 355                 "       r->m_memcnt = 0; /* it's shared */",
 356         "       #endif",
 357         "       r->m_memcnt = memcnt;",
 358         "#endif",
 359         "       if (a_cycles && core_id == 1)",
 360         "       {       r->m_nstates  = nstates;",
 361         "               r->m_nShadow  = nstates;",
 362         "       } else",
 363         "       {       r->m_nstates  = nstates;",
 364         "               r->m_nShadow  = nShadow;",
 365         "       }",
 366         "       r->m_truncs   = truncs;",
 367         "       r->m_truncs2  = truncs2;",
 368         "       r->m_nlinks   = nlinks;",
 369         "       r->m_ngrabs   = ngrabs;",
 370         "       r->m_nlost    = nlost;",
 371         "       r->m_hcmp     = hcmp;",
 372         "       r->m_frame_wait = frame_wait;",
 373         "       r->m_hmax     = hmax;",
 374         "       r->m_svmax    = svmax;",
 375         "       r->m_smax     = smax;",
 376         "       r->m_mreached = mreached;",
 377         "       r->m_errors   = errors;",
 378         "       r->m_VMAX     = vmax_seen;",
 379         "       r->m_PMAX     = (short) pmax_seen;",
 380         "       r->m_QMAX     = (short) qmax_seen;",
 381         "       ptr = (uchar *) &(r->m_R);",
 382         "       for (i = 0; i <= _NP_; i++)     /* all proctypes */",
 383         "       {       memcpy(ptr, reached[i], NrStates[i]*sizeof(uchar));",
 384         "               ptr += NrStates[i]*sizeof(uchar);",
 385         "       }",
 386         "       if (verbose>1)",
 387         "       {       cpu_printf(\"Put Results nstates %%g (sz %%d)\\n\", nstates, ptr - &(r->m_R));",
 388         "       }",
 389         "}",
 390         "",
 391         "void snapshot(void);",
 392         "",
 393         "void",
 394         "retrieve_info(SM_results *r)",
 395         "{      int i, j;",
 396         "       volatile uchar *ptr;",
 397         "",
 398         "       snapshot();     /* for a final report */",
 399         "",
 400         "       enter_critical(GLOBAL_LOCK);",
 401         "#ifdef SEP_HEAP",
 402         "       if (verbose)",
 403         "       {       printf(\"cpu%%d: local heap-left %%ld KB (%%d MB)\\n\",",
 404         "                       core_id, (long) (my_size/1024), (int) (my_size/1048576));",
 405         "       }",
 406         "#endif",
 407         "       if (verbose && core_id == 0)",
 408         "       {       printf(\"qmax: \");",
 409         "               for (i = 0; i < NCORE; i++)",
 410         "               {       printf(\"%%d \", prmax[i]);",
 411         "               }",
 412         "#ifndef NGQ",
 413         "               printf(\"G: %%d\", *grmax);",
 414         "#endif",
 415         "               printf(\"\\n\");",
 416         "       }",
 417         "       leave_critical(GLOBAL_LOCK);",
 418         "",
 419         "       memcnt  += r->m_memcnt;",
 420         "       nstates += r->m_nstates;",
 421         "       nShadow += r->m_nShadow;",
 422         "       truncs  += r->m_truncs;",
 423         "       truncs2 += r->m_truncs2;",
 424         "       nlinks  += r->m_nlinks;",
 425         "       ngrabs  += r->m_ngrabs;",
 426         "       nlost   += r->m_nlost;",
 427         "       hcmp    += r->m_hcmp;",
 428         "       /* frame_wait += r->m_frame_wait; */",
 429         "       errors  += r->m_errors;",
 430         "",
 431         "       if (hmax  < r->m_hmax)  hmax  = r->m_hmax;",
 432         "       if (svmax < r->m_svmax) svmax = r->m_svmax;",
 433         "       if (smax  < r->m_smax)  smax  = r->m_smax;",
 434         "       if (mreached < r->m_mreached) mreached = r->m_mreached;",
 435         "",
 436         "       if (vmax_seen < r->m_VMAX) vmax_seen = r->m_VMAX;",
 437         "       if (pmax_seen < (int) r->m_PMAX) pmax_seen = (int) r->m_PMAX;",
 438         "       if (qmax_seen < (int) r->m_QMAX) qmax_seen = (int) r->m_QMAX;",
 439         "",
 440         "       ptr = &(r->m_R);",
 441         "       for (i = 0; i <= _NP_; i++)     /* all proctypes */",
 442         "       {       for (j = 0; j < NrStates[i]; j++)",
 443         "               {       if (*(ptr + j) != 0)",
 444         "                       {       reached[i][j] = 1;",
 445         "               }       }",
 446         "               ptr += NrStates[i]*sizeof(uchar);",
 447         "       }",
 448         "       if (verbose>1)",
 449         "       {       cpu_printf(\"Got Results (%%d)\\n\", (int) (ptr - &(r->m_R)));",
 450         "               snapshot();",
 451         "       }",
 452         "}",
 453         "",
 454         "#if !defined(WIN32) && !defined(WIN64)",
 455         "static void",
 456         "rm_shared_segments(void)",
 457         "{      int m;",
 458         "       volatile sh_Allocater *nxt_pool;",
 459         "       /*",
 460         "        * mark all shared memory segments for removal ",
 461         "        * the actual removes wont happen intil last process dies or detaches",
 462         "        * the shmctl calls can return -1 if not all procs have detached yet",
 463         "        */",
 464         "       for (m = 0; m < NR_QS; m++)     /* +1 for global q */",
 465         "       {       if (shmid[m] != -1)",
 466         "               {       (void) shmctl(shmid[m], IPC_RMID, NULL);",
 467         "       }       }",
 468         "#ifdef SEP_STATE",
 469         "       if (shmid_M != -1)",
 470         "       {       (void) shmctl(shmid_M, IPC_RMID, NULL);",
 471         "       }",
 472         "#else",
 473         "       if (shmid_S != -1)",
 474         "       {       (void) shmctl(shmid_S, IPC_RMID, NULL);",
 475         "       }",
 476         "       for (last_pool = first_pool; last_pool != NULL; last_pool = nxt_pool)",
 477         "       {       shmid_M = (int) (last_pool->dc_id);",
 478         "               nxt_pool = last_pool->nxt;      /* as a pre-caution only */",
 479         "               if (shmid_M != -1)",
 480         "               {       (void) shmctl(shmid_M, IPC_RMID, NULL);",
 481         "       }       }",
 482         "#endif",
 483         "}",
 484         "#endif",
 485         "",
 486         "void",
 487         "sudden_stop(char *s)",
 488         "{      char b[64];",
 489         "       int i;",
 490         "",
 491         "       printf(\"cpu%%d: stop - %%s\\n\", core_id, s);",
 492         "#if !defined(WIN32) && !defined(WIN64)",
 493         "       if (proxy_pid != 0)",
 494         "       {       rm_shared_segments();",
 495         "       }",
 496         "#endif",
 497         "       if (search_terminated != NULL)",
 498         "       {       if (*search_terminated != 0)",
 499         "               {       if (verbose)",
 500         "                       {       printf(\"cpu%%d: termination initiated (%%d)\\n\",",
 501         "                                       core_id, (int) *search_terminated);",
 502         "                       }",
 503         "               } else",
 504         "               {       if (verbose)",
 505         "                       {       printf(\"cpu%%d: initiated termination\\n\", core_id);",
 506         "                       }",
 507         "                       *search_terminated |= 8;        /* sudden_stop */",
 508         "               }",
 509         "               if (core_id == 0)",
 510         "               {       if (((*search_terminated) & 4)  /* uerror in one of the cpus */",
 511         "                       && !((*search_terminated) & (8|32|128|256))) /* abnormal stop */",
 512         "                       {       if (errors == 0) errors++; /* we know there is at least 1 */",
 513         "                       }",
 514         "                       wrapup(); /* incomplete stats, but at least something */",
 515         "               }",
 516         "               return;",
 517         "       } /* else: should rarely happen, take more drastic measures */",
 518         "",
 519         "       if (core_id == 0)       /* local root process */",
 520         "       {       for (i = 1; i < NCORE; i++)     /* not for 0 of course */",
 521         "               {       int ignore;",
 522         "#if defined(WIN32) || defined(WIN64)",
 523         "                               DWORD dwExitCode = 0;",
 524         "                               GetExitCodeProcess(worker_handles[i], &dwExitCode);",
 525         "                               if (dwExitCode == STILL_ACTIVE)",
 526         "                               {       TerminateProcess(worker_handles[i], 0);",
 527         "                               }",
 528         "                               printf(\"cpu0: terminate %%d %%d\\n\",",
 529         "                                       (int) worker_pids[i], (dwExitCode == STILL_ACTIVE));",
 530         "#else",
 531         "                               sprintf(b, \"kill -%%d %%d\", (int) SIGKILL, (int) worker_pids[i]);",
 532         "                               ignore = system(b);     /* if this is a proxy: receive half */",
 533         "                               printf(\"cpu0: %%s\\n\", b);",
 534         "#endif",
 535         "               }",
 536         "               issued_kill++;",
 537         "       } else",
 538         "       {       /* on WIN32/WIN64 -- these merely kills the root process... */",
 539         "               if (was_interrupted == 0)",     /* 2=SIGINT to root to trigger stop */
 540         "               {       int ignore;",
 541         "                       sprintf(b, \"kill -%%d %%d\", (int) SIGINT, (int) worker_pids[0]);",
 542         "                       ignore = system(b);     /* warn the root process */",
 543         "                       printf(\"cpu%%d: %%s\\n\", core_id, b);",
 544         "                       issued_kill++;",
 545         "       }       }",
 546         "}",
 547         "",
 548         "#define iam_alive()    is_alive[core_id]++",   /* for crash detection */
 549         "",
 550         "extern int crash_test(double);",
 551         "extern void crash_reset(void);",
 552         "",
 553         "int",
 554         "someone_crashed(int wait_type)",
 555         "{      static double last_value = 0.0;",
 556         "       static int count = 0;",
 557         "",
 558         "       if (search_terminated == NULL",
 559         "       || *search_terminated != 0)",
 560         "       {",
 561         "               if (!(*search_terminated & (8|32|128|256)))",
 562         "               {       if (count++ < 100*NCORE)",
 563         "                       {       return 0;",
 564         "               }       }",
 565         "               return 1;",
 566         "       }",
 567         "       /* check left neighbor only */",
 568         "       if (last_value == is_alive[(core_id + NCORE - 1) %% NCORE])",
 569         "       {       if (count++ >= 100)     /* to avoid unnecessary checks */",
 570         "               {       return 1;",
 571         "               }",
 572         "               return 0;",
 573         "       }",
 574         "       last_value = is_alive[(core_id + NCORE - 1) %% NCORE];",
 575         "       count = 0;",
 576         "       crash_reset();",
 577         "       return 0;",
 578         "}",
 579         "",
 580         "void",
 581         "sleep_report(void)",
 582         "{",
 583         "       enter_critical(GLOBAL_LOCK);",
 584         "       if (verbose)",
 585         "       {",
 586         "#ifdef NGQ",
 587         "               printf(\"cpu%%d: locks: global %%g\\tother %%g\\t\",",
 588         "                       core_id, glock_wait[0], lock_wait - glock_wait[0]);",
 589         "#else",
 590         "               printf(\"cpu%%d: locks: GL %%g, RQ %%g, WQ %%g, HT %%g\\t\",",
 591         "                       core_id, glock_wait[0], glock_wait[1], glock_wait[2],",
 592         "                       lock_wait - glock_wait[0] - glock_wait[1] - glock_wait[2]);",
 593         "#endif",
 594         "               printf(\"waits: states %%g slots %%g\\n\", frame_wait, free_wait);",
 595         "#ifndef NGQ",
 596         "               printf(\"cpu%%d: gq [tries %%g, room %%g, noroom %%g]\\n\", core_id, gq_tries, gq_hasroom, gq_hasnoroom);",
 597         "               if (core_id == 0 && (*gr_readmiss >= 1.0 || *gr_readmiss >= 1.0 || *grcnt != 0))",
 598         "               printf(\"cpu0: gq [readmiss: %%g, writemiss: %%g cnt %%d]\\n\", *gr_readmiss, *gr_writemiss, *grcnt);",
 599         "#endif",
 600         "       }",
 601         "       if (free_wait > 1000000.)",
 602         "       #ifndef NGQ",
 603         "       if (!a_cycles)",
 604         "       {       printf(\"hint: this search may be faster with a larger work-queue\\n\");",
 605         "               printf(\"       (-DSET_WQ_SIZE=N with N>%%g), and/or with -DUSE_DISK\\n\",",
 606         "                       GWQ_SIZE/sizeof(SM_frame));",
 607         "               printf(\"      or with a larger value for -zN (N>%%ld)\\n\", z_handoff);",
 608         "       #else",
 609         "       {       printf(\"hint: this search may be faster if compiled without -DNGQ, with -DUSE_DISK, \");",
 610         "               printf(\"or with a larger -zN (N>%%d)\\n\", z_handoff);",
 611         "       #endif",
 612         "       }",
 613         "       leave_critical(GLOBAL_LOCK);",
 614         "}",
 615         "",
 616         "#ifndef MAX_DSK_FILE",
 617         "       #define MAX_DSK_FILE    1000000 /* default is max 1M states per file */",
 618         "#endif",
 619         "",
 620         "void",
 621         "multi_usage(FILE *fd)",
 622         "{      static int warned = 0;",
 623         "       if (warned > 0) { return; } else { warned++; }",
 624         "       fprintf(fd, \"\\n\");",
 625         "       fprintf(fd, \"Defining multi-core mode:\\n\\n\");",
 626         "       fprintf(fd, \"        -DDUAL_CORE --> same as -DNCORE=2\\n\");",
 627         "       fprintf(fd, \"        -DQUAD_CORE --> same as -DNCORE=4\\n\");",
 628         "       fprintf(fd, \"        -DNCORE=N   --> enables multi_core verification if N>1\\n\");",
 629         "       fprintf(fd, \"\\n\");",
 630         "       fprintf(fd, \"Additional directives supported in multi-core mode:\\n\\n\");",
 631         "       fprintf(fd, \"        -DSEP_STATE --> forces separate statespaces instead of a single shared state space\\n\");",
 632         "       fprintf(fd, \"        -DNUSE_DISK --> use disk for storing states when a work queue overflows\\n\");",
 633         "       fprintf(fd, \"        -DMAX_DSK_FILE --> max nr of states per diskfile (%%d)\\n\", MAX_DSK_FILE);",
 634         "       fprintf(fd, \"        -DFULL_TRAIL --> support full error trails (increases memory use)\\n\");",
 635         "       fprintf(fd, \"\\n\");",
 636         "       fprintf(fd, \"More advanced use (should rarely need changing):\\n\\n\");",
 637         "       fprintf(fd, \"     To change the nr of states that can be stored in the global queue\\n\");",
 638         "       fprintf(fd, \"     (lower numbers allow for more states to be stored, prefer multiples of 8):\\n\");",
 639         "       fprintf(fd, \"        -DVMAX=N    --> upperbound on statevector for handoffs (N=%%d)\\n\", VMAX);",
 640         "       fprintf(fd, \"        -DPMAX=N    --> upperbound on nr of procs (default: N=%%d)\\n\", PMAX);",
 641         "       fprintf(fd, \"        -DQMAX=N    --> upperbound on nr of channels (default: N=%%d)\\n\", QMAX);",
 642         "       fprintf(fd, \"\\n\");",
 643 #if 0
 644         "#if !defined(WIN32) && !defined(WIN64)",
 645         "       fprintf(fd, \"     To change the size of spin's individual shared memory segments for cygwin/linux:\\n\");",
 646         "       fprintf(fd, \"        -DSET_SEG_SIZE=N --> default %%g (Mbytes)\\n\", SEG_SIZE/(1048576.));",
 647         "       fprintf(fd, \"\\n\");",
 648         "#endif",
 649 #endif
 650         "       fprintf(fd, \"     To set the total amount of memory reserved for the global workqueue:\\n\");",
 651         "       fprintf(fd, \"        -DSET_WQ_SIZE=N --> default: N=128 (defined in MBytes)\\n\\n\");",
 652 #if 0
 653         "       fprintf(fd, \"     To omit the global workqueue completely (bad idea):\\n\");",
 654         "       fprintf(fd, \"        -DNGQ\\n\\n\");",
 655 #endif
 656         "       fprintf(fd, \"     To force the use of a single global heap, instead of separate heaps:\\n\");",
 657         "       fprintf(fd, \"        -DGLOB_HEAP\\n\");",
 658         "       fprintf(fd, \"\\n\");",
 659         "       fprintf(fd, \"     To define a fct to initialize data before spawning processes (use quotes):\\n\");",
 660         "       fprintf(fd, \"        \\\"-DC_INIT=fct()\\\"\\n\");",
 661         "       fprintf(fd, \"\\n\");",
 662         "       fprintf(fd, \"     Timer settings for termination and crash detection:\\n\");",
 663         "       fprintf(fd, \"        -DSHORT_T=N --> timeout for termination detection trigger (N=%%g)\\n\", (double) SHORT_T);",
 664         "       fprintf(fd, \"        -DLONG_T=N  --> timeout for giving up on termination detection (N=%%g)\\n\", (double) LONG_T);",
 665         "       fprintf(fd, \"        -DONESECOND --> (1<<29) --> timeout waiting for a free slot -- to check for crash\\n\");",
 666         "       fprintf(fd, \"        -DT_ALERT   --> collect stats on crash alert timeouts\\n\\n\");",
 667         "       fprintf(fd, \"Help with Linux/Windows/Cygwin configuration for multi-core:\\n\");",
 668         "       fprintf(fd, \"  http://spinroot.com/spin/multicore/V5_Readme.html\\n\");",
 669         "       fprintf(fd, \"\\n\");",
 670         "}",
 671         "#if NCORE>1 && defined(FULL_TRAIL)",
 672         "typedef struct Stack_Tree {",
 673         "       uchar         pr;       /* process that made transition */",
 674         "       T_ID        t_id;       /* id of transition */",
 675         "       volatile struct Stack_Tree *prv; /* backward link towards root */",
 676         "} Stack_Tree;",
 677         "",
 678         "H_el *grab_shared(int);",
 679         "volatile Stack_Tree **stack_last; /* in shared memory */",
 680         "char *stack_cache = NULL;      /* local */",
 681         "int  nr_cached = 0;            /* local */",
 682         "",
 683         "#ifndef CACHE_NR",
 684         "       #define CACHE_NR        1024",
 685         "#endif",
 686         "",
 687         "volatile Stack_Tree *",
 688         "stack_prefetch(void)",
 689         "{      volatile Stack_Tree *st;",
 690         "",
 691         "       if (nr_cached == 0)",
 692         "       {       stack_cache = (char *) grab_shared(CACHE_NR * sizeof(Stack_Tree));",
 693         "               nr_cached = CACHE_NR;",
 694         "       }",
 695         "       st = (volatile Stack_Tree *) stack_cache;",
 696         "       stack_cache += sizeof(Stack_Tree);",
 697         "       nr_cached--;",
 698         "       return st;",
 699         "}",
 700         "",
 701         "void",
 702         "Push_Stack_Tree(short II, T_ID t_id)",
 703         "{      volatile Stack_Tree *st;",
 704         "",
 705         "       st = (volatile Stack_Tree *) stack_prefetch();",
 706         "       st->pr = II;",
 707         "       st->t_id = t_id;",
 708         "       st->prv = (Stack_Tree *) stack_last[core_id];",
 709         "       stack_last[core_id] = st;",
 710         "}",
 711         "",
 712         "void",
 713         "Pop_Stack_Tree(void)",
 714         "{      volatile Stack_Tree *cf = stack_last[core_id];",
 715         "",
 716         "       if (cf)",
 717         "       {       stack_last[core_id] = cf->prv;",
 718         "       } else if (nr_handoffs * z_handoff + depth > 0)",
 719         "       {       printf(\"cpu%%d: error pop_stack_tree (depth %%ld)\\n\",",
 720         "                       core_id, depth);",
 721         "       }",
 722         "}",
 723         "#endif", /* NCORE>1 && FULL_TRAIL */
 724         "",
 725         "void",
 726         "e_critical(int which)",
 727         "{      double cnt_start;",
 728         "",
 729         "       if (readtrail || iamin[which] > 0)",
 730         "       {       if (!readtrail && verbose)",
 731         "               {       printf(\"cpu%%d: Double Lock on %%d (now %%d)\\n\",",
 732         "                               core_id, which, iamin[which]+1);",
 733         "                       fflush(stdout);",
 734         "               }",
 735         "               iamin[which]++; /* local variable */",
 736         "               return;",
 737         "       }",
 738         "",
 739         "       cnt_start = lock_wait;",
 740         "",
 741         "       while (sh_lock != NULL) /* as long as we have shared memory */",
 742         "       {       int r = tas(&sh_lock[which]);",
 743         "               if (r == 0)",
 744         "               {       iamin[which] = 1;",
 745         "                       return;         /* locked */",
 746         "               }",
 747         "",
 748         "               lock_wait++;",
 749         "#ifndef NGQ",
 750         "               if (which < 3) { glock_wait[which]++; }",
 751         "#else",
 752         "               if (which == 0) { glock_wait[which]++; }",
 753         "#endif",
 754         "               iam_alive();",
 755         "",
 756         "               if (lock_wait - cnt_start > TenSeconds)",
 757         "               {       printf(\"cpu%%d: lock timeout on %%d\\n\", core_id, which);",
 758         "                       cnt_start = lock_wait;",
 759         "                       if (someone_crashed(1))",
 760         "                       {       sudden_stop(\"lock timeout\");",
 761         "                               pan_exit(1);",
 762         "       }       }       }",
 763         "}",
 764         "",
 765         "void",
 766         "x_critical(int which)",
 767         "{",
 768         "       if (iamin[which] != 1)",
 769         "       {       if (iamin[which] > 1)",
 770         "               {       iamin[which]--; /* this is thread-local - no races on this one */",
 771         "                       if (!readtrail && verbose)",
 772         "                       {       printf(\"cpu%%d: Partial Unlock on %%d (%%d more needed)\\n\",",
 773         "                                       core_id, which, iamin[which]);",
 774         "                               fflush(stdout);",
 775         "                       }",
 776         "                       return;",
 777         "               } else /* iamin[which] <= 0 */",
 778         "               {       if (!readtrail)",
 779         "                       {       printf(\"cpu%%d: Invalid Unlock iamin[%%d] = %%d\\n\",",
 780         "                                       core_id, which, iamin[which]);",
 781         "                               fflush(stdout);",
 782         "                       }",
 783         "                       return;",
 784         "       }       }",
 785         "",
 786         "       if (sh_lock != NULL)",
 787         "       {       iamin[which]   = 0;",
 788         "#if defined(__powerpc64__)",
 789         "       #if 1",
 790         "               __sync_synchronize();   /* srirajpaul */",
 791         "       #else",
 792         "               __lwsync();             /* xlc compiler only */",
 793         "       #endif",
 794         "#endif",
 795         "               sh_lock[which] = 0;     /* unlock */",
 796         "       }",
 797         "}",
 798         "",
 799         "void",
 800         "#if defined(WIN32) || defined(WIN64)",
 801         "start_proxy(char *s, DWORD r_pid)",
 802         "#else",
 803         "start_proxy(char *s, int r_pid)",
 804         "#endif",
 805         "{      char  Q_arg[16], Z_arg[16], Y_arg[16];",
 806         "       char *args[32], *ptr;",
 807         "       int   argcnt = 0;",
 808         "",
 809         "       sprintf(Q_arg, \"-Q%%d\", getpid());",
 810         "       sprintf(Y_arg, \"-Y%%d\", r_pid);",
 811         "       sprintf(Z_arg, \"-Z%%d\", proxy_pid /* core_id */);",
 812         "",
 813         "       args[argcnt++] = \"proxy\";",
 814         "       args[argcnt++] = s; /* -r or -s */",
 815         "       args[argcnt++] = Q_arg;",
 816         "       args[argcnt++] = Z_arg;",
 817         "       args[argcnt++] = Y_arg;",
 818         "",
 819         "       if (strlen(o_cmdline) > 0)",
 820         "       {       ptr = o_cmdline; /* assume args separated by spaces */",
 821         "               do {    args[argcnt++] = ptr++;",
 822         "                       if ((ptr = strchr(ptr, ' ')) != NULL)",
 823         "                       {       while (*ptr == ' ')",
 824         "                               {       *ptr++ = '\\0';",
 825         "                               }",
 826         "                       } else",
 827         "                       {       break;",
 828         "                       }",
 829         "               } while (argcnt < 31);",
 830         "       }",
 831         "       args[argcnt] = NULL;",
 832         "#if defined(WIN32) || defined(WIN64)",
 833         "       execvp(\"pan_proxy\", args); /* no return */",
 834         "#else",
 835         "       execvp(\"./pan_proxy\", args); /* no return */",
 836         "#endif",
 837         "       Uerror(\"pan_proxy exec failed\");",
 838         "}",
 839         "/*** end of common code fragment ***/",
 840         "",
 841         "#if !defined(WIN32) && !defined(WIN64)",
 842         "void",
 843         "init_shm(void)         /* initialize shared work-queues - linux/cygwin */",
 844         "{      key_t   key[NR_QS];",
 845         "       int     n, m;",
 846         "       int     must_exit = 0;",
 847         "",
 848         "       if (core_id == 0 && verbose)",
 849         "       {       printf(\"cpu0: step 3: allocate shared workqueues %%g MB\\n\",",
 850         "                       ((double) NCORE * LWQ_SIZE + GWQ_SIZE) / (1048576.) );",
 851         "       }",
 852         "       for (m = 0; m < NR_QS; m++)             /* last q is the global q */",
 853         "       {       double qsize = (m == NCORE) ? GWQ_SIZE : LWQ_SIZE;",
 854         "               key[m] = ftok(PanSource, m+1);", /* m must be nonzero, 1..NCORE */
 855         "               if (key[m] == -1)",
 856         "               {       perror(\"ftok shared queues\"); must_exit = 1; break;",
 857         "               }",
 858         "",
 859         "               if (core_id == 0)       /* root creates */",
 860         "               {       /* check for stale copy */",
 861         "                       shmid[m] = shmget(key[m], (size_t) qsize, 0600);",
 862         "                       if (shmid[m] != -1)     /* yes there is one; remove it */",
 863         "                       {       printf(\"cpu0: removing stale q%%d, status: %%d\\n\",",
 864         "                                       m, shmctl(shmid[m], IPC_RMID, NULL));",
 865         "                       }",
 866         "                       shmid[m] = shmget(key[m], (size_t) qsize, 0600|IPC_CREAT|IPC_EXCL);",
 867         "                       memcnt += qsize;",
 868         "               } else                  /* workers attach */",
 869         "               {       shmid[m] = shmget(key[m], (size_t) qsize, 0600);",
 870         "                       /* never called, since we create shm *before* we fork */",
 871         "               }",
 872         "               if (shmid[m] == -1)",
 873         "               {       perror(\"shmget shared queues\"); must_exit = 1; break;",
 874         "               }",
 875         "",
 876         "               shared_mem[m] = (char *) shmat(shmid[m], (void *) 0, 0);        /* attach */",
 877         "               if (shared_mem[m] == (char *) -1)",
 878         "               { fprintf(stderr, \"error: cannot attach shared wq %%d (%%d Mb)\\n\",",
 879         "                               m+1, (int) (qsize/(1048576.)));",
 880         "                 perror(\"shmat shared queues\"); must_exit = 1; break;",
 881         "               }",
 882         "",
 883         "               m_workq[m] = (SM_frame *) shared_mem[m];",
 884         "               if (core_id == 0)",
 885         "               {       int nframes = (m == NCORE) ? GN_FRAMES : LN_FRAMES;",
 886         "                       for (n = 0; n < nframes; n++)",
 887         "                       {       m_workq[m][n].m_vsize = 0;",
 888         "                               m_workq[m][n].m_boq = 0;",
 889         "       }       }       }",
 890         "",
 891         "       if (must_exit)",
 892         "       {       rm_shared_segments();",
 893         "               fprintf(stderr, \"pan: check './pan --' for usage details\\n\");",
 894         "               pan_exit(1);    /* calls cleanup_shm */",
 895         "       }",
 896         "}",
 897         "",
 898         "static uchar *",
 899         "prep_shmid_S(size_t n)         /* either sets SS or H_tab, linux/cygwin */",
 900         "{      char    *rval;",
 901         "#ifndef SEP_STATE",
 902         "       key_t   key;",
 903         "",
 904         "       if (verbose && core_id == 0)",
 905         "       {",
 906         "       #ifdef BITSTATE",
 907         "               printf(\"cpu0: step 1: allocate shared bitstate %%g Mb\\n\",",
 908         "                       (double) n / (1048576.));",
 909         "       #else",
 910         "               printf(\"cpu0: step 1: allocate shared hastable %%g Mb\\n\",",
 911         "                       (double) n / (1048576.));",
 912         "       #endif",
 913         "       }",
 914         "       #ifdef MEMLIM", /* memlim has a value */
 915         "       if (memcnt + (double) n > memlim)",
 916         "       {       printf(\"cpu0: S %%8g + %%d Kb exceeds memory limit of %%8g Mb\\n\",",
 917         "                       memcnt/1024., (int) (n/1024), memlim/(1048576.));",
 918         "               printf(\"cpu0: insufficient memory -- aborting\\n\");",
 919         "               exit(1);",
 920         "       }",
 921         "       #endif",
 922         "",
 923         "       key = ftok(PanSource, NCORE+2); /* different from queues */",
 924         "       if (key == -1)",
 925         "       {       perror(\"ftok shared bitstate or hashtable\");",
 926         "               fprintf(stderr, \"pan: check './pan --' for usage details\\n\");",
 927         "               pan_exit(1);",
 928         "       }",
 929         "",
 930         "       if (core_id == 0)       /* root */",
 931         "       {       shmid_S = shmget(key, n, 0600);",
 932         "               if (shmid_S != -1)",
 933         "               {       printf(\"cpu0: removing stale segment, status: %%d\\n\",",
 934         "                               (int) shmctl(shmid_S, IPC_RMID, NULL));",
 935         "               }",
 936         "               shmid_S = shmget(key, n, 0600 | IPC_CREAT | IPC_EXCL);",
 937         "               memcnt += (double) n;",
 938         "       } else                  /* worker */",
 939         "       {       shmid_S = shmget(key, n, 0600);",
 940         "       }",
 941         "       if (shmid_S == -1)",
 942         "       {       perror(\"shmget shared bitstate or hashtable too large?\");",
 943         "               fprintf(stderr, \"pan: check './pan --' for usage details\\n\");",
 944         "               pan_exit(1);",
 945         "       }",
 946         "",
 947         "       rval = (char *) shmat(shmid_S, (void *) 0, 0);  /* attach */",
 948         "       if ((char *) rval == (char *) -1)",
 949         "       {       perror(\"shmat shared bitstate or hashtable\");",
 950         "               fprintf(stderr, \"pan: check './pan --' for usage details\\n\");",
 951         "               pan_exit(1);",
 952         "       }",
 953         "#else",
 954         "       rval = (char *) emalloc(n);",
 955         "#endif",
 956         "       return (uchar *) rval;",
 957         "}",
 958         "",
 959         "#define TRY_AGAIN      1",
 960         "#define NOT_AGAIN      0",
 961         "",
 962         "static char shm_prep_result;",
 963         "",
 964         "static uchar *",
 965         "prep_state_mem(size_t n)               /* sets memory arena for states linux/cygwin */",
 966         "{      char    *rval;",
 967         "       key_t   key;",
 968         "       static int cnt = 3;             /* start larger than earlier ftok calls */",
 969         "",
 970         "       shm_prep_result = NOT_AGAIN;    /* default */",
 971         "       if (verbose && core_id == 0)",
 972         "       {       printf(\"cpu0: step 2+: pre-allocate memory arena %%d of %%6.2g Mb\\n\",",
 973         "                       cnt-3, (double) n / (1048576.));",
 974         "       }",
 975         "       #ifdef MEMLIM",
 976         "       if (memcnt + (double) n > memlim)",
 977         "       {       printf(\"cpu0: error: M %%.0f + %%.0f Kb exceeds memory limit of %%.0f Mb\\n\",",
 978         "                       memcnt/1024.0, (double) n/1024.0, memlim/(1048576.));",
 979         "               return NULL;",
 980         "       }",
 981         "       #endif",
 982         "",
 983         "       key = ftok(PanSource, NCORE+cnt); cnt++;", /* starts at NCORE+3 */
 984         "       if (key == -1)",
 985         "       {       perror(\"ftok T\");",
 986         "               printf(\"pan: check './pan --' for usage details\\n\");",
 987         "               pan_exit(1);",
 988         "       }",
 989         "",
 990         "       if (core_id == 0)",
 991         "       {       shmid_M = shmget(key, n, 0600);",
 992         "               if (shmid_M != -1)",
 993         "               {       printf(\"cpu0: removing stale memory segment %%d, status: %%d\\n\",",
 994         "                               cnt-3, shmctl(shmid_M, IPC_RMID, NULL));",
 995         "               }",
 996         "               shmid_M = shmget(key, n, 0600 | IPC_CREAT | IPC_EXCL);",
 997         "               /* memcnt += (double) n; -- only amount actually used is counted */",
 998         "       } else",
 999         "       {       shmid_M = shmget(key, n, 0600);",
1000         "       ",
1001         "       }",
1002         "       if (shmid_M == -1)",
1003         "       {       if (verbose)",
1004         "               {       printf(\"error: failed to get pool of shared memory %%d of %%.0f Mb\\n\",",
1005         "                               cnt-3, ((double)n)/(1048576.));",
1006         "                       perror(\"state mem\");",
1007         "                       printf(\"pan: check './pan --' for usage details\\n\");",
1008         "               }",
1009         "               shm_prep_result = TRY_AGAIN;",
1010         "               return NULL;",
1011         "       }",
1012         "       rval = (char *) shmat(shmid_M, (void *) 0, 0);  /* attach */",
1013         "",
1014         "       if ((char *) rval == (char *) -1)",
1015         "       {       printf(\"cpu%%d error: failed to attach pool of shared memory %%d of %%.0f Mb\\n\",",
1016         "                        core_id, cnt-3, ((double)n)/(1048576.));",
1017         "               perror(\"state mem\");",
1018         "               return NULL;",
1019         "       }",
1020         "       return (uchar *) rval;",
1021         "}",
1022         "",
1023         "void",
1024         "init_HT(unsigned long n)       /* cygwin/linux version */",
1025         "{      volatile char   *x;",
1026         "       double  get_mem;",
1027         "#ifndef SEP_STATE",
1028         "       volatile char   *dc_mem_start;",
1029         "       double  need_mem, got_mem = 0.;",
1030         "#endif",
1031         "",
1032 "#ifdef SEP_STATE",
1033         " #ifndef MEMLIM",
1034         "       if (verbose)",
1035         "       {       printf(\"cpu0: steps 0,1: no -DMEMLIM set\\n\");", /* cannot happen */
1036         "       }",
1037         " #else",
1038         "       if (verbose)",
1039         "       {       printf(\"cpu0: steps 0,1: -DMEMLIM=%%d Mb - (hashtable %%g Mb + workqueues %%g Mb)\\n\",",
1040         "               MEMLIM, ((double)n/(1048576.)), (((double) NCORE * LWQ_SIZE) + GWQ_SIZE) /(1048576.) );",
1041         "       }",
1042         " #endif",
1043         "       get_mem = NCORE * sizeof(double) + (1 + CS_NR) * sizeof(void *) + 4*sizeof(void *) + 2*sizeof(double);",
1044         "       /* NCORE * is_alive + search_terminated + CS_NR * sh_lock + 6 gr vars */",
1045         "       get_mem += 4 * NCORE * sizeof(void *); /* prfree, prfull, prcnt, prmax */",
1046         " #ifdef FULL_TRAIL",
1047         "       get_mem += (NCORE) * sizeof(Stack_Tree *); /* NCORE * stack_last */",
1048         " #endif",
1049         "       x = (volatile char *) prep_state_mem((size_t) get_mem); /* work queues and basic structs */",
1050         "       shmid_X = (long) x;",
1051         "       if (x == NULL)", /* do not repeat for smaller sizes */
1052         "       {       printf(\"cpu0: could not allocate shared memory, see ./pan --\\n\");",
1053         "               exit(1);",
1054         "       }",
1055         "       search_terminated = (volatile unsigned int *) x; /* comes first */",
1056         "       x += sizeof(void *); /* maintain alignment */",
1057         "",
1058         "       is_alive   = (volatile double *) x;",
1059         "       x += NCORE * sizeof(double);",
1060         "",
1061         "       sh_lock   = (volatile int *) x;",
1062         "       x += CS_NR * sizeof(void *);", /* allow 1 word per entry */
1063         "",
1064         "       grfree    = (volatile int *) x;",
1065         "       x += sizeof(void *);",
1066         "       grfull    = (volatile int *) x;",
1067         "       x += sizeof(void *);",
1068         "       grcnt    = (volatile int *) x;",
1069         "       x += sizeof(void *);",
1070         "       grmax    = (volatile int *) x;",
1071         "       x += sizeof(void *);",
1072         "       prfree = (volatile int *) x;",
1073         "       x += NCORE * sizeof(void *);",
1074         "       prfull = (volatile int *) x;",
1075         "       x += NCORE * sizeof(void *);",
1076         "       prcnt = (volatile int *) x;",
1077         "       x += NCORE * sizeof(void *);",
1078         "       prmax = (volatile int *) x;",
1079         "       x += NCORE * sizeof(void *);",
1080         "       gr_readmiss    = (volatile double *) x;",
1081         "       x += sizeof(double);",
1082         "       gr_writemiss    = (volatile double *) x;",
1083         "       x += sizeof(double);",
1084         "",
1085         "       #ifdef FULL_TRAIL",
1086         "               stack_last = (volatile Stack_Tree **) x;",
1087         "               x += NCORE * sizeof(Stack_Tree *);",
1088         "       #endif",
1089         "",
1090         "       #ifndef BITSTATE",
1091         "               H_tab = (H_el **) emalloc(n);",
1092         "       #endif",
1093 "#else",
1094         "       #ifndef MEMLIM",
1095         "               #warning MEMLIM not set", /* cannot happen */
1096         "               #define MEMLIM  (2048)",
1097         "       #endif",
1098         "",
1099         "       if (core_id == 0 && verbose)",
1100         "       {       printf(\"cpu0: step 0: -DMEMLIM=%%d Mb minus hashtable+workqs (%%g + %%g Mb) leaves %%g Mb\\n\",",
1101         "                       MEMLIM, ((double)n/(1048576.)), (NCORE * LWQ_SIZE + GWQ_SIZE)/(1048576.),",
1102         "                       (memlim - memcnt - (double) n - (NCORE * LWQ_SIZE + GWQ_SIZE))/(1048576.));",
1103         "       }",
1104         "       #ifndef BITSTATE",
1105         "               H_tab = (H_el **) prep_shmid_S((size_t) n);     /* hash_table */",
1106         "       #endif",
1107         "       need_mem = memlim - memcnt - ((double) NCORE * LWQ_SIZE) - GWQ_SIZE;",
1108         "       if (need_mem <= 0.)",
1109         "       {       Uerror(\"internal error -- shared state memory\");",
1110         "       }",
1111         "",
1112         "       if (core_id == 0 && verbose)",
1113         "       {       printf(\"cpu0: step 2: pre-allocate shared state memory %%g Mb\\n\",",
1114         "                       need_mem/(1048576.));",
1115         "       }",
1116         "#ifdef SEP_HEAP",
1117         "       SEG_SIZE = need_mem / NCORE;",
1118         "       if (verbose && core_id == 0)",
1119         "       {       printf(\"cpu0: setting segsize to %%6g MB\\n\",",
1120         "                       SEG_SIZE/(1048576.));",
1121         "       }",
1122         "       #if defined(CYGWIN) || defined(__CYGWIN__)",
1123         "       if (SEG_SIZE > 512.*1024.*1024.)",
1124         "       {       printf(\"warning: reducing SEG_SIZE of %%g MB to 512MB (exceeds max for Cygwin)\\n\",",
1125         "                       SEG_SIZE/(1024.*1024.));",
1126         "               SEG_SIZE = 512.*1024.*1024.;",
1127         "       }",
1128         "       #endif",
1129         "#endif",
1130         "       mem_reserved = need_mem;",
1131         "       while (need_mem > 1024.)",
1132         "       {       get_mem = need_mem;",
1133         "shm_more:",
1134         "               if (get_mem > (double) SEG_SIZE)",
1135         "               {       get_mem = (double) SEG_SIZE;",
1136         "               }",
1137         "               if (get_mem <= 0.0) break;",
1138         "",
1139         "               /* for allocating states: */",
1140         "               x = dc_mem_start = (volatile char *) prep_state_mem((size_t) get_mem);",
1141         "               if (x == NULL)",
1142         "               {       if (shm_prep_result == NOT_AGAIN",
1143         "                       ||  first_pool != NULL",
1144         "                       ||  SEG_SIZE < (16. * 1048576.))",
1145         "                       {       break;",
1146         "                       }",
1147         "                       SEG_SIZE /= 2.;",
1148         "                       if (verbose)",
1149         "                       {       printf(\"pan: lowered segsize to %%f\\n\", SEG_SIZE);",
1150         "                       }",
1151         "                       if (SEG_SIZE >= 1024.)",
1152         "                       {       goto shm_more;", /* always terminates */
1153         "                       }",
1154         "                       break;",
1155         "               }",
1156         "",
1157         "               need_mem -= get_mem;",
1158         "               got_mem  += get_mem;",
1159         "               if (first_pool == NULL)",
1160         "               {       search_terminated = (volatile unsigned int *) x; /* comes first */",
1161         "                       x += sizeof(void *); /* maintain alignment */",
1162         "",
1163         "                       is_alive   = (volatile double *) x;",
1164         "                       x += NCORE * sizeof(double);",
1165         "",
1166         "                       sh_lock   = (volatile int *) x;",
1167         "                       x += CS_NR * sizeof(void *);", /* allow 1 word per entry */
1168         "",
1169         "                       grfree    = (volatile int *) x;",
1170         "                       x += sizeof(void *);",
1171         "                       grfull    = (volatile int *) x;",
1172         "                       x += sizeof(void *);",
1173         "                       grcnt    = (volatile int *) x;",
1174         "                       x += sizeof(void *);",
1175         "                       grmax    = (volatile int *) x;",
1176         "                       x += sizeof(void *);",
1177         "                       prfree = (volatile int *) x;",
1178         "                       x += NCORE * sizeof(void *);",
1179         "                       prfull = (volatile int *) x;",
1180         "                       x += NCORE * sizeof(void *);",
1181         "                       prcnt = (volatile int *) x;",
1182         "                       x += NCORE * sizeof(void *);",
1183         "                       prmax = (volatile int *) x;",
1184         "                       x += NCORE * sizeof(void *);",
1185         "                       gr_readmiss  = (volatile double *) x;",
1186         "                       x += sizeof(double);",
1187         "                       gr_writemiss = (volatile double *) x;",
1188         "                       x += sizeof(double);",
1189         " #ifdef FULL_TRAIL",
1190         "                       stack_last = (volatile Stack_Tree **) x;",
1191         "                       x += NCORE * sizeof(Stack_Tree *);",
1192         " #endif",
1193         "                       if (((long)x)&(sizeof(void *)-1)) /* 64-bit word alignment */",
1194         "                       {       x += sizeof(void *)-(((long)x)&(sizeof(void *)-1));",
1195         "                       }",
1196         "",
1197         "                       #ifdef COLLAPSE",
1198         "                       ncomps = (unsigned long *) x;",
1199         "                       x += (256+2) * sizeof(unsigned long);",
1200         "                       #endif",
1201         "               }",
1202         "",
1203         "               dc_shared = (sh_Allocater *) x; /* must be in shared memory */",
1204         "               x += sizeof(sh_Allocater);",
1205         "",
1206         "               if (core_id == 0)       /* root only */",
1207         "               {       dc_shared->dc_id     = shmid_M;",
1208         "                       dc_shared->dc_start  = dc_mem_start;",
1209         "                       dc_shared->dc_arena  = x;",
1210         "                       dc_shared->pattern   = 1234567; /* protection */",
1211         "                       dc_shared->dc_size   = (long) get_mem - (long) (x - dc_mem_start);",
1212         "                       dc_shared->nxt       = (long) 0;",
1213         "",
1214         "                       if (last_pool == NULL)",
1215         "                       {       first_pool = last_pool = dc_shared;",
1216         "                       } else",
1217         "                       {       last_pool->nxt = dc_shared;",
1218         "                               last_pool = dc_shared;",
1219         "                       }",
1220         "               } else if (first_pool == NULL)",
1221         "               {       first_pool = dc_shared;",
1222         "       }       }",
1223         "",
1224         "       if (need_mem > 1024.)",
1225         "       {       printf(\"cpu0: could allocate only %%g Mb of shared memory (wanted %%g more)\\n\",",
1226         "                       got_mem/(1048576.), need_mem/(1048576.));",
1227         "       }",
1228         "",
1229         "       if (!first_pool)",
1230         "       {       printf(\"cpu0: insufficient memory -- aborting.\\n\");",
1231         "               exit(1);",
1232         "       }",
1233         "       /* we are still single-threaded at this point, with core_id 0 */",
1234         "       dc_shared = first_pool;",
1235         "",
1236 "#endif", /* !SEP_STATE */
1237         "}",
1238         "",
1239         "void",
1240         "cleanup_shm(int val)",
1241         "{      volatile sh_Allocater *nxt_pool;",
1242         "       unsigned long cnt = 0;",
1243         "       int m;",
1244         "",
1245         "       if (nibis != 0)",
1246         "       {       printf(\"cpu%%d: Redundant call to cleanup_shm(%%d)\\n\", core_id, val);",
1247         "               return;",
1248         "       } else",
1249         "       {       nibis = 1;",
1250         "       }",
1251         "       if (search_terminated != NULL)",
1252         "       {       *search_terminated |= 16; /* cleanup_shm */",
1253         "       }",
1254         "",
1255         "       for (m = 0; m < NR_QS; m++)",
1256         "       {       if (shmdt((void *) shared_mem[m]) > 0)",
1257         "               {       perror(\"shmdt detaching from shared queues\");",
1258         "       }       }",
1259         "",
1260         "#ifdef SEP_STATE",
1261         "       if (shmdt((void *) shmid_X) != 0)",
1262         "       {       perror(\"shmdt detaching from shared state memory\");",
1263         "       }",
1264         "#else",
1265         "       #ifdef BITSTATE",
1266         "               if (SS > 0 && shmdt((void *) SS) != 0)",
1267         "               {       if (verbose)",
1268         "                       {       perror(\"shmdt detaching from shared bitstate arena\");",
1269         "               }       }",
1270         "       #else",
1271         "               if (core_id == 0)",
1272         "               {       /* before detaching: */",
1273         "                       for (nxt_pool = dc_shared; nxt_pool != NULL; nxt_pool = nxt_pool->nxt)",
1274         "                       {       cnt += nxt_pool->dc_size;",
1275         "                       }",
1276         "                       if (verbose)",
1277         "                       {       printf(\"cpu0: done, %%ld Mb of shared state memory left\\n\",",
1278         "                                       cnt / (long)(1048576));",
1279         "               }       }",
1280         "",
1281         "               if (shmdt((void *) H_tab) != 0)",
1282         "               {       perror(\"shmdt detaching from shared hashtable\");",
1283         "               }",
1284         "",
1285         "               for (last_pool = first_pool; last_pool != NULL; last_pool = nxt_pool)",
1286         "               {       nxt_pool = last_pool->nxt;",
1287         "                       if (shmdt((void *) last_pool->dc_start) != 0)",
1288         "                       {       perror(\"shmdt detaching from shared state memory\");",
1289         "               }       }",
1290         "               first_pool = last_pool = NULL;  /* precaution */",
1291         "       #endif",
1292         "#endif",
1293         "       /* detached from shared memory - so cannot use cpu_printf */",
1294         "       if (verbose)",
1295         "       {       printf(\"cpu%%d: done -- got %%ld states from queue\\n\",",
1296         "                       core_id, nstates_get);",
1297         "       }",
1298         "}",
1299         "",
1300         "extern void give_up(int);",
1301         "extern void Read_Queue(int);",
1302         "",
1303         "void",
1304         "mem_get(void)",
1305         "{      SM_frame   *f;",
1306         "       int is_parent;",
1307         "",
1308         "#if defined(MA) && !defined(SEP_STATE)",
1309         "       #error MA without SEP_STATE is not supported with multi-core",
1310         "#endif",
1311         "#ifdef BFS",
1312         "       #error instead of -DNCORE -DBFS use -DBFS_PAR",
1313         "#endif",
1314         "#ifdef SC",
1315         "       #error SC is not supported with multi-core",
1316         "#endif",
1317         "       init_shm();     /* we are single threaded when this starts */",
1318         "",
1319         "       if (core_id == 0 && verbose)",
1320         "       {       printf(\"cpu0: step 4: calling fork()\\n\");",
1321         "       }",
1322         "       fflush(stdout);",
1323         "",
1324         "/*     if NCORE > 1 the child or the parent should fork N-1 more times",
1325         " *     the parent is the only process with core_id == 0 and is_parent > 0",
1326         " *     the workers have is_parent = 0 and core_id = 1..NCORE-1",
1327         " */",
1328         "       if (core_id == 0)",
1329         "       {       worker_pids[0] = getpid();      /* for completeness */",
1330         "               while (++core_id < NCORE)       /* first worker sees core_id = 1 */",
1331         "               {       is_parent = fork();",
1332         "                       if (is_parent == -1)",
1333         "                       {       Uerror(\"fork failed\");",
1334         "                       }",
1335         "                       if (is_parent == 0)     /* this is a worker process */",
1336         "                       {       if (proxy_pid == core_id)       /* always non-zero */",
1337         "                               {       start_proxy(\"-r\", 0); /* no return */",
1338         "                               }",
1339         "                               goto adapt;     /* root process continues spawning */",
1340         "                       }",
1341         "                       worker_pids[core_id] = is_parent;",
1342         "               }",
1343         "               /* note that core_id is now NCORE */",
1344         "               if (proxy_pid > 0 && proxy_pid < NCORE)", /* add send-half of proxy */
1345         "               {       proxy_pid_snd = fork();",
1346         "                       if (proxy_pid_snd == -1)",
1347         "                       {       Uerror(\"proxy fork failed\");",
1348         "                       }",
1349         "                       if (proxy_pid_snd == 0)",
1350         "                       {       start_proxy(\"-s\", worker_pids[proxy_pid]); /* no return */",
1351         "               }       } /* else continue */",
1352
1353         "               if (is_parent > 0)",
1354         "               {       core_id = 0;    /* reset core_id for root process */",
1355         "               }",
1356         "       } else  /* worker */",
1357         "       {       static char db0[16];    /* good for up to 10^6 cores */",
1358         "               static char db1[16];",
1359         "adapt:         tprefix = db0; sprefix = db1;",
1360         "               sprintf(tprefix, \"cpu%%d_trail\", core_id);",
1361         "               sprintf(sprefix, \"cpu%%d_rst\", core_id);",
1362         "               memcnt = 0;     /* count only additionally allocated memory */",
1363         "       }",
1364         "       signal(SIGINT, give_up);",
1365         "",
1366         "       if (proxy_pid == 0)             /* not in a cluster setup, pan_proxy must attach */",
1367         "       {       rm_shared_segments();   /* mark all shared segments for removal on exit */",
1368         "       }", /* doing it early means less chance of being unable to do this */
1369         "       if (verbose)",
1370         "       {       cpu_printf(\"starting core_id %%d -- pid %%d\\n\", core_id, getpid());",
1371         "       }",
1372
1373         "#if defined(SEP_HEAP) && !defined(SEP_STATE)", /* set my_heap and adjust dc_shared */
1374         "       {       int i;",
1375         "               volatile sh_Allocater *ptr;",
1376         "               ptr = first_pool;",
1377         "               for (i = 0; i < NCORE  && ptr != NULL; i++)",
1378         "               {       if (i == core_id)",
1379         "                       {       my_heap = (char *) ptr->dc_arena;",
1380         "                               my_size = (long) ptr->dc_size;",
1381         "                               if (verbose)",
1382         "                               cpu_printf(\"local heap %%ld MB\\n\", my_size/(1048576));",
1383         "                               break;",
1384         "                       }",
1385         "                       ptr = ptr->nxt; /* local */",
1386         "               }",
1387         "               if (my_heap == NULL)",
1388         "               {       printf(\"cpu%%d: no local heap\\n\", core_id);",
1389         "                       pan_exit(1);",
1390         "               } /* else */",
1391         "       #if defined(CYGWIN) || defined(__CYGWIN__)",
1392         "               ptr = first_pool;",
1393         "               for (i = 0; i < NCORE  && ptr != NULL; i++)",
1394         "               {       ptr = ptr->nxt; /* local */",
1395         "               }",
1396         "               dc_shared = ptr; /* any remainder */",
1397         "       #else",
1398         "               dc_shared = NULL; /* used all mem for local heaps */",
1399         "       #endif",
1400         "       }",
1401         "#endif",
1402
1403         "       if (core_id == 0 && !remote_party)",
1404         "       {       new_state();            /* cpu0 explores root */",
1405         "               if (verbose)",
1406         "               cpu_printf(\"done with 1st dfs, nstates %%g (put %%d states), read q\\n\",",
1407         "                       nstates, nstates_put);",
1408         "               dfs_phase2 = 1;",
1409         "       }",
1410         "       Read_Queue(core_id);    /* all cores */",
1411         "",
1412         "       if (verbose)",
1413         "       {       cpu_printf(\"put %%6d states into queue -- got %%6d\\n\",",
1414         "                       nstates_put, nstates_get);",
1415         "       }",
1416         "       if (proxy_pid != 0)",
1417         "       {       rm_shared_segments();",
1418         "       }",
1419         "       done = 1;",
1420         "       wrapup();",
1421         "       exit(0);",
1422         "}",
1423         "",
1424         "#else",
1425         "int unpack_state(SM_frame *, int);",
1426         "#endif",
1427         "",
1428         "H_el *",
1429         "grab_shared(int n)",
1430         "{",
1431         "#ifndef SEP_STATE",
1432         "       char *rval = (char *) 0;",
1433         "",
1434         "       if (n == 0)",
1435         "       {       printf(\"cpu%%d: grab shared zero\\n\", core_id); fflush(stdout);",
1436         "               return (H_el *) rval;",
1437         "       } else if (n&(sizeof(void *)-1))",
1438         "       {       n += sizeof(void *)-(n&(sizeof(void *)-1)); /* alignment */",
1439         "       }",
1440         "",
1441         "#ifdef SEP_HEAP",
1442         "       /* no locking */",
1443         "       if (my_heap != NULL && my_size > n)",
1444         "       {       rval = my_heap;",
1445         "               my_heap += n;",
1446         "               my_size -= n;",
1447         "               goto done;",
1448         "       }",
1449         "#endif",
1450         "",
1451         "       if (!dc_shared)",
1452         "       {       sudden_stop(\"pan: out of memory\");",
1453         "       }",
1454         "",
1455         "       /* another lock is always already in effect when this is called */",
1456         "       /* but not always the same lock -- i.e., on different parts of the hashtable */",
1457         "       enter_critical(GLOBAL_LOCK);    /* this must be independently mutex */",
1458         "#if defined(SEP_HEAP) && !defined(WIN32) && !defined(WIN64)",
1459         "       {       static int noted = 0;",
1460         "               if (!noted)",
1461         "               {       noted = 1;",
1462         "                       printf(\"cpu%%d: global heap has %%ld bytes left, needed %%d\\n\",",
1463         "                               core_id, dc_shared?dc_shared->dc_size:0, n);",
1464         "       }       }",
1465         "#endif",
1466         "#if 0",        /* for debugging */
1467         "               if (dc_shared->pattern != 1234567)",
1468         "               {       leave_critical(GLOBAL_LOCK);",
1469         "                       Uerror(\"overrun -- memory corruption\");",
1470         "               }",
1471         "#endif",
1472         "               if (dc_shared->dc_size < n)",
1473         "               {       if (verbose)",
1474         "                       { printf(\"Next Pool %%g Mb + %%d\\n\", memcnt/(1048576.), n);",
1475         "                       }",
1476         "                       if (dc_shared->nxt == NULL",
1477         "                       ||  dc_shared->nxt->dc_arena == NULL",
1478         "                       ||  dc_shared->nxt->dc_size < n)",
1479         "                       {       printf(\"cpu%%d: memcnt %%g Mb + wanted %%d bytes more\\n\",",
1480         "                                       core_id, memcnt / (1048576.), n);",
1481         "                               leave_critical(GLOBAL_LOCK);",
1482         "                               sudden_stop(\"out of memory -- aborting\");",
1483         "                               wrapup();       /* exits */",
1484         "                       } else",
1485         "                       {       dc_shared = (sh_Allocater *) dc_shared->nxt;",
1486         "               }       }",
1487         "",
1488         "               rval = (char *) dc_shared->dc_arena;",
1489         "               dc_shared->dc_arena += n;",
1490         "               dc_shared->dc_size  -= (long) n;",
1491         "#if 0",
1492         "               if (VVERBOSE)",
1493         "               printf(\"cpu%%d grab shared (%%d bytes) -- %%ld left\\n\",",
1494         "                       core_id, n, dc_shared->dc_size);",
1495         "#endif",
1496         "       leave_critical(GLOBAL_LOCK);",
1497         "done:",
1498         "       memset(rval, 0, n);",
1499         "       memcnt += (double) n;",
1500         "",
1501         "       return (H_el *) rval;",
1502         "#else",
1503         "       return (H_el *) emalloc(n);",
1504         "#endif",
1505         "}",
1506         "",
1507         "SM_frame *",
1508         "Get_Full_Frame(int n)",
1509         "{      SM_frame *f;",
1510         "       double cnt_start = frame_wait;",
1511         "",
1512         "       f = &m_workq[n][prfull[n]];",
1513         "       while (f->m_vsize == 0) /* await full slot LOCK : full frame */",
1514         "       {       iam_alive();",
1515         "#ifndef NGQ",
1516         "       #ifndef SAFETY",
1517         "               if (!a_cycles || core_id != 0)",
1518         "       #endif",
1519         "               if (*grcnt > 0) /* accessed outside lock, but safe even if wrong */",
1520         "               {       enter_critical(GQ_RD);  /* gq - read access */",
1521         "                       if (*grcnt > 0)         /* could have changed */",
1522         "                       {       f = &m_workq[NCORE][*grfull];   /* global q */",
1523         "                               if (f->m_vsize == 0)",
1524         "                               {       /* writer is still filling the slot */",
1525         "                                       *gr_writemiss++;",
1526         "                                       f = &m_workq[n][prfull[n]]; /* reset */",
1527         "                               } else",
1528         "                               {       *grfull = (*grfull+1) %% (GN_FRAMES);",
1529         "                                               enter_critical(GQ_WR);",
1530         "                                               *grcnt = *grcnt - 1;",
1531         "                                               leave_critical(GQ_WR);",
1532         "                                       leave_critical(GQ_RD);",
1533         "                                       return f;",
1534         "                       }       }",
1535         "                       leave_critical(GQ_RD);",
1536         "               }",
1537         "#endif",
1538         "               if (frame_wait++ - cnt_start > Delay)",
1539         "               {       if (0)", /* too frequent to enable this one */
1540         "                       {       cpu_printf(\"timeout on q%%d -- %%u -- query %%d\\n\",",
1541         "                                       n, f, query_in_progress);",
1542         "                       }",
1543         "                       return (SM_frame *) 0;  /* timeout */",
1544         "       }       }",
1545         "       iam_alive();",
1546         "       if (VVERBOSE) cpu_printf(\"got frame from q%%d\\n\", n);",
1547         "       prfull[n] = (prfull[n] + 1) %% (LN_FRAMES);",
1548         "       enter_critical(QLOCK(n));",
1549         "               prcnt[n]--; /* lock out increments */",
1550         "       leave_critical(QLOCK(n));",
1551         "       return f;",
1552         "}",
1553         "",
1554         "SM_frame *",
1555         "Get_Free_Frame(int n)",
1556         "{      SM_frame *f;",
1557         "       double cnt_start = free_wait;",
1558         "",
1559         "       if (VVERBOSE) { cpu_printf(\"get free frame from q%%d\\n\", n); }",
1560         "",
1561         "       if (n == NCORE) /* global q */",
1562         "       {       f = &(m_workq[n][lrfree]);",
1563         "       } else",
1564         "       {       f = &(m_workq[n][prfree[n]]);",
1565         "       }",
1566         "       while (f->m_vsize != 0) /* await free slot LOCK : free slot */",
1567         "       {       iam_alive();",
1568         "               if (free_wait++ - cnt_start > OneSecond)",
1569         "               {       if (verbose)",
1570         "                       {       cpu_printf(\"timeout waiting for free slot q%%d\\n\", n);",
1571         "                       }",
1572         "                       cnt_start = free_wait;",
1573         "                       if (someone_crashed(1))",
1574         "                       {       printf(\"cpu%%d: search terminated\\n\", core_id);",
1575         "                               sudden_stop(\"get free frame\");",
1576         "                               pan_exit(1);",
1577         "       }       }       }",
1578         "       if (n != NCORE)",
1579         "       {       prfree[n] = (prfree[n] + 1) %% (LN_FRAMES);",
1580         "               enter_critical(QLOCK(n));",
1581         "                       prcnt[n]++; /* lock out decrements */",
1582         "                       if (prmax[n] < prcnt[n])",
1583         "                       {       prmax[n] = prcnt[n];",
1584         "                       }",
1585         "               leave_critical(QLOCK(n));",
1586         "       }",
1587         "       return f;",
1588         "}",
1589         "",
1590         "#ifndef NGQ",
1591         "int",
1592         "GlobalQ_HasRoom(void)",
1593         "{      int rval = 0;",
1594         "",
1595         "       gq_tries++;",
1596         "       if (*grcnt < GN_FRAMES) /* there seems to be room */",
1597         "       {       enter_critical(GQ_WR);  /* gq write access */",
1598         "               if (*grcnt < GN_FRAMES)",
1599         "               {       if (m_workq[NCORE][*grfree].m_vsize != 0)",
1600         "                       {       /* can happen if reader is slow emptying slot */",
1601         "                               *gr_readmiss++;",
1602         "                               goto out; /* dont wait: release lock and return */",
1603         "                       }",
1604         "                       lrfree = *grfree;       /* Get_Free_Frame use lrfree in this mode */",
1605         "                       *grfree = (*grfree + 1) %% GN_FRAMES;", /* next process looks at next slot */
1606         "                       *grcnt = *grcnt + 1;    /* count nr of slots filled -- no additional lock needed */",
1607         "                       if (*grmax < *grcnt) *grmax = *grcnt;",
1608         "                       leave_critical(GQ_WR);  /* for short lock duration */",
1609         "                       gq_hasroom++;",
1610         "                       mem_put(NCORE);         /* copy state into reserved slot */",
1611         "                       rval = 1;               /* successfull handoff */",
1612         "               } else",
1613         "               {       gq_hasnoroom++;",
1614         "out:                   leave_critical(GQ_WR);",        /* should be rare */
1615         "       }       }",
1616         "       return rval;",
1617         "}",
1618         "#endif",
1619         "",
1620         "int",
1621         "unpack_state(SM_frame *f, int from_q)",
1622         "{      int i, j;",
1623         "       static H_el D_State;",
1624         "",
1625         "       if (f->m_vsize > 0)",
1626         "       {       boq   = f->m_boq;",
1627         "               if (boq > 256)",
1628         "               {       cpu_printf(\"saw control %%d, expected state\\n\", boq);",
1629         "                       return 0;",
1630         "               }",
1631         "               vsize = f->m_vsize;",
1632         "correct:",
1633         "               memcpy((uchar *) &now, (uchar *) f->m_now, vsize);",
1634         "       #if !defined(NOCOMP) && !defined(HC)",
1635         "               for (i = j = 0; i < VMAX; i++, j = (j+1)%%8)",
1636         "               {       Mask[i] = (f->m_mask[i/8] & (1<<j)) ? 1 : 0;",
1637         "               }",
1638         "       #endif",
1639         "               if (now._nr_pr > 0)",
1640         "               {       memcpy((uchar *) proc_offset, (uchar *) f->m_p_offset, now._nr_pr * sizeof(OFFT));",
1641         "                       memcpy((uchar *) proc_skip,   (uchar *) f->m_p_skip,   now._nr_pr * sizeof(uchar));",
1642         "               }",
1643         "               if (now._nr_qs > 0)",
1644         "               {       memcpy((uchar *) q_offset,    (uchar *) f->m_q_offset, now._nr_qs * sizeof(OFFT));",
1645         "                       memcpy((uchar *) q_skip,      (uchar *) f->m_q_skip,   now._nr_qs * sizeof(uchar));",
1646         "               }",
1647         "#ifndef NOVSZ",
1648         "               if (vsize != now._vsz)",
1649         "               {       cpu_printf(\"vsize %%d != now._vsz %%d (type %%d) %%d\\n\",",
1650         "                               vsize, now._vsz, f->m_boq, f->m_vsize);",
1651         "                       vsize = now._vsz;",
1652         "                       goto correct;   /* rare event: a race */",
1653         "               }",
1654         "#endif",
1655         "               hmax = max(hmax, vsize);",
1656         "",
1657         "               if (f != &cur_Root)",
1658         "               {       memcpy((uchar *) &cur_Root, (uchar *) f, sizeof(SM_frame));",
1659         "               }",
1660         "",
1661         "               if (((now._a_t) & 1) == 1)      /* i.e., when starting nested DFS */",
1662         "               {       A_depth = depthfound = 0;",
1663         "                       memcpy((uchar *)&A_Root, (uchar *)&now, vsize);",
1664         "               }",
1665         "               nr_handoffs = f->nr_handoffs;",
1666         "       } else",
1667         "       {       cpu_printf(\"pan: state empty\\n\");",
1668         "       }",
1669         "",
1670         "       depth = 0;",
1671         "       trpt = &trail[1];",
1672         "       trpt->tau    = f->m_tau;",
1673         "       trpt->o_pm   = f->m_o_pm;",
1674         "",
1675         "       (trpt-1)->ostate = &D_State; /* stub */",
1676         "       trpt->ostate = &D_State;",
1677         "",
1678         "#ifdef FULL_TRAIL",
1679         "       if (upto > 0)",
1680         "       {       stack_last[core_id] = (Stack_Tree *) f->m_stack;",
1681         "       }",
1682         "       #if defined(VERBOSE)",
1683         "       if (stack_last[core_id])",
1684         "       {       cpu_printf(\"%%d: UNPACK -- SET m_stack %%u (%%d,%%d)\\n\",",
1685         "                       depth, stack_last[core_id], stack_last[core_id]->pr,",
1686         "                       stack_last[core_id]->t_id);",
1687         "       }",
1688         "       #endif",
1689         "#endif",
1690         "",
1691         "       if (!trpt->o_t)",
1692         "       {       static Trans D_Trans;",
1693         "               trpt->o_t = &D_Trans;",
1694         "       }",
1695         "",
1696         "       #ifdef VERI",
1697         "       if ((trpt->tau & 4) != 4)",
1698         "       {       trpt->tau |= 4; /* the claim moves first */",
1699         "               cpu_printf(\"warning: trpt was not up to date\\n\");",
1700         "       }",
1701         "       #endif",
1702         "",
1703         "       for (i = 0; i < (int) now._nr_pr; i++)",
1704         "       {       P0 *ptr = (P0 *) pptr(i);",
1705         "       #ifndef NP",
1706         "               if (accpstate[ptr->_t][ptr->_p])",
1707         "               {       trpt->o_pm |= 2;",
1708         "               }",
1709         "       #else",
1710         "               if (progstate[ptr->_t][ptr->_p])",
1711         "               {       trpt->o_pm |= 4;",
1712         "               }",
1713         "       #endif",
1714         "       }",
1715         "",
1716         "       #ifdef EVENT_TRACE",
1717         "               #ifndef NP",
1718         "                       if (accpstate[EVENT_TRACE][now._event])",
1719         "                       {       trpt->o_pm |= 2;",
1720         "                       }",
1721         "               #else",
1722         "                       if (progstate[EVENT_TRACE][now._event])",
1723         "                       {       trpt->o_pm |= 4;",
1724         "                       }",
1725         "               #endif",
1726         "       #endif",
1727         "",
1728         "       #if defined(C_States) && (HAS_TRACK==1)",
1729         "               /* restore state of tracked C objects */",
1730         "               c_revert((uchar *) &(now.c_state[0]));",
1731         "               #if (HAS_STACK==1)",
1732         "               c_unstack((uchar *) f->m_c_stack); /* unmatched tracked data */",
1733         "               #endif",
1734         "       #endif",
1735         "       return 1;",
1736         "}",
1737         "",
1738         "void",
1739         "write_root(void)       /* for trail file */",
1740         "{      int fd;",
1741         "",
1742         "       if (iterative == 0 && Nr_Trails > 1)",
1743         "               sprintf(fnm, \"%%s%%d.%%s\", TrailFile, Nr_Trails-1, sprefix);",
1744         "       else",
1745         "               sprintf(fnm, \"%%s.%%s\", TrailFile, sprefix);",
1746         "",
1747         "       if (cur_Root.m_vsize == 0)",
1748         "       {       (void) unlink(fnm); /* remove possible old copy */",
1749         "               return; /* its the default initial state */",
1750         "       }",
1751         "",
1752         "       if ((fd = creat(fnm, TMODE)) < 0)",
1753         "       {       char *q;",
1754         "               if ((q = strchr(TrailFile, \'.\')))",
1755         "               {       *q = \'\\0\';           /* strip .pml */",
1756         "                       if (iterative == 0 && Nr_Trails-1 > 0)",
1757         "                               sprintf(fnm, \"%%s%%d.%%s\", TrailFile, Nr_Trails-1, sprefix);",
1758         "                       else",
1759         "                               sprintf(fnm, \"%%s.%%s\", TrailFile, sprefix);",
1760         "                       *q = \'.\';",
1761         "                       fd = creat(fnm, TMODE);",
1762         "               }",
1763         "               if (fd < 0)",
1764         "               {       cpu_printf(\"pan: cannot create %%s\\n\", fnm);",
1765         "                       perror(\"cause\");",
1766         "                       return;",
1767         "       }       }",
1768         "",
1769         "       if (write(fd, &cur_Root, sizeof(SM_frame)) != sizeof(SM_frame))",
1770         "       {       cpu_printf(\"pan: error writing %%s\\n\", fnm);",
1771         "       } else",
1772         "       {       cpu_printf(\"pan: wrote %%s\\n\", fnm);",
1773         "       }",
1774         "       close(fd);",
1775         "}",
1776         "",
1777         "void",
1778         "set_root(void)",
1779         "{      int fd;",
1780         "       char *q;",
1781         "       char MyFile[512];",     /* enough to hold a reasonable pathname */
1782         "       char MySuffix[16];",
1783         "       char *ssuffix = \"rst\";",
1784         "       int  try_core = 1;",
1785         "",
1786         "       strcpy(MyFile, TrailFile);",
1787         "try_again:",
1788         "       if (whichtrail > 0)",
1789         "       {       sprintf(fnm, \"%%s%%d.%%s\", MyFile, whichtrail, ssuffix);",
1790         "               fd = open(fnm, O_RDONLY, 0);",
1791         "               if (fd < 0 && (q = strchr(MyFile, \'.\')))",
1792         "               {       *q = \'\\0\';   /* strip .pml */",
1793         "                       sprintf(fnm, \"%%s%%d.%%s\", MyFile, whichtrail, ssuffix);",
1794         "                       *q = \'.\';",
1795         "                       fd = open(fnm, O_RDONLY, 0);",
1796         "               }",
1797         "       } else",
1798         "       {       sprintf(fnm, \"%%s.%%s\", MyFile, ssuffix);",
1799         "               fd = open(fnm, O_RDONLY, 0);",
1800         "               if (fd < 0 && (q = strchr(MyFile, \'.\')))",
1801         "               {       *q = \'\\0\';   /* strip .pml */",
1802         "                       sprintf(fnm, \"%%s.%%s\", MyFile, ssuffix);",
1803         "                       *q = \'.\';",
1804         "                       fd = open(fnm, O_RDONLY, 0);",
1805         "       }       }",
1806         "",
1807         "       if (fd < 0)",
1808         "       {       if (try_core < NCORE)",
1809         "               {       ssuffix = MySuffix;",
1810         "                       sprintf(ssuffix, \"cpu%%d_rst\", try_core++);",
1811         "                       goto try_again;",
1812         "               }",
1813         "               cpu_printf(\"no file '%%s.rst' or '%%s' (not an error)\\n\", MyFile, fnm);",
1814         "       } else",
1815         "       {       if (read(fd, &cur_Root, sizeof(SM_frame)) != sizeof(SM_frame))",
1816         "               {       cpu_printf(\"read error %%s\\n\", fnm);",
1817         "                       close(fd);",
1818         "                       pan_exit(1);",
1819         "               }",
1820         "               close(fd);",
1821         "               (void) unpack_state(&cur_Root, -2);",
1822         "#ifdef SEP_STATE",
1823         "               cpu_printf(\"partial trail -- last few steps only\\n\");",
1824         "#endif",
1825         "               cpu_printf(\"restored root from '%%s'\\n\", fnm);",
1826         "               printf(\"=====State:=====\\n\");",
1827         "               {       int i, j; P0 *z;",
1828         "                       for (i = 0; i < now._nr_pr; i++)",
1829         "                       {       z = (P0 *)pptr(i);",
1830         "                               printf(\"proc %%2d (%%s) \", i, procname[z->_t]);",
1831
1832         "                               for (j = 0; src_all[j].src; j++)",
1833         "                               if (src_all[j].tp == (int) z->_t)",
1834         "                               {       printf(\" %%s:%%d \",",
1835         "                                               PanSource, src_all[j].src[z->_p]);",
1836         "                                       break;",
1837         "                               }",
1838         "                               printf(\"(state %%d)\\n\", z->_p);",
1839         "                               c_locals(i, z->_t);",
1840         "                       }",
1841         "                       c_globals();",
1842         "               }",
1843         "               printf(\"================\\n\");",
1844         "       }",
1845         "}",
1846         "",
1847         "#ifdef USE_DISK",
1848         "unsigned long dsk_written, dsk_drained;",
1849         "void mem_drain(void);",
1850         "#endif",
1851         "",
1852         "void",
1853         "m_clear_frame(SM_frame *f)", /* clear room for stats */
1854         "{      int i, clr_sz = sizeof(SM_results);",
1855         "",
1856         "       for (i = 0; i <= _NP_; i++)     /* all proctypes */",
1857         "       {       clr_sz += NrStates[i]*sizeof(uchar);",
1858         "       }",
1859         "       memset(f, 0, clr_sz);",
1860         "       /* caution if sizeof(SM_results) > sizeof(SM_frame) */",
1861         "}",
1862         "",
1863         "#define TargetQ_Full(n)        (m_workq[n][prfree[n]].m_vsize != 0)", /* no free slot */
1864         "#define TargetQ_NotFull(n)     (m_workq[n][prfree[n]].m_vsize == 0)", /* avoiding prcnt */
1865         "",
1866         "int",
1867         "AllQueuesEmpty(void)",
1868         "{      int q;",
1869         "#ifndef NGQ",
1870         "       if (*grcnt != 0)",
1871         "       {       return 0;",
1872         "       }",
1873         "#endif",
1874         "       for (q = 0; q < NCORE; q++)",
1875         "       {       if (prcnt[q] != 0)", /* not locked, ok if race */
1876         "               {       return 0;",
1877         "       }       }",
1878         "       return 1;",
1879         "}",
1880         "",
1881         "void",
1882         "Read_Queue(int q)",
1883         "{      SM_frame   *f, *of;",
1884         "       int     remember, target_q;",
1885         "       SM_results *r;",
1886         "       double patience = 0.0;",
1887         "",
1888         "       target_q = (q + 1) %% NCORE;",
1889         "",
1890         "       for (;;)",
1891         "       {       f = Get_Full_Frame(q);",
1892         "               if (!f) /* 1 second timeout -- and trigger for Query */",
1893         "               {       if (someone_crashed(2))",
1894         "                       {       printf(\"cpu%%d: search terminated [code %%d]\\n\",",
1895         "                                       core_id, search_terminated?*search_terminated:-1);",
1896         "                               sudden_stop(\"\");",
1897         "                               pan_exit(1);",
1898         "                       }",
1899         "#ifdef TESTING",
1900         "       /* to profile with cc -pg and gprof pan.exe -- set handoff depth beyond maxdepth */",
1901         "                       exit(0);",
1902         "#endif",
1903         "                       remember = *grfree;",
1904         "                       if (core_id == 0                /* root can initiate termination */",
1905         "                       && remote_party == 0            /* and only the original root */",
1906         "                       && query_in_progress == 0       /* unless its already in progress */",
1907         "                       && AllQueuesEmpty())",
1908         "                       {       f = Get_Free_Frame(target_q);",
1909         "                               query_in_progress = 1;  /* only root process can do this */",
1910         "                               if (!f) { Uerror(\"Fatal1: no free slot\"); }",
1911         "                               f->m_boq = QUERY;       /* initiate Query */",
1912         "                               if (verbose)",
1913         "                               {  cpu_printf(\"snd QUERY to q%%d (%%d) into slot %%d\\n\",",
1914         "                                       target_q, nstates_get + 1, prfree[target_q]-1);",
1915         "                               }",
1916         "                               f->m_vsize = remember + 1;",
1917         "                               /* number will not change unless we receive more states */",
1918         "                       } else if (patience++ > OneHour) /* one hour watchdog timer */",
1919         "                       {       cpu_printf(\"timeout -- giving up\\n\");",
1920         "                               sudden_stop(\"queue timeout\");",
1921         "                               pan_exit(1);",
1922         "                       }",
1923         "                       if (0) cpu_printf(\"timed out -- try again\\n\");",
1924         "                       continue;       ",
1925         "               }",
1926         "               patience = 0.0; /* reset watchdog */",
1927         "",
1928         "               if (f->m_boq == QUERY)",
1929         "               {       if (verbose)",
1930         "                       {       cpu_printf(\"got QUERY on q%%d (%%d <> %%d) from slot %%d\\n\",",
1931         "                                       q, f->m_vsize, nstates_put + 1, prfull[q]-1);",
1932         "                               snapshot();",
1933         "                       }",
1934         "                       remember = f->m_vsize;",
1935         "                       f->m_vsize = 0; /* release slot */",
1936         "",
1937         "                       if (core_id == 0 && remote_party == 0)  /* original root cpu0 */",
1938         "                       {       if (query_in_progress == 1      /* didn't send more states in the interim */",
1939         "                               &&  *grfree + 1 == remember)    /* no action on global queue meanwhile */",
1940         "                               {       if (verbose) cpu_printf(\"Termination detected\\n\");",
1941         "                                       if (TargetQ_Full(target_q))",
1942         "                                       {       if (verbose)",
1943         "                                               cpu_printf(\"warning: target q is full\\n\");",
1944         "                                       }",
1945         "                                       f = Get_Free_Frame(target_q);",
1946         "                                       if (!f) { Uerror(\"Fatal2: no free slot\"); }",
1947         "                                       m_clear_frame(f);",
1948         "                                       f->m_boq = QUIT; /* send final Quit, collect stats */",
1949         "                                       f->m_vsize = 111; /* anything non-zero will do */",
1950         "                                       if (verbose)",
1951         "                                       cpu_printf(\"put QUIT on q%%d\\n\", target_q);",
1952         "                               } else",
1953         "                               {       if (verbose) cpu_printf(\"Stale Query\\n\");",
1954         "#ifdef USE_DISK",
1955         "                                       mem_drain();",
1956         "#endif",
1957         "                               }",
1958         "                               query_in_progress = 0;",
1959         "                       } else",
1960         "                       {       if (TargetQ_Full(target_q))",
1961         "                               {       if (verbose)",
1962         "                                       cpu_printf(\"warning: forward query - target q full\\n\");",
1963         "                               }",
1964         "                               f = Get_Free_Frame(target_q);",
1965         "                               if (verbose)",
1966         "                               cpu_printf(\"snd QUERY response to q%%d (%%d <> %%d) in slot %%d\\n\",",
1967         "                                       target_q, remember, *grfree + 1, prfree[target_q]-1);",
1968         "                               if (!f) { Uerror(\"Fatal4: no free slot\"); }",
1969         "",
1970         "                               if (*grfree + 1 == remember)    /* no action on global queue */",
1971         "                               {       f->m_boq = QUERY;       /* forward query, to root */",
1972         "                                       f->m_vsize = remember;",
1973         "                               } else",
1974         "                               {       f->m_boq = QUERY_F;     /* no match -- busy */",
1975         "                                       f->m_vsize = 112;       /* anything non-zero */",
1976         "#ifdef USE_DISK",
1977         "                                       if (dsk_written != dsk_drained)",
1978         "                                       {       mem_drain();",
1979         "                                       }",
1980         "#endif",
1981         "                       }       }",
1982         "                       continue;",
1983         "               }",
1984         "",
1985         "               if (f->m_boq == QUERY_F)",
1986         "               {       if (verbose)",
1987         "                       {       cpu_printf(\"got QUERY_F on q%%d from slot %%d\\n\", q, prfull[q]-1);",
1988         "                       }",
1989         "                       f->m_vsize = 0; /* release slot */",
1990         "",
1991         "                       if (core_id == 0 && remote_party == 0)          /* original root cpu0 */",
1992         "                       {       if (verbose) cpu_printf(\"No Match on Query\\n\");",
1993         "                               query_in_progress = 0;",
1994         "                       } else",
1995         "                       {       if (TargetQ_Full(target_q))",
1996         "                               {       if (verbose) cpu_printf(\"warning: forwarding query_f, target queue full\\n\");",
1997         "                               }",
1998         "                               f = Get_Free_Frame(target_q);",
1999         "                               if (verbose) cpu_printf(\"forward QUERY_F to q%%d into slot %%d\\n\",",
2000         "                                               target_q, prfree[target_q]-1);",
2001         "                               if (!f) { Uerror(\"Fatal5: no free slot\"); }",
2002         "                               f->m_boq = QUERY_F;             /* cannot terminate yet */",
2003         "                               f->m_vsize = 113;               /* anything non-zero */",
2004         "                       }",
2005         "#ifdef USE_DISK",
2006         "                       if (dsk_written != dsk_drained)",
2007         "                       {       mem_drain();",
2008         "                       }",
2009         "#endif",
2010         "                       continue;",
2011         "               }",
2012         "",
2013         "               if (f->m_boq == QUIT)",
2014         "               {       if (0) cpu_printf(\"done -- local memcnt %%g Mb\\n\", memcnt/(1048576.));",
2015         "                       retrieve_info((SM_results *) f); /* collect and combine stats */",
2016         "                       if (verbose)",
2017         "                       {       cpu_printf(\"received Quit\\n\");",
2018         "                               snapshot();",
2019         "                       }",
2020         "                       f->m_vsize = 0; /* release incoming slot */",
2021         "                       if (core_id != 0)",
2022         "                       {       f = Get_Free_Frame(target_q); /* new outgoing slot */",
2023         "                               if (!f) { Uerror(\"Fatal6: no free slot\"); }",
2024         "                               m_clear_frame(f);       /* start with zeroed stats */",
2025         "                               record_info((SM_results *) f);",
2026         "                               f->m_boq = QUIT;        /* forward combined results */",
2027         "                               f->m_vsize = 114;       /* anything non-zero */",
2028         "                               if (verbose>1)",
2029         "                               cpu_printf(\"fwd Results to q%%d\\n\", target_q);",
2030         "                       }",
2031         "                       break;                  /* successful termination */",
2032         "               }",
2033         "",
2034         "               /* else: 0<= boq <= 255, means STATE transfer */",
2035         "               if (unpack_state(f, q) != 0)",
2036         "               {       nstates_get++;",
2037         "                       f->m_vsize = 0; /* release slot */",
2038         "                       if (VVERBOSE) cpu_printf(\"Got state\\n\");",
2039         "",
2040         "                       if (search_terminated != NULL",
2041         "                       &&  *search_terminated == 0)",
2042         "                       {       new_state();    /* explore successors */",
2043         "                               memset((uchar *) &cur_Root, 0, sizeof(SM_frame));       /* avoid confusion */",
2044         "                       } else",
2045         "                       {       pan_exit(0);",
2046         "                       }",
2047         "               } else",
2048         "               {       pan_exit(0);",
2049         "       }       }",
2050         "       if (verbose) cpu_printf(\"done got %%d put %%d\\n\", nstates_get, nstates_put);",
2051         "       sleep_report();",
2052         "}",
2053         "",
2054         "void",
2055         "give_up(int unused_x)",
2056         "{",
2057         "       if (search_terminated != NULL)",
2058         "       {       *search_terminated |= 32;       /* give_up */",
2059         "       }",
2060         "       if (!writing_trail)",
2061         "       {       was_interrupted = 1;",
2062         "               snapshot();",
2063         "               cpu_printf(\"Give Up\\n\");",
2064         "               sleep_report();",
2065         "               pan_exit(1);",
2066         "       } else /* we are already terminating */",
2067         "       {       cpu_printf(\"SIGINT\\n\");",
2068         "       }",
2069         "}",
2070         "",
2071         "void",
2072         "check_overkill(void)",
2073         "{",
2074         "       vmax_seen = (vmax_seen + 7)/ 8;",
2075         "       vmax_seen *= 8; /* round up to a multiple of 8 */",
2076         "",
2077         "       if (core_id == 0",
2078         "       &&  !remote_party",
2079         "       &&  nstates_put > 0",
2080         "       &&  VMAX - vmax_seen > 8)",
2081         "       {",
2082         "#ifdef BITSTATE",
2083         "               printf(\"cpu0: max VMAX value seen in this run: \");",
2084         "#else",
2085         "               printf(\"cpu0: recommend recompiling with \");",
2086         "#endif",
2087         "               printf(\"-DVMAX=%%d\\n\", vmax_seen);",
2088         "       }",
2089         "}",
2090         "",
2091         "void",
2092         "mem_put(int q) /* handoff state to other cpu, workq q */",
2093         "{      SM_frame *f;",
2094         "       int i, j;",
2095         "",
2096         "       if (vsize > VMAX)",
2097         "       {       vsize = (vsize + 7)/8; vsize *= 8; /* round up */",
2098         "               printf(\"pan: recompile with -DVMAX=N with N >= %%d\\n\", (int) vsize);",
2099         "               Uerror(\"aborting\");",
2100         "       }",
2101         "       if (now._nr_pr > PMAX)",
2102         "       {       printf(\"pan: recompile with -DPMAX=N with N >= %%d\\n\", now._nr_pr);",
2103         "               Uerror(\"aborting\");",
2104         "       }",
2105         "       if (now._nr_qs > QMAX)",
2106         "       {       printf(\"pan: recompile with -DQMAX=N with N >= %%d\\n\", now._nr_qs);",
2107         "               Uerror(\"aborting\");",
2108         "       }",
2109         "       if (vsize > vmax_seen) vmax_seen = vsize;",
2110         "       if (now._nr_pr > pmax_seen) pmax_seen = now._nr_pr;",
2111         "       if (now._nr_qs > qmax_seen) qmax_seen = now._nr_qs;",
2112         "",
2113         "       f = Get_Free_Frame(q);  /* not called in likely deadlock states */",
2114         "       if (!f) { Uerror(\"Fatal3: no free slot\"); }",
2115         "",
2116         "       if (VVERBOSE) cpu_printf(\"putting state into q%%d\\n\", q);",
2117         "",
2118         "       memcpy((uchar *) f->m_now,  (uchar *) &now, vsize);",
2119         "#if !defined(NOCOMP) && !defined(HC)",
2120         "       memset((uchar *) f->m_mask, 0, (VMAX+7)/8 * sizeof(char));",
2121         "       for (i = j = 0; i < VMAX; i++, j = (j+1)%%8)",
2122         "       {       if (Mask[i])",
2123         "               {       f->m_mask[i/8] |= (1<<j);",
2124         "       }       }",
2125         "#endif",
2126         "       if (now._nr_pr > 0)",
2127         "       { memcpy((uchar *) f->m_p_offset, (uchar *) proc_offset, now._nr_pr * sizeof(OFFT));",
2128         "         memcpy((uchar *) f->m_p_skip,   (uchar *) proc_skip,   now._nr_pr * sizeof(uchar));",
2129         "       }",
2130         "       if (now._nr_qs > 0)",
2131         "       { memcpy((uchar *) f->m_q_offset, (uchar *) q_offset, now._nr_qs * sizeof(OFFT));",
2132         "         memcpy((uchar *) f->m_q_skip,   (uchar *) q_skip,   now._nr_qs * sizeof(uchar));",
2133         "       }",
2134         "#if defined(C_States) && (HAS_TRACK==1) && (HAS_STACK==1)",
2135         "       c_stack((uchar *) f->m_c_stack); /* save unmatched tracked data */",
2136         "#endif",
2137         "#ifdef FULL_TRAIL",
2138         "       f->m_stack = stack_last[core_id];",
2139         "#endif",
2140         "       f->nr_handoffs = nr_handoffs+1;",
2141         "       f->m_tau    = trpt->tau;",
2142         "       f->m_o_pm   = trpt->o_pm;",
2143         "       f->m_boq    = boq;",
2144         "       f->m_vsize  = vsize;    /* must come last - now the other cpu can see it */",
2145         "",
2146         "       if (query_in_progress == 1)",
2147         "               query_in_progress = 2;  /* make sure we know, if a query makes the rounds */",
2148         "       nstates_put++;",
2149         "}",
2150         "",
2151         "#ifdef USE_DISK",
2152         "int Dsk_W_Nr, Dsk_R_Nr;",
2153         "int dsk_file = -1, dsk_read = -1;",
2154         "unsigned long dsk_written, dsk_drained;",
2155         "char dsk_name[512];",
2156         "",
2157         "#ifndef BFS_DISK",
2158         "#if defined(WIN32) || defined(WIN64)",
2159         "       #define RFLAGS  (O_RDONLY|O_BINARY)",
2160         "       #define WFLAGS  (O_CREAT|O_WRONLY|O_TRUNC|O_BINARY)",
2161         "#else",
2162         "       #define RFLAGS  (O_RDONLY)",
2163         "       #define WFLAGS  (O_CREAT|O_WRONLY|O_TRUNC)",
2164         "#endif",
2165         "#endif",
2166         "",
2167         "void",
2168         "dsk_stats(void)",
2169         "{      int i;",
2170         "",
2171         "       if (dsk_written > 0)",
2172         "       {       cpu_printf(\"dsk_written %%d states in %%d files\\ncpu%%d: dsk_drained %%6d states\\n\",",
2173         "                       dsk_written, Dsk_W_Nr, core_id, dsk_drained);",
2174         "               close(dsk_read);",
2175         "               close(dsk_file);",
2176         "               for (i = 0; i < Dsk_W_Nr; i++)",
2177         "               {       sprintf(dsk_name, \"Q%%.3d_%%.3d.tmp\", i, core_id);",
2178         "                       unlink(dsk_name);",
2179         "       }       }",
2180         "}",
2181         "",
2182         "void",
2183         "mem_drain(void)",
2184         "{      SM_frame *f, g;",
2185         "       int q = (core_id + 1) %% NCORE; /* target q */",
2186         "       int sz;",
2187         "",
2188         "       if (dsk_read < 0",
2189         "       ||  dsk_written <= dsk_drained)",
2190         "       {       return;",
2191         "       }",
2192         "",
2193         "       while (dsk_written > dsk_drained",
2194         "       && TargetQ_NotFull(q))",
2195         "       {       f = Get_Free_Frame(q);",
2196         "               if (!f) { Uerror(\"Fatal: unhandled condition\"); }",
2197         "",
2198         "               if ((dsk_drained+1)%%MAX_DSK_FILE == 0) /* 100K states max per file */",
2199         "               {       (void) close(dsk_read);         /* close current read handle */",
2200         "                       sprintf(dsk_name, \"Q%%.3d_%%.3d.tmp\", Dsk_R_Nr++, core_id);",
2201         "                       (void) unlink(dsk_name);        /* remove current file */",
2202         "                       sprintf(dsk_name, \"Q%%.3d_%%.3d.tmp\", Dsk_R_Nr, core_id);",
2203         "                       cpu_printf(\"reading %%s\\n\", dsk_name);",
2204         "                       dsk_read = open(dsk_name, RFLAGS); /* open next file */",
2205         "                       if (dsk_read < 0)",
2206         "                       {       Uerror(\"could not open dsk file\");",
2207         "               }       }",
2208         "               if (read(dsk_read, &g, sizeof(SM_frame)) != sizeof(SM_frame))",
2209         "               {       Uerror(\"bad dsk file read\");",
2210         "               }",
2211         "               sz = g.m_vsize;",
2212         "               g.m_vsize = 0;",
2213         "               memcpy(f, &g, sizeof(SM_frame));",
2214         "               f->m_vsize = sz;        /* last */",
2215         "",
2216         "               dsk_drained++;",
2217         "       }",
2218         "}",
2219         "",
2220         "void",
2221         "mem_file(void)",
2222         "{      SM_frame f;",
2223         "       int i, j, q = (core_id + 1) %% NCORE;   /* target q */",
2224         "",
2225         "       if (vsize > VMAX)",
2226         "       {       printf(\"pan: recompile with -DVMAX=N with N >= %%d\\n\", vsize);",
2227         "               Uerror(\"aborting\");",
2228         "       }",
2229         "       if (now._nr_pr > PMAX)",
2230         "       {       printf(\"pan: recompile with -DPMAX=N with N >= %%d\\n\", now._nr_pr);",
2231         "               Uerror(\"aborting\");",
2232         "       }",
2233         "       if (now._nr_qs > QMAX)",
2234         "       {       printf(\"pan: recompile with -DQMAX=N with N >= %%d\\n\", now._nr_qs);",
2235         "               Uerror(\"aborting\");",
2236         "       }",
2237         "",
2238         "       if (VVERBOSE) cpu_printf(\"filing state for q%%d\\n\", q);",
2239         "",
2240         "       memcpy((uchar *) f.m_now,  (uchar *) &now, vsize);",
2241         "#if !defined(NOCOMP) && !defined(HC)",
2242         "       memset((uchar *) f.m_mask, 0, (VMAX+7)/8 * sizeof(char));",
2243         "       for (i = j = 0; i < VMAX; i++, j = (j+1)%%8)",
2244         "       {       if (Mask[i])",
2245         "               {       f.m_mask[i/8] |= (1<<j);",
2246         "       }       }",
2247         "#endif",
2248         "       if (now._nr_pr > 0)",
2249         "       {       memcpy((uchar *)f.m_p_offset, (uchar *)proc_offset, now._nr_pr*sizeof(OFFT));",
2250         "               memcpy((uchar *)f.m_p_skip,   (uchar *)proc_skip,   now._nr_pr*sizeof(uchar));",
2251         "       }",
2252         "       if (now._nr_qs > 0)",
2253         "       {       memcpy((uchar *) f.m_q_offset, (uchar *) q_offset, now._nr_qs*sizeof(OFFT));",
2254         "               memcpy((uchar *) f.m_q_skip,   (uchar *) q_skip,   now._nr_qs*sizeof(uchar));",
2255         "       }",
2256         "#if defined(C_States) && (HAS_TRACK==1) && (HAS_STACK==1)",
2257         "       c_stack((uchar *) f.m_c_stack); /* save unmatched tracked data */",
2258         "#endif",
2259         "#ifdef FULL_TRAIL",
2260         "       f.m_stack  = stack_last[core_id];",
2261         "#endif",
2262         "       f.nr_handoffs = nr_handoffs+1;",
2263         "       f.m_tau    = trpt->tau;",
2264         "       f.m_o_pm   = trpt->o_pm;",
2265         "       f.m_boq    = boq;",
2266         "       f.m_vsize  = vsize;",
2267         "",
2268         "       if (query_in_progress == 1)",
2269         "       {       query_in_progress = 2;",
2270         "       }",
2271         "       if (dsk_file < 0)",
2272         "       {       sprintf(dsk_name, \"Q%%.3d_%%.3d.tmp\", Dsk_W_Nr, core_id);",
2273         "               dsk_file = open(dsk_name, WFLAGS, 0644);",
2274         "               dsk_read = open(dsk_name, RFLAGS);",
2275         "               if (dsk_file < 0 || dsk_read < 0)",
2276         "               {       cpu_printf(\"File: <%%s>\\n\", dsk_name);",
2277         "                       Uerror(\"cannot open diskfile\");",
2278         "               }",
2279         "               Dsk_W_Nr++; /* nr of next file to open */",
2280         "               cpu_printf(\"created temporary diskfile %%s\\n\", dsk_name);",
2281         "       } else if ((dsk_written+1)%%MAX_DSK_FILE == 0)",
2282         "       {       close(dsk_file); /* close write handle */",
2283         "               sprintf(dsk_name, \"Q%%.3d_%%.3d.tmp\", Dsk_W_Nr++, core_id);",
2284         "               dsk_file = open(dsk_name, WFLAGS, 0644);",
2285         "               if (dsk_file < 0)",
2286         "               {       cpu_printf(\"File: <%%s>\\n\", dsk_name);",
2287         "                       Uerror(\"aborting: cannot open new diskfile\");",
2288         "               }",
2289         "               cpu_printf(\"created temporary diskfile %%s\\n\", dsk_name);",
2290         "       }",
2291         "       if (write(dsk_file, &f, sizeof(SM_frame)) != sizeof(SM_frame))",
2292         "       {       Uerror(\"aborting -- disk write failed (disk full?)\");",
2293         "       }",
2294         "       nstates_put++;",
2295         "       dsk_written++;",
2296         "}",
2297         "#endif",
2298         "",
2299         "int",
2300         "mem_hand_off(void)",
2301         "{",
2302         "       if (search_terminated == NULL",
2303         "       ||  *search_terminated != 0)    /* not a full crash check */",
2304         "       {       pan_exit(0);",
2305         "       }",
2306         "       iam_alive();            /* on every transition of Down */",
2307         "#ifdef USE_DISK",
2308         "       mem_drain();            /* maybe call this also on every Up */",
2309         "#endif",
2310         "       if (depth > z_handoff   /* above handoff limit */",
2311         "#ifndef SAFETY",
2312         "       &&  !a_cycles           /* not in liveness mode */",
2313         "#endif",
2314         "#if SYNC",
2315         "       &&  boq == -1           /* not mid-rv */",
2316         "#endif",
2317         "#ifdef VERI",
2318         "       &&  (trpt->tau&4)        /* claim moves first  */",
2319         "       &&  !((trpt-1)->tau&128) /* not a stutter move */",
2320         "#endif",
2321         "       &&  !(trpt->tau&8))     /* not an atomic move */",
2322         "       {       int q = (core_id + 1) %% NCORE; /* circular handoff */",
2323         "       #ifdef GENEROUS",
2324         "               if (prcnt[q] < LN_FRAMES)", /* not the best strategy */
2325         "       #else",
2326         "               if (TargetQ_NotFull(q)",
2327         "               && (dfs_phase2 == 0 || prcnt[core_id] > 0))", /* not locked, ok if race */
2328         "       #endif",
2329         "               {       mem_put(q);",   /* only 1 writer: lock-free */
2330         "                       return 1;",
2331         "               }",
2332         "               {       int rval;",
2333         "       #ifndef NGQ",
2334         "                       rval = GlobalQ_HasRoom();",
2335         "       #else",
2336         "                       rval = 0;",
2337         "       #endif",
2338         "       #ifdef USE_DISK",
2339         "                       if (rval == 0)",
2340         "                       {       void mem_file(void);",
2341         "                               mem_file();",
2342         "                               rval = 1;",
2343         "                       }",
2344         "       #endif",
2345         "                       return rval;",
2346         "               }",
2347         "       }",
2348         "       return 0; /* i.e., no handoff */",
2349         "}",
2350         "",
2351         "void",
2352         "mem_put_acc(void)      /* liveness mode */",
2353         "{      int q = (core_id + 1) %% NCORE;",
2354         "",
2355         "       if (search_terminated == NULL",
2356         "       ||  *search_terminated != 0)",
2357         "       {       pan_exit(0);",
2358         "       }",
2359         "#ifdef USE_DISK",
2360         "       mem_drain();",
2361         "#endif",
2362         "       /* some tortured use of preprocessing: */",
2363         "#if !defined(NGQ) || defined(USE_DISK)",
2364         "       if (TargetQ_Full(q))",
2365         "       {",
2366         "#endif",
2367         "#ifndef NGQ",
2368         "               if (GlobalQ_HasRoom())",
2369         "               {       return;",
2370         "               }",
2371         "#endif",
2372         "#ifdef USE_DISK",
2373         "               mem_file();",
2374         "       } else",
2375         "#else",
2376         "       #if !defined(NGQ) || defined(USE_DISK)",
2377         "       }",
2378         "       #endif",
2379         "#endif",
2380         "       {       mem_put(q);",
2381         "       }",
2382         "}",
2383         "",
2384         "#if defined(WIN32) || defined(WIN64)", /* visual studio */
2385         "void",
2386         "init_shm(void)         /* initialize shared work-queues */",
2387         "{      char    key[512];",
2388         "       int     n, m;",
2389         "       int     must_exit = 0;",
2390         "",
2391         "       if (core_id == 0 && verbose)",
2392         "       {       printf(\"cpu0: step 3: allocate shared work-queues %%g Mb\\n\",",
2393         "                       ((double) NCORE * LWQ_SIZE + GWQ_SIZE) / (1048576.));",
2394         "       }",
2395         "       for (m = 0; m < NR_QS; m++)     /* last q is global 1 */",
2396         "       {       double qsize = (m == NCORE) ? GWQ_SIZE : LWQ_SIZE;",
2397         "               sprintf(key, \"Global\\\\pan_%%s_%%.3d\", PanSource, m);",
2398         "               if (core_id == 0)",     /* root process creates shared memory segments */
2399         "               {       shmid[m] = CreateFileMapping(",
2400         "                               INVALID_HANDLE_VALUE,   /* use paging file */",
2401         "                               NULL,                   /* default security */",
2402         "                               PAGE_READWRITE,         /* access permissions */",
2403         "                               0,                      /* high-order 4 bytes */",
2404         "                               qsize,                  /* low-order bytes, size in bytes */",
2405         "                               key);                   /* name */",
2406         "               } else                  /* worker nodes just open these segments */",
2407         "               {       shmid[m] = OpenFileMapping(",
2408         "                               FILE_MAP_ALL_ACCESS,    /* read/write access */",
2409         "                               FALSE,                  /* children do not inherit handle */",
2410         "                               key);",
2411         "               }",
2412         "               if (shmid[m] == NULL)",
2413         "               {       fprintf(stderr, \"cpu%%d: could not create or open shared queues\\n\",",
2414         "                               core_id);",
2415         "                       must_exit = 1;",
2416         "                       break;",
2417         "               }",
2418         "               /* attach: */",
2419         "               shared_mem[m] = (char *) MapViewOfFile(shmid[m], FILE_MAP_ALL_ACCESS, 0, 0, 0);",
2420         "               if (shared_mem[m] == NULL)",
2421         "               { fprintf(stderr, \"cpu%%d: cannot attach shared q%%d (%%d Mb)\\n\",",
2422         "                       core_id, m+1, (int) (qsize/(1048576.)));",
2423         "                 must_exit = 1;",
2424         "                 break;",
2425         "               }",
2426         "",
2427         "               memcnt += qsize;",
2428         "",
2429         "               m_workq[m] = (SM_frame *) shared_mem[m];",
2430         "               if (core_id == 0)",
2431         "               {       int nframes = (m == NCORE) ? GN_FRAMES : LN_FRAMES;",
2432         "                       for (n = 0; n < nframes; n++)",
2433         "                       {       m_workq[m][n].m_vsize = 0;",
2434         "                               m_workq[m][n].m_boq = 0;",
2435         "       }       }       }",
2436         "",
2437         "       if (must_exit)",
2438         "       {       fprintf(stderr, \"pan: check './pan --' for usage details\\n\");",
2439         "               pan_exit(1);    /* calls cleanup_shm */",
2440         "       }",
2441         "}",
2442         "",
2443         "static uchar *",
2444         "prep_shmid_S(size_t n)         /* either sets SS or H_tab, WIN32/WIN64 */",
2445         "{      char    *rval;",
2446         "#ifndef SEP_STATE",
2447         "       char    key[512];",
2448         "",
2449         "       if (verbose && core_id == 0)",
2450         "       {",
2451         "       #ifdef BITSTATE",
2452         "               printf(\"cpu0: step 1: allocate shared bitstate %%g Mb\\n\",",
2453         "                       (double) n / (1048576.));",
2454         "       #else",
2455         "               printf(\"cpu0: step 1: allocate shared hastable %%g Mb\\n\",",
2456         "                       (double) n / (1048576.));",
2457         "       #endif",
2458         "       }",
2459         "       #ifdef MEMLIM",
2460         "       if (memcnt + (double) n > memlim)",
2461         "       {       printf(\"cpu%%d: S %%8g + %%d Kb exceeds memory limit of %%8g Mb\\n\",",
2462         "                       core_id, memcnt/1024., n/1024, memlim/(1048576.));",
2463         "               printf(\"cpu%%d: insufficient memory -- aborting\\n\", core_id);",
2464         "               exit(1);",
2465         "       }",
2466         "       #endif",
2467         "",
2468         "       /* make key different from queues: */",
2469         "       sprintf(key, \"Global\\\\pan_%%s_%%.3d\", PanSource, NCORE+2); /* different from qs */",
2470         "",
2471         "       if (core_id == 0)       /* root */",
2472         "       {       shmid_S = CreateFileMapping(INVALID_HANDLE_VALUE, NULL,",
2473         "#ifdef WIN64",
2474         "                       PAGE_READWRITE, (n>>32), (n & 0xffffffff), key);",
2475         "#else",
2476         "                       PAGE_READWRITE, 0, n, key);",
2477         "#endif",
2478         "               memcnt += (double) n;",
2479         "       } else                  /* worker */",
2480         "       {       shmid_S = OpenFileMapping(FILE_MAP_ALL_ACCESS, FALSE, key);",
2481         "       }",
2482
2483         "       if (shmid_S == NULL)",
2484         "       {",
2485         "       #ifdef BITSTATE",
2486         "               fprintf(stderr, \"cpu%%d: cannot %%s shared bitstate\",",
2487         "                       core_id, core_id?\"open\":\"create\");",
2488         "       #else",
2489         "               fprintf(stderr, \"cpu%%d: cannot %%s shared hashtable\",",
2490         "                       core_id, core_id?\"open\":\"create\");",
2491         "       #endif",
2492         "               fprintf(stderr, \"pan: check './pan --' for usage details\\n\");",
2493         "               pan_exit(1);",
2494         "       }",
2495         "",
2496         "       rval = (char *) MapViewOfFile(shmid_S, FILE_MAP_ALL_ACCESS, 0, 0, 0);   /* attach */",
2497         "       if ((char *) rval == NULL)",
2498         "       { fprintf(stderr, \"cpu%%d: cannot attach shared bitstate or hashtable\\n\", core_id);",
2499         "         fprintf(stderr, \"pan: check './pan --' for usage details\\n\");",
2500         "         pan_exit(1);",
2501         "       }",
2502         "#else",
2503         "       rval = (char *) emalloc(n);",
2504         "#endif",
2505         "       return (uchar *) rval;",
2506         "}",
2507         "",
2508         "static uchar *",
2509         "prep_state_mem(size_t n)               /* WIN32/WIN64 sets memory arena for states */",
2510         "{      char    *rval;",
2511         "       char    key[512];",
2512         "       static int cnt = 3;             /* start larger than earlier ftok calls */",
2513         "",
2514         "       if (verbose && core_id == 0)",
2515         "       {       printf(\"cpu0: step 2+: pre-allocate memory arena %%d of %%g Mb\\n\",",
2516         "                       cnt-3, (double) n / (1048576.));",
2517         "       }",
2518         "       #ifdef MEMLIM",
2519         "       if (memcnt + (double) n > memlim)",
2520         "       {       printf(\"cpu%%d: error: M %%.0f + %%.0f exceeds memory limit of %%.0f Kb\\n\",",
2521         "                       core_id, memcnt/1024.0, (double) n/1024.0, memlim/1024.0);",
2522         "               return NULL;",
2523         "       }",
2524         "       #endif",
2525         "",
2526         "       sprintf(key, \"Global\\\\pan_%%s_%%.3d\", PanSource, NCORE+cnt); cnt++;",
2527         "",
2528         "       if (core_id == 0)",
2529         "       {       shmid_M = CreateFileMapping(INVALID_HANDLE_VALUE, NULL,",
2530         "#ifdef WIN64",
2531         "                       PAGE_READWRITE, (n>>32), (n & 0xffffffff), key);",
2532         "#else",
2533         "                       PAGE_READWRITE, 0, n, key);",
2534         "#endif",
2535         "       } else",
2536         "       {       shmid_M = OpenFileMapping(FILE_MAP_ALL_ACCESS, FALSE, key);",
2537         "       }",
2538         "       if (shmid_M == NULL)",
2539         "       {       printf(\"cpu%%d: failed to get pool of shared memory nr %%d of size %%d\\n\",",
2540         "                       core_id, cnt-3, n);",
2541         "               printf(\"pan: check './pan --' for usage details\\n\");",
2542         "               return NULL;",
2543         "       }",
2544         "       rval = (char *) MapViewOfFile(shmid_M, FILE_MAP_ALL_ACCESS, 0, 0, 0);   /* attach */",
2545         "",
2546         "       if (rval == NULL)",
2547         "       { printf(\"cpu%%d: failed to attach pool of shared memory nr %%d of size %%d\\n\",",
2548         "               core_id, cnt-3, n);",
2549         "         return NULL;",
2550         "       }",
2551         "       return (uchar *) rval;",
2552         "}",
2553         "",
2554         "void",
2555         "init_HT(unsigned long n)       /* WIN32/WIN64 version */",
2556         "{      volatile char   *x;",
2557         "       double  get_mem;",
2558         "#ifndef SEP_STATE",
2559         "       char    *dc_mem_start;",
2560         "#endif",
2561         "       if (verbose) printf(\"cpu%%d: initialization for Windows\\n\", core_id);",
2562         "",
2563 "#ifdef SEP_STATE",
2564         " #ifndef MEMLIM",
2565         "       if (verbose)",
2566         "       {       printf(\"cpu0: steps 0,1: no -DMEMLIM set\\n\");",
2567         "       }",
2568         " #else",
2569         "       if (verbose)",
2570         "       printf(\"cpu0: steps 0,1: -DMEMLIM=%%d Mb - (hashtable %%g Mb + workqueues %%g Mb)\\n\",",
2571         "               MEMLIM, ((double)n/(1048576.)), ((double) NCORE * LWQ_SIZE + GWQ_SIZE)/(1048576.));",
2572         "#endif",
2573         "       get_mem = NCORE * sizeof(double) + (1 + CS_NR) * sizeof(void *)+ 4*sizeof(void *) + 2*sizeof(double);",
2574         "       /* NCORE * is_alive + search_terminated + CS_NR * sh_lock + 6 gr vars */",
2575         "       get_mem += 4 * NCORE * sizeof(void *);", /* prfree, prfull, prcnt, prmax */
2576         " #ifdef FULL_TRAIL",
2577         "       get_mem += (NCORE) * sizeof(Stack_Tree *);",
2578         "       /* NCORE * stack_last */",
2579         " #endif",
2580         "       x = (volatile char *) prep_state_mem((size_t) get_mem);",
2581         "       shmid_X = (void *) x;",
2582         "       if (x == NULL)",
2583         "       {       printf(\"cpu0: could not allocate shared memory, see ./pan --\\n\");",
2584         "               exit(1);",
2585         "       }",
2586         "       search_terminated = (volatile unsigned int *) x; /* comes first */",
2587         "       x += sizeof(void *); /* maintain alignment */",
2588         "",
2589         "       is_alive   = (volatile double *) x;",
2590         "       x += NCORE * sizeof(double);",
2591         "",
2592         "       sh_lock   = (volatile int *) x;",
2593         "       x += CS_NR * sizeof(void *); /* allow 1 word per entry */",
2594         "",
2595         "       grfree    = (volatile int *) x;",
2596         "       x += sizeof(void *);",
2597         "       grfull    = (volatile int *) x;",
2598         "       x += sizeof(void *);",
2599         "       grcnt    = (volatile int *) x;",
2600         "       x += sizeof(void *);",
2601         "       grmax    = (volatile int *) x;",
2602         "       x += sizeof(void *);",
2603         "       prfree = (volatile int *) x;",
2604         "       x += NCORE * sizeof(void *);",
2605         "       prfull = (volatile int *) x;",
2606         "       x += NCORE * sizeof(void *);",
2607         "       prcnt = (volatile int *) x;",
2608         "       x += NCORE * sizeof(void *);",
2609         "       prmax = (volatile int *) x;",
2610         "       x += NCORE * sizeof(void *);",
2611         "       gr_readmiss    = (volatile double *) x;",
2612         "       x += sizeof(double);",
2613         "       gr_writemiss    = (volatile double *) x;",
2614         "       x += sizeof(double);",
2615         "",
2616         "       #ifdef FULL_TRAIL",
2617         "               stack_last = (volatile Stack_Tree **) x;",
2618         "               x += NCORE * sizeof(Stack_Tree *);",
2619         "       #endif",
2620         "",
2621         "       #ifndef BITSTATE",
2622         "               H_tab = (H_el **) emalloc(n);",
2623         "       #endif",
2624 "#else",
2625         "       #ifndef MEMLIM",
2626         "               #warning MEMLIM not set",       /* cannot happen */
2627         "               #define MEMLIM  (2048)",
2628         "       #endif",
2629         "",
2630         "       if (core_id == 0 && verbose)",
2631         "               printf(\"cpu0: step 0: -DMEMLIM=%%d Mb - (hashtable %%g Mb + workqueues %%g Mb) = %%g Mb for state storage\\n\",",
2632         "               MEMLIM, ((double)n/(1048576.)), ((double) NCORE * LWQ_SIZE + GWQ_SIZE)/(1048576.),",
2633         "               (memlim - memcnt - (double) n - ((double) NCORE * LWQ_SIZE + GWQ_SIZE))/(1048576.));",
2634         "       #ifndef BITSTATE",
2635         "               H_tab = (H_el **) prep_shmid_S((size_t) n);     /* hash_table */",
2636         "       #endif",
2637         "       get_mem = memlim - memcnt - ((double) NCORE) * LWQ_SIZE - GWQ_SIZE;",
2638         "       if (get_mem <= 0)",
2639         "       {       Uerror(\"internal error -- shared state memory\");",
2640         "       }",
2641         "",
2642         "       if (core_id == 0 && verbose)",
2643         "       {       printf(\"cpu0: step 2: shared state memory %%g Mb\\n\",",
2644         "                       get_mem/(1048576.));",
2645         "       }",
2646         "       x = dc_mem_start = (char *) prep_state_mem((size_t) get_mem);   /* for states */",
2647         "       if (x == NULL)",
2648         "       {       printf(\"cpu%%d: insufficient memory -- aborting\\n\", core_id);",
2649         "               exit(1);",
2650         "       }",
2651         "",
2652         "       search_terminated = (volatile unsigned int *) x; /* comes first */",
2653         "       x += sizeof(void *); /* maintain alignment */",
2654         "",
2655         "       is_alive   = (volatile double *) x;",
2656         "       x += NCORE * sizeof(double);",
2657         "",
2658         "       sh_lock   = (volatile int *) x;",
2659         "       x += CS_NR * sizeof(int);",
2660         "",
2661         "       grfree    = (volatile int *) x;",
2662         "       x += sizeof(void *);",
2663         "       grfull    = (volatile int *) x;",
2664         "       x += sizeof(void *);",
2665         "       grcnt    = (volatile int *) x;",
2666         "       x += sizeof(void *);",
2667         "       grmax    = (volatile int *) x;",
2668         "       x += sizeof(void *);",
2669         "       prfree = (volatile int *) x;",
2670         "       x += NCORE * sizeof(void *);",
2671         "       prfull = (volatile int *) x;",
2672         "       x += NCORE * sizeof(void *);",
2673         "       prcnt = (volatile int *) x;",
2674         "       x += NCORE * sizeof(void *);",
2675         "       prmax = (volatile int *) x;",
2676         "       x += NCORE * sizeof(void *);",
2677         "       gr_readmiss = (volatile double *) x;",
2678         "       x += sizeof(double);",
2679         "       gr_writemiss = (volatile double *) x;",
2680         "       x += sizeof(double);",
2681         "",
2682         " #ifdef FULL_TRAIL",
2683         "       stack_last = (volatile Stack_Tree **) x;",
2684         "       x += NCORE * sizeof(Stack_Tree *);",
2685         " #endif",
2686         "       if (((long)x)&(sizeof(void *)-1))       /* word alignment */",
2687         "       {       x += sizeof(void *)-(((long)x)&(sizeof(void *)-1)); /* 64-bit align */",
2688         "       }",
2689         "",
2690         "       #ifdef COLLAPSE",
2691         "       ncomps = (unsigned long *) x;",
2692         "       x += (256+2) * sizeof(unsigned long);",
2693         "       #endif",
2694         "",
2695         "       dc_shared = (sh_Allocater *) x; /* in shared memory */",
2696         "       x += sizeof(sh_Allocater);",
2697         "",
2698         "       if (core_id == 0)       /* root only */",
2699         "       {       dc_shared->dc_id     = shmid_M;",
2700         "               dc_shared->dc_start  = (void *) dc_mem_start;",
2701         "               dc_shared->dc_arena  = x;",
2702         "               dc_shared->pattern   = 1234567;",
2703         "               dc_shared->dc_size   = (long) get_mem - (long) (x - dc_mem_start);",
2704         "               dc_shared->nxt       = NULL;",
2705         "       }",
2706 "#endif",
2707         "}",
2708         "",
2709         "#if defined(WIN32) || defined(WIN64) || defined(__i386__) || defined(__x86_64__)",
2710         "extern BOOLEAN InterlockedBitTestAndSet(LONG volatile* Base, LONG Bit);",
2711         "int",
2712         "tas(volatile LONG *s)", /* atomic test and set */
2713         "{      return InterlockedBitTestAndSet(s, 1);",
2714         "}",
2715         "#else",
2716         "       #error missing definition of test and set operation for this platform",
2717         "#endif",
2718         "",
2719         "void",
2720         "cleanup_shm(int val)",
2721         "{      int m;",
2722         "       static int nibis = 0;",
2723         "",
2724         "       if (nibis != 0)",
2725         "       {       printf(\"cpu%%d: Redundant call to cleanup_shm(%%d)\\n\", core_id, val);",
2726         "               return;",
2727         "       } else",
2728         "       {       nibis = 1;",
2729         "       }",
2730         "       if (search_terminated != NULL)",
2731         "       {       *search_terminated |= 16; /* cleanup_shm */",
2732         "       }",
2733         "",
2734         "       for (m = 0; m < NR_QS; m++)",
2735         "       {       if (shmid[m] != NULL)",
2736         "               {       UnmapViewOfFile((char *) shared_mem[m]);",
2737         "                       CloseHandle(shmid[m]);",
2738         "       }       }",
2739         "#ifdef SEP_STATE",
2740         "       UnmapViewOfFile((void *) shmid_X);",
2741         "       CloseHandle((void *) shmid_M);",
2742         "#else",
2743         "       #ifdef BITSTATE",
2744         "               if (shmid_S != NULL)",
2745         "               {       UnmapViewOfFile(SS);",
2746         "                       CloseHandle(shmid_S);",
2747         "               }",
2748         "       #else",
2749         "               if (core_id == 0 && verbose)",
2750         "               {       printf(\"cpu0: done, %%ld Mb of shared state memory left\\n\",",
2751         "                               dc_shared->dc_size / (long)(1048576));",
2752         "               }",
2753         "               if (shmid_S != NULL)",
2754         "               {       UnmapViewOfFile(H_tab);",
2755         "                       CloseHandle(shmid_S);",
2756         "               }",
2757         "               shmid_M = (void *) (dc_shared->dc_id);",
2758         "               UnmapViewOfFile((char *) dc_shared->dc_start);",
2759         "               CloseHandle(shmid_M);",
2760         "       #endif",
2761         "#endif",
2762         "       /* detached from shared memory - so cannot use cpu_printf */",
2763         "       if (verbose)",
2764         "       {       printf(\"cpu%%d: done -- got %%d states from queue\\n\",",
2765         "                       core_id, nstates_get);",
2766         "       }",
2767         "}",
2768         "",
2769         "void",
2770         "mem_get(void)",
2771         "{      SM_frame   *f;",
2772         "       int is_parent;",
2773         "",
2774         "#if defined(MA) && !defined(SEP_STATE)",
2775         "       #error MA requires SEP_STATE in multi-core mode",
2776         "#endif",
2777         "#ifdef BFS",
2778         "       #error instead of -DNCORE -DBFS use -DBFS_PAR",
2779         "#endif",
2780         "#ifdef SC",
2781         "       #error SC is not supported in multi-core mode",
2782         "#endif",
2783         "       init_shm();     /* we are single threaded when this starts */",
2784         "       signal(SIGINT, give_up);        /* windows control-c interrupt */",
2785         "",
2786         "       if (core_id == 0 && verbose)",
2787         "       {       printf(\"cpu0: step 4: creating additional workers (proxy %%d)\\n\",",
2788         "                       proxy_pid);",
2789         "       }",
2790         "#if 0",
2791         "       if NCORE > 1 the child or the parent should fork N-1 more times",
2792         "       the parent is the only process with core_id == 0 and is_parent > 0",
2793         "       the others (workers) have is_parent = 0 and core_id = 1..NCORE-1",
2794         "#endif",
2795         "       if (core_id == 0)                       /* root starts up the workers */",
2796         "       {       worker_pids[0] = (DWORD) getpid();      /* for completeness */",
2797         "               while (++core_id < NCORE)       /* first worker sees core_id = 1 */",
2798         "               {       char cmdline[64];",
2799         "                       STARTUPINFO si = { sizeof(si) };",
2800         "                       PROCESS_INFORMATION pi;",
2801         "",
2802         "                       if (proxy_pid == core_id)       /* always non-zero */",
2803         "                       {       sprintf(cmdline, \"pan_proxy.exe -r %%s-Q%%d -Z%%d\",",
2804         "                                       o_cmdline, getpid(), core_id);",
2805         "                       } else",
2806         "                       {       sprintf(cmdline, \"pan.exe %%s-Q%%d -Z%%d\",",
2807         "                                       o_cmdline, getpid(), core_id);",
2808         "                       }",
2809         "                       if (verbose) printf(\"cpu%%d: spawn %%s\\n\", core_id, cmdline);",
2810         "",
2811         "                       is_parent = CreateProcess(0, cmdline, 0, 0, FALSE, 0, 0, 0, &si, &pi);",
2812         "                       if (is_parent == 0)",
2813         "                       {       Uerror(\"fork failed\");",
2814         "                       }",
2815         "                       worker_pids[core_id] = pi.dwProcessId;",
2816         "                       worker_handles[core_id] = pi.hProcess;",
2817         "                       if (verbose)",
2818         "                       {       cpu_printf(\"created core %%d, pid %%d\\n\",",
2819         "                                       core_id, pi.dwProcessId);",
2820         "                       }",
2821         "                       if (proxy_pid == core_id)       /* we just created the receive half */",
2822         "                       {       /* add proxy send, store pid in proxy_pid_snd */",
2823         "                               sprintf(cmdline, \"pan_proxy.exe -s %%s-Q%%d -Z%%d -Y%%d\",",
2824         "                                       o_cmdline, getpid(), core_id, worker_pids[proxy_pid]);",
2825         "                               if (verbose) printf(\"cpu%%d: spawn %%s\\n\", core_id, cmdline);",
2826         "                               is_parent = CreateProcess(0, cmdline, 0,0, FALSE, 0,0,0, &si, &pi);",
2827         "                               if (is_parent == 0)",
2828         "                               {       Uerror(\"fork failed\");",
2829         "                               }",
2830         "                               proxy_pid_snd = pi.dwProcessId;",
2831         "                               proxy_handle_snd = pi.hProcess;",
2832         "                               if (verbose)",
2833         "                               {       cpu_printf(\"created core %%d, pid %%d (send proxy)\\n\",",
2834         "                                               core_id, pi.dwProcessId);",
2835         "               }       }       }",
2836         "               core_id = 0;            /* reset core_id for root process */",
2837         "       } else  /* worker */",
2838         "       {       static char db0[16];    /* good for up to 10^6 cores */",
2839         "               static char db1[16];",
2840         "               tprefix = db0; sprefix = db1;",
2841         "               sprintf(tprefix, \"cpu%%d_trail\", core_id);    /* avoid conflicts on file access */",
2842         "               sprintf(sprefix, \"cpu%%d_rst\", core_id);",
2843         "               memcnt = 0;     /* count only additionally allocated memory */",
2844         "       }",
2845         "       if (verbose)",
2846         "       {       cpu_printf(\"starting core_id %%d -- pid %%d\\n\", core_id, getpid());",
2847         "       }",
2848         "       if (core_id == 0 && !remote_party)",
2849         "       {       new_state();    /* root starts the search */",
2850         "               if (verbose)",
2851         "               cpu_printf(\"done with 1st dfs, nstates %%g (put %%d states), start reading q\\n\",",
2852         "                       nstates, nstates_put);",
2853         "               dfs_phase2 = 1;",
2854         "       }",
2855         "       Read_Queue(core_id);    /* all cores */",
2856         "",
2857         "       if (verbose)",
2858         "       {       cpu_printf(\"put %%6d states into queue -- got %%6d\\n\",",
2859         "                       nstates_put, nstates_get);",
2860         "       }",
2861         "       done = 1;",
2862         "       wrapup();",
2863         "       exit(0);",
2864         "}",
2865         "#endif", /* WIN32 || WIN64 */
2866         "",
2867         "#ifdef BITSTATE",
2868         "void",
2869         "init_SS(unsigned long n)",
2870         "{",
2871         "       SS = (uchar *) prep_shmid_S((size_t) n);",
2872         "       init_HT(0L);", /* locks and shared memory for Stack_Tree allocations */
2873         "}",
2874         "#endif", /* BITSTATE */
2875         "",
2876         "#endif", /* NCORE>1 */
2877         0,
2878 };