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