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