/***** 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 char *pan_par[] = { /* generates pan.p */
"#include <sys/ipc.h>",
"#include <sys/shm.h>",
"#include <time.h>", /* for nanosleep */
"#include <assert.h>",
"#include <limits.h>",
"#ifdef BFS_DISK",
"#include <unistd.h>", /* for rmdir */
"#include <sys/stat.h>", /* for mkdir */
"#include <sys/types.h>",
"#include <fcntl.h>", /* 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,
};
|
