/***** spin: pangen1.h *****/ /* Copyright (c) 2011-2012 */ /* All Rights Reserved. This software is for educational purposes only. */ /* No guarantee whatsoever is expressed or implied by the distribution of */ /* this code. Permission is given to distribute this code provided that */ /* this introductory message is not removed and no monies are exchanged. */ /* Software written by Gerard J. Holzmann. For tool documentation see: */ /* http://spinroot.com/ */ /* Send all bug-reports and/or questions to: bugs@spinroot.com */ static const char *pan_par[] = { /* generates pan.p */ "#include ", "#include ", "#include ", /* for nanosleep */ "#include ", "#include ", "#ifdef BFS_DISK", "#include ", /* for rmdir */ "#include ", /* for mkdir */ "#include ", "#include ", /* for open */ "#endif", "", "#define Max(a,b) (((a)>(b))?(a):(b))", "#ifndef WAIT_MAX", " #define WAIT_MAX 2 /* seconds */", "#endif", "#define BFS_GEN 2 /* current and next generation */", "", "typedef struct BFS_Slot BFS_Slot;", "typedef struct BFS_shared BFS_shared;", "typedef struct BFS_data BFS_data;", "", "struct BFS_data {", " double memcnt;", " double nstates;", " double nlinks;", " double truncs;", " ulong mreached;", " ulong vsize;", " ulong memory_left;", " ulong punted;", " ulong errors;", " int override; /* after crash, if another proc clears locks */", "};", "", "struct BFS_shared { /* about 13K for BFS_MAXPROCS=16 and BFS_MAXLOCKS=1028 */", " volatile ulong quit; /* set to signal termination -- one word */", " volatile ulong started;", "", " volatile uchar sh_owner[BFS_MAXLOCKS]; /* optional */", "#ifdef BFS_CHECK", " volatile uchar in_count[BFS_MAXLOCKS]; /* optional */", "#endif", " volatile int sh_locks[BFS_MAXLOCKS];", " volatile ulong wait_count[BFS_MAXLOCKS]; /* optional */", "", " volatile BFS_data bfs_data[BFS_MAXPROCS];", " volatile uchar bfs_flag[BFS_MAXPROCS]; /* running 0, normal exit 1, abnormal 2 */", " volatile uchar bfs_idle[BFS_MAXPROCS]; /* set when all input queues are empty */", "#ifdef BFS_DISK", " volatile uchar bfs_out_cnt[BFS_MAXPROCS]; /* set when core writes a state */", "#endif", "", " volatile BFS_Slot *head[BFS_GEN][BFS_MAXPROCS][BFS_MAXPROCS];", "#ifdef BFS_FIFO", " volatile BFS_Slot *tail[BFS_GEN][BFS_MAXPROCS][BFS_MAXPROCS];", " volatile BFS_Slot *dels[BFS_GEN][BFS_MAXPROCS][BFS_MAXPROCS];", "#endif", "#ifdef BFS_LOGMEM", " volatile ulong logmem[1024];", "#endif", " volatile ulong mem_left;", " volatile uchar *allocator; /* start of shared heap, must be last */", "};", "", "enum bfs_types { EMPTY = 0, STATE, DELETED };", "", "struct BFS_Slot {", " #ifdef BFS_FIFO", " enum bfs_types type; /* message type */", " #endif", " BFS_State *s_data; /* state data */", " BFS_Slot *nxt; /* linked list */", "};", "", "extern volatile uchar *bfs_get_shared_mem(key_t, size_t);", "extern BFS_Slot * bfs_new_slot(BFS_Trail *);", "extern BFS_Slot * bfs_next(void);", "extern BFS_Slot * bfs_pack_state(Trail *, BFS_Trail *, int);", "extern SV_Hold * bfs_new_sv(int);", "#if NRUNS>0", "extern EV_Hold * bfs_new_sv_mask(int);", "#endif", "extern BFS_Trail * bfs_grab_trail(void);", "extern BFS_Trail * bfs_unpack_state(BFS_Slot *);", "extern int bfs_all_empty(void);", "extern int bfs_all_idle(void);", "extern int bfs_all_running(void);", "extern int bfs_idle_and_empty(void);", "extern size_t bfs_find_largest(key_t);", "", "extern void bfs_clear_locks(void);", "extern void bfs_drop_shared_memory(void);", "extern void bfs_explore_state(BFS_Slot *);", "extern void bfs_initial_state(void);", "extern void bfs_mark_done(int);", "extern void bfs_printf(const char *fmt, ...);", "extern void bfs_push_state(Trail *, BFS_Trail *, int);", "extern void bfs_recycle(BFS_Slot *);", "extern void bfs_release_trail(BFS_Trail *);", "extern void bfs_run(void);", "extern void bfs_setup_mem(void);", "extern void bfs_setup(void);", "extern void bfs_shutdown(const char *);", "extern void bfs_statistics(void);", "extern void bfs_store_state(Trail *, short);", "extern void bfs_set_toggle(void);", "extern void bfs_update(void);", "", "#ifdef MA", " #error cannot combine -DMA with -DBFS_PAR", " /* would require us to parallize g_store */", "#endif", "#ifdef BCS", " #error cannot combine -DBCS with -DBFS_PAR", "#endif", "#ifdef BFS_DISK", " #ifdef BFS_FIFO", " #error cannot combine BFS_DISK and BFS_FIFO", " #endif", " extern void bfs_disk_start(void);", " extern void bfs_disk_stop(void);", " extern void bfs_disk_out(void);", " extern void bfs_disk_inp(void);", " extern void bfs_disk_iclose(void);", " extern void bfs_disk_oclose(void);", " int bfs_out_fd[BFS_MAXPROCS];", " int bfs_inp_fd[BFS_MAXPROCS];", "#endif", "", "static BFS_shared *shared_memory;", "static BFS_Slot *bfs_free_slot; /* local free list */", "static BFS_Slot bfs_null;", "static SV_Hold *bfs_svfree[VECTORSZ];", "static uchar *bfs_heap; /* local pointer into heap */", "static ulong bfs_left; /* local part of shared heap */", "#if NRUNS>0", "static void bfs_keep(EV_Hold *);", "#endif", "static long bfs_sent; /* nr msgs sent -- local to each process */", "static long bfs_rcvd; /* nr msgs rcvd */", "static long bfs_sleep_cnt; /* stats */", "static long bfs_wcount;", "static long bfs_gcount;", "static ulong bfs_total_shared;", "#ifdef BFS_STAGGER", " static int bfs_stage_cnt = 0;", " static void bfs_stagger_flush(void);", "#endif", "static int bfs_toggle; /* local variable, 0 or 1 */", "static int bfs_qscan; /* scan input queues in order */", "static ulong bfs_snapped;", "static int shared_mem_id;", "#ifndef NOREDUCE", "static int bfs_nps; /* no preselection */", "#endif", "ulong bfs_punt; /* states dropped for lack of memory */", "#if defined(VERBOSE) || defined(BFS_CHECK)", "static const char *bfs_sname[] = {", " \"EMPTY\", /* 0 */", " \"STATE\", /* 1 */", " \"STATE\", /* 2 = DELETED */", " 0", "};", "#endif", "static const char *bfs_lname[] = { /* match values defined in pangen2.c */", " \"global lock\", /* BFS_GLOB */", " \"ordinal\", /* BFS_ORD */", " \"shared memory\", /* BFS_MEM */", " \"print to stdout\", /* BFS_PRINT */", " \"hashtable\", /* BFS_STATE */", " 0", "};", "", "static ulong bfs_count[DELETED+1]; /* indexed with bfs_types: EMPTY=0, STATE=1, DELETED=2 */", "", "static int bfs_keep_state;", "", "int Cores = 1;", "int who_am_i = 0; /* root */", "", "#ifdef L_BOUND", " int L_bound = L_BOUND;", "#endif", "", "#ifdef BFS_CHECK", "void", "bfs_dump_now(char *s)", "{ int i; char *p = (char *) &now;", "", " e_critical(BFS_PRINT);", " printf(\"%%s\\t\", s);", " printf(\"%%3lu: \", vsize);", " for (i = 0; i < vsize; i++)", " { printf(\"%%3d \", *p++);", " }", " printf(\" %%s\\noffsets:\\t\", s);", " for (i = 0; i < now._nr_pr; i++)", " { printf(\"%%3d \", proc_offset[i]);", " }", " printf(\"\\n\");", " x_critical(BFS_PRINT);", "}", "", "void", "view_state(char *s) /* debugging */", "{ int i;", " char *p;", " e_critical(BFS_PRINT);", " printf(\"cpu%%02d %%s: \", who_am_i, s);", " p = (char *)&now;", " for (i = 0; i < vsize; i++)", " printf(\"%%3d, \", *p++);", " printf(\"\\n\"); fflush(stdout);", " x_critical(BFS_PRINT);", "}", "#endif", "", "void", "bfs_main(int ncores, int cycles)", "{", " if (cycles)", " { fprintf(stderr, \"pan: cycle detection is not supported in this mode\\n\");", " exit(1);", " }", "", " if (ncores == 0) /* i.e., find out */", " { FILE *fd;", " char buf[512];", " if ((fd = fopen(\"/proc/cpuinfo\", \"r\")) == NULL)", " { /* cannot tell */", " ncores = Cores; /* use the default */", " } else", " { while (fgets(buf, sizeof(buf), fd))", " { if (strncmp(buf, \"processor\", strlen(\"processor\")) == 0)", " { ncores++;", " } }", " fclose(fd);", " ncores--;", " if (verbose)", " { printf(\"pan: %%d available cores\\n\", ncores+1);", " } } }", " if (ncores >= BFS_MAXPROCS)", " { Cores = BFS_MAXPROCS-1; /* why -1? */", " } else if (ncores < 1)", " { Cores = 1;", " } else", " { Cores = ncores;", " }", " printf(\"pan: using %%d core%%s\\n\", Cores, (Cores>1)?\"s\":\"\");", " fflush(stdout);", "#ifdef BFS_DISK", " bfs_disk_start();", /* create .spin */ "#endif", " bfs_setup(); /* shared memory segments and fork */", " bfs_run();", " if (who_am_i == 0)", " { stop_timer(0);", " }", " bfs_statistics();", " bfs_mark_done(1);", " if (who_am_i == 0)", " { report_time();", "#ifdef BFS_DISK", " bfs_disk_stop();", "#endif", " }", "#ifdef C_EXIT", " C_EXIT; /* trust that it defines a fct */", "#endif", " bfs_drop_shared_memory();", " exit(0);", "}", "", "void", "bfs_setup_mem(void)", "{ size_t n;", " key_t key;", "#ifdef BFS_FIFO", " bfs_null.type = EMPTY;", "#endif", " ntrpt = (Trail *) emalloc(sizeof(Trail));", /* just once */ "", " if ((key = ftok(\".\", (int) 'L')) == -1)", " { perror(\"ftok shared memory\");", " exit(1);", " }", " n = bfs_find_largest(key);", " bfs_total_shared = (ulong) n;", "", " shared_memory = (BFS_shared *) bfs_get_shared_mem(key, n); /* root */", " shared_memory->allocator = (uchar *) shared_memory + sizeof(BFS_shared);", " shared_memory->mem_left = (ulong) (n - sizeof(BFS_shared));", "}", "", "ulong bfs_LowLim;", "#ifndef BFS_RESERVE", " #define BFS_RESERVE 5", /* keep memory on global heap in reserve for first few cores */ /* that run out of their local allocation of shared mem */ /* 1~50 percent, 2~30 percent, 5~20 percent, >Cores=none */ "#else", " #if BFS_RESERVE<1", " #error BFS_RESERVE must be at least 1", " #endif", "#endif", "", "void", "bfs_setup(void) /* executed by root */", "{ int i, j;", " ulong n; /* share of shared memory allocated to each core */", "", " n = shared_memory->mem_left / (Cores + Cores/(BFS_RESERVE)); /* keep some reserve */", "", " if ((n%%sizeof(void *)) != 0)", " { n -= (n%%sizeof(void *)); /* align, without exceeding total */", " }", " for (i = 0; i < Cores-1; i++)", " { j = fork();", " if (j == -1)", " { bfs_printf(\"fork failed\\n\");", " exit(1);", " }", " if (j == 0)", " { who_am_i = i+1; /* 1..Cores-1 */", " break;", " } }", "", " e_critical(BFS_MEM);", " bfs_heap = (uchar *) shared_memory->allocator;", " shared_memory->allocator += n;", " shared_memory->mem_left -= n;", " x_critical(BFS_MEM);", "", " bfs_left = n;", " bfs_runs = 1;", " bfs_LowLim = n / (2 * (ulong) Cores);", /* 50% */ "}", "", "void", "bfs_run(void)", "{ BFS_Slot *v;", "", "#ifdef BFS_DISK", " bfs_disk_out();", /* create outqs */ "#endif", " if (who_am_i == 0)", " { bfs_initial_state();", " }", "#ifdef BFS_DISK", " #ifdef BFS_STAGGER", " bfs_stagger_flush();", " #endif", " bfs_disk_oclose();", /* sync and close outqs */ "#endif", "#ifdef BFS_FIFO", " static int i_count;", "#endif", "", " srand(321);", " bfs_qscan = 0;", " bfs_toggle = 1 - bfs_toggle; /* after initial state */", " e_critical(BFS_GLOB);", " shared_memory->started++;", " x_critical(BFS_GLOB);", "", " while (shared_memory->started != Cores) /* wait for all cores to connect */", " { usleep(1);", " }", "", "#ifdef BFS_DISK", " bfs_disk_out();", " bfs_disk_inp();", "#endif", "", " start_timer();", " while (shared_memory->quit == 0)", " { v = bfs_next(); /* get next message from current generation */", " if (v->s_data) /* v->type == STATE || v->type == DELETED */", " { bfs_count[STATE]++;", "#ifdef VERBOSE", " bfs_printf(\"GOT STATE (depth %%d, nr %%u)\\n\",", " v->s_data->t_info->o_tt, v->s_data->nr);", "#endif", " /* last resort: start dropping states when out of memory */", " if (bfs_left > 1024 || shared_memory->mem_left > 1024)", " { bfs_explore_state(v);", " } else", " { static int warned_loss = 0;", " if (warned_loss == 0 && who_am_i == 0)", " { warned_loss++;", " bfs_printf(\"out of shared memory - losing states\\n\");", " }", " bfs_punt++;", " }", "#if !defined(BFS_FIFO) && !defined(BFS_NORECYCLE)", " bfs_recycle(v);", "#endif", "#ifdef BFS_FIFO", " i_count = 0;", "#endif", " } else", " { bfs_count[EMPTY]++;", "#if defined(BFS_FIFO) && defined(BFS_CHECK)", " assert(v->type == EMPTY);", "#endif", "#ifdef BFS_FIFO", " if (who_am_i == 0)", " { if (bfs_idle_and_empty())", " { if (i_count++ > 10)", " { shared_memory->quit = 1;", " }", " else usleep(1);", " }", " } else if (!bfs_all_running())", " { bfs_shutdown(\"early termination\");", " }", "#else", " if (who_am_i == 0)", " { if (bfs_all_idle()) /* wait for it */", " { if (!bfs_all_empty()) /* more states to process */", " { bfs_set_toggle();", " goto do_toggle;", " } else /* done */", " { shared_memory->quit = 1; /* step 4 */", " }", " } else", " { bfs_sleep_cnt++;", " }", " } else", " { /* wait for quit or idle bit to be reset by root */", " while (shared_memory->bfs_idle[who_am_i] == 1", " && shared_memory->quit == 0)", " { if (bfs_all_running())", " { bfs_sleep_cnt++;", " usleep(10); /* new 6.2.3 */", " } else", " { bfs_shutdown(\"early termination\");", " /* no return */", " } }", "do_toggle: bfs_qscan = 0;", "#ifdef BFS_DISK", " bfs_disk_iclose();", " bfs_disk_oclose();", "#endif", " bfs_toggle = 1 - bfs_toggle;", "#ifdef BFS_DISK", " bfs_disk_out();", " bfs_disk_inp();", "#endif", " #ifdef BFS_CHECK", " bfs_printf(\"toggle: recv from %%d, send to %%d\\n\",", " bfs_toggle, 1 - bfs_toggle);", " #endif", " }", "#endif", " } }", "#ifdef BFS_CHECK", " bfs_printf(\"done, sent %%5ld recvd %%5ld punt %%5lu sleep: %%ld\\n\",", " bfs_sent, bfs_rcvd, bfs_punt, bfs_sleep_cnt);", "#endif", "}", "", "void", "bfs_report_mem(void) /* called from within wrapup() */", "{", " printf(\"%%9.3f total shared memory usage\\n\\n\",", " ((double) bfs_total_shared - (double) bfs_left)/(1024.*1024.));", "}", "", "void", "bfs_statistics(void)", "{", " #ifdef VERBOSE", " enum bfs_types i;", " #endif", " if (verbose)", " bfs_printf(\"states sent %%7ld recvd %%7ld stored %%8g sleeps: %%4ld, %%4ld, %%ld\\n\",", " bfs_sent, bfs_rcvd, nstates, bfs_wcount, bfs_gcount, bfs_sleep_cnt);", " if (0) bfs_printf(\"states punted %%7lu\\n\", bfs_punt);", " #ifdef VERBOSE", " for (i = EMPTY; i <= DELETED; i++)", " { if (bfs_count[i] > 0)", " { bfs_printf(\"%%6s %%8lu\\n\",", " bfs_sname[i], bfs_count[i]);", " } }", " #endif", " bfs_update();", "", " if (who_am_i == 0 && shared_memory)", " { int i; ulong count = 0L;", " done = 1;", "", " e_critical(BFS_PRINT);", " wrapup();", " if (verbose)", " { printf(\"\\nlock-wait counts:\\n\");", " for (i = 0; i < BFS_STATE; i++)", " printf(\"%%16s %%9lu\\n\",", " bfs_lname[i], shared_memory->wait_count[i]);", "#ifndef BITSTATE", " for (i = BFS_STATE; i < BFS_MAXLOCKS; i++)", " { if (0)", " printf(\" [%%6d] %%9lu\\n\",", " i, shared_memory->wait_count[i]);", " count += shared_memory->wait_count[i];", " }", " printf(\"%%16s %%9lu (avg per region)\\n\",", " bfs_lname[BFS_STATE], count/(BFS_MAXLOCKS - BFS_STATE));", "#endif", " }", " fflush(stdout);", " x_critical(BFS_PRINT);", " }", "}", "", "void", "bfs_snapshot(void)", "{ clock_t stop_time;", " double delta_time;", " struct tms stop_tm;", " volatile BFS_data *s;", "", " e_critical(BFS_PRINT);", " printf(\"cpu%%02d Depth= %%7lu States= %%8.3g Transitions= %%8.3g \",", " who_am_i, mreached, nstates, nstates+truncs);", " printf(\"Memory= %%9.3f\\t\", memcnt/1048576.);", " printf(\"SharedMLeft= %%4lu \", bfs_left/1048576);", " stop_time = times(&stop_tm);", " delta_time = ((double) (stop_time - start_time))/((double) sysconf(_SC_CLK_TCK));", " if (delta_time > 0.01)", " { printf(\"t= %%6.3g R= %%6.0g\\n\", delta_time, nstates/delta_time);", " } else", " { printf(\"t= %%6.3g R= %%6.0g\\n\", 0., 0.);", " }", " fflush(stdout);", " x_critical(BFS_PRINT);", "", " s = &shared_memory->bfs_data[who_am_i];", " s->mreached = (ulong) mreached;", " s->vsize = (ulong) vsize;", " s->errors = (int) errors;", " s->memcnt = (double) memcnt;", " s->nstates = (double) nstates;", " s->nlinks = (double) nlinks;", " s->truncs = (double) truncs;", " s->memory_left = (ulong) bfs_left;", " s->punted = (ulong) bfs_punt;", " bfs_snapped++; /* for bfs_best */", "}", "", "void", "bfs_shutdown(const char *s)", "{", " bfs_clear_locks(); /* in case we interrupted at a bad point */", " if (!strstr(s, \"early \") || verbose)", " { bfs_printf(\"stop (%%s)\\n\", s);", " }", " bfs_update();", " if (who_am_i == 0)", " { wrapup();", "#ifdef BFS_DISK", " bfs_disk_stop();", "#endif", " }", " bfs_mark_done(2);", " pan_exit(2);", "}", "", "SV_Hold *bfs_free_hold;", "", "SV_Hold *", "bfs_get_hold(void)", "{ SV_Hold *x;", " if (bfs_free_hold)", " { x = bfs_free_hold;", " bfs_free_hold = bfs_free_hold->nxt;", " } else", " { x = (SV_Hold *) sh_malloc((ulong) sizeof(SV_Hold));", " }", " return x;", "}", "", "BFS_Trail *", "bfs_unpack_state(BFS_Slot *n) /* called in bfs_explore_state */", "{ BFS_Trail *otrpt;", " BFS_State *bfs_t;", " int vecsz;", "", " if (!n || !n->s_data || !n->s_data->t_info)", " { bfs_Uerror(\"internal error\");", " }", " otrpt = (BFS_Trail *) ((BFS_State *) n->s_data)->t_info;", "", " trpt->ostate = otrpt->ostate;", " trpt->st = otrpt->st;", " trpt->o_tt = otrpt->o_tt;", " trpt->pr = otrpt->pr;", " trpt->tau = otrpt->tau;", " trpt->o_pm = otrpt->o_pm;", " if (trpt->ostate)", " trpt->o_t = t_id_lkup[otrpt->t_id];", "#if defined(C_States) && (HAS_TRACK==1)", " c_revert((uchar *) &(now.c_state[0]));", "#endif", " if (trpt->o_pm & 4) /* rv succeeded */", " { return (BFS_Trail *) 0; /* revisit not needed */", " }", "#ifndef NOREDUCE", " bfs_nps = 0;", "#endif", " if (trpt->o_pm & 8) /* rv attempt failed */", " { revrv++;", " if (trpt->tau&8)", " { trpt->tau &= ~8; /* break atomic */", "#ifndef NOREDUCE", " } else if (trpt->tau&32) /* void preselection */", " { trpt->tau &= ~32;", " bfs_nps = 1; /* no preselection in repeat */", "#endif", " } }", " trpt->o_pm &= ~(4|8);", " if (trpt->o_tt > mreached)", " { static ulong nr = 0L, nc;", " mreached = trpt->o_tt;", " nc = (long) nstates/FREQ;", " if (nc > nr)", " { nr = nc;", " bfs_snapshot();", " } }", " depth = trpt->o_tt;", " if (depth >= maxdepth)", " {", "#if SYNC", " if (boq != -1)", " { BFS_Trail *x = (BFS_Trail *) trpt->ostate;", " if (x) x->o_pm |= 4; /* rv not failing */", " }", "#endif", " truncs++;", " if (!warned)", " { warned = 1;", " bfs_printf(\"error: max search depth too small\\n\");", " }", " if (bounded)", " { bfs_uerror(\"depth limit reached\");", " }", " return (BFS_Trail *) 0;", " }", "", " bfs_t = n->s_data;", "#if NRUNS>0", " vsize = bfs_t->omask->sz;", "#else", " vsize = ((State *) (bfs_t->osv))->_vsz;", "#endif", "#if SYNC", " boq = bfs_t->boq;", "#endif", "", "#if defined(Q_PROVISO) && !defined(BITSTATE) && defined(FULLSTACK)", " #ifdef USE_TDH", " if (((uchar *)(bfs_t->lstate))) /* if BFS_INQ is set */", " { *((uchar *) bfs_t->lstate) = 0; /* turn it off */", " }", " #else", " if (bfs_t->lstate) /* bfs_par */", " { bfs_t->lstate->tagged = 0; /* bfs_par state removed from q */", " }", " #endif", "#endif", " memcpy((char *) &now, (uchar *) bfs_t->osv, vsize);", "#if !defined(NOCOMP) && !defined(HC) && NRUNS>0", " Mask = (uchar *) bfs_t->omask->sv; /* in shared memory */", "#endif", "#ifdef BFS_CHECK", " if (0) bfs_dump_now(\"got1\");", "#endif", "#ifdef TRIX", " re_populate();", "#else", " #if NRUNS>0", " if (now._nr_pr > 0)", " {", " #if VECTORSZ>32000", " proc_offset = (int *) bfs_t->omask->po;", " #else", " proc_offset = (short *) bfs_t->omask->po;", " #endif", " proc_skip = (uchar *) bfs_t->omask->ps;", " }", " if (now._nr_qs > 0)", " {", " #if VECTORSZ>32000", " q_offset = (int *) bfs_t->omask->qo;", " #else", " q_offset = (short *) bfs_t->omask->qo;", " #endif", " q_skip = (uchar *) bfs_t->omask->qs;", " }", " #endif", "#endif", " vecsz = ((State *) bfs_t->osv)->_vsz;", "#ifdef BFS_CHECK", " assert(vecsz > 0 && vecsz < VECTORSZ);", "#endif", " { SV_Hold *x = bfs_get_hold();", " x->sv = bfs_t->osv;", " x->nxt = bfs_svfree[vecsz];", " bfs_svfree[vecsz] = x;", " bfs_t->osv = (State *) 0;", " }", "#if NRUNS>0", " bfs_keep(bfs_t->omask);", "#endif", "", "#ifdef BFS_CHECK", " if (0) bfs_dump_now(\"got2\");", " if (0) view_state(\"after\");", "#endif", " return (BFS_Trail *) bfs_t->t_info;", "}", "void", "bfs_initial_state(void)", "{", "#ifdef BFS_CHECK", " assert(trpt != NULL);", "#endif", " trpt->ostate = (H_el *) 0;", " trpt->o_tt = -1;", " trpt->tau = 0;", "#ifdef VERI", " trpt->tau |= 4; /* claim moves first */", "#endif", " bfs_store_state(trpt, boq); /* initial state : bfs_lib.c */", "}", "", "#ifdef BITSTATE", " #define bfs_do_store(v, n) b_store(v, n)", "#else", " #ifdef USE_TDH", " #define bfs_do_store(v, n) o_store(v, n)", " #else", " #define bfs_do_store(v, n) h_store(v, n)", " #endif", "#endif", "", "#ifdef BFS_SEP_HASH", "int", "bfs_seen_before(void)", "{ /* cannot set trpt->tau |= 64 to mark successors outside stack */", " /* since the check is done remotely and the trpt value is gone */", " #ifdef VERI", " if (!trpt->ostate /* initial state */", " || ((trpt->tau&4) /* starting claim moves(s) */", " && !(((BFS_Trail *)trpt->ostate)->tau&4))) /* prev move: prog */", " { return 0; /* claim move: mid-state not stored */", " } /* else */", " #endif", " if (!bfs_do_store((char *)&now, vsize)) /* sep_hash */", " { nstates++; /* local count */", " return 0; /* new state */", " }", " #ifdef BFS_CHECK", " bfs_printf(\"seen before\\n\");", " #endif", " truncs++;", " return 1; /* old state */", "}", "#endif", "", "void", "bfs_explore_state(BFS_Slot *v) /* generate all successors of v */", "{ BFS_Trail *otrpt;", " Trans *t;", "#ifdef HAS_UNLESS", " int E_state;", "#endif", " int tt;", " short II, To = BASE, From = (short) (now._nr_pr-1);", " short oboq = boq;", " uchar _n, _m, ot;", "", " memset(ntrpt, 0, sizeof(Trail));", " otrpt = bfs_unpack_state(v); /* BFS_Trail */", "", " if (!otrpt) { return; } /* e.g., depth limit reached */", "#ifdef L_BOUND", " #if defined(VERBOSE)", " bfs_printf(\"Unpacked state with l_bound %%d -- sds %%p\\n\",", " now._l_bnd, now._l_sds);", " #endif", "#endif", "", "#if defined(C_States) && (HAS_TRACK==1)", " c_revert((uchar *) &(now.c_state[0]));", "#endif", "", "#ifdef BFS_SEP_HASH", " if (bfs_seen_before()) return;", "#endif", "", "#ifdef VERI", /* could move to just before store_state */ " if (now._nr_pr == 0 /* claim terminated */", " || stopstate[((Pclaim *)pptr(0))->_t][((Pclaim *)pptr(0))->_p])", " { bfs_uerror(\"end state in claim reached\");", " }", "#endif", " trpt->tau &= ~1; /* timeout off */", "#ifdef VERI", " if (trpt->tau&4) /* claim move */", " { trpt->tau |= (otrpt->tau)&1; /* inherit from prog move */", " From = To = 0; /* claim */", " goto Repeat_two;", " }", "#endif", "#ifndef NOREDUCE", " if (boq == -1 && !(trpt->tau&8) && bfs_nps == 0)", " for (II = now._nr_pr-1; II >= BASE; II -= 1)", " {", "Pickup: this = pptr(II);", " tt = (int) ((P0 *)this)->_p;", " ot = (uchar) ((P0 *)this)->_t;", " if (trans[ot][tt]->atom & 8)", " { t = trans[ot][tt];", " if (t->qu[0] != 0)", " { if (!q_cond(II, t))", " continue;", " }", " From = To = II;", " trpt->tau |= 32; /* preselect marker */", " #ifdef VERBOSE", " bfs_printf(\"%%3ld: proc %%d PreSelected (tau=%%d)\\n\", ", " depth, II, trpt->tau);", " #endif", " goto Repeat_two;", " } }", " trpt->tau &= ~32;", "#endif", "", "Repeat_one:", " if (trpt->tau&8)", " { From = To = (short ) trpt->pr; /* atomic */", " } else", " { From = now._nr_pr-1;", " To = BASE;", " }", "#if defined(VERI) || !defined(NOREDUCE) || defined(ETIM)", "Repeat_two: /* MainLoop */", "#endif", " _n = _m = 0;", " for (II = From; II >= To; II -= 1) /* all processes */", " {", "#ifdef BFS_CHECK", " bfs_printf(\"proc %%d (%%d - %%d)\\n\", II, From, To);", "#endif", "#if SYNC ", " if (boq != -1 && trpt->pr == II)", " { continue; /* no rendezvous with same proc */", " }", "#endif", " this = pptr(II);", " tt = (int) ((P0 *)this)->_p;", " ot = (uchar) ((P0 *)this)->_t;", " ntrpt->pr = (uchar) II;", " ntrpt->st = tt; ", " trpt->o_pm &= ~1; /* no move yet */", "#ifdef EVENT_TRACE", " trpt->o_event = now._event;", "#endif", "#ifdef HAS_PRIORITY", " if (!highest_priority(((P0 *)this)->_pid, t))", " { continue;", " }", "#else", " #ifdef HAS_PROVIDED", " if (!provided(II, ot, tt, t))", " { continue;", " }", " #endif", "#endif", "#ifdef HAS_UNLESS", " E_state = 0;", "#endif", " for (t = trans[ot][tt]; t; t = t->nxt) /* all process transitions */", " {", "#ifdef BFS_CHECK", " assert(t_id_lkup[t->t_id] == t); /* for reverse lookup in bfs_unpack_state */", "#endif", "#ifdef VERBOSE", " if (0) bfs_printf(\"\\tproc %%d tr %%d\\n\", II, t->forw);", "#endif", "#ifdef HAS_UNLESS", " if (E_state > 0", " && E_state != t->e_trans)", " break;", "#endif", " /* trpt->o_t = */ ntrpt->o_t = t;", " oboq = boq;", "", " if (!(_m = do_transit(t, II)))", " continue;", "", " trpt->o_pm |= 1; /* we moved */", " (trpt+1)->o_m = _m; /* for unsend */", "#ifdef PEG", " peg[t->forw]++;", "#endif", "#ifdef VERBOSE", " e_critical(BFS_PRINT);", " printf(\"%%3ld: proc %%d exec %%d, \",", " depth, II, t->forw);", " printf(\"%%d to %%d, %%s %%s %%s\",", " tt, t->st, t->tp,", " (t->atom&2)?\"atomic\":\"\",", " (boq != -1)?\"rendez-vous\":\"\");", " #ifdef HAS_UNLESS", " if (t->e_trans)", " printf(\" (escapes to state %%d)\", t->st);", " #endif", " printf(\" %%saccepting [tau=%%d]\\n\",", " (trpt->o_pm&2)?\"\":\"non-\", trpt->tau);", " x_critical(BFS_PRINT);", "#endif", "#ifdef HAS_UNLESS", " E_state = t->e_trans;", " #if SYNC>0", " if (t->e_trans > 0 && boq != -1)", " { fprintf(efd, \"error: rendezvous stmnt in the escape clause\\n\");", " fprintf(efd, \" of unless stmnt not compatible with -DBFS\\n\");", " pan_exit(1);", " }", " #endif", "#endif", " if (t->st > 0)", " { ((P0 *)this)->_p = t->st;", " }", " /* use the ostate ptr, with type *H_el, to temporarily store *BFS_Trail */", "#ifdef BFS_NOTRAIL", " ntrpt->ostate = (H_el *) 0; /* no error-traces in this mode */", "#else", " ntrpt->ostate = (H_el *) otrpt; /* parent stackframe */", "#endif", " /* ntrpt->st = tt; * was already set above */", "", " if (boq == -1 && (t->atom&2)) /* atomic */", " { ntrpt->tau = 8; /* record for next move */", " } else", " { ntrpt->tau = 0; /* no timeout or preselect etc */", " }", "#ifdef VERI", " ntrpt->tau |= trpt->tau&4; /* if claim, inherit */", " if (boq == -1 && !(ntrpt->tau&8)) /* unless rv or atomic */", " { if (ntrpt->tau&4) /* claim */", " { ntrpt->tau &= ~4; /* switch to prog */", " } else", " { ntrpt->tau |= 4; /* switch to claim */", " } }", "#endif", "#ifdef L_BOUND", " { uchar obnd = now._l_bnd;", " uchar *os = now._l_sds;", " #ifdef VERBOSE", " bfs_printf(\"saving bound %%d -- sds %%p\\n\", obnd, (void *) os);", " #endif", "#endif", "", " bfs_store_state(ntrpt, oboq);", "#ifdef EVENT_TRACE", " now._event = trpt->o_event;", "#endif", " /* undo move and generate other successor states */", " trpt++; /* this is where ovals and ipt are set */", " do_reverse(t, II, _m); /* restore now. */", "#ifdef L_BOUND", " #ifdef VERBOSE", " bfs_printf(\"restoring bound %%d -- sds %%p\\n\", obnd, (void *) os);", " #endif", " now._l_bnd = obnd;", " now._l_sds = os;", " }", "#endif", " trpt--;", "#ifdef VERBOSE", " e_critical(BFS_PRINT);", " printf(\"%%3ld: proc %%d \", depth, II);", " printf(\"reverses %%d, %%d to %%d,\", t->forw, tt, t->st);", " printf(\" %%s [abit=%%d,adepth=%%d,\", t->tp, now._a_t, 0);", " printf(\"tau=%%d,%%d]\\n\", trpt->tau, (trpt-1)->tau);", " x_critical(BFS_PRINT);", "#endif", " reached[ot][t->st] = 1;", " reached[ot][tt] = 1;", "", " ((P0 *)this)->_p = tt;", " _n |= _m;", " } }", "#ifdef VERBOSE", " bfs_printf(\"done _n = %%d\\n\", _n);", "#endif", "", "#ifndef NOREDUCE", " /* preselected - no succ definitely outside stack */", " if ((trpt->tau&32) && !(trpt->tau&64))", " { From = now._nr_pr-1; To = BASE;", " #ifdef VERBOSE", " bfs_printf(\"%%3ld: proc %%d UnSelected (_n=%%d, tau=%%d)\\n\", ", " depth, II+1, (int) _n, trpt->tau);", " #endif", " _n = 0; trpt->tau &= ~32;", " if (II >= BASE)", " { goto Pickup;", " }", " goto Repeat_two;", " }", " trpt->tau &= ~(32|64);", "#endif", " if (_n == 0", "#ifdef VERI", " && !(trpt->tau&4)", "#endif", " )", " { /* no successor states generated */", " if (boq != -1) /* was rv move */", " { BFS_Trail *x = (BFS_Trail *) trpt->ostate; /* pre-rv state */", " if (x && ((x->tau&8) || (x->tau&32))) /* break atomic or preselect */", " { x->o_pm |= 8; /* mark failure */", " this = pptr(otrpt->pr);", " ((P0 *) this)->_p = otrpt->st; /* reset state */", " unsend(boq); /* retract rv offer */", " boq = -1;", "#ifdef VERBOSE", " printf(\"repush state\\n\");", "#endif", " bfs_push_state(NULL, x, x->o_tt); /* repush rv fail */", " } /* else the rv need not be retried */", " } else if (now._nr_pr > BASE) /* possible deadlock */", " { if ((trpt->tau&8)) /* atomic step blocked */", " { trpt->tau &= ~(1|8); /* 1=timeout, 8=atomic */", " goto Repeat_one;", " }", "#ifdef ETIM", " /* if timeouts were used in the model */", " if (!(trpt->tau&1))", " { trpt->tau |= 1; /* enable timeout */", " goto Repeat_two;", " }", "#endif", " if (!noends && !endstate())", " { bfs_uerror(\"invalid end state.\");", " }", " }", "#ifdef VERI", " else /* boq == -1 && now._nr_pr == BASE && trpt->tau != 4 */", " { trpt->tau |= 4; /* switch to claim for stutter moves */", " #ifdef VERBOSE", " printf(\"%%3ld: proc -1 exec -1, (stutter move)\\n\", depth, II);", " #endif", " bfs_store_state(trpt, boq);", /* doesn't store it but queues it */ " #ifdef VERBOSE", " printf(\"%%3ld: proc -1 reverses -1, (stutter move)\\n\", depth, II);", " #endif", " trpt->tau &= ~4; /* undo, probably not needed */", " }", "#endif", " }", "#ifdef BFS_NOTRAIL", " bfs_release_trail(otrpt);", "#endif", "}", "#ifndef BFS_FIFO", "void", "bfs_recycle(BFS_Slot *n)", "{", " #ifdef BFS_CHECK", " assert(n != &bfs_null);", " #endif", " n->nxt = bfs_free_slot;", " bfs_free_slot = n;", "", " #ifdef BFS_CHECK", " bfs_printf(\"recycles %%s -- %%p\\n\",", " n->s_data?\"STATE\":\"EMPTY\", (void *) n);", " #endif", "}", "#endif", "#ifdef BFS_FIFO", "int", "bfs_empty(int p)", /* return Cores if all empty or index of first non-empty q of p */ "{ int i;", " const int dst = 0;", " for (i = 0; i < Cores; i++)", " { if (shared_memory->head[dst][p][i] != (BFS_Slot *) 0)", " {", " volatile BFS_Slot *x = shared_memory->head[dst][p][i];", " while (x && x->type == DELETED)", " { x = x->nxt;", " }", " if (!x)", " { continue;", " }", " if (p == who_am_i)", " { shared_memory->head[dst][p][i] = x;", " }", " #ifdef BFS_CHECK", " bfs_printf(\"input q [%%d][%%d][%%d] !empty\\n\",", " dst, p, i);", " #endif", " return i;", " } }", " #ifdef BFS_CHECK", " bfs_printf(\"all input qs [%%d][%%d][0..max] empty\\n\",", " dst, p);", " #endif ", " return Cores;", "}", "#endif", "#ifdef BFS_DISK", "void", "bfs_ewrite(int fd, const void *p, size_t count)", "{", " if (write(fd, p, count) != count)", " { perror(\"diskwrite\");", " Uerror(\"aborting\");", " }", "}", "", "void", "bfs_eread(int fd, void *p, size_t count)", "{", " if (read(fd, p, count) != count)", " { perror(\"diskread\");", " Uerror(\"aborting\");", " }", "}", "", "void", "bfs_sink_disk(int who_are_you, BFS_Slot *n)", "{ SV_Hold *x;", "#ifdef VERBOSE", " bfs_printf(\"sink_disk -> %%d\\n\", who_are_you);", "#endif", " bfs_ewrite(bfs_out_fd[who_are_you], (const void *) n->s_data->t_info, sizeof(BFS_Trail));", " bfs_ewrite(bfs_out_fd[who_are_you], (const void *) &vsize, sizeof(ulong));", " bfs_ewrite(bfs_out_fd[who_are_you], &now, vsize);", "", " bfs_release_trail(n->s_data->t_info);", " n->s_data->t_info = (BFS_Trail *) 0;", "", "#if NRUNS>0", " bfs_ewrite(bfs_out_fd[who_are_you], (const void *) &(n->s_data->omask), sizeof(EV_Hold *));", "#endif", "#ifdef Q_PROVISO", " bfs_ewrite(bfs_out_fd[who_are_you], (const void *) &(n->s_data->lstate), sizeof(H_el *));", "#endif", "#if SYNC>0", " bfs_ewrite(bfs_out_fd[who_are_you], (const void *) &(n->s_data->boq), sizeof(short));", "#endif", "#if VERBOSE", " bfs_ewrite(bfs_out_fd[who_are_you], (const void *) &(n->s_data->nr), sizeof(ulong));", "#endif", " shared_memory->bfs_out_cnt[who_am_i] = 1;", /* wrote at least one state */ "}", "void", "bfs_source_disk(int fd, volatile BFS_Slot *n)", "{ ulong nb; /* local temporary */", " SV_Hold *x;", "#ifdef VERBOSE", " bfs_printf(\"source_disk <- %%d\\n\", who_am_i);", "#endif", " n->s_data->t_info = bfs_grab_trail();", " bfs_eread(fd, (void *) n->s_data->t_info, sizeof(BFS_Trail));", " bfs_eread(fd, (void *) &nb, sizeof(ulong));", "", " x = bfs_new_sv(nb); /* space for osv isn't already allocated */", " n->s_data->osv = x->sv;", " x->sv = (State *) 0;", " x->nxt = bfs_free_hold;", " bfs_free_hold = x;", "", " bfs_eread(fd, (void *) n->s_data->osv, (size_t) nb);", "#if NRUNS>0", " bfs_eread(fd, (void *) &(n->s_data->omask), sizeof(EV_Hold *));", "#endif", "#ifdef Q_PROVISO", " bfs_eread(fd, (void *) &(n->s_data->lstate), sizeof(H_el *));", "#endif", "#if SYNC>0", " bfs_eread(fd, (void *) &(n->s_data->boq), sizeof(short));", "#endif", "#if VERBOSE", " bfs_eread(fd, (void *) &(n->s_data->nr), sizeof(ulong));", "#endif", "}", "#endif", "", "#ifdef BFS_STAGGER", "static BFS_Slot *bfs_stage[BFS_STAGGER];", "", "static void", "bfs_stagger_flush(void)", "{ int i, who_are_you;", " int dst = 1 - bfs_toggle;", " BFS_Slot *n;", " who_are_you = (rand()%%Cores);", /* important: all to the same cpu, but reversed */ " for (i = bfs_stage_cnt-1; i >= 0; i--)", " { n = bfs_stage[i];", "#ifdef BFS_DISK", " bfs_sink_disk(who_are_you, n);", " bfs_stage[i] = (BFS_Slot *) 0;", "#endif", " n->nxt = (BFS_Slot *) shared_memory->head[dst][who_are_you][who_am_i];", " shared_memory->head[dst][who_are_you][who_am_i] = n;", " /* bfs_sent++; */", " }", " #ifdef VERBOSE", " bfs_printf(\"stagger flush %%d states to %%d\\n\",", " bfs_stage_cnt, who_are_you);", " #endif", " bfs_stage_cnt = 0;", "}", "", "void", "bfs_stagger_add(BFS_Slot *n)", "{", " if (bfs_stage_cnt == BFS_STAGGER)", " { bfs_stagger_flush();", " }", " bfs_stage[bfs_stage_cnt++] = n;", "}", "#endif", "", "void", "bfs_push_state(Trail *x, BFS_Trail *y, int tt)", "{ int who_are_you;", " BFS_Slot *n = bfs_pack_state(x, y, tt);", "#ifdef BFS_FIFO", " const int dst = 0;", "#else", " int dst = 1 - bfs_toggle;", "#endif", "", "#ifdef BFS_GREEDY", " who_are_you = who_am_i; /* for testing only */", "#else", " if (bfs_keep_state > 0)", " { who_are_you = bfs_keep_state - 1;", " } else", " {", " #ifdef BFS_STAGGER", " who_are_you = -1;", " bfs_stagger_add(n);", " goto done;", " #else", " who_are_you = (rand()%%Cores);", " #endif", " }", "#endif", "#ifdef BFS_FIFO", " if (!shared_memory->tail[dst][who_are_you][who_am_i])", " { shared_memory->dels[dst][who_are_you][who_am_i] =", " shared_memory->tail[dst][who_are_you][who_am_i] =", " shared_memory->head[dst][who_are_you][who_am_i] = n;", " } else", " { shared_memory->tail[dst][who_are_you][who_am_i]->nxt = n;", " shared_memory->tail[dst][who_are_you][who_am_i] = n;", " }", " shared_memory->bfs_idle[who_are_you] = 0;", "#else", " #ifdef BFS_DISK", " bfs_sink_disk(who_are_you, n);", " #endif", " n->nxt = (BFS_Slot *) shared_memory->head[dst][who_are_you][who_am_i];", " shared_memory->head[dst][who_are_you][who_am_i] = n;", "#endif", "#ifdef BFS_STAGGER", "done:", "#endif", "#ifdef VERBOSE", " bfs_printf(\"PUT STATE (depth %%ld, nr %%u) to %%d -- s_data: %%p\\n\",", " tt, n->s_data->nr, who_are_you, n->s_data);", "#endif", " bfs_sent++;", "}", "", "BFS_Slot *", "bfs_next(void)", "{ volatile BFS_Slot *n = &bfs_null;", " #ifdef BFS_FIFO", " const int src = 0;", " bfs_qscan = bfs_empty(who_am_i);", " #else", " const int src = bfs_toggle;", " while (bfs_qscan < Cores", " && shared_memory->head[src][who_am_i][bfs_qscan] == (BFS_Slot *) 0)", " { bfs_qscan++;", " }", " #endif", " if (bfs_qscan < Cores)", " {", " #ifdef BFS_FIFO", /* no wait for toggles */ " shared_memory->bfs_idle[who_am_i] = 0;", " for (n = shared_memory->head[src][who_am_i][bfs_qscan]; n; n = n->nxt)", " { if (n->type != DELETED)", " { break;", " } }", " #ifdef BFS_CHECK", " assert(n && n->type == STATE); /* q cannot be empty */", " #endif", " if (n->nxt)", " { shared_memory->head[src][who_am_i][bfs_qscan] = n->nxt;", " }", /* else, do not remove it - yet - avoid empty queues */ " n->type = DELETED;", " #else", " n = shared_memory->head[src][who_am_i][bfs_qscan];", " shared_memory->head[src][who_am_i][bfs_qscan] = n->nxt;", " #if defined(BFS_FIFO) && defined(BFS_CHECK)", " assert(n->type == STATE);", " #endif", " n->nxt = (BFS_Slot *) 0;", " #ifdef BFS_DISK", " /* the states actually show up in reverse order (FIFO iso LIFO) here */", " /* but that doesnt really matter as long as the count is right */", " bfs_source_disk(bfs_inp_fd[bfs_qscan], n); /* get the data */", " #endif", " #endif", " #ifdef BFS_CHECK", " bfs_printf(\"rcv STATE from [%%d][%%d][%%d]\\n\",", " src, who_am_i, bfs_qscan);", " #endif", " bfs_rcvd++;", " } else", " {", " #ifdef BFS_STAGGER", " if (bfs_stage_cnt > 0)", " { bfs_stagger_flush();", " }", " #endif", " shared_memory->bfs_idle[who_am_i] = 1;", " #if defined(BFS_FIFO) && defined(BFS_CHECK)", " assert(n->type == EMPTY);", " #endif", " }", " return (BFS_Slot *) n;", "}", "", "int", "bfs_all_empty(void)", "{ int i;", "#ifdef BFS_DISK", " for (i = 0; i < Cores; i++)", " { if (shared_memory->bfs_out_cnt[i] != 0)", " {", " #ifdef VERBOSE", " bfs_printf(\"bfs_all_empty %%d not empty\\n\", i);", " #endif", " return 0;", " } }", "#else", " int p;", " #ifdef BFS_FIFO", " const int dst = 0;", " #else", " int dst = 1 - bfs_toggle; /* next generation */", " #endif", " for (p = 0; p < Cores; p++)", " for (i = 0; i < Cores; i++)", " { if (shared_memory->head[dst][p][i] != (BFS_Slot *) 0)", " { return 0;", " } }", "#endif", "#ifdef VERBOSE", " bfs_printf(\"bfs_all_empty\\n\");", "#endif", " return 1;", "}", "", "#ifdef BFS_FIFO", "BFS_Slot *", "bfs_sweep(void)", "{ BFS_Slot *n;", " int i;", " for (i = 0; i < Cores; i++)", " for (n = (BFS_Slot *) shared_memory->dels[0][who_am_i][i];", " n && n != shared_memory->head[0][who_am_i][i];", " n = n->nxt)", " { if (n->type == DELETED && n->nxt)", " { shared_memory->dels[0][who_am_i][i] = n->nxt;", " n->nxt = (BFS_Slot *) 0;", " return n;", " } }", " return (BFS_Slot *) sh_malloc((ulong) sizeof(BFS_Slot));", "}", "#endif", "", "typedef struct BFS_T_Hold BFS_T_Hold;", "struct BFS_T_Hold {", " volatile BFS_Trail *t;", " BFS_T_Hold *nxt;", "};", "BFS_T_Hold *bfs_t_held, *bfs_t_free;", "", "BFS_Trail *", "bfs_grab_trail(void)", /* call in bfs_source_disk and bfs_new_slot */ "{ BFS_Trail *t;", " BFS_T_Hold *h;", "", "#ifdef VERBOSE", " bfs_printf(\"grab trail - bfs_t_held %%p\\n\", (void *) bfs_t_held);", "#endif", " if (bfs_t_held)", " { h = bfs_t_held;", " bfs_t_held = bfs_t_held->nxt;", " t = (BFS_Trail *) h->t;", " h->t = (BFS_Trail *) 0; /* make sure it cannot be reused */", " h->nxt = bfs_t_free;", " bfs_t_free = h;", "", " } else", " { t = (BFS_Trail *) sh_malloc((ulong) sizeof(BFS_Trail));", " }", "#ifdef BFS_CHECK", " assert(t);", "#endif", " t->ostate = (H_el *) 0;", "#ifdef VERBOSE", " bfs_printf(\"grab trail %%p\\n\", (void *) t);", "#endif", " return t;", "}", "", "#if defined(BFS_DISK) || defined(BFS_NOTRAIL)", "void", "bfs_release_trail(BFS_Trail *t)", /* call in bfs_sink_disk (not bfs_recycle) */ "{ BFS_T_Hold *h;", " #ifdef BFS_CHECK", " assert(t);", " #endif", " #ifdef VERBOSE", " bfs_printf(\"release trail %%p\\n\", (void *) t);", " #endif", " if (bfs_t_free)", " { h = bfs_t_free;", " bfs_t_free = bfs_t_free->nxt;", " } else", " { h = (BFS_T_Hold *) emalloc(sizeof(BFS_T_Hold));", " }", " h->t = t;", " h->nxt = bfs_t_held;", " bfs_t_held = h;", " #ifdef VERBOSE", " bfs_printf(\"release trail - bfs_t_held %%p\\n\", (void *) bfs_t_held);", " #endif", "}", "#endif", "", "BFS_Slot *", "bfs_new_slot(BFS_Trail *f)", "{ BFS_Slot *t;", "", "#ifdef BFS_FIFO", " t = bfs_sweep();", "#else", " if (bfs_free_slot) /* local */", " { t = bfs_free_slot;", " bfs_free_slot = bfs_free_slot->nxt;", " t->nxt = (BFS_Slot *) 0;", " } else", " { t = (BFS_Slot *) sh_malloc((ulong) sizeof(BFS_Slot));", " }", "#endif", " if (t->s_data)", " { memset(t->s_data, 0, sizeof(BFS_State));", " } else", " { t->s_data = (BFS_State *) sh_malloc((ulong) sizeof(BFS_State));", " }", "", " /* we keep a ptr to the frame of parent states, which is */", " /* used for reconstructing path and recovering failed rvs etc */", " /* we should not overwrite the data at this address with a memset */", "", " if (f)", " { t->s_data->t_info = f;", " } else", " { t->s_data->t_info = bfs_grab_trail();", " }", " return t;", "}", "", "SV_Hold *", "bfs_new_sv(int n)", "{ SV_Hold *h;", "", " if (bfs_svfree[n])", " { h = bfs_svfree[n];", " bfs_svfree[n] = h->nxt;", " h->nxt = (SV_Hold *) 0;", " } else", " { h = (SV_Hold *) sh_malloc((ulong) sizeof(SV_Hold));", "#if 0", " h->sz = n;", "#endif", " h->sv = (State *) sh_malloc((ulong)(sizeof(State) - VECTORSZ + n));", " }", " memcpy((char *)h->sv, (char *)&now, n);", " return h;", "}", "#if NRUNS>0", "static EV_Hold *kept[VECTORSZ]; /* local */", "", "static void", "bfs_keep(EV_Hold *v)", "{ EV_Hold *h;", "", " for (h = kept[v->sz]; h; h = h->nxt) /* check local list */", " { if (v->nrpr == h->nrpr", " && v->nrqs == h->nrqs", "#if !defined(NOCOMP) && !defined(HC)", " && (v->sv == h->sv || memcmp((char *) v->sv, (char *) h->sv, v->sz) == 0)", "#endif", "#ifdef TRIX", " )", "#else", " #if NRUNS>0", " #if VECTORSZ>32000", " && (memcmp((char *) v->po, (char *) h->po, v->nrpr * sizeof(int)) == 0)", " && (memcmp((char *) v->qo, (char *) h->qo, v->nrqs * sizeof(int)) == 0)", " #else", " && (memcmp((char *) v->po, (char *) h->po, v->nrpr * sizeof(short)) == 0)", " && (memcmp((char *) v->qo, (char *) h->qo, v->nrqs * sizeof(short)) == 0)", " #endif", " && (memcmp((char *) v->ps, (char *) h->ps, v->nrpr * sizeof(uchar)) == 0)", " && (memcmp((char *) v->qs, (char *) h->qs, v->nrqs * sizeof(uchar)) == 0))", " #else", " )", " #endif", "#endif", " { break;", " } }", "", " if (!h) /* we don't have one like it yet */", " { v->nxt = kept[v->sz]; /* keep the original owner field */", " kept[v->sz] = v;", " /* all ptrs inside are to shared memory, but nxt is local */", " }", "}", "", "EV_Hold *", "bfs_new_sv_mask(int n)", "{ EV_Hold *h;", "", " for (h = kept[n]; h; h = h->nxt)", " { if ((now._nr_pr == h->nrpr)", " && (now._nr_qs == h->nrqs)", "#if !defined(NOCOMP) && !defined(HC) && NRUNS>0", " && ((char *) Mask == h->sv || (memcmp((char *) Mask, h->sv, n) == 0))", "#endif", "#ifdef TRIX", " )", "#else", " #if NRUNS>0", " #if VECTORSZ>32000", " && (memcmp((char *) proc_offset, (char *) h->po, now._nr_pr * sizeof(int)) == 0)", " && (memcmp((char *) q_offset, (char *) h->qo, now._nr_qs * sizeof(int)) == 0)", " #else", " && (memcmp((char *) proc_offset, (char *) h->po, now._nr_pr * sizeof(short)) == 0)", " && (memcmp((char *) q_offset, (char *) h->qo, now._nr_qs * sizeof(short)) == 0)", " #endif", " && (memcmp((char *) proc_skip, (char *) h->ps, now._nr_pr * sizeof(uchar)) == 0)", " && (memcmp((char *) q_skip, (char *) h->qs, now._nr_qs * sizeof(uchar)) == 0))", " #else", " )", " #endif", "#endif", " { break;", " } }", "", " if (!h)", " { /* once created, the contents are never modified */", " h = (EV_Hold *) sh_malloc((ulong)sizeof(EV_Hold));", " h->owner = who_am_i;", " h->sz = n;", " h->nrpr = now._nr_pr;", " h->nrqs = now._nr_qs;", "#if !defined(NOCOMP) && !defined(HC) && NRUNS>0", " h->sv = (char *) Mask; /* in shared memory, and never modified */", "#endif", "#if NRUNS>0 && !defined(TRIX)", " if (now._nr_pr > 0)", " { h->ps = (char *) proc_skip;", " h->po = (char *) proc_offset;", " }", " if (now._nr_qs > 0)", " { h->qs = (char *) q_skip;", " h->qo = (char *) q_offset;", " }", "#endif", " h->nxt = kept[n];", " kept[n] = h;", " }", " return h;", "}", "#endif", /* NRUNS>0 */ "BFS_Slot *", "bfs_pack_state(Trail *f, BFS_Trail *g, int search_depth)", "{ BFS_Slot *t = bfs_new_slot(g);", "", "#ifdef BFS_CHECK", " assert(t->s_data != NULL);", " assert(t->s_data->t_info != NULL);", " assert(f || g);", "#endif", " if (!g)", " { t->s_data->t_info->ostate = f->ostate;", " t->s_data->t_info->st = f->st;", " t->s_data->t_info->o_tt = search_depth;", " t->s_data->t_info->pr = f->pr;", " t->s_data->t_info->tau = f->tau;", " t->s_data->t_info->o_pm = f->o_pm;", " if (f->o_t)", " { t->s_data->t_info->t_id = f->o_t->t_id;", " } else", " { t->s_data->t_info->t_id = -1;", " t->s_data->t_info->ostate = NULL;", " }", " } /* else t->s_data->t_info == g */", "#if SYNC", " t->s_data->boq = boq;", "#endif", "#ifdef VERBOSE", " { static ulong u_cnt;", " t->s_data->nr = u_cnt++;", " }", "#endif", "#ifdef TRIX", " sv_populate(); /* make sure now is up to date */", "#endif", "#ifndef BFS_DISK", " { SV_Hold *x = bfs_new_sv(vsize);", " t->s_data->osv = x->sv;", " x->sv = (State *) 0;", " x->nxt = bfs_free_hold;", " bfs_free_hold = x;", " }", "#endif", "#if NRUNS>0", " t->s_data->omask = bfs_new_sv_mask(vsize);", "#endif", "", "#if defined(Q_PROVISO) && !defined(BITSTATE)", " t->s_data->lstate = Lstate; /* Lstate is set in o_store or h_store */", "#endif", "#ifdef BFS_FIFO", " t->type = STATE;", "#endif", " return t;", "}", "", "void", "bfs_store_state(Trail *t, short oboq)", "{", "#ifdef TRIX", " sv_populate();", "#endif", "#if defined(VERI) && defined(Q_PROVISO) && !defined(BITSTATE) && defined(FULLSTACK)", " if (!(t->tau&4)", /* prog move */ " && t->ostate)", /* not initial state */ " { t->tau |= ((BFS_Trail *) t->ostate)->tau&64;", " } /* lift 64 across claim moves */", "#endif", "", "#ifdef BFS_SEP_HASH", " #if SYNC", " if (boq == -1 && oboq != -1) /* post-rv */", " { BFS_Trail *x = (BFS_Trail *) trpt->ostate; /* pre-rv state */", " if (x)", " { x->o_pm |= 4; /* rv complete */", " } }", " #endif", " d_sfh((uchar *)&now, (int) vsize); /* sep-hash -- sets K1 -- overkill */", " bfs_keep_state = K1%%Cores + 1;", " bfs_push_state(t, NULL, trpt->o_tt+1); /* bfs_store_state - sep_hash */", " bfs_keep_state = 0;", "#else", " #ifdef VERI", #if 0 in VERI mode store the state when (!t->ostate || (t->tau&4)) in initial state and after each program move i.e., dont store when !(!t->ostate || (t->tau&4)) = (t->ostate && !(t->tau&4)) the *first* time that the tau flag is not set: possibly after a series of claim moves in an atomic sequence #endif " if (!(t->tau&4) && t->ostate && (((BFS_Trail *)t->ostate)->tau&4))", " { /* do not store intermediate state */", " #if defined(VERBOSE) && defined(L_BOUND)", " bfs_printf(\"Un-Stored state bnd %%d -- sds %%p\\n\",", " now._l_bnd, now._l_sds);", " #endif", " bfs_push_state(t, NULL, trpt->o_tt+1); /* claim move */", " } else", " #endif", " if (!bfs_do_store((char *)&now, vsize)) /* includes bfs_visited */", " { nstates++; /* local count */", " trpt->tau |= 64; /* bfs: succ outside stack */", " #if SYNC", " if (boq == -1 && oboq != -1) /* post-rv */", " { BFS_Trail *x = ", " (BFS_Trail *) trpt->ostate; /* pre-rv state */", " if (x)", " { x->o_pm |= 4; /* rv complete */", " } }", " #endif", " bfs_push_state(t, NULL, trpt->o_tt+1); /* successor */", " } else", " { truncs++;", " #ifdef BFS_CHECK", " bfs_printf(\"seen before\\n\");", " #endif", " #if defined(Q_PROVISO) && !defined(BITSTATE) && defined(FULLSTACK)", " #ifdef USE_TDH", " if (Lstate)", /* if BFS_INQ is set */ " { trpt->tau |= 64;", " }", " #else", " if (Lstate && Lstate->tagged) /* bfs_store_state */", " { trpt->tau |= 64;", " }", " #endif", " #endif", " }", "#endif", "}", "", "/*** support routines ***/", "", "void", "bfs_clear_locks(void)", "{ int i;", "", " /* clear any locks held by this process only */", " if (shared_memory)", " for (i = 0; i < BFS_MAXLOCKS; i++)", " { if (shared_memory->sh_owner[i] == who_am_i + 1)", " { shared_memory->sh_locks[i] = 0;", "#ifdef BFS_CHECK", " shared_memory->in_count[i] = 0;", "#endif", " shared_memory->sh_owner[i] = 0;", " } }", "}", "", "void", "e_critical(int which)", "{ int w;", "#ifdef BFS_CHECK", " assert(which >= 0 && which < BFS_MAXLOCKS);", "#endif", " if (shared_memory == NULL) return;", " while (tas(&(shared_memory->sh_locks[which])) != 0)", " { w = shared_memory->sh_owner[which]; /* sh_locks[which] could be 0 by now */", " assert(w >= 0 && w <= BFS_MAXPROCS);", " if (w > 0 && shared_memory->bfs_flag[w-1] == 2)", " { /* multiple processes can get here; only one should do this: */", " if (tas(&(shared_memory->bfs_data[w - 1].override)) == 0)", " { fprintf(stderr, \"cpu%%02d: override lock %%d - held by %%d\\n\",", " who_am_i, which, shared_memory->sh_owner[which]);", "#ifdef BFS_CHECK", " shared_memory->in_count[which] = 0;", "#endif", " shared_memory->sh_locks[which] = 0;", " shared_memory->sh_owner[which] = 0;", " } }", " shared_memory->wait_count[which]++; /* not atomic of course */", " }", "#ifdef BFS_CHECK", " if (shared_memory->in_count[which] != 0)", " { fprintf(stderr, \"cpu%%02d: cannot happen lock %%d count %%d\\n\", who_am_i,", " which, shared_memory->in_count[which]);", " }", " shared_memory->in_count[which]++;", "#endif", " shared_memory->sh_owner[which] = who_am_i+1;", "}", "", "void", "x_critical(int which)", "{", " if (shared_memory == NULL) return;", "#ifdef BFS_CHECK", " assert(shared_memory->in_count[which] == 1);", " shared_memory->in_count[which] = 0;", "#endif", " shared_memory->sh_locks[which] = 0;", " shared_memory->sh_owner[which] = 0;", "}", "", "void", "bfs_printf(const char *fmt, ...)", "{ va_list args;", "", " e_critical(BFS_PRINT);", "#ifdef BFS_CHECK", " if (1) { int i=who_am_i; while (i-- > 0) printf(\" \"); }", "#endif", " printf(\"cpu%%02d: \", who_am_i);", " va_start(args, fmt);", " vprintf(fmt, args);", " va_end(args);", " fflush(stdout);", " x_critical(BFS_PRINT);", "}", "", "int", "bfs_all_idle(void)", "{ int i;", "", " if (shared_memory)", " for (i = 0; i < Cores; i++)", " { if (shared_memory->bfs_flag[i] == 0", " && shared_memory->bfs_idle[i] == 0)", " { return 0;", " } }", " return 1;", "}", "", "#ifdef BFS_FIFO", "int", "bfs_idle_and_empty(void)", "{ int p; /* read-only */", " for (p = 0; p < Cores; p++)", " { if (shared_memory->bfs_flag[p] == 0", " && shared_memory->bfs_idle[p] == 0)", " { return 0;", " } }", " for (p = 0; p < Cores; p++)", " { if (bfs_empty(p) < Cores)", " { return 0;", " } }", " return 1;", "}", "#endif", "", "void", "bfs_set_toggle(void) /* executed by root */", "{ int i;", "", " if (shared_memory)", " for (i = 0; i < Cores; i++)", " { shared_memory->bfs_idle[i] = 0;", " }", "}", "", "int", "bfs_all_running(void) /* crash detection */", "{ int i;", " for (i = 0; i < Cores; i++)", " { if (!shared_memory || shared_memory->bfs_flag[i] > 1)", " { return 0;", " } }", " return 1;", "}", "", "void", "bfs_mark_done(int code)", "{", " if (shared_memory)", " { shared_memory->bfs_flag[who_am_i] = (int) code;", " shared_memory->quit = 1;", " }", "}", "", "static uchar *", "bfs_offset(int c)", "{ int p, N;", "#ifdef COLLAPSE", " uchar *q = (uchar *) ncomps; /* it is the first object allocated */", " q += (256+2) * sizeof(ulong); /* preserve contents of ncomps */", "#else", " uchar *q = (uchar *) &(shared_memory->allocator);", "#endif", " /* _NP_+1 proctypes, reachability info:", " * reached[x : 0 .. _NP_+1][ 0 .. NrStates[x] ]", " */", " for (p = N = 0; p <= _NP_; p++)", " { N += NrStates[p]; /* sum for all proctypes */", " }", "", " /* space needed per proctype: N bytes */", " /* rounded up to a multiple of the word size */", " if ((N%%sizeof(void *)) != 0) /* aligned */", " { N += sizeof(void *) - (N%%sizeof(void *));", " }", "", " q += ((c - 1) * (_NP_ + 1) * N);", " return q;", "}", "", "static void", "bfs_putreached(void)", "{ uchar *q;", " int p;", "", " assert(who_am_i > 0);", "", " q = bfs_offset(who_am_i);", " for (p = 0; p <= _NP_; p++)", " { memcpy((void *) q, (const void *) reached[p], (size_t) NrStates[p]);", " q += NrStates[p];", " }", "}", "", "static void", "bfs_getreached(int c)", "{ uchar *q;", " int p, i;", "", " assert(who_am_i == 0 && c >= 1 && c < Cores);", "", " q = (uchar *) bfs_offset(c);", " for (p = 0; p <= _NP_; p++)", " for (i = 0; i < NrStates[p]; i++)", " { reached[p][i] += *q++; /* update local copy */", " }", "}", "", "void", "bfs_update(void)", "{ int i;", " volatile BFS_data *s;", "", " if (!shared_memory) return;", "", " s = &shared_memory->bfs_data[who_am_i];", " if (who_am_i == 0)", " { shared_memory->bfs_flag[who_am_i] = 3; /* or else others dont stop */", " bfs_gcount = 0;", " for (i = 1; i < Cores; i++) /* start at 1 not 0 */", " { while (shared_memory->bfs_flag[i] == 0)", " { sleep(1);", " if (bfs_gcount++ > WAIT_MAX) /* excessively long wait */", " { printf(\"cpu00: give up waiting for cpu%%2d (%%d cores)\\n\", i, Cores);", " bfs_gcount = 0;", " break;", " } }", " s = &shared_memory->bfs_data[i];", " mreached = Max(mreached, s->mreached);", " hmax = vsize = Max(vsize, s->vsize);", " errors += s->errors;", " memcnt += s->memcnt;", " nstates += s->nstates;", " nlinks += s->nlinks;", " truncs += s->truncs;", " bfs_left += s->memory_left;", " bfs_punt += s->punted;", " bfs_getreached(i);", " }", " } else", " { s->mreached = (ulong) mreached;", " s->vsize = (ulong) vsize;", " s->errors = (int) errors;", " s->memcnt = (double) memcnt;", " s->nstates = (double) nstates;", " s->nlinks = (double) nlinks;", " s->truncs = (double) truncs;", " s->memory_left = (ulong) bfs_left;", " s->punted = (ulong) bfs_punt;", " bfs_putreached();", " }", "}", "", "volatile uchar *", "sh_pre_malloc(ulong n) /* used before the local heaps are populated */", "{ volatile uchar *ptr = NULL;", "", " assert(!bfs_runs);", " if ((n%%sizeof(void *)) != 0)", " { n += sizeof(void *) - (n%%sizeof(void *));", " assert((n%%sizeof(void *)) == 0);", " }", "", " e_critical(BFS_MEM); /* needed? */", " if (shared_memory->mem_left < n + 7)", /* 7 for possible alignment */ " { x_critical(BFS_MEM);", " bfs_printf(\"want %%lu, have %%lu\\n\",", " n, shared_memory->mem_left);", " bfs_shutdown(\"out of shared memory\");", " assert(0); /* should be unreachable */", " }", " ptr = shared_memory->allocator;", "#if WS>4", /* align to 8 byte boundary */ " { int b = (int) ((uint64_t) ptr)&7;", " if (b != 0)", " { ptr += (8-b);", " shared_memory->allocator = ptr;", " } }", "#endif", " shared_memory->allocator += n;", " shared_memory->mem_left -= n;", " x_critical(BFS_MEM);", "", " bfs_pre_allocated += n;", "", " return ptr;", "}", "", "volatile uchar *", "sh_malloc(ulong n)", "{ volatile uchar *ptr = NULL;", "#ifdef BFS_CHECK", " assert(bfs_runs);", "#endif", " if ((n%%sizeof(void *)) != 0)", " { n += sizeof(void *) - (n%%sizeof(void *));", "#ifdef BFS_CHECK", " assert((n%%sizeof(void *)) == 0);", "#endif", " }", "", " /* local heap -- no locks needed */", " if (bfs_left < n)", " { e_critical(BFS_MEM);", " if (shared_memory->mem_left >= n)", " { ptr = (uchar *) shared_memory->allocator;", " shared_memory->allocator += n;", " shared_memory->mem_left -= n;", " x_critical(BFS_MEM);", " return ptr;", " }", " x_critical(BFS_MEM);", "#ifdef BFS_LOGMEM", " int i;", " e_critical(BFS_MEM);", " for (i = 0; i < 1024; i++)", " { if (shared_memory->logmem[i] > 0)", " { bfs_printf(\"\tlog[%%d]\t%%d\\n\", i, shared_memory->logmem[i]);", " } }", " x_critical(BFS_MEM);", "#endif", " bfs_shutdown(\"out of shared memory\"); /* no return */", " }", "#ifdef BFS_LOGMEM", " e_critical(BFS_MEM);", " if (n < 1023)", " { shared_memory->logmem[n]++;", " } else", " { shared_memory->logmem[1023]++;", " }", " x_critical(BFS_MEM);", "#endif", " ptr = (uchar *) bfs_heap;", " bfs_heap += n;", " bfs_left -= n;", "", " if (0) printf(\"sh_malloc %%ld\\n\", n);", " return ptr;", "}", "", "volatile uchar *", "bfs_get_shared_mem(key_t key, size_t n)", "{ char *rval;", "", " assert(who_am_i == 0);", "", " shared_mem_id = shmget(key, n, 0600 | IPC_CREAT | IPC_EXCL); /* create */", " if (shared_mem_id == -1)", " { fprintf(stderr, \"cpu%%02d: tried to get %%d MB of shared memory\\n\",", " who_am_i, (int) n/(1024*1024));", " perror(\"shmget\");", " exit(1);", " }", " if ((rval = (char *) shmat(shared_mem_id, (void *) 0, 0)) == (char *) -1) /* attach */", " { perror(\"shmat\");", " exit(1);", " }", " return (uchar *) rval;", "}", "", "void", "bfs_drop_shared_memory(void)", "{", " if (who_am_i == 0)", " { printf(\"pan: releasing shared memory...\");", " fflush(stdout);", " }", " if (shared_memory)", " { shmdt(shared_memory); /* detach */", " if (who_am_i == 0)", " { shmctl(shared_mem_id, IPC_RMID, (void *) 0); /* remove */", " } }", " if (who_am_i == 0)", " { printf(\"done\\n\");", " fflush(stdout);", " }", "}", "", "size_t", "bfs_find_largest(key_t key)", "{ size_t n;", " const size_t delta = 32*1024*1024;", " int temp_id = -1;", " int atleastonce = 0;", "", " for (n = delta; ; n += delta)", " { if (WS <= 4 && n >= 1024*1024*1024)", /* was n >= INT_MAX */ " { n = 1024*1024*1024;", " break;", " }", "#ifdef MEMLIM", " if ((double) n > memlim)", " { n = (size_t) memlim;", " break;", " }", "#endif", " temp_id = shmget(key, n, 0600); /* check for stale copy */", " if (temp_id != -1)", " { if (shmctl(temp_id, IPC_RMID, ((void *) 0)) < 0) /* remove */", " { perror(\"remove_segment_fails 2\");", " exit(1);", " } }", "", " temp_id = shmget(key, n, 0600 | IPC_CREAT | IPC_EXCL); /* create new */", " if (temp_id == -1)", " { n -= delta;", " break;", " } else", " { atleastonce++;", " if (shmctl(temp_id, IPC_RMID, ((void *) 0)) < 0)", " { perror(\"remove_segment_fails 0\");", " exit(1);", " } } }", "", " if (!atleastonce)", " { printf(\"cpu%%02d: no shared memory n=%%d\\n\", who_am_i, (int) n);", " exit(1);", " }", "", " printf(\"cpu%%02d: largest shared memory segment: %%lu MB\\n\",", " who_am_i, (ulong) n/(1024*1024));", "#if 0", " #ifdef BFS_SEP_HASH", " n /= 2; /* not n /= Cores because the queues take most memory */", " printf(\"cpu%%02d: using %%lu MB\\n\", who_am_i, (ulong) n/(1024*1024));", " #endif", "#endif", " fflush(stdout);", "", " if ((n/(1024*1024)) == 32)", " { if (sizeof(void *) == 4) /* a 32 bit machine */", " { fprintf(stderr, \"\\t32MB is the default; increase it to 1 GB with:\\n\");", " fprintf(stderr, \"\\tsudo /sbin/sysctl kernel.shmmax=%%d\\n\", (1<<30));", " fprintf(stderr, \"\\tsudo /sbin/sysctl kernel.shmall=%%d\\n\", (1<<30)/8192);", " } else if (sizeof(void *) == 8) /* a 64 bit machine */", " { fprintf(stderr, \"\\t32MB is the default; increase it to 30 GB with:\\n\");", " fprintf(stderr, \"\\tsudo /sbin/sysctl kernel.shmmax=32212254720\\n\");", " fprintf(stderr, \"\\tsudo /sbin/sysctl kernel.shmall=7864320\\n\");", " fprintf(stderr, \"\\tor for 60 GB:\\n\");", " fprintf(stderr, \"\\tsudo /sbin/sysctl kernel.shmmax=60000000000\\n\");", " fprintf(stderr, \"\\tsudo /sbin/sysctl kernel.shmall=30000000\\n\");", " } else", " { fprintf(stderr, \"\\tweird wordsize %%d\\n\", (int) sizeof(void *));", " } }", "", " return n;", "}", "#ifdef BFS_DISK", "void", "bfs_disk_start(void)", /* setup .spin*/ "{ int unused = system(\"rm -fr .spin\");", " if (mkdir(\".spin\", 0777) != 0)", " { perror(\"mkdir\");", " Uerror(\"aborting\");", " }", "}", "void", "bfs_disk_stop(void)", /* remove .spin */ "{", " if (system(\"rm -fr .spin\") < 0)", " { perror(\"rm -fr .spin/\");", " }", "}", "void", "bfs_disk_inp(void)", /* this core only */ "{ int i; char fnm[16];", "#ifdef VERBOSE", " bfs_printf(\"inp %%d %%d 0..%%d\\n\", bfs_toggle, who_am_i, Cores);", "#endif", " for (i = 0; i < Cores; i++)", " { sprintf(fnm, \".spin/q%%d_%%d_%%d\", bfs_toggle, who_am_i, i);", " if ((bfs_inp_fd[i] = open(fnm, 0444)) < 0)", " { perror(\"open\");", " Uerror(fnm);", " } }", "}", "void", "bfs_disk_out(void)", /* this core only */ "{ int i; char fnm[16];", "#ifdef VERBOSE", " bfs_printf(\"out %%d 0..%%d %%d\\n\", 1-bfs_toggle, Cores, who_am_i);", "#endif", " shared_memory->bfs_out_cnt[who_am_i] = 0;", " for (i = 0; i < Cores; i++)", " { sprintf(fnm, \".spin/q%%d_%%d_%%d\", 1-bfs_toggle, i, who_am_i);", " if ((bfs_out_fd[i] = creat(fnm, 0666)) < 0)", " { perror(\"creat\");", " Uerror(fnm);", " } }", "}", "void", "bfs_disk_iclose(void)", "{ int i;", "#ifdef VERBOSE", " bfs_printf(\"close_inp\\n\");", "#endif", " for (i = 0; i < Cores; i++)", " { if (close(bfs_inp_fd[i]) < 0)", " { perror(\"iclose\");", " } }", "}", "void", "bfs_disk_oclose(void)", "{ int i;", "#ifdef VERBOSE", " bfs_printf(\"close_out\\n\");", "#endif", " for (i = 0; i < Cores; i++)", " { if (fsync(bfs_out_fd[i]) < 0)", " { perror(\"fsync\");", " }", " if (close(bfs_out_fd[i]) < 0)", " { perror(\"oclose\");", " } }", "}", "#endif", "void", "bfs_write_snap(int fd)", "{ if (write(fd, snap, strlen(snap)) != strlen(snap))", " { printf(\"pan: error writing %%s\\n\", fnm);", " bfs_shutdown(\"file system error\");", " }", "}", "", "void", "bfs_one_step(BFS_Trail *t, int fd)", "{ if (t && t->t_id != (T_ID) -1)", " { sprintf(snap, \"%%d:%%d:%%d\\n\",", " trcnt++, t->pr, t->t_id);", " bfs_write_snap(fd);", " }", "}", "", "void", "bfs_putter(BFS_Trail *t, int fd)", "{ if (t && t != (BFS_Trail *) t->ostate)", " bfs_putter((BFS_Trail *) t->ostate, fd);", "#ifdef L_BOUND", " if (depthfound == trcnt)", " { strcpy(snap, \"-1:-1:-1\\n\");", " bfs_write_snap(fd);", " depthfound = -1;", " }", "#endif", " bfs_one_step(t, fd);", "}", "", "void", "bfs_nuerror(char *str)", "{ int fd = make_trail();", "", " if (fd < 0) return;", "#ifdef VERI", " sprintf(snap, \"-2:%%d:-2\\n\", (uchar) ((P0 *)pptr(0))->_t);", " bfs_write_snap(fd);", "#endif", "#ifdef MERGED", " sprintf(snap, \"-4:-4:-4\\n\");", " bfs_write_snap(fd);", "#endif", " trcnt = 1;", " if (strstr(str, \"invalid\"))", " { bfs_putter((BFS_Trail *) trpt->ostate, fd);", " } else", " { BFS_Trail x;", " memset((char *) &x, 0, sizeof(BFS_Trail));", " x.pr = trpt->pr;", " x.t_id = (trpt->o_t)?trpt->o_t->t_id:0;", " x.ostate = trpt->ostate;", " bfs_putter(&x, fd);", " }", " close(fd);", " if (errors >= upto && upto != 0)", " { bfs_shutdown(str);", " }", "}", "", "void", "bfs_uerror(char *str)", "{ static char laststr[256];", "", " errors++;", " if (strncmp(str, laststr, 254) != 0)", " { bfs_printf(\"pan:%%d: %%s (at depth %%ld)\\n\",", " errors, str, ((depthfound == -1)?depth:depthfound));", " strncpy(laststr, str, 254);", " }", "#ifdef HAS_CODE", " if (readtrail) { wrap_trail(); return; }", "#endif", " if (every_error != 0 || errors == upto)", " { bfs_nuerror(str);", " }", " if (errors >= upto && upto != 0)", " { bfs_shutdown(\"bfs_uerror\");", " }", " depthfound = -1;", "}\n", "void", "bfs_Uerror(char *str)", "{ /* bfs_uerror(str); */", " bfs_printf(\"pan:%%d: %%s (at depth %%ld)\\n\", ++errors, str,", " ((depthfound == -1)?depth:depthfound));", " bfs_shutdown(\"bfs_Uerror\");", "}", 0, };