1 /***** spin: pangen7.h *****/ 2 3 /* 4 * This file is part of the public release of Spin. It is subject to the 5 * terms in the LICENSE file that is included in this source directory. 6 * Tool documentation is available at http://spinroot.com 7 */ 8 9 static const char *pan_par[] = { /* generates pan.p */ 10 "#include <sys/ipc.h>", 11 "#include <sys/shm.h>", 12 "#include <time.h>", /* for nanosleep */ 13 "#include <assert.h>", 14 "#include <limits.h>", 15 "#ifdef BFS_DISK", 16 "#include <unistd.h>", /* for rmdir */ 17 "#include <sys/stat.h>", /* for mkdir */ 18 "#include <sys/types.h>", 19 "#include <fcntl.h>", /* for open */ 20 "#endif", 21 "", 22 "#define Max(a,b) (((a)>(b))?(a):(b))", 23 "#ifndef WAIT_MAX", 24 " #define WAIT_MAX 2 /* seconds */", 25 "#endif", 26 "#define BFS_GEN 2 /* current and next generation */", 27 "", 28 "typedef struct BFS_Slot BFS_Slot;", 29 "typedef struct BFS_shared BFS_shared;", 30 "typedef struct BFS_data BFS_data;", 31 "", 32 "struct BFS_Slot {", 33 " #ifdef BFS_FIFO", 34 " enum bfs_types type; /* message type */", 35 " #endif", 36 " BFS_State *s_data; /* state data */", 37 " #ifndef BFS_QSZ", 38 " BFS_Slot *nxt; /* linked list */", 39 " #endif", 40 "};", 41 "", 42 "struct BFS_data {", 43 " double memcnt;", 44 " double nstates;", 45 " double nlinks;", 46 " double truncs;", 47 " ulong mreached;", 48 " ulong vsize;", 49 " ulong memory_left;", 50 " ulong punted;", 51 " ulong errors;", 52 " int override; /* after crash, if another proc clears locks */", 53 "};", 54 "", 55 "struct BFS_shared { /* about 13K for BFS_MAXPROCS=16 and BFS_MAXLOCKS=1028 */", 56 " volatile ulong quit; /* set to signal termination -- one word */", 57 " volatile ulong started;", 58 "", 59 " volatile uchar sh_owner[BFS_MAXLOCKS]; /* optional */", 60 "#ifdef BFS_CHECK", 61 " volatile uchar in_count[BFS_MAXLOCKS]; /* optional */", 62 "#endif", 63 " volatile int sh_locks[BFS_MAXLOCKS];", 64 " volatile ulong wait_count[BFS_MAXLOCKS]; /* optional */", 65 "", 66 " volatile BFS_data bfs_data[BFS_MAXPROCS];", 67 " volatile uchar bfs_flag[BFS_MAXPROCS]; /* running 0, normal exit 1, abnormal 2 */", 68 " volatile uchar bfs_idle[BFS_MAXPROCS]; /* set when all input queues are empty */", 69 "#ifdef BFS_DISK", 70 " volatile uchar bfs_out_cnt[BFS_MAXPROCS]; /* set when core writes a state */", 71 "#endif", 72 "", 73 "#ifdef BFS_QSZ", 74 " #define BFS_NORECYCLE", 75 " #if BFS_QSZ<=0", 76 " #error BFS_QSZ must be positive", 77 " #endif", 78 " #ifdef BFS_FIFO", 79 " #error BFS_QSZ cannot be combined with BFS_FIFO", 80 " #endif", 81 " #ifdef BFS_DISK", 82 " #error BFS_QSZ cannot be combined with BFS_DISK", 83 " #endif", 84 " volatile BFS_Slot bfsq[BFS_GEN][BFS_MAXPROCS][BFS_MAXPROCS][BFS_QSZ];", 85 " volatile uint bfs_ix[BFS_GEN][BFS_MAXPROCS][BFS_MAXPROCS];", 86 "#else", 87 " volatile BFS_Slot *head[BFS_GEN][BFS_MAXPROCS][BFS_MAXPROCS];", 88 "#endif", 89 "", 90 "#ifdef BFS_FIFO", 91 " volatile BFS_Slot *tail[BFS_GEN][BFS_MAXPROCS][BFS_MAXPROCS];", 92 " volatile BFS_Slot *dels[BFS_GEN][BFS_MAXPROCS][BFS_MAXPROCS];", 93 "#endif", 94 "#ifdef BFS_LOGMEM", 95 " volatile ulong logmem[1024];", 96 "#endif", 97 " volatile ulong mem_left;", 98 " volatile uchar *allocator; /* start of shared heap, must be last */", 99 "};", 100 "", 101 "enum bfs_types { EMPTY = 0, STATE, DELETED };", 102 "", 103 "extern volatile uchar *bfs_get_shared_mem(key_t, size_t);", 104 "extern BFS_Slot * bfs_new_slot(BFS_Trail *);", 105 "extern BFS_Slot * bfs_prep_slot(BFS_Trail *, BFS_Slot *);", 106 "extern BFS_Slot * bfs_next(void);", 107 "extern BFS_Slot * bfs_pack_state(Trail *, BFS_Trail *, int, BFS_Slot *);", 108 "extern SV_Hold * bfs_new_sv(int);", 109 "#if NRUNS>0", 110 "extern EV_Hold * bfs_new_sv_mask(int);", 111 "#endif", 112 "extern BFS_Trail * bfs_grab_trail(void);", 113 "extern BFS_Trail * bfs_unpack_state(BFS_Slot *);", 114 "extern int bfs_all_empty(void);", 115 "extern int bfs_all_idle(void);", 116 "extern int bfs_all_running(void);", 117 "extern int bfs_idle_and_empty(void);", 118 "extern size_t bfs_find_largest(key_t);", 119 "", 120 "extern void bfs_clear_locks(void);", 121 "extern void bfs_drop_shared_memory(void);", 122 "extern void bfs_explore_state(BFS_Slot *);", 123 "extern void bfs_initial_state(void);", 124 "extern void bfs_mark_done(int);", 125 "extern void bfs_printf(const char *fmt, ...);", 126 "extern void bfs_push_state(Trail *, BFS_Trail *, int);", 127 "extern void bfs_recycle(BFS_Slot *);", 128 "extern void bfs_release_trail(BFS_Trail *);", 129 "extern void bfs_run(void);", 130 "extern void bfs_setup_mem(void);", 131 "extern void bfs_setup(void);", 132 "extern void bfs_shutdown(const char *);", 133 "extern void bfs_statistics(void);", 134 "extern void bfs_store_state(Trail *, short);", 135 "extern void bfs_set_toggle(void);", 136 "extern void bfs_update(void);", 137 "", 138 "#ifdef MA", 139 " #error cannot combine -DMA with -DBFS_PAR", 140 " /* would require us to parallelize g_store */", 141 "#endif", 142 "#ifdef BCS", 143 " #error cannot combine -DBCS with -DBFS_PAR", 144 "#endif", 145 "#ifdef BFS_DISK", 146 " #ifdef BFS_FIFO", 147 " #error cannot combine BFS_DISK and BFS_FIFO", 148 " #endif", 149 " extern void bfs_disk_start(void);", 150 " extern void bfs_disk_stop(void);", 151 " extern void bfs_disk_out(void);", 152 " extern void bfs_disk_inp(void);", 153 " extern void bfs_disk_iclose(void);", 154 " extern void bfs_disk_oclose(void);", 155 " int bfs_out_fd[BFS_MAXPROCS];", 156 " int bfs_inp_fd[BFS_MAXPROCS];", 157 "#endif", 158 "", 159 "static BFS_shared *shared_memory;", 160 "#ifndef BFS_QSZ", 161 "static BFS_Slot *bfs_free_slot; /* local free list */", 162 "#endif", 163 "static BFS_Slot bfs_null;", 164 "static SV_Hold *bfs_svfree[VECTORSZ];", 165 "static uchar *bfs_heap; /* local pointer into heap */", 166 "static ulong bfs_left; /* local part of shared heap */", 167 "#if NRUNS>0", 168 "static void bfs_keep(EV_Hold *);", 169 "#endif", 170 "static long bfs_sent; /* nr msgs sent -- local to each process */", 171 "static long bfs_rcvd; /* nr msgs rcvd */", 172 "static long bfs_sleep_cnt; /* stats */", 173 "static long bfs_wcount;", 174 "static long bfs_gcount;", 175 "static ulong bfs_total_shared;", 176 "#ifdef BFS_STAGGER", 177 " static int bfs_stage_cnt = 0;", 178 " static void bfs_stagger_flush(void);", 179 "#endif", 180 "static int bfs_toggle; /* local variable, 0 or 1 */", 181 "static int bfs_qscan; /* scan input queues in order */", 182 "static ulong bfs_snapped;", 183 "static int shared_mem_id;", 184 "#ifndef NOREDUCE", 185 "static int bfs_nps; /* no preselection */", 186 "#endif", 187 "ulong bfs_punt; /* states dropped for lack of memory */", 188 "#if defined(VERBOSE) || defined(BFS_CHECK)", 189 "static const char *bfs_sname[] = {", 190 " \"EMPTY\", /* 0 */", 191 " \"STATE\", /* 1 */", 192 " \"STATE\", /* 2 = DELETED */", 193 " 0", 194 "};", 195 "#endif", 196 "static const char *bfs_lname[] = { /* match values defined in pangen2.c */", 197 " \"global lock\", /* BFS_GLOB */", 198 " \"ordinal\", /* BFS_ORD */", 199 " \"shared memory\", /* BFS_MEM */", 200 " \"print to stdout\", /* BFS_PRINT */", 201 " \"hashtable\", /* BFS_STATE */", 202 " 0", 203 "};", 204 "", 205 "static ulong bfs_count[DELETED+1]; /* indexed with bfs_types: EMPTY=0, STATE=1, DELETED=2 */", 206 "", 207 "static int bfs_keep_state;", 208 "", 209 "int Cores = 1;", 210 "int who_am_i = 0; /* root */", 211 "", 212 "#ifdef L_BOUND", 213 " int L_bound = L_BOUND;", 214 "#endif", 215 "", 216 "#ifdef BFS_CHECK", 217 "void", 218 "bfs_dump_now(char *s)", 219 "{ int i; char *p = (char *) &now;", 220 "", 221 " e_critical(BFS_PRINT);", 222 " printf(\"%%s\\t\", s);", 223 " printf(\"%%3lu: \", vsize);", 224 " for (i = 0; i < vsize; i++)", 225 " { printf(\"%%3d \", *p++);", 226 " }", 227 " printf(\" %%s\\noffsets:\\t\", s);", 228 " for (i = 0; i < now._nr_pr; i++)", 229 " { printf(\"%%3d \", proc_offset[i]);", 230 " }", 231 " printf(\"\\n\");", 232 " x_critical(BFS_PRINT);", 233 "}", 234 "", 235 "void", 236 "view_state(char *s) /* debugging */", 237 "{ int i;", 238 " char *p;", 239 " e_critical(BFS_PRINT);", 240 " printf(\"cpu%%02d %%s: \", who_am_i, s);", 241 " p = (char *)&now;", 242 " for (i = 0; i < vsize; i++)", 243 " printf(\"%%3d, \", *p++);", 244 " printf(\"\\n\"); fflush(stdout);", 245 " x_critical(BFS_PRINT);", 246 "}", 247 "#endif", 248 "", 249 "void", 250 "bfs_main(int ncores, int cycles)", 251 "{", 252 " if (cycles)", 253 " { fprintf(stderr, \"pan: cycle detection is not supported in this mode\\n\");", 254 " exit(1);", 255 " }", 256 "", 257 " if (ncores == 0) /* i.e., find out */", 258 " { FILE *fd;", 259 " char buf[512];", 260 " if ((fd = fopen(\"/proc/cpuinfo\", \"r\")) == NULL)", 261 " { /* cannot tell */", 262 " ncores = Cores; /* use the default */", 263 " } else", 264 " { while (fgets(buf, sizeof(buf), fd))", 265 " { if (strncmp(buf, \"processor\", strlen(\"processor\")) == 0)", 266 " { ncores++;", 267 " } }", 268 " fclose(fd);", 269 " ncores--;", 270 " if (verbose)", 271 " { printf(\"pan: %%d available cores\\n\", ncores+1);", 272 " } } }", 273 " if (ncores >= BFS_MAXPROCS)", 274 " { Cores = BFS_MAXPROCS-1; /* why -1? */", 275 " } else if (ncores < 1)", 276 " { Cores = 1;", 277 " } else", 278 " { Cores = ncores;", 279 " }", 280 " printf(\"pan: using %%d core%%s\\n\", Cores, (Cores>1)?\"s\":\"\");", 281 " fflush(stdout);", 282 "#ifdef BFS_DISK", 283 " bfs_disk_start();", /* create .spin */ 284 "#endif", 285 " bfs_setup(); /* shared memory segments and fork */", 286 " bfs_run();", 287 " if (who_am_i == 0)", 288 " { stop_timer(0);", 289 " }", 290 " bfs_statistics();", 291 " bfs_mark_done(1);", 292 " if (who_am_i == 0)", 293 " { report_time();", 294 "#ifdef BFS_DISK", 295 " bfs_disk_stop();", 296 "#endif", 297 " }", 298 "#ifdef C_EXIT", 299 " C_EXIT; /* trust that it defines a fct */", 300 "#endif", 301 " bfs_drop_shared_memory();", 302 " exit(0);", 303 "}", 304 "", 305 "void", 306 "bfs_setup_mem(void)", 307 "{ size_t n;", 308 " key_t key;", 309 "#ifdef BFS_FIFO", 310 " bfs_null.type = EMPTY;", 311 "#endif", 312 " ntrpt = (Trail *) emalloc(sizeof(Trail));", /* just once */ 313 "", 314 " if ((key = ftok(\".\", (int) 'L')) == -1)", 315 " { perror(\"ftok shared memory\");", 316 " exit(1);", 317 " }", 318 " n = bfs_find_largest(key);", 319 " bfs_total_shared = (ulong) n;", 320 "", 321 " shared_memory = (BFS_shared *) bfs_get_shared_mem(key, n); /* root */", 322 " shared_memory->allocator = (uchar *) shared_memory + sizeof(BFS_shared);", 323 " shared_memory->mem_left = (ulong) (n - sizeof(BFS_shared));", 324 "}", 325 "", 326 "ulong bfs_LowLim;", 327 "#ifndef BFS_RESERVE", 328 " #define BFS_RESERVE 5", 329 /* keep memory on global heap in reserve for first few cores */ 330 /* that run out of their local allocation of shared mem */ 331 /* 1~50 percent, 2~30 percent, 5~20 percent, >Cores=none */ 332 "#else", 333 " #if BFS_RESERVE<1", 334 " #error BFS_RESERVE must be at least 1", 335 " #endif", 336 "#endif", 337 "", 338 "void", 339 "bfs_setup(void) /* executed by root */", 340 "{ int i, j;", 341 " ulong n; /* share of shared memory allocated to each core */", 342 "", 343 " n = shared_memory->mem_left / (Cores + Cores/(BFS_RESERVE)); /* keep some reserve */", 344 "", 345 " if ((n%%sizeof(void *)) != 0)", 346 " { n -= (n%%sizeof(void *)); /* align, without exceeding total */", 347 " }", 348 " for (i = 0; i < Cores-1; i++)", 349 " { j = fork();", 350 " if (j == -1)", 351 " { bfs_printf(\"fork failed\\n\");", 352 " exit(1);", 353 " }", 354 " if (j == 0)", 355 " { who_am_i = i+1; /* 1..Cores-1 */", 356 " break;", 357 " } }", 358 "", 359 " e_critical(BFS_MEM);", 360 " bfs_heap = (uchar *) shared_memory->allocator;", 361 " shared_memory->allocator += n;", 362 " shared_memory->mem_left -= n;", 363 " x_critical(BFS_MEM);", 364 "", 365 " bfs_left = n;", 366 " bfs_runs = 1;", 367 " bfs_LowLim = n / (2 * (ulong) Cores);", /* 50% */ 368 "}", 369 "", 370 "void", 371 "bfs_run(void)", 372 "{ BFS_Slot *v;", 373 "", 374 "#ifdef BFS_DISK", 375 " bfs_disk_out();", /* create outqs */ 376 "#endif", 377 " if (who_am_i == 0)", 378 " { bfs_initial_state();", 379 " }", 380 "#ifdef BFS_DISK", 381 " #ifdef BFS_STAGGER", 382 " bfs_stagger_flush();", 383 " #endif", 384 " bfs_disk_oclose();", /* sync and close outqs */ 385 "#endif", 386 "#ifdef BFS_FIFO", 387 " static int i_count;", 388 "#endif", 389 "", 390 " srand(s_rand+HASH_NR);", 391 " bfs_qscan = 0;", 392 " bfs_toggle = 1 - bfs_toggle; /* after initial state */", 393 " e_critical(BFS_GLOB);", 394 " shared_memory->started++;", 395 " x_critical(BFS_GLOB);", 396 "", 397 " while (shared_memory->started != Cores) /* wait for all cores to connect */", 398 " { usleep(1);", 399 " }", 400 "", 401 "#ifdef BFS_DISK", 402 " bfs_disk_out();", 403 " bfs_disk_inp();", 404 "#endif", 405 "", 406 " start_timer();", 407 " while (shared_memory->quit == 0)", 408 " { v = bfs_next(); /* get next message from current generation */", 409 " if (v->s_data) /* v->type == STATE || v->type == DELETED */", 410 " { bfs_count[STATE]++;", 411 "#ifdef VERBOSE", 412 " bfs_printf(\"GOT STATE (depth %%d, nr %%u)\\n\",", 413 " v->s_data->t_info->o_tt, v->s_data->nr);", 414 "#endif", 415 " /* last resort: start dropping states when out of memory */", 416 " if (bfs_left > 1024 || shared_memory->mem_left > 1024)", 417 " { bfs_explore_state(v);", 418 " } else", 419 " { static int warned_loss = 0;", 420 " if (warned_loss == 0 && who_am_i == 0)", 421 " { warned_loss++;", 422 " bfs_printf(\"out of shared memory - losing states\\n\");", 423 " }", 424 " bfs_punt++;", 425 " }", 426 "#if !defined(BFS_FIFO) && !defined(BFS_NORECYCLE)", 427 " bfs_recycle(v);", 428 "#endif", 429 "#ifdef BFS_FIFO", 430 " i_count = 0;", 431 "#endif", 432 " } else", 433 " { bfs_count[EMPTY]++;", 434 "#if defined(BFS_FIFO) && defined(BFS_CHECK)", 435 " assert(v->type == EMPTY);", 436 "#endif", 437 "#ifdef BFS_FIFO", 438 " if (who_am_i == 0)", 439 " { if (bfs_idle_and_empty())", 440 " { if (i_count++ > 10)", 441 " { shared_memory->quit = 1;", 442 " }", 443 " else usleep(1);", 444 " }", 445 " } else if (!bfs_all_running())", 446 " { bfs_shutdown(\"early termination\");", 447 " }", 448 "#else", 449 " if (who_am_i == 0)", 450 " { if (bfs_all_idle()) /* wait for it */", 451 " { if (!bfs_all_empty()) /* more states to process */", 452 " { bfs_set_toggle();", 453 " goto do_toggle;", 454 " } else /* done */", 455 " { shared_memory->quit = 1; /* step 4 */", 456 " }", 457 " } else", 458 " { bfs_sleep_cnt++;", 459 " }", 460 " } else", 461 " { /* wait for quit or idle bit to be reset by root */", 462 " while (shared_memory->bfs_idle[who_am_i] == 1", 463 " && shared_memory->quit == 0)", 464 " { if (bfs_all_running())", 465 " { bfs_sleep_cnt++;", 466 " usleep(10); /* new 6.2.3 */", 467 " } else", 468 " { bfs_shutdown(\"early termination\");", 469 " /* no return */", 470 " } }", 471 "do_toggle: bfs_qscan = 0;", 472 "#ifdef BFS_DISK", 473 " bfs_disk_iclose();", 474 " bfs_disk_oclose();", 475 "#endif", 476 " bfs_toggle = 1 - bfs_toggle;", 477 "#ifdef BFS_DISK", 478 " bfs_disk_out();", 479 " bfs_disk_inp();", 480 "#endif", 481 " #ifdef BFS_CHECK", 482 " bfs_printf(\"toggle: recv from %%d, send to %%d\\n\",", 483 " bfs_toggle, 1 - bfs_toggle);", 484 " #endif", 485 " }", 486 "#endif", 487 " } }", 488 "#ifdef BFS_CHECK", 489 " bfs_printf(\"done, sent %%5ld recvd %%5ld punt %%5lu sleep: %%ld\\n\",", 490 " bfs_sent, bfs_rcvd, bfs_punt, bfs_sleep_cnt);", 491 "#endif", 492 "}", 493 "", 494 "void", 495 "bfs_report_mem(void) /* called from within wrapup() */", 496 "{", 497 " printf(\"%%9.3f total shared memory usage\\n\\n\",", 498 " ((double) bfs_total_shared - (double) bfs_left)/(1024.*1024.));", 499 "}", 500 "", 501 "void", 502 "bfs_statistics(void)", 503 "{", 504 " #ifdef VERBOSE", 505 " enum bfs_types i;", 506 " #endif", 507 " if (verbose)", 508 " bfs_printf(\"states sent %%7ld recvd %%7ld stored %%8g sleeps: %%4ld, %%4ld, %%ld\\n\",", 509 " bfs_sent, bfs_rcvd, nstates, bfs_wcount, bfs_gcount, bfs_sleep_cnt);", 510 " if (0) bfs_printf(\"states punted %%7lu\\n\", bfs_punt);", 511 " #ifdef VERBOSE", 512 " for (i = EMPTY; i <= DELETED; i++)", 513 " { if (bfs_count[i] > 0)", 514 " { bfs_printf(\"%%6s %%8lu\\n\",", 515 " bfs_sname[i], bfs_count[i]);", 516 " } }", 517 " #endif", 518 " bfs_update();", 519 "", 520 " if (who_am_i == 0 && shared_memory)", 521 " { int i; ulong count = 0L;", 522 " done = 1;", 523 "", 524 " e_critical(BFS_PRINT);", 525 " wrapup();", 526 " if (verbose)", 527 " { printf(\"\\nlock-wait counts:\\n\");", 528 " for (i = 0; i < BFS_STATE; i++)", 529 " printf(\"%%16s %%9lu\\n\",", 530 " bfs_lname[i], shared_memory->wait_count[i]);", 531 "#ifndef BITSTATE", 532 " for (i = BFS_STATE; i < BFS_MAXLOCKS; i++)", 533 " { if (0)", 534 " printf(\" [%%6d] %%9lu\\n\",", 535 " i, shared_memory->wait_count[i]);", 536 " count += shared_memory->wait_count[i];", 537 " }", 538 " printf(\"%%16s %%9lu (avg per region)\\n\",", 539 " bfs_lname[BFS_STATE], count/(BFS_MAXLOCKS - BFS_STATE));", 540 "#endif", 541 " }", 542 " fflush(stdout);", 543 " x_critical(BFS_PRINT);", 544 " }", 545 "}", 546 "", 547 "void", 548 "bfs_snapshot(void)", 549 "{ clock_t stop_time;", 550 " double delta_time;", 551 " struct tms stop_tm;", 552 " volatile BFS_data *s;", 553 "", 554 " e_critical(BFS_PRINT);", 555 " printf(\"cpu%%02d Depth= %%7lu States= %%8.3g Transitions= %%8.3g \",", 556 " who_am_i, mreached, nstates, nstates+truncs);", 557 " printf(\"Memory= %%9.3f\\t\", memcnt/1048576.);", 558 " printf(\"SharedMLeft= %%4lu \", bfs_left/1048576);", 559 " stop_time = times(&stop_tm);", 560 " delta_time = ((double) (stop_time - start_time))/((double) sysconf(_SC_CLK_TCK));", 561 " if (delta_time > 0.01)", 562 " { printf(\"t= %%6.3g R= %%6.0g\\n\", delta_time, nstates/delta_time);", 563 " } else", 564 " { printf(\"t= %%6.3g R= %%6.0g\\n\", 0., 0.);", 565 " }", 566 " fflush(stdout);", 567 " x_critical(BFS_PRINT);", 568 "", 569 " s = &shared_memory->bfs_data[who_am_i];", 570 " s->mreached = (ulong) mreached;", 571 " s->vsize = (ulong) vsize;", 572 " s->errors = (int) errors;", 573 " s->memcnt = (double) memcnt;", 574 " s->nstates = (double) nstates;", 575 " s->nlinks = (double) nlinks;", 576 " s->truncs = (double) truncs;", 577 " s->memory_left = (ulong) bfs_left;", 578 " s->punted = (ulong) bfs_punt;", 579 " bfs_snapped++; /* for bfs_best */", 580 "}", 581 "", 582 "void", 583 "bfs_shutdown(const char *s)", 584 "{", 585 " bfs_clear_locks(); /* in case we interrupted at a bad point */", 586 " if (!strstr(s, \"early \") || verbose)", 587 " { bfs_printf(\"stop (%%s)\\n\", s);", 588 " }", 589 " bfs_update();", 590 " if (who_am_i == 0)", 591 " { wrapup();", 592 "#ifdef BFS_DISK", 593 " bfs_disk_stop();", 594 "#endif", 595 " }", 596 " bfs_mark_done(2);", 597 " pan_exit(2);", 598 "}", 599 "", 600 "SV_Hold *bfs_free_hold;", 601 "", 602 "SV_Hold *", 603 "bfs_get_hold(void)", 604 "{ SV_Hold *x;", 605 " if (bfs_free_hold)", 606 " { x = bfs_free_hold;", 607 " bfs_free_hold = bfs_free_hold->nxt;", 608 " } else", 609 " { x = (SV_Hold *) sh_malloc((ulong) sizeof(SV_Hold));", 610 " }", 611 " return x;", 612 "}", 613 "", 614 "BFS_Trail *", 615 "bfs_unpack_state(BFS_Slot *n) /* called in bfs_explore_state */", 616 "{ BFS_Trail *otrpt;", 617 " BFS_State *bfs_t;", 618 " int vecsz;", 619 "", 620 " if (!n || !n->s_data || !n->s_data->t_info)", 621 " { bfs_Uerror(\"internal error\");", 622 " }", 623 " otrpt = (BFS_Trail *) ((BFS_State *) n->s_data)->t_info;", 624 "", 625 " trpt->ostate = otrpt->ostate;", 626 " trpt->st = otrpt->st;", 627 " trpt->o_tt = otrpt->o_tt;", 628 " trpt->pr = otrpt->pr;", 629 " trpt->tau = otrpt->tau;", 630 " trpt->o_pm = otrpt->o_pm;", 631 " if (trpt->ostate)", 632 " trpt->o_t = t_id_lkup[otrpt->t_id];", 633 "#if defined(C_States) && (HAS_TRACK==1)", 634 " c_revert((uchar *) &(now.c_state[0]));", 635 "#endif", 636 " if (trpt->o_pm & 4) /* rv succeeded */", 637 " { return (BFS_Trail *) 0; /* revisit not needed */", 638 " }", 639 "#ifndef NOREDUCE", 640 " bfs_nps = 0;", 641 "#endif", 642 " if (trpt->o_pm & 8) /* rv attempt failed */", 643 " { revrv++;", 644 " if (trpt->tau&8)", 645 " { trpt->tau &= ~8; /* break atomic */", 646 "#ifndef NOREDUCE", 647 " } else if (trpt->tau&32) /* void preselection */", 648 " { trpt->tau &= ~32;", 649 " bfs_nps = 1; /* no preselection in repeat */", 650 "#endif", 651 " } }", 652 " trpt->o_pm &= ~(4|8);", 653 " if (trpt->o_tt > mreached)", 654 " { static ulong nr = 0L, nc;", 655 " mreached = trpt->o_tt;", 656 " nc = (long) nstates/FREQ;", 657 " if (nc > nr)", 658 " { nr = nc;", 659 " bfs_snapshot();", 660 " } }", 661 " depth = trpt->o_tt;", 662 " if (depth >= maxdepth)", 663 " {", 664 "#if SYNC", 665 " if (boq != -1)", 666 " { BFS_Trail *x = (BFS_Trail *) trpt->ostate;", 667 " if (x) x->o_pm |= 4; /* rv not failing */", 668 " }", 669 "#endif", 670 " truncs++;", 671 " if (!warned)", 672 " { warned = 1;", 673 " bfs_printf(\"error: max search depth too small\\n\");", 674 " }", 675 " if (bounded)", 676 " { bfs_uerror(\"depth limit reached\");", 677 " }", 678 " return (BFS_Trail *) 0;", 679 " }", 680 "", 681 " bfs_t = n->s_data;", 682 "#if NRUNS>0", 683 " vsize = bfs_t->omask->sz;", 684 "#else", 685 " vsize = ((State *) (bfs_t->osv))->_vsz;", 686 "#endif", 687 "#if SYNC", 688 " boq = bfs_t->boq;", 689 "#endif", 690 "", 691 "#if defined(Q_PROVISO) && !defined(BITSTATE) && defined(FULLSTACK)", 692 " #ifdef USE_TDH", 693 " if (((uchar *)(bfs_t->lstate))) /* if BFS_INQ is set */", 694 " { *((uchar *) bfs_t->lstate) = 0; /* turn it off */", 695 " }", 696 " #else", 697 " if (bfs_t->lstate) /* bfs_par */", 698 " { bfs_t->lstate->tagged = 0; /* bfs_par state removed from q */", 699 " }", 700 " #endif", 701 "#endif", 702 " memcpy((char *) &now, (uchar *) bfs_t->osv, vsize);", 703 "#if !defined(NOCOMP) && !defined(HC) && NRUNS>0", 704 " Mask = (uchar *) bfs_t->omask->sv; /* in shared memory */", 705 "#endif", 706 "#ifdef BFS_CHECK", 707 " if (0) bfs_dump_now(\"got1\");", 708 "#endif", 709 "#ifdef TRIX", 710 " re_populate();", 711 "#else", 712 " #if NRUNS>0", 713 " if (now._nr_pr > 0)", 714 " {", 715 " #if VECTORSZ>32000", 716 " proc_offset = (int *) bfs_t->omask->po;", 717 " #else", 718 " proc_offset = (short *) bfs_t->omask->po;", 719 " #endif", 720 " proc_skip = (uchar *) bfs_t->omask->ps;", 721 " }", 722 " if (now._nr_qs > 0)", 723 " {", 724 " #if VECTORSZ>32000", 725 " q_offset = (int *) bfs_t->omask->qo;", 726 " #else", 727 " q_offset = (short *) bfs_t->omask->qo;", 728 " #endif", 729 " q_skip = (uchar *) bfs_t->omask->qs;", 730 " }", 731 " #endif", 732 "#endif", 733 " vecsz = ((State *) bfs_t->osv)->_vsz;", 734 "#ifdef BFS_CHECK", 735 " assert(vecsz > 0 && vecsz < VECTORSZ);", 736 "#endif", 737 " { SV_Hold *x = bfs_get_hold();", 738 " x->sv = bfs_t->osv;", 739 " x->nxt = bfs_svfree[vecsz];", 740 " bfs_svfree[vecsz] = x;", 741 " bfs_t->osv = (State *) 0;", 742 " }", 743 "#if NRUNS>0", 744 " bfs_keep(bfs_t->omask);", 745 "#endif", 746 "", 747 "#ifdef BFS_CHECK", 748 " if (0) bfs_dump_now(\"got2\");", 749 " if (0) view_state(\"after\");", 750 "#endif", 751 " return (BFS_Trail *) bfs_t->t_info;", 752 "}", 753 "void", 754 "bfs_initial_state(void)", 755 "{", 756 "#ifdef BFS_CHECK", 757 " assert(trpt != NULL);", 758 "#endif", 759 " trpt->ostate = (H_el *) 0;", 760 " trpt->o_tt = -1;", 761 " trpt->tau = 0;", 762 "#ifdef VERI", 763 " trpt->tau |= 4; /* claim moves first */", 764 "#endif", 765 " bfs_store_state(trpt, boq); /* initial state : bfs_lib.c */", 766 "}", 767 "", 768 "#ifdef BITSTATE", 769 " #define bfs_do_store(v, n) b_store(v, n)", 770 "#else", 771 " #ifdef USE_TDH", 772 " #define bfs_do_store(v, n) o_store(v, n)", 773 " #else", 774 " #define bfs_do_store(v, n) h_store(v, n)", 775 " #endif", 776 "#endif", 777 "", 778 "#ifdef BFS_SEP_HASH", 779 "int", 780 "bfs_seen_before(void)", 781 "{ /* cannot set trpt->tau |= 64 to mark successors outside stack */", 782 " /* since the check is done remotely and the trpt value is gone */", 783 " #ifdef VERI", 784 " if (!trpt->ostate /* initial state */", 785 " || ((trpt->tau&4) /* starting claim moves(s) */", 786 " && !(((BFS_Trail *)trpt->ostate)->tau&4))) /* prev move: prog */", 787 " { return 0; /* claim move: mid-state not stored */", 788 " } /* else */", 789 " #endif", 790 " if (!bfs_do_store((char *)&now, vsize)) /* sep_hash */", 791 " { nstates++; /* local count */", 792 " return 0; /* new state */", 793 " }", 794 " #ifdef BFS_CHECK", 795 " bfs_printf(\"seen before\\n\");", 796 " #endif", 797 " truncs++;", 798 " return 1; /* old state */", 799 "}", 800 "#endif", 801 "", 802 "void", 803 "bfs_explore_state(BFS_Slot *v) /* generate all successors of v */", 804 "{ BFS_Trail *otrpt;", 805 " Trans *t;", 806 "#ifdef HAS_UNLESS", 807 " int E_state;", 808 "#endif", 809 " int tt;", 810 " short II, To = BASE, From = (short) (now._nr_pr-1);", 811 " short oboq = boq;", 812 " uchar _n, _m, ot;", 813 "", 814 " memset(ntrpt, 0, sizeof(Trail));", 815 " otrpt = bfs_unpack_state(v); /* BFS_Trail */", 816 "", 817 " if (!otrpt) { return; } /* e.g., depth limit reached */", 818 "#ifdef L_BOUND", 819 " #if defined(VERBOSE)", 820 " bfs_printf(\"Unpacked state with l_bound %%d -- sds %%p\\n\",", 821 " now._l_bnd, now._l_sds);", 822 " #endif", 823 "#endif", 824 "", 825 "#if defined(C_States) && (HAS_TRACK==1)", 826 " c_revert((uchar *) &(now.c_state[0]));", 827 "#endif", 828 "", 829 "#ifdef BFS_SEP_HASH", 830 " if (bfs_seen_before()) return;", 831 "#endif", 832 "", 833 "#ifdef VERI", /* could move to just before store_state */ 834 " if (now._nr_pr == 0 /* claim terminated */", 835 " || stopstate[((Pclaim *)pptr(0))->_t][((Pclaim *)pptr(0))->_p])", 836 " { bfs_uerror(\"end state in claim reached\");", 837 " }", 838 "#endif", 839 " trpt->tau &= ~1; /* timeout off */", 840 "#ifdef VERI", 841 " if (trpt->tau&4) /* claim move */", 842 " { trpt->tau |= (otrpt->tau)&1; /* inherit from prog move */", 843 " From = To = 0; /* claim */", 844 " goto Repeat_two;", 845 " }", 846 "#endif", 847 "#ifndef NOREDUCE", 848 " if (boq == -1 && !(trpt->tau&8) && bfs_nps == 0)", 849 " for (II = now._nr_pr-1; II >= BASE; II -= 1)", 850 " {", 851 "Pickup: _this = pptr(II);", 852 " tt = (int) ((P0 *)_this)->_p;", 853 " ot = (uchar) ((P0 *)_this)->_t;", 854 " if (trans[ot][tt]->atom & 8)", 855 " { t = trans[ot][tt];", 856 " if (t->qu[0] != 0)", 857 " { if (!q_cond(II, t))", 858 " continue;", 859 " }", 860 " From = To = II;", 861 " trpt->tau |= 32; /* preselect marker */", 862 " #ifdef VERBOSE", 863 " bfs_printf(\"%%3ld: proc %%d PreSelected (tau=%%d)\\n\", ", 864 " depth, II, trpt->tau);", 865 " #endif", 866 " goto Repeat_two;", 867 " } }", 868 " trpt->tau &= ~32;", 869 "#endif", 870 "", 871 "Repeat_one:", 872 " if (trpt->tau&8)", 873 " { From = To = (short ) trpt->pr; /* atomic */", 874 " } else", 875 " { From = now._nr_pr-1;", 876 " To = BASE;", 877 " }", 878 "#if defined(VERI) || !defined(NOREDUCE) || defined(ETIM)", 879 "Repeat_two: /* MainLoop */", 880 "#endif", 881 " _n = _m = 0;", 882 " for (II = From; II >= To; II -= 1) /* all processes */", 883 " {", 884 "#ifdef BFS_CHECK", 885 " bfs_printf(\"proc %%d (%%d - %%d)\\n\", II, From, To);", 886 "#endif", 887 "#if SYNC ", 888 " if (boq != -1 && trpt->pr == II)", 889 " { continue; /* no rendezvous with same proc */", 890 " }", 891 "#endif", 892 " _this = pptr(II);", 893 " tt = (int) ((P0 *)_this)->_p;", 894 " ot = (uchar) ((P0 *)_this)->_t;", 895 " ntrpt->pr = (uchar) II;", 896 " ntrpt->st = tt; ", 897 " trpt->o_pm &= ~1; /* no move yet */", 898 "#ifdef EVENT_TRACE", 899 " trpt->o_event = now._event;", 900 "#endif", 901 "#ifdef HAS_PRIORITY", 902 " if (!highest_priority(((P0 *)_this)->_pid, II, t))", 903 " { continue;", 904 " }", 905 "#else", 906 " #ifdef HAS_PROVIDED", 907 " if (!provided(II, ot, tt, t))", 908 " { continue;", 909 " }", 910 " #endif", 911 "#endif", 912 "#ifdef HAS_UNLESS", 913 " E_state = 0;", 914 "#endif", 915 " for (t = trans[ot][tt]; t; t = t->nxt) /* all process transitions */", 916 " {", 917 "#ifdef BFS_CHECK", 918 " assert(t_id_lkup[t->t_id] == t); /* for reverse lookup in bfs_unpack_state */", 919 "#endif", 920 "#ifdef VERBOSE", 921 " if (0) bfs_printf(\"\\tproc %%d tr %%d\\n\", II, t->forw);", 922 "#endif", 923 "#ifdef HAS_UNLESS", 924 " if (E_state > 0", 925 " && E_state != t->e_trans)", 926 " break;", 927 "#endif", 928 " /* trpt->o_t = */ ntrpt->o_t = t;", 929 " oboq = boq;", 930 "", 931 " if (!(_m = do_transit(t, II)))", 932 " continue;", 933 "", 934 " trpt->o_pm |= 1; /* we moved */", 935 " (trpt+1)->o_m = _m; /* for unsend */", 936 "#ifdef PEG", 937 " peg[t->forw]++;", 938 "#endif", 939 "#ifdef VERBOSE", 940 " e_critical(BFS_PRINT);", 941 " printf(\"%%3ld: proc %%d exec %%d, \",", 942 " depth, II, t->forw);", 943 " printf(\"%%d to %%d, %%s %%s %%s\",", 944 " tt, t->st, t->tp,", 945 " (t->atom&2)?\"atomic\":\"\",", 946 " (boq != -1)?\"rendez-vous\":\"\");", 947 " #ifdef HAS_UNLESS", 948 " if (t->e_trans)", 949 " printf(\" (escapes to state %%d)\", t->st);", 950 " #endif", 951 " printf(\" %%saccepting [tau=%%d]\\n\",", 952 " (trpt->o_pm&2)?\"\":\"non-\", trpt->tau);", 953 " x_critical(BFS_PRINT);", 954 "#endif", 955 "#ifdef HAS_UNLESS", 956 " E_state = t->e_trans;", 957 " #if SYNC>0", 958 " if (t->e_trans > 0 && boq != -1)", 959 " { fprintf(efd, \"error: rendezvous stmnt in the escape clause\\n\");", 960 " fprintf(efd, \" of unless stmnt not compatible with -DBFS\\n\");", 961 " pan_exit(1);", 962 " }", 963 " #endif", 964 "#endif", 965 " if (t->st > 0)", 966 " { ((P0 *)_this)->_p = t->st;", 967 " }", 968 " /* use the ostate ptr, with type *H_el, to temporarily store *BFS_Trail */", 969 "#ifdef BFS_NOTRAIL", 970 " ntrpt->ostate = (H_el *) 0; /* no error-traces in this mode */", 971 "#else", 972 " ntrpt->ostate = (H_el *) otrpt; /* parent stackframe */", 973 "#endif", 974 " /* ntrpt->st = tt; * was already set above */", 975 "", 976 " if (boq == -1 && (t->atom&2)) /* atomic */", 977 " { ntrpt->tau = 8; /* record for next move */", 978 " } else", 979 " { ntrpt->tau = 0; /* no timeout or preselect etc */", 980 " }", 981 "#ifdef VERI", 982 " ntrpt->tau |= trpt->tau&4; /* if claim, inherit */", 983 " if (boq == -1 && !(ntrpt->tau&8)) /* unless rv or atomic */", 984 " { if (ntrpt->tau&4) /* claim */", 985 " { ntrpt->tau &= ~4; /* switch to prog */", 986 " } else", 987 " { ntrpt->tau |= 4; /* switch to claim */", 988 " } }", 989 "#endif", 990 "#ifdef L_BOUND", 991 " { uchar obnd = now._l_bnd;", 992 " uchar *os = now._l_sds;", 993 " #ifdef VERBOSE", 994 " bfs_printf(\"saving bound %%d -- sds %%p\\n\", obnd, (void *) os);", 995 " #endif", 996 "#endif", 997 "", 998 " bfs_store_state(ntrpt, oboq);", 999 "#ifdef EVENT_TRACE", 1000 " now._event = trpt->o_event;", 1001 "#endif", 1002 " /* undo move and generate other successor states */", 1003 " trpt++; /* this is where ovals and ipt are set */", 1004 " do_reverse(t, II, _m); /* restore now. */", 1005 "#ifdef L_BOUND", 1006 " #ifdef VERBOSE", 1007 " bfs_printf(\"restoring bound %%d -- sds %%p\\n\", obnd, (void *) os);", 1008 " #endif", 1009 " now._l_bnd = obnd;", 1010 " now._l_sds = os;", 1011 " }", 1012 "#endif", 1013 " trpt--;", 1014 "#ifdef VERBOSE", 1015 " e_critical(BFS_PRINT);", 1016 " printf(\"%%3ld: proc %%d \", depth, II);", 1017 " printf(\"reverses %%d, %%d to %%d,\", t->forw, tt, t->st);", 1018 " printf(\" %%s [abit=%%d,adepth=%%d,\", t->tp, now._a_t, 0);", 1019 " printf(\"tau=%%d,%%d]\\n\", trpt->tau, (trpt-1)->tau);", 1020 " x_critical(BFS_PRINT);", 1021 "#endif", 1022 " reached[ot][t->st] = 1;", 1023 " reached[ot][tt] = 1;", 1024 "", 1025 " ((P0 *)_this)->_p = tt;", 1026 " _n |= _m;", 1027 " } }", 1028 "#ifdef VERBOSE", 1029 " bfs_printf(\"done _n = %%d\\n\", _n);", 1030 "#endif", 1031 "", 1032 "#ifndef NOREDUCE", 1033 " /* preselected - no succ definitely outside stack */", 1034 " if ((trpt->tau&32) && !(trpt->tau&64))", 1035 " { From = now._nr_pr-1; To = BASE;", 1036 " #ifdef VERBOSE", 1037 " bfs_printf(\"%%3ld: proc %%d UnSelected (_n=%%d, tau=%%d)\\n\", ", 1038 " depth, II+1, (int) _n, trpt->tau);", 1039 " #endif", 1040 " _n = 0; trpt->tau &= ~32;", 1041 " if (II >= BASE)", 1042 " { goto Pickup;", 1043 " }", 1044 " goto Repeat_two;", 1045 " }", 1046 " trpt->tau &= ~(32|64);", 1047 "#endif", 1048 " if (_n == 0", 1049 "#ifdef VERI", 1050 " && !(trpt->tau&4)", 1051 "#endif", 1052 " )", 1053 " { /* no successor states generated */", 1054 " if (boq != -1) /* was rv move */", 1055 " { BFS_Trail *x = (BFS_Trail *) trpt->ostate; /* pre-rv state */", 1056 " if (x && ((x->tau&8) || (x->tau&32))) /* break atomic or preselect */", 1057 " { x->o_pm |= 8; /* mark failure */", 1058 " _this = pptr(otrpt->pr);", 1059 " ((P0 *) _this)->_p = otrpt->st; /* reset state */", 1060 " unsend(boq); /* retract rv offer */", 1061 " boq = -1;", 1062 "#ifdef VERBOSE", 1063 " printf(\"repush state\\n\");", 1064 "#endif", 1065 " bfs_push_state(NULL, x, x->o_tt); /* repush rv fail */", 1066 " } /* else the rv need not be retried */", 1067 " } else if (now._nr_pr > BASE) /* possible deadlock */", 1068 " { if ((trpt->tau&8)) /* atomic step blocked */", 1069 " { trpt->tau &= ~(1|8); /* 1=timeout, 8=atomic */", 1070 " goto Repeat_one;", 1071 " }", 1072 "#ifdef ETIM", 1073 " /* if timeouts were used in the model */", 1074 " if (!(trpt->tau&1))", 1075 " { trpt->tau |= 1; /* enable timeout */", 1076 " goto Repeat_two;", 1077 " }", 1078 "#endif", 1079 " if (!noends && !endstate())", 1080 " { bfs_uerror(\"invalid end state.\");", 1081 " }", 1082 " }", 1083 "#ifdef VERI", 1084 " else /* boq == -1 && now._nr_pr == BASE && trpt->tau != 4 */", 1085 " { trpt->tau |= 4; /* switch to claim for stutter moves */", 1086 " #ifdef VERBOSE", 1087 " printf(\"%%3ld: proc -1 exec -1, (stutter move)\\n\", depth, II);", 1088 " #endif", 1089 " bfs_store_state(trpt, boq);", /* doesn't store it but queues it */ 1090 " #ifdef VERBOSE", 1091 " printf(\"%%3ld: proc -1 reverses -1, (stutter move)\\n\", depth, II);", 1092 " #endif", 1093 " trpt->tau &= ~4; /* undo, probably not needed */", 1094 " }", 1095 "#endif", 1096 " }", 1097 "#ifdef BFS_NOTRAIL", 1098 " bfs_release_trail(otrpt);", 1099 "#endif", 1100 "}", 1101 "#if !defined(BFS_FIFO) && !defined(BFS_NORECYCLE)", 1102 "void", 1103 "bfs_recycle(BFS_Slot *n)", 1104 "{", 1105 " #ifdef BFS_CHECK", 1106 " assert(n != &bfs_null);", 1107 " #endif", 1108 " n->nxt = bfs_free_slot;", 1109 " bfs_free_slot = n;", 1110 "", 1111 " #ifdef BFS_CHECK", 1112 " bfs_printf(\"recycles %%s -- %%p\\n\",", 1113 " n->s_data?\"STATE\":\"EMPTY\", (void *) n);", 1114 " #endif", 1115 "}", 1116 "#endif", 1117 "#ifdef BFS_FIFO", 1118 "int", 1119 "bfs_empty(int p)", /* return Cores if all empty or index of first non-empty q of p */ 1120 "{ int i;", 1121 " const int dst = 0;", 1122 " for (i = 0; i < Cores; i++)", 1123 " { if (shared_memory->head[dst][p][i] != (BFS_Slot *) 0)", 1124 " {", 1125 " volatile BFS_Slot *x = shared_memory->head[dst][p][i];", 1126 " while (x && x->type == DELETED)", 1127 " { x = x->nxt;", 1128 " }", 1129 " if (!x)", 1130 " { continue;", 1131 " }", 1132 " if (p == who_am_i)", 1133 " { shared_memory->head[dst][p][i] = x;", 1134 " }", 1135 " #ifdef BFS_CHECK", 1136 " bfs_printf(\"input q [%%d][%%d][%%d] !empty\\n\",", 1137 " dst, p, i);", 1138 " #endif", 1139 " return i;", 1140 " } }", 1141 " #ifdef BFS_CHECK", 1142 " bfs_printf(\"all input qs [%%d][%%d][0..max] empty\\n\",", 1143 " dst, p);", 1144 " #endif ", 1145 " return Cores;", 1146 "}", 1147 "#endif", 1148 "#ifdef BFS_DISK", 1149 "void", 1150 "bfs_ewrite(int fd, const void *p, size_t count)", 1151 "{", 1152 " if (write(fd, p, count) != count)", 1153 " { perror(\"diskwrite\");", 1154 " Uerror(\"aborting\");", 1155 " }", 1156 "}", 1157 "", 1158 "void", 1159 "bfs_eread(int fd, void *p, size_t count)", 1160 "{", 1161 " if (read(fd, p, count) != count)", 1162 " { perror(\"diskread\");", 1163 " Uerror(\"aborting\");", 1164 " }", 1165 "}", 1166 "", 1167 "void", 1168 "bfs_sink_disk(int who_are_you, BFS_Slot *n)", 1169 "{ SV_Hold *x;", 1170 "#ifdef VERBOSE", 1171 " bfs_printf(\"sink_disk -> %%d\\n\", who_are_you);", 1172 "#endif", 1173 " bfs_ewrite(bfs_out_fd[who_are_you], (const void *) n->s_data->t_info, sizeof(BFS_Trail));", 1174 " bfs_ewrite(bfs_out_fd[who_are_you], (const void *) &vsize, sizeof(ulong));", 1175 " bfs_ewrite(bfs_out_fd[who_are_you], &now, vsize);", 1176 "", 1177 " bfs_release_trail(n->s_data->t_info);", 1178 " n->s_data->t_info = (BFS_Trail *) 0;", 1179 "", 1180 "#if NRUNS>0", 1181 " bfs_ewrite(bfs_out_fd[who_are_you], (const void *) &(n->s_data->omask), sizeof(EV_Hold *));", 1182 "#endif", 1183 "#ifdef Q_PROVISO", 1184 " bfs_ewrite(bfs_out_fd[who_are_you], (const void *) &(n->s_data->lstate), sizeof(H_el *));", 1185 "#endif", 1186 "#if SYNC>0", 1187 " bfs_ewrite(bfs_out_fd[who_are_you], (const void *) &(n->s_data->boq), sizeof(short));", 1188 "#endif", 1189 "#if VERBOSE", 1190 " bfs_ewrite(bfs_out_fd[who_are_you], (const void *) &(n->s_data->nr), sizeof(ulong));", 1191 "#endif", 1192 " shared_memory->bfs_out_cnt[who_am_i] = 1;", /* wrote at least one state */ 1193 "}", 1194 "void", 1195 "bfs_source_disk(int fd, volatile BFS_Slot *n)", 1196 "{ ulong nb; /* local temporary */", 1197 " SV_Hold *x;", 1198 "#ifdef VERBOSE", 1199 " bfs_printf(\"source_disk <- %%d\\n\", who_am_i);", 1200 "#endif", 1201 " n->s_data->t_info = bfs_grab_trail();", 1202 " bfs_eread(fd, (void *) n->s_data->t_info, sizeof(BFS_Trail));", 1203 " bfs_eread(fd, (void *) &nb, sizeof(ulong));", 1204 "", 1205 " x = bfs_new_sv(nb); /* space for osv isn't already allocated */", 1206 " n->s_data->osv = x->sv;", 1207 " x->sv = (State *) 0;", 1208 " x->nxt = bfs_free_hold;", 1209 " bfs_free_hold = x;", 1210 "", 1211 " bfs_eread(fd, (void *) n->s_data->osv, (size_t) nb);", 1212 "#if NRUNS>0", 1213 " bfs_eread(fd, (void *) &(n->s_data->omask), sizeof(EV_Hold *));", 1214 "#endif", 1215 "#ifdef Q_PROVISO", 1216 " bfs_eread(fd, (void *) &(n->s_data->lstate), sizeof(H_el *));", 1217 "#endif", 1218 "#if SYNC>0", 1219 " bfs_eread(fd, (void *) &(n->s_data->boq), sizeof(short));", 1220 "#endif", 1221 "#if VERBOSE", 1222 " bfs_eread(fd, (void *) &(n->s_data->nr), sizeof(ulong));", 1223 "#endif", 1224 "}", 1225 "#endif", 1226 "", 1227 "#ifndef BFS_QSZ", 1228 " #ifdef BFS_STAGGER", 1229 "static BFS_Slot *bfs_stage[BFS_STAGGER];", 1230 "", 1231 "static void", 1232 "bfs_stagger_flush(void)", 1233 "{ int i, who_are_you;", 1234 " int dst = 1 - bfs_toggle;", 1235 " BFS_Slot *n;", 1236 " who_are_you = (rand()%%Cores);", /* important: all to the same cpu, but reversed */ 1237 " for (i = bfs_stage_cnt-1; i >= 0; i--)", 1238 " { n = bfs_stage[i];", 1239 " #ifdef BFS_DISK", 1240 " bfs_sink_disk(who_are_you, n);", 1241 " bfs_stage[i] = (BFS_Slot *) 0;", 1242 " #endif", 1243 " n->nxt = (BFS_Slot *) shared_memory->head[dst][who_are_you][who_am_i];", 1244 " shared_memory->head[dst][who_are_you][who_am_i] = n;", 1245 " /* bfs_sent++; */", 1246 " }", 1247 " #ifdef VERBOSE", 1248 " bfs_printf(\"stagger flush %%d states to %%d\\n\",", 1249 " bfs_stage_cnt, who_are_you);", 1250 " #endif", 1251 " bfs_stage_cnt = 0;", 1252 "}", 1253 "", 1254 "void", 1255 "bfs_stagger_add(BFS_Slot *n)", 1256 "{", 1257 " if (bfs_stage_cnt == BFS_STAGGER)", 1258 " { bfs_stagger_flush();", 1259 " }", 1260 " bfs_stage[bfs_stage_cnt++] = n;", 1261 "}", 1262 " #endif", 1263 "#endif", 1264 "", 1265 "void", 1266 "bfs_push_state(Trail *x, BFS_Trail *y, int tt)", 1267 "{ int who_are_you;", 1268 "#ifdef BFS_FIFO", 1269 " const int dst = 0;", 1270 "#else", 1271 " int dst = 1 - bfs_toggle;", 1272 "#endif", 1273 "#ifdef BFS_QSZ", 1274 " uint z;", 1275 " if (bfs_keep_state > 0)", 1276 " { who_are_you = bfs_keep_state - 1;", 1277 " } else", 1278 " { who_are_you = (rand()%%Cores);", 1279 " }", 1280 " z = shared_memory->bfs_ix[dst][who_are_you][who_am_i];", 1281 " if (z >= BFS_QSZ)", 1282 " { static int warned_qloss = 0;", 1283 " if (warned_qloss == 0 && who_am_i == 0)", 1284 " { warned_qloss++;", 1285 " bfs_printf(\"BFS_QSZ too small - losing states\\n\");", 1286 " }", 1287 " bfs_punt++;", 1288 " return;", 1289 " }", 1290 " shared_memory->bfs_ix[dst][who_are_you][who_am_i] = z+1;", 1291 " BFS_Slot *n = bfs_pack_state(x, y, tt, bfs_prep_slot(y, ", 1292 " (BFS_Slot *) &(shared_memory->bfsq[dst][who_are_you][who_am_i][z])));", 1293 "#else", 1294 " BFS_Slot *n = bfs_pack_state(x, y, tt, bfs_new_slot(y));", 1295 "", 1296 " #ifdef BFS_GREEDY", 1297 " who_are_you = who_am_i; /* for testing only */", 1298 " #else", 1299 " if (bfs_keep_state > 0)", 1300 " { who_are_you = bfs_keep_state - 1;", 1301 " } else", 1302 " {", 1303 " #ifdef BFS_STAGGER", 1304 " who_are_you = -1;", 1305 " bfs_stagger_add(n);", 1306 " goto done;", 1307 " #else", 1308 " who_are_you = (rand()%%Cores);", 1309 " #endif", 1310 " }", 1311 " #endif", 1312 " #ifdef BFS_FIFO", 1313 " if (!shared_memory->tail[dst][who_are_you][who_am_i])", 1314 " { shared_memory->dels[dst][who_are_you][who_am_i] =", 1315 " shared_memory->tail[dst][who_are_you][who_am_i] =", 1316 " shared_memory->head[dst][who_are_you][who_am_i] = n;", 1317 " } else", 1318 " { shared_memory->tail[dst][who_are_you][who_am_i]->nxt = n;", 1319 " shared_memory->tail[dst][who_are_you][who_am_i] = n;", 1320 " }", 1321 " shared_memory->bfs_idle[who_are_you] = 0;", 1322 " #else", 1323 " #ifdef BFS_DISK", 1324 " bfs_sink_disk(who_are_you, n);", 1325 " #endif", 1326 " n->nxt = (BFS_Slot *) shared_memory->head[dst][who_are_you][who_am_i];", 1327 " shared_memory->head[dst][who_are_you][who_am_i] = n;", 1328 " #endif", 1329 " #ifdef BFS_STAGGER", 1330 "done:", 1331 " #endif", 1332 "#endif", /* BFS_QSZ */ 1333 "#ifdef VERBOSE", 1334 " bfs_printf(\"PUT STATE (depth %%ld, nr %%u) to %%d -- s_data: %%p\\n\",", 1335 " tt, n->s_data->nr, who_are_you, n->s_data);", 1336 "#endif", 1337 " bfs_sent++;", 1338 "}", 1339 "", 1340 "BFS_Slot *", 1341 "bfs_next(void)", 1342 "{ volatile BFS_Slot *n = &bfs_null;", 1343 " #ifdef BFS_FIFO", 1344 " const int src = 0;", 1345 " bfs_qscan = bfs_empty(who_am_i);", 1346 " #else", 1347 " const int src = bfs_toggle;", 1348 " #ifdef BFS_QSZ", 1349 " while (bfs_qscan < Cores", 1350 " && shared_memory->bfs_ix[src][who_am_i][bfs_qscan] == 0)", 1351 " { bfs_qscan++;", 1352 " }", 1353 " #else", 1354 " while (bfs_qscan < Cores", 1355 " && shared_memory->head[src][who_am_i][bfs_qscan] == (BFS_Slot *) 0)", 1356 " { bfs_qscan++;", 1357 " }", 1358 " #endif", 1359 " #endif", 1360 " if (bfs_qscan < Cores)", 1361 " {", 1362 " #ifdef BFS_FIFO", /* no wait for toggles */ 1363 " shared_memory->bfs_idle[who_am_i] = 0;", 1364 " for (n = shared_memory->head[src][who_am_i][bfs_qscan]; n; n = n->nxt)", 1365 " { if (n->type != DELETED)", 1366 " { break;", 1367 " } }", 1368 " #ifdef BFS_CHECK", 1369 " assert(n && n->type == STATE); /* q cannot be empty */", 1370 " #endif", 1371 " if (n->nxt)", 1372 " { shared_memory->head[src][who_am_i][bfs_qscan] = n->nxt;", 1373 " }", /* else, do not remove it - yet - avoid empty queues */ 1374 " n->type = DELETED;", 1375 " #else", 1376 " #ifdef BFS_QSZ", 1377 " uint x = --shared_memory->bfs_ix[src][who_am_i][bfs_qscan];", 1378 " n = &(shared_memory->bfsq[src][who_am_i][bfs_qscan][x]);", 1379 " #else", 1380 " n = shared_memory->head[src][who_am_i][bfs_qscan];", 1381 " shared_memory->head[src][who_am_i][bfs_qscan] = n->nxt;", 1382 " #if defined(BFS_FIFO) && defined(BFS_CHECK)", 1383 " assert(n->type == STATE);", 1384 " #endif", 1385 " n->nxt = (BFS_Slot *) 0;", 1386 " #endif", 1387 " #ifdef BFS_DISK", 1388 " /* the states actually show up in reverse order (FIFO iso LIFO) here */", 1389 " /* but that doesn't really matter as long as the count is right */", 1390 " bfs_source_disk(bfs_inp_fd[bfs_qscan], n); /* get the data */", 1391 " #endif", 1392 1393 " #endif", 1394 " #ifdef BFS_CHECK", 1395 " bfs_printf(\"rcv STATE from [%%d][%%d][%%d]\\n\",", 1396 " src, who_am_i, bfs_qscan);", 1397 " #endif", 1398 " bfs_rcvd++;", 1399 " } else", 1400 " {", 1401 " #if defined(BFS_STAGGER) && !defined(BFS_QSZ)", 1402 " if (bfs_stage_cnt > 0)", 1403 " { bfs_stagger_flush();", 1404 " }", 1405 " #endif", 1406 " shared_memory->bfs_idle[who_am_i] = 1;", 1407 " #if defined(BFS_FIFO) && defined(BFS_CHECK)", 1408 " assert(n->type == EMPTY);", 1409 " #endif", 1410 " }", 1411 " return (BFS_Slot *) n;", 1412 "}", 1413 "", 1414 "int", 1415 "bfs_all_empty(void)", 1416 "{ int i;", 1417 "#ifdef BFS_DISK", 1418 " for (i = 0; i < Cores; i++)", 1419 " { if (shared_memory->bfs_out_cnt[i] != 0)", 1420 " {", 1421 " #ifdef VERBOSE", 1422 " bfs_printf(\"bfs_all_empty %%d not empty\\n\", i);", 1423 " #endif", 1424 " return 0;", 1425 " } }", 1426 "#else", 1427 " int p;", 1428 " #ifdef BFS_FIFO", 1429 " const int dst = 0;", 1430 " #else", 1431 " int dst = 1 - bfs_toggle; /* next generation */", 1432 " #endif", 1433 " for (p = 0; p < Cores; p++)", 1434 " for (i = 0; i < Cores; i++)", 1435 " #ifdef BFS_QSZ", 1436 " { if (shared_memory->bfs_ix[dst][p][i] > 0)", 1437 " #else", 1438 " { if (shared_memory->head[dst][p][i] != (BFS_Slot *) 0)", 1439 " #endif", 1440 " { return 0;", 1441 " } }", 1442 "#endif", 1443 "#ifdef VERBOSE", 1444 " bfs_printf(\"bfs_all_empty\\n\");", 1445 "#endif", 1446 " return 1;", 1447 "}", 1448 "", 1449 "#ifdef BFS_FIFO", 1450 "BFS_Slot *", 1451 "bfs_sweep(void)", 1452 "{ BFS_Slot *n;", 1453 " int i;", 1454 " for (i = 0; i < Cores; i++)", 1455 " for (n = (BFS_Slot *) shared_memory->dels[0][who_am_i][i];", 1456 " n && n != shared_memory->head[0][who_am_i][i];", 1457 " n = n->nxt)", 1458 " { if (n->type == DELETED && n->nxt)", 1459 " { shared_memory->dels[0][who_am_i][i] = n->nxt;", 1460 " n->nxt = (BFS_Slot *) 0;", 1461 " return n;", 1462 " } }", 1463 " return (BFS_Slot *) sh_malloc((ulong) sizeof(BFS_Slot));", 1464 "}", 1465 "#endif", 1466 "", 1467 "typedef struct BFS_T_Hold BFS_T_Hold;", 1468 "struct BFS_T_Hold {", 1469 " volatile BFS_Trail *t;", 1470 " BFS_T_Hold *nxt;", 1471 "};", 1472 "BFS_T_Hold *bfs_t_held, *bfs_t_free;", 1473 "", 1474 "BFS_Trail *", 1475 "bfs_grab_trail(void)", /* call in bfs_source_disk and bfs_new_slot */ 1476 "{ BFS_Trail *t;", 1477 " BFS_T_Hold *h;", 1478 "", 1479 "#ifdef VERBOSE", 1480 " bfs_printf(\"grab trail - bfs_t_held %%p\\n\", (void *) bfs_t_held);", 1481 "#endif", 1482 " if (bfs_t_held)", 1483 " { h = bfs_t_held;", 1484 " bfs_t_held = bfs_t_held->nxt;", 1485 " t = (BFS_Trail *) h->t;", 1486 " h->t = (BFS_Trail *) 0; /* make sure it cannot be reused */", 1487 " h->nxt = bfs_t_free;", 1488 " bfs_t_free = h;", 1489 "", 1490 " } else", 1491 " { t = (BFS_Trail *) sh_malloc((ulong) sizeof(BFS_Trail));", 1492 " }", 1493 "#ifdef BFS_CHECK", 1494 " assert(t);", 1495 "#endif", 1496 " t->ostate = (H_el *) 0;", 1497 "#ifdef VERBOSE", 1498 " bfs_printf(\"grab trail %%p\\n\", (void *) t);", 1499 "#endif", 1500 " return t;", 1501 "}", 1502 "", 1503 "#if defined(BFS_DISK) || defined(BFS_NOTRAIL)", 1504 "void", 1505 "bfs_release_trail(BFS_Trail *t)", /* call in bfs_sink_disk (not bfs_recycle) */ 1506 "{ BFS_T_Hold *h;", 1507 " #ifdef BFS_CHECK", 1508 " assert(t);", 1509 " #endif", 1510 " #ifdef VERBOSE", 1511 " bfs_printf(\"release trail %%p\\n\", (void *) t);", 1512 " #endif", 1513 " if (bfs_t_free)", 1514 " { h = bfs_t_free;", 1515 " bfs_t_free = bfs_t_free->nxt;", 1516 " } else", 1517 " { h = (BFS_T_Hold *) emalloc(sizeof(BFS_T_Hold));", 1518 " }", 1519 " h->t = t;", 1520 " h->nxt = bfs_t_held;", 1521 " bfs_t_held = h;", 1522 " #ifdef VERBOSE", 1523 " bfs_printf(\"release trail - bfs_t_held %%p\\n\", (void *) bfs_t_held);", 1524 " #endif", 1525 "}", 1526 "#endif", 1527 "", 1528 "#ifndef BFS_QSZ", 1529 "BFS_Slot *", 1530 "bfs_new_slot(BFS_Trail *f)", 1531 "{ BFS_Slot *t;", 1532 "", 1533 "#ifdef BFS_FIFO", 1534 " t = bfs_sweep();", 1535 "#else", 1536 " if (bfs_free_slot) /* local */", 1537 " { t = bfs_free_slot;", 1538 " bfs_free_slot = bfs_free_slot->nxt;", 1539 " t->nxt = (BFS_Slot *) 0;", 1540 " } else", 1541 " { t = (BFS_Slot *) sh_malloc((ulong) sizeof(BFS_Slot));", 1542 " }", 1543 "#endif", 1544 " if (t->s_data)", 1545 " { memset(t->s_data, 0, sizeof(BFS_State));", 1546 " } else", 1547 " { t->s_data = (BFS_State *) sh_malloc((ulong) sizeof(BFS_State));", 1548 " }", 1549 "", 1550 " /* we keep a ptr to the frame of parent states, which is */", 1551 " /* used for reconstructing path and recovering failed rvs etc */", 1552 " /* we should not overwrite the data at this address with a memset */", 1553 "", 1554 " if (f)", 1555 " { t->s_data->t_info = f;", 1556 " } else", 1557 " { t->s_data->t_info = bfs_grab_trail();", 1558 " }", 1559 " return t;", 1560 "}", 1561 "#else", 1562 "BFS_Slot *", 1563 "bfs_prep_slot(BFS_Trail *f, BFS_Slot *t)", 1564 "{", 1565 " if (t->s_data)", 1566 " { memset(t->s_data, 0, sizeof(BFS_State));", 1567 " } else", 1568 " { t->s_data = (BFS_State *) sh_malloc((ulong) sizeof(BFS_State));", 1569 " }", 1570 " if (f)", 1571 " { t->s_data->t_info = f;", 1572 " } else", 1573 " { t->s_data->t_info = bfs_grab_trail();", 1574 " }", 1575 " return t;", 1576 "}", 1577 "#endif", 1578 "", 1579 "SV_Hold *", 1580 "bfs_new_sv(int n)", 1581 "{ SV_Hold *h;", 1582 "", 1583 " if (bfs_svfree[n])", 1584 " { h = bfs_svfree[n];", 1585 " bfs_svfree[n] = h->nxt;", 1586 " h->nxt = (SV_Hold *) 0;", 1587 " } else", 1588 " { h = (SV_Hold *) sh_malloc((ulong) sizeof(SV_Hold));", 1589 "#if 0", 1590 " h->sz = n;", 1591 "#endif", 1592 " h->sv = (State *) sh_malloc((ulong)(sizeof(State) - VECTORSZ + n));", 1593 " }", 1594 " memcpy((char *)h->sv, (char *)&now, n);", 1595 " return h;", 1596 "}", 1597 "#if NRUNS>0", 1598 "static EV_Hold *kept[VECTORSZ]; /* local */", 1599 "", 1600 "static void", 1601 "bfs_keep(EV_Hold *v)", 1602 "{ EV_Hold *h;", 1603 "", 1604 " for (h = kept[v->sz]; h; h = h->nxt) /* check local list */", 1605 " { if (v->nrpr == h->nrpr", 1606 " && v->nrqs == h->nrqs", 1607 "#if !defined(NOCOMP) && !defined(HC)", 1608 " && (v->sv == h->sv || memcmp((char *) v->sv, (char *) h->sv, v->sz) == 0)", 1609 "#endif", 1610 "#ifdef TRIX", 1611 " )", 1612 "#else", 1613 " #if NRUNS>0", 1614 " #if VECTORSZ>32000", 1615 " && (memcmp((char *) v->po, (char *) h->po, v->nrpr * sizeof(int)) == 0)", 1616 " && (memcmp((char *) v->qo, (char *) h->qo, v->nrqs * sizeof(int)) == 0)", 1617 " #else", 1618 " && (memcmp((char *) v->po, (char *) h->po, v->nrpr * sizeof(short)) == 0)", 1619 " && (memcmp((char *) v->qo, (char *) h->qo, v->nrqs * sizeof(short)) == 0)", 1620 " #endif", 1621 " && (memcmp((char *) v->ps, (char *) h->ps, v->nrpr * sizeof(uchar)) == 0)", 1622 " && (memcmp((char *) v->qs, (char *) h->qs, v->nrqs * sizeof(uchar)) == 0))", 1623 " #else", 1624 " )", 1625 " #endif", 1626 "#endif", 1627 " { break;", 1628 " } }", 1629 "", 1630 " if (!h) /* we don't have one like it yet */", 1631 " { v->nxt = kept[v->sz]; /* keep the original owner field */", 1632 " kept[v->sz] = v;", 1633 " /* all ptrs inside are to shared memory, but nxt is local */", 1634 " }", 1635 "}", 1636 "", 1637 "EV_Hold *", 1638 "bfs_new_sv_mask(int n)", 1639 "{ EV_Hold *h;", 1640 "", 1641 " for (h = kept[n]; h; h = h->nxt)", 1642 " { if ((now._nr_pr == h->nrpr)", 1643 " && (now._nr_qs == h->nrqs)", 1644 "#if !defined(NOCOMP) && !defined(HC) && NRUNS>0", 1645 " && ((char *) Mask == h->sv || (memcmp((char *) Mask, h->sv, n) == 0))", 1646 "#endif", 1647 "#ifdef TRIX", 1648 " )", 1649 "#else", 1650 " #if NRUNS>0", 1651 " #if VECTORSZ>32000", 1652 " && (memcmp((char *) proc_offset, (char *) h->po, now._nr_pr * sizeof(int)) == 0)", 1653 " && (memcmp((char *) q_offset, (char *) h->qo, now._nr_qs * sizeof(int)) == 0)", 1654 " #else", 1655 " && (memcmp((char *) proc_offset, (char *) h->po, now._nr_pr * sizeof(short)) == 0)", 1656 " && (memcmp((char *) q_offset, (char *) h->qo, now._nr_qs * sizeof(short)) == 0)", 1657 " #endif", 1658 " && (memcmp((char *) proc_skip, (char *) h->ps, now._nr_pr * sizeof(uchar)) == 0)", 1659 " && (memcmp((char *) q_skip, (char *) h->qs, now._nr_qs * sizeof(uchar)) == 0))", 1660 " #else", 1661 " )", 1662 " #endif", 1663 "#endif", 1664 " { break;", 1665 " } }", 1666 "", 1667 " if (!h)", 1668 " { /* once created, the contents are never modified */", 1669 " h = (EV_Hold *) sh_malloc((ulong)sizeof(EV_Hold));", 1670 " h->owner = who_am_i;", 1671 " h->sz = n;", 1672 " h->nrpr = now._nr_pr;", 1673 " h->nrqs = now._nr_qs;", 1674 "#if !defined(NOCOMP) && !defined(HC) && NRUNS>0", 1675 " h->sv = (char *) Mask; /* in shared memory, and never modified */", 1676 "#endif", 1677 "#if NRUNS>0 && !defined(TRIX)", 1678 " if (now._nr_pr > 0)", 1679 " { h->ps = (char *) proc_skip;", 1680 " h->po = (char *) proc_offset;", 1681 " }", 1682 " if (now._nr_qs > 0)", 1683 " { h->qs = (char *) q_skip;", 1684 " h->qo = (char *) q_offset;", 1685 " }", 1686 "#endif", 1687 " h->nxt = kept[n];", 1688 " kept[n] = h;", 1689 " }", 1690 " return h;", 1691 "}", 1692 "#endif", /* NRUNS>0 */ 1693 "BFS_Slot *", 1694 "bfs_pack_state(Trail *f, BFS_Trail *g, int search_depth, BFS_Slot *t)", 1695 "{", 1696 "#ifdef BFS_CHECK", 1697 " assert(t->s_data != NULL);", 1698 " assert(t->s_data->t_info != NULL);", 1699 " assert(f || g);", 1700 "#endif", 1701 " if (!g)", 1702 " { t->s_data->t_info->ostate = f->ostate;", 1703 " t->s_data->t_info->st = f->st;", 1704 " t->s_data->t_info->o_tt = search_depth;", 1705 " t->s_data->t_info->pr = f->pr;", 1706 " t->s_data->t_info->tau = f->tau;", 1707 " t->s_data->t_info->o_pm = f->o_pm;", 1708 " if (f->o_t)", 1709 " { t->s_data->t_info->t_id = f->o_t->t_id;", 1710 " } else", 1711 " { t->s_data->t_info->t_id = -1;", 1712 " t->s_data->t_info->ostate = NULL;", 1713 " }", 1714 " } /* else t->s_data->t_info == g */", 1715 "#if SYNC", 1716 " t->s_data->boq = boq;", 1717 "#endif", 1718 "#ifdef VERBOSE", 1719 " { static ulong u_cnt;", 1720 " t->s_data->nr = u_cnt++;", 1721 " }", 1722 "#endif", 1723 "#ifdef TRIX", 1724 " sv_populate(); /* make sure now is up to date */", 1725 "#endif", 1726 "#ifndef BFS_DISK", 1727 " { SV_Hold *x = bfs_new_sv(vsize);", 1728 " t->s_data->osv = x->sv;", 1729 " x->sv = (State *) 0;", 1730 " x->nxt = bfs_free_hold;", 1731 " bfs_free_hold = x;", 1732 " }", 1733 "#endif", 1734 "#if NRUNS>0", 1735 " t->s_data->omask = bfs_new_sv_mask(vsize);", 1736 "#endif", 1737 "", 1738 "#if defined(Q_PROVISO) && !defined(BITSTATE) && !defined(NOREDUCE)", 1739 " t->s_data->lstate = Lstate; /* Lstate is set in o_store or h_store */", 1740 "#endif", 1741 "#ifdef BFS_FIFO", 1742 " t->type = STATE;", 1743 "#endif", 1744 " return t;", 1745 "}", 1746 "", 1747 "void", 1748 "bfs_store_state(Trail *t, short oboq)", 1749 "{", 1750 "#ifdef TRIX", 1751 " sv_populate();", 1752 "#endif", 1753 "#if defined(VERI) && defined(Q_PROVISO) && !defined(BITSTATE) && defined(FULLSTACK)", 1754 " if (!(t->tau&4)", /* prog move */ 1755 " && t->ostate)", /* not initial state */ 1756 " { t->tau |= ((BFS_Trail *) t->ostate)->tau&64;", 1757 " } /* lift 64 across claim moves */", 1758 "#endif", 1759 "", 1760 "#ifdef BFS_SEP_HASH", 1761 " #if SYNC", 1762 " if (boq == -1 && oboq != -1) /* post-rv */", 1763 " { BFS_Trail *x = (BFS_Trail *) trpt->ostate; /* pre-rv state */", 1764 " if (x)", 1765 " { x->o_pm |= 4; /* rv complete */", 1766 " } }", 1767 " #endif", 1768 " d_sfh((uchar *)&now, (int) vsize); /* sep-hash -- sets K1 -- overkill */", 1769 " bfs_keep_state = K1%%Cores + 1;", 1770 " bfs_push_state(t, NULL, trpt->o_tt+1); /* bfs_store_state - sep_hash */", 1771 " bfs_keep_state = 0;", 1772 "#else", 1773 " #ifdef VERI", 1774 #if 0 1775 in VERI mode store the state when 1776 (!t->ostate || (t->tau&4)) in initial state and after each program move 1777 1778 i.e., dont store when !(!t->ostate || (t->tau&4)) = (t->ostate && !(t->tau&4)) 1779 the *first* time that the tau flag is not set: 1780 possibly after a series of claim moves in an atomic sequence 1781 #endif 1782 " if (!(t->tau&4) && t->ostate && (((BFS_Trail *)t->ostate)->tau&4))", 1783 " { /* do not store intermediate state */", 1784 " #if defined(VERBOSE) && defined(L_BOUND)", 1785 " bfs_printf(\"Un-Stored state bnd %%d -- sds %%p\\n\",", 1786 " now._l_bnd, now._l_sds);", 1787 " #endif", 1788 " bfs_push_state(t, NULL, trpt->o_tt+1); /* claim move */", 1789 " } else", 1790 " #endif", 1791 " if (!bfs_do_store((char *)&now, vsize)) /* includes bfs_visited */", 1792 " { nstates++; /* local count */", 1793 " trpt->tau |= 64; /* bfs: succ outside stack */", 1794 " #if SYNC", 1795 " if (boq == -1 && oboq != -1) /* post-rv */", 1796 " { BFS_Trail *x = ", 1797 " (BFS_Trail *) trpt->ostate; /* pre-rv state */", 1798 " if (x)", 1799 " { x->o_pm |= 4; /* rv complete */", 1800 " } }", 1801 " #endif", 1802 " bfs_push_state(t, NULL, trpt->o_tt+1); /* successor */", 1803 " } else", 1804 " { truncs++;", 1805 " #ifdef BFS_CHECK", 1806 " bfs_printf(\"seen before\\n\");", 1807 " #endif", 1808 " #if defined(Q_PROVISO) && !defined(BITSTATE) && defined(FULLSTACK)", 1809 " #ifdef USE_TDH", 1810 " if (Lstate)", /* if BFS_INQ is set */ 1811 " { trpt->tau |= 64;", 1812 " }", 1813 " #else", 1814 " if (Lstate && Lstate->tagged) /* bfs_store_state */", 1815 " { trpt->tau |= 64;", 1816 " }", 1817 " #endif", 1818 " #endif", 1819 " }", 1820 "#endif", 1821 "}", 1822 "", 1823 "/*** support routines ***/", 1824 "", 1825 "void", 1826 "bfs_clear_locks(void)", 1827 "{ int i;", 1828 "", 1829 " /* clear any locks held by this process only */", 1830 " if (shared_memory)", 1831 " for (i = 0; i < BFS_MAXLOCKS; i++)", 1832 " { if (shared_memory->sh_owner[i] == who_am_i + 1)", 1833 " { shared_memory->sh_locks[i] = 0;", 1834 "#ifdef BFS_CHECK", 1835 " shared_memory->in_count[i] = 0;", 1836 "#endif", 1837 " shared_memory->sh_owner[i] = 0;", 1838 " } }", 1839 "}", 1840 "", 1841 "void", 1842 "e_critical(int which)", 1843 "{ int w;", 1844 "#ifdef BFS_CHECK", 1845 " assert(which >= 0 && which < BFS_MAXLOCKS);", 1846 "#endif", 1847 " if (shared_memory == NULL) return;", 1848 " while (tas(&(shared_memory->sh_locks[which])) != 0)", 1849 " { w = shared_memory->sh_owner[which]; /* sh_locks[which] could be 0 by now */", 1850 " assert(w >= 0 && w <= BFS_MAXPROCS);", 1851 " if (w > 0 && shared_memory->bfs_flag[w-1] == 2)", 1852 " { /* multiple processes can get here; only one should do this: */", 1853 " if (tas(&(shared_memory->bfs_data[w - 1].override)) == 0)", 1854 " { fprintf(stderr, \"cpu%%02d: override lock %%d - held by %%d\\n\",", 1855 " who_am_i, which, shared_memory->sh_owner[which]);", 1856 "#ifdef BFS_CHECK", 1857 " shared_memory->in_count[which] = 0;", 1858 "#endif", 1859 " shared_memory->sh_locks[which] = 0;", 1860 " shared_memory->sh_owner[which] = 0;", 1861 " } }", 1862 " shared_memory->wait_count[which]++; /* not atomic of course */", 1863 " }", 1864 "#ifdef BFS_CHECK", 1865 " if (shared_memory->in_count[which] != 0)", 1866 " { fprintf(stderr, \"cpu%%02d: cannot happen lock %%d count %%d\\n\", who_am_i,", 1867 " which, shared_memory->in_count[which]);", 1868 " }", 1869 " shared_memory->in_count[which]++;", 1870 "#endif", 1871 " shared_memory->sh_owner[which] = who_am_i+1;", 1872 "}", 1873 "", 1874 "void", 1875 "x_critical(int which)", 1876 "{", 1877 " if (shared_memory == NULL) return;", 1878 "#ifdef BFS_CHECK", 1879 " assert(shared_memory->in_count[which] == 1);", 1880 " shared_memory->in_count[which] = 0;", 1881 "#endif", 1882 " shared_memory->sh_locks[which] = 0;", 1883 " shared_memory->sh_owner[which] = 0;", 1884 "}", 1885 "", 1886 "void", 1887 "bfs_printf(const char *fmt, ...)", 1888 "{ va_list args;", 1889 "", 1890 " e_critical(BFS_PRINT);", 1891 "#ifdef BFS_CHECK", 1892 " if (1) { int i=who_am_i; while (i-- > 0) printf(\" \"); }", 1893 "#endif", 1894 " printf(\"cpu%%02d: \", who_am_i);", 1895 " va_start(args, fmt);", 1896 " vprintf(fmt, args);", 1897 " va_end(args);", 1898 " fflush(stdout);", 1899 " x_critical(BFS_PRINT);", 1900 "}", 1901 "", 1902 "int", 1903 "bfs_all_idle(void)", 1904 "{ int i;", 1905 "", 1906 " if (shared_memory)", 1907 " for (i = 0; i < Cores; i++)", 1908 " { if (shared_memory->bfs_flag[i] == 0", 1909 " && shared_memory->bfs_idle[i] == 0)", 1910 " { return 0;", 1911 " } }", 1912 " return 1;", 1913 "}", 1914 "", 1915 "#ifdef BFS_FIFO", 1916 "int", 1917 "bfs_idle_and_empty(void)", 1918 "{ int p; /* read-only */", 1919 " for (p = 0; p < Cores; p++)", 1920 " { if (shared_memory->bfs_flag[p] == 0", 1921 " && shared_memory->bfs_idle[p] == 0)", 1922 " { return 0;", 1923 " } }", 1924 " for (p = 0; p < Cores; p++)", 1925 " { if (bfs_empty(p) < Cores)", 1926 " { return 0;", 1927 " } }", 1928 " return 1;", 1929 "}", 1930 "#endif", 1931 "", 1932 "void", 1933 "bfs_set_toggle(void) /* executed by root */", 1934 "{ int i;", 1935 "", 1936 " if (shared_memory)", 1937 " for (i = 0; i < Cores; i++)", 1938 " { shared_memory->bfs_idle[i] = 0;", 1939 " }", 1940 "}", 1941 "", 1942 "int", 1943 "bfs_all_running(void) /* crash detection */", 1944 "{ int i;", 1945 " for (i = 0; i < Cores; i++)", 1946 " { if (!shared_memory || shared_memory->bfs_flag[i] > 1)", 1947 " { return 0;", 1948 " } }", 1949 " return 1;", 1950 "}", 1951 "", 1952 "void", 1953 "bfs_mark_done(int code)", 1954 "{", 1955 " if (shared_memory)", 1956 " { shared_memory->bfs_flag[who_am_i] = (int) code;", 1957 " shared_memory->quit = 1;", 1958 " }", 1959 "}", 1960 "", 1961 "static uchar *", 1962 "bfs_offset(int c)", 1963 "{ int p, N;", 1964 "#ifdef COLLAPSE", 1965 " uchar *q = (uchar *) ncomps; /* it is the first object allocated */", 1966 " q += (256+2) * sizeof(ulong); /* preserve contents of ncomps */", 1967 "#else", 1968 " uchar *q = (uchar *) &(shared_memory->allocator);", 1969 "#endif", 1970 " /* _NP_+1 proctypes, reachability info:", 1971 " * reached[x : 0 .. _NP_+1][ 0 .. NrStates[x] ]", 1972 " */", 1973 " for (p = N = 0; p <= _NP_; p++)", 1974 " { N += NrStates[p]; /* sum for all proctypes */", 1975 " }", 1976 "", 1977 " /* space needed per proctype: N bytes */", 1978 " /* rounded up to a multiple of the word size */", 1979 " if ((N%%sizeof(void *)) != 0) /* aligned */", 1980 " { N += sizeof(void *) - (N%%sizeof(void *));", 1981 " }", 1982 "", 1983 " q += ((c - 1) * (_NP_ + 1) * N);", 1984 " return q;", 1985 "}", 1986 "", 1987 "static void", 1988 "bfs_putreached(void)", 1989 "{ uchar *q;", 1990 " int p;", 1991 "", 1992 " assert(who_am_i > 0);", 1993 "", 1994 " q = bfs_offset(who_am_i);", 1995 " for (p = 0; p <= _NP_; p++)", 1996 " { memcpy((void *) q, (const void *) reached[p], (size_t) NrStates[p]);", 1997 " q += NrStates[p];", 1998 " }", 1999 "}", 2000 "", 2001 "static void", 2002 "bfs_getreached(int c)", 2003 "{ uchar *q;", 2004 " int p, i;", 2005 "", 2006 " assert(who_am_i == 0 && c >= 1 && c < Cores);", 2007 "", 2008 " q = (uchar *) bfs_offset(c);", 2009 " for (p = 0; p <= _NP_; p++)", 2010 " for (i = 0; i < NrStates[p]; i++)", 2011 " { reached[p][i] += *q++; /* update local copy */", 2012 " }", 2013 "}", 2014 "", 2015 "void", 2016 "bfs_update(void)", 2017 "{ int i;", 2018 " volatile BFS_data *s;", 2019 "", 2020 " if (!shared_memory) return;", 2021 "", 2022 " s = &shared_memory->bfs_data[who_am_i];", 2023 " if (who_am_i == 0)", 2024 " { shared_memory->bfs_flag[who_am_i] = 3; /* or else others don't stop */", 2025 " bfs_gcount = 0;", 2026 " for (i = 1; i < Cores; i++) /* start at 1 not 0 */", 2027 " { while (shared_memory->bfs_flag[i] == 0)", 2028 " { sleep(1);", 2029 " if (bfs_gcount++ > WAIT_MAX) /* excessively long wait */", 2030 " { printf(\"cpu00: give up waiting for cpu%%2d (%%d cores)\\n\", i, Cores);", 2031 " bfs_gcount = 0;", 2032 " break;", 2033 " } }", 2034 " s = &shared_memory->bfs_data[i];", 2035 " mreached = Max(mreached, s->mreached);", 2036 " hmax = vsize = Max(vsize, s->vsize);", 2037 " errors += s->errors;", 2038 " memcnt += s->memcnt;", 2039 " nstates += s->nstates;", 2040 " nlinks += s->nlinks;", 2041 " truncs += s->truncs;", 2042 " bfs_left += s->memory_left;", 2043 " bfs_punt += s->punted;", 2044 " bfs_getreached(i);", 2045 " }", 2046 " } else", 2047 " { s->mreached = (ulong) mreached;", 2048 " s->vsize = (ulong) vsize;", 2049 " s->errors = (int) errors;", 2050 " s->memcnt = (double) memcnt;", 2051 " s->nstates = (double) nstates;", 2052 " s->nlinks = (double) nlinks;", 2053 " s->truncs = (double) truncs;", 2054 " s->memory_left = (ulong) bfs_left;", 2055 " s->punted = (ulong) bfs_punt;", 2056 " bfs_putreached();", 2057 " }", 2058 "}", 2059 "", 2060 "volatile uchar *", 2061 "sh_pre_malloc(ulong n) /* used before the local heaps are populated */", 2062 "{ volatile uchar *ptr = NULL;", 2063 "", 2064 " assert(!bfs_runs);", 2065 " if ((n%%sizeof(void *)) != 0)", 2066 " { n += sizeof(void *) - (n%%sizeof(void *));", 2067 " assert((n%%sizeof(void *)) == 0);", 2068 " }", 2069 "", 2070 " e_critical(BFS_MEM); /* needed? */", 2071 " if (shared_memory->mem_left < n + 7)", /* 7 for possible alignment */ 2072 " { x_critical(BFS_MEM);", 2073 " bfs_printf(\"want %%lu, have %%lu\\n\",", 2074 " n, shared_memory->mem_left);", 2075 " bfs_shutdown(\"out of shared memory\");", 2076 " assert(0); /* should be unreachable */", 2077 " }", 2078 " ptr = shared_memory->allocator;", 2079 "#if WS>4", /* align to 8 byte boundary */ 2080 " { int b = (int) ((uint64_t) ptr)&7;", 2081 " if (b != 0)", 2082 " { ptr += (8-b);", 2083 " shared_memory->allocator = ptr;", 2084 " } }", 2085 "#endif", 2086 " shared_memory->allocator += n;", 2087 " shared_memory->mem_left -= n;", 2088 " x_critical(BFS_MEM);", 2089 "", 2090 " bfs_pre_allocated += n;", 2091 "", 2092 " return ptr;", 2093 "}", 2094 "", 2095 "volatile uchar *", 2096 "sh_malloc(ulong n)", 2097 "{ volatile uchar *ptr = NULL;", 2098 "#ifdef BFS_CHECK", 2099 " assert(bfs_runs);", 2100 "#endif", 2101 " if ((n%%sizeof(void *)) != 0)", 2102 " { n += sizeof(void *) - (n%%sizeof(void *));", 2103 "#ifdef BFS_CHECK", 2104 " assert((n%%sizeof(void *)) == 0);", 2105 "#endif", 2106 " }", 2107 "", 2108 " /* local heap -- no locks needed */", 2109 " if (bfs_left < n)", 2110 " { e_critical(BFS_MEM);", 2111 " if (shared_memory->mem_left >= n)", 2112 " { ptr = (uchar *) shared_memory->allocator;", 2113 " shared_memory->allocator += n;", 2114 " shared_memory->mem_left -= n;", 2115 " x_critical(BFS_MEM);", 2116 " return ptr;", 2117 " }", 2118 " x_critical(BFS_MEM);", 2119 "#ifdef BFS_LOGMEM", 2120 " int i;", 2121 " e_critical(BFS_MEM);", 2122 " for (i = 0; i < 1024; i++)", 2123 " { if (shared_memory->logmem[i] > 0)", 2124 " { bfs_printf(\"\tlog[%%d]\t%%d\\n\", i, shared_memory->logmem[i]);", 2125 " } }", 2126 " x_critical(BFS_MEM);", 2127 "#endif", 2128 " bfs_shutdown(\"out of shared memory\"); /* no return */", 2129 " }", 2130 "#ifdef BFS_LOGMEM", 2131 " e_critical(BFS_MEM);", 2132 " if (n < 1023)", 2133 " { shared_memory->logmem[n]++;", 2134 " } else", 2135 " { shared_memory->logmem[1023]++;", 2136 " }", 2137 " x_critical(BFS_MEM);", 2138 "#endif", 2139 " ptr = (uchar *) bfs_heap;", 2140 " bfs_heap += n;", 2141 " bfs_left -= n;", 2142 "", 2143 " if (0) printf(\"sh_malloc %%ld\\n\", n);", 2144 " return ptr;", 2145 "}", 2146 "", 2147 "volatile uchar *", 2148 "bfs_get_shared_mem(key_t key, size_t n)", 2149 "{ char *rval;", 2150 "", 2151 " assert(who_am_i == 0);", 2152 "", 2153 " shared_mem_id = shmget(key, n, 0600 | IPC_CREAT | IPC_EXCL); /* create */", 2154 " if (shared_mem_id == -1)", 2155 " { fprintf(stderr, \"cpu%%02d: tried to get %%d MB of shared memory\\n\",", 2156 " who_am_i, (int) n/(1024*1024));", 2157 " perror(\"shmget\");", 2158 " exit(1);", 2159 " }", 2160 " if ((rval = (char *) shmat(shared_mem_id, (void *) 0, 0)) == (char *) -1) /* attach */", 2161 " { perror(\"shmat\");", 2162 " exit(1);", 2163 " }", 2164 " return (uchar *) rval;", 2165 "}", 2166 "", 2167 "void", 2168 "bfs_drop_shared_memory(void)", 2169 "{", 2170 " if (who_am_i == 0)", 2171 " { printf(\"pan: releasing shared memory...\");", 2172 " fflush(stdout);", 2173 " }", 2174 " if (shared_memory)", 2175 " { shmdt(shared_memory); /* detach */", 2176 " if (who_am_i == 0)", 2177 " { shmctl(shared_mem_id, IPC_RMID, (void *) 0); /* remove */", 2178 " } }", 2179 " if (who_am_i == 0)", 2180 " { printf(\"done\\n\");", 2181 " fflush(stdout);", 2182 " }", 2183 "}", 2184 "", 2185 "size_t", 2186 "bfs_find_largest(key_t key)", 2187 "{ size_t n;", 2188 " const size_t delta = 32*1024*1024;", 2189 " int temp_id = -1;", 2190 " int atleastonce = 0;", 2191 "", 2192 " for (n = delta; ; n += delta)", 2193 " { if (WS <= 4 && n >= 1024*1024*1024)", /* was n >= INT_MAX */ 2194 " { n = 1024*1024*1024;", 2195 " break;", 2196 " }", 2197 "#ifdef MEMLIM", 2198 " if ((double) n > memlim)", 2199 " { n = (size_t) memlim;", 2200 " break;", 2201 " }", 2202 "#endif", 2203 " temp_id = shmget(key, n, 0600); /* check for stale copy */", 2204 " if (temp_id != -1)", 2205 " { if (shmctl(temp_id, IPC_RMID, ((void *) 0)) < 0) /* remove */", 2206 " { perror(\"remove_segment_fails 2\");", 2207 " exit(1);", 2208 " } }", 2209 "", 2210 " temp_id = shmget(key, n, 0600 | IPC_CREAT | IPC_EXCL); /* create new */", 2211 " if (temp_id == -1)", 2212 " { n -= delta;", 2213 " break;", 2214 " } else", 2215 " { atleastonce++;", 2216 " if (shmctl(temp_id, IPC_RMID, ((void *) 0)) < 0)", 2217 " { perror(\"remove_segment_fails 0\");", 2218 " exit(1);", 2219 " } } }", 2220 "", 2221 " if (!atleastonce)", 2222 " { printf(\"cpu%%02d: no shared memory n=%%d\\n\", who_am_i, (int) n);", 2223 " exit(1);", 2224 " }", 2225 "", 2226 " printf(\"cpu%%02d: largest shared memory segment: %%lu MB\\n\",", 2227 " who_am_i, (ulong) n/(1024*1024));", 2228 "#if 0", 2229 " #ifdef BFS_SEP_HASH", 2230 " n /= 2; /* not n /= Cores because the queues take most memory */", 2231 " printf(\"cpu%%02d: using %%lu MB\\n\", who_am_i, (ulong) n/(1024*1024));", 2232 " #endif", 2233 "#endif", 2234 " fflush(stdout);", 2235 "", 2236 " if ((n/(1024*1024)) == 32)", 2237 " { if (sizeof(void *) == 4) /* a 32 bit machine */", 2238 " { fprintf(stderr, \"\\t32MB is the default; increase it to 1 GB with:\\n\");", 2239 " fprintf(stderr, \"\\tsudo /sbin/sysctl kernel.shmmax=%%d\\n\", (1<<30));", 2240 " fprintf(stderr, \"\\tsudo /sbin/sysctl kernel.shmall=%%d\\n\", (1<<30)/8192);", 2241 " } else if (sizeof(void *) == 8) /* a 64 bit machine */", 2242 " { fprintf(stderr, \"\\t32MB is the default; increase it to 30 GB with:\\n\");", 2243 " fprintf(stderr, \"\\tsudo /sbin/sysctl kernel.shmmax=32212254720\\n\");", 2244 " fprintf(stderr, \"\\tsudo /sbin/sysctl kernel.shmall=7864320\\n\");", 2245 " fprintf(stderr, \"\\tor for 60 GB:\\n\");", 2246 " fprintf(stderr, \"\\tsudo /sbin/sysctl kernel.shmmax=60000000000\\n\");", 2247 " fprintf(stderr, \"\\tsudo /sbin/sysctl kernel.shmall=30000000\\n\");", 2248 " } else", 2249 " { fprintf(stderr, \"\\tweird wordsize %%d\\n\", (int) sizeof(void *));", 2250 " } }", 2251 "", 2252 " return n;", 2253 "}", 2254 "#ifdef BFS_DISK", 2255 "void", 2256 "bfs_disk_start(void)", /* setup .spin*/ 2257 "{ int unused = system(\"rm -fr .spin\");", 2258 " if (mkdir(\".spin\", 0777) != 0)", 2259 " { perror(\"mkdir\");", 2260 " Uerror(\"aborting\");", 2261 " }", 2262 "}", 2263 "void", 2264 "bfs_disk_stop(void)", /* remove .spin */ 2265 "{", 2266 " if (system(\"rm -fr .spin\") < 0)", 2267 " { perror(\"rm -fr .spin/\");", 2268 " }", 2269 "}", 2270 "void", 2271 "bfs_disk_inp(void)", /* this core only */ 2272 "{ int i; char fnm[16];", 2273 "#ifdef VERBOSE", 2274 " bfs_printf(\"inp %%d %%d 0..%%d\\n\", bfs_toggle, who_am_i, Cores);", 2275 "#endif", 2276 " for (i = 0; i < Cores; i++)", 2277 " { sprintf(fnm, \".spin/q%%d_%%d_%%d\", bfs_toggle, who_am_i, i);", 2278 " if ((bfs_inp_fd[i] = open(fnm, 0444)) < 0)", 2279 " { perror(\"open\");", 2280 " Uerror(fnm);", 2281 " } }", 2282 "}", 2283 "void", 2284 "bfs_disk_out(void)", /* this core only */ 2285 "{ int i; char fnm[16];", 2286 "#ifdef VERBOSE", 2287 " bfs_printf(\"out %%d 0..%%d %%d\\n\", 1-bfs_toggle, Cores, who_am_i);", 2288 "#endif", 2289 " shared_memory->bfs_out_cnt[who_am_i] = 0;", 2290 " for (i = 0; i < Cores; i++)", 2291 " { sprintf(fnm, \".spin/q%%d_%%d_%%d\", 1-bfs_toggle, i, who_am_i);", 2292 " if ((bfs_out_fd[i] = creat(fnm, 0666)) < 0)", 2293 " { perror(\"creat\");", 2294 " Uerror(fnm);", 2295 " } }", 2296 "}", 2297 "void", 2298 "bfs_disk_iclose(void)", 2299 "{ int i;", 2300 "#ifdef VERBOSE", 2301 " bfs_printf(\"close_inp\\n\");", 2302 "#endif", 2303 " for (i = 0; i < Cores; i++)", 2304 " { if (close(bfs_inp_fd[i]) < 0)", 2305 " { perror(\"iclose\");", 2306 " } }", 2307 "}", 2308 "void", 2309 "bfs_disk_oclose(void)", 2310 "{ int i;", 2311 "#ifdef VERBOSE", 2312 " bfs_printf(\"close_out\\n\");", 2313 "#endif", 2314 " for (i = 0; i < Cores; i++)", 2315 " { if (fsync(bfs_out_fd[i]) < 0)", 2316 " { perror(\"fsync\");", 2317 " }", 2318 " if (close(bfs_out_fd[i]) < 0)", 2319 " { perror(\"oclose\");", 2320 " } }", 2321 "}", 2322 "#endif", 2323 "void", 2324 "bfs_write_snap(int fd)", 2325 "{ if (write(fd, snap, strlen(snap)) != strlen(snap))", 2326 " { printf(\"pan: error writing %%s\\n\", fnm);", 2327 " bfs_shutdown(\"file system error\");", 2328 " }", 2329 "}", 2330 "", 2331 "void", 2332 "bfs_one_step(BFS_Trail *t, int fd)", 2333 "{ if (t && t->t_id != (T_ID) -1)", 2334 " { sprintf(snap, \"%%d:%%d:%%d\\n\",", 2335 " trcnt++, t->pr, t->t_id);", 2336 " bfs_write_snap(fd);", 2337 " }", 2338 "}", 2339 "", 2340 "void", 2341 "bfs_putter(BFS_Trail *t, int fd)", 2342 "{ if (t && t != (BFS_Trail *) t->ostate)", 2343 " bfs_putter((BFS_Trail *) t->ostate, fd);", 2344 "#ifdef L_BOUND", 2345 " if (depthfound == trcnt)", 2346 " { strcpy(snap, \"-1:-1:-1\\n\");", 2347 " bfs_write_snap(fd);", 2348 " depthfound = -1;", 2349 " }", 2350 "#endif", 2351 " bfs_one_step(t, fd);", 2352 "}", 2353 "", 2354 "void", 2355 "bfs_nuerror(char *str)", 2356 "{ int fd = make_trail();", 2357 "", 2358 " if (fd < 0) return;", 2359 "#ifdef VERI", 2360 " sprintf(snap, \"-2:%%d:-2\\n\", (uchar) ((P0 *)pptr(0))->_t);", 2361 " bfs_write_snap(fd);", 2362 "#endif", 2363 "#ifdef MERGED", 2364 " sprintf(snap, \"-4:-4:-4\\n\");", 2365 " bfs_write_snap(fd);", 2366 "#endif", 2367 " trcnt = 1;", 2368 " if (strstr(str, \"invalid\"))", 2369 " { bfs_putter((BFS_Trail *) trpt->ostate, fd);", 2370 " } else", 2371 " { BFS_Trail x;", 2372 " memset((char *) &x, 0, sizeof(BFS_Trail));", 2373 " x.pr = trpt->pr;", 2374 " x.t_id = (trpt->o_t)?trpt->o_t->t_id:0;", 2375 " x.ostate = trpt->ostate;", 2376 " bfs_putter(&x, fd);", 2377 " }", 2378 " close(fd);", 2379 " if (errors >= upto && upto != 0)", 2380 " { bfs_shutdown(str);", 2381 " }", 2382 "}", 2383 "", 2384 "void", 2385 "bfs_uerror(char *str)", 2386 "{ static char laststr[256];", 2387 "", 2388 " errors++;", 2389 " if (strncmp(str, laststr, 254) != 0)", 2390 " { bfs_printf(\"pan:%%lu: %%s (at depth %%ld)\\n\",", 2391 " errors, str, ((depthfound == -1)?depth:depthfound));", 2392 " strncpy(laststr, str, 254);", 2393 " }", 2394 "#ifdef HAS_CODE", 2395 " if (readtrail) { wrap_trail(); return; }", 2396 "#endif", 2397 " if (every_error != 0 || errors == upto)", 2398 " { bfs_nuerror(str);", 2399 " }", 2400 " if (errors >= upto && upto != 0)", 2401 " { bfs_shutdown(\"bfs_uerror\");", 2402 " }", 2403 " depthfound = -1;", 2404 "}\n", 2405 "void", 2406 "bfs_Uerror(char *str)", 2407 "{ /* bfs_uerror(str); */", 2408 " bfs_printf(\"pan:%%lu: %%s (at depth %%ld)\\n\", ++errors, str,", 2409 " ((depthfound == -1)?depth:depthfound));", 2410 " bfs_shutdown(\"bfs_Uerror\");", 2411 "}", 2412 0, 2413 }; 2414