#include #include #include #include #include #ifdef BFS_DISK #include #include #include #include #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_Slot { #ifdef BFS_FIFO enum bfs_types type; /* message type */ #endif BFS_State *s_data; /* state data */ #ifndef BFS_QSZ BFS_Slot *nxt; /* linked list */ #endif }; 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 #ifdef BFS_QSZ #define BFS_NORECYCLE #if BFS_QSZ<=0 #error BFS_QSZ must be positive #endif #ifdef BFS_FIFO #error BFS_QSZ cannot be combined with BFS_FIFO #endif #ifdef BFS_DISK #error BFS_QSZ cannot be combined with BFS_DISK #endif volatile BFS_Slot bfsq[BFS_GEN][BFS_MAXPROCS][BFS_MAXPROCS][BFS_QSZ]; volatile uint bfs_ix[BFS_GEN][BFS_MAXPROCS][BFS_MAXPROCS]; #else volatile BFS_Slot *head[BFS_GEN][BFS_MAXPROCS][BFS_MAXPROCS]; #endif #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 }; extern volatile uchar *bfs_get_shared_mem(key_t, size_t); extern BFS_Slot * bfs_new_slot(BFS_Trail *); extern BFS_Slot * bfs_prep_slot(BFS_Trail *, BFS_Slot *); extern BFS_Slot * bfs_next(void); extern BFS_Slot * bfs_pack_state(Trail *, BFS_Trail *, int, BFS_Slot *); 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 parallelize 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; #ifndef BFS_QSZ static BFS_Slot *bfs_free_slot; /* local free list */ #endif 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(); #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)); 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 #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); } void bfs_run(void) { BFS_Slot *v; #ifdef BFS_DISK bfs_disk_out(); #endif if (who_am_i == 0) { bfs_initial_state(); } #ifdef BFS_DISK #ifdef BFS_STAGGER bfs_stagger_flush(); #endif bfs_disk_oclose(); #endif #ifdef BFS_FIFO static int i_count; #endif srand(s_rand+HASH_NR); 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 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, II, 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); #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 } #if !defined(BFS_FIFO) && !defined(BFS_NORECYCLE) 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) { 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; } 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 #ifndef BFS_QSZ #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); 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 #endif void bfs_push_state(Trail *x, BFS_Trail *y, int tt) { int who_are_you; #ifdef BFS_FIFO const int dst = 0; #else int dst = 1 - bfs_toggle; #endif #ifdef BFS_QSZ uint z; if (bfs_keep_state > 0) { who_are_you = bfs_keep_state - 1; } else { who_are_you = (rand()%Cores); } z = shared_memory->bfs_ix[dst][who_are_you][who_am_i]; if (z >= BFS_QSZ) { static int warned_qloss = 0; if (warned_qloss == 0 && who_am_i == 0) { warned_qloss++; bfs_printf("BFS_QSZ too small - losing states\n"); } bfs_punt++; return; } shared_memory->bfs_ix[dst][who_are_you][who_am_i] = z+1; BFS_Slot *n = bfs_pack_state(x, y, tt, bfs_prep_slot(y, (BFS_Slot *) &(shared_memory->bfsq[dst][who_are_you][who_am_i][z]))); #else BFS_Slot *n = bfs_pack_state(x, y, tt, bfs_new_slot(y)); #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 #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; #ifdef BFS_QSZ while (bfs_qscan < Cores && shared_memory->bfs_ix[src][who_am_i][bfs_qscan] == 0) { bfs_qscan++; } #else while (bfs_qscan < Cores && shared_memory->head[src][who_am_i][bfs_qscan] == (BFS_Slot *) 0) { bfs_qscan++; } #endif #endif if (bfs_qscan < Cores) { #ifdef BFS_FIFO 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; } n->type = DELETED; #else #ifdef BFS_QSZ uint x = --shared_memory->bfs_ix[src][who_am_i][bfs_qscan]; n = &(shared_memory->bfsq[src][who_am_i][bfs_qscan][x]); #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; #endif #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 { #if defined(BFS_STAGGER) && !defined(BFS_QSZ) 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++) #ifdef BFS_QSZ { if (shared_memory->bfs_ix[dst][p][i] > 0) #else { if (shared_memory->head[dst][p][i] != (BFS_Slot *) 0) #endif { 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) { 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) { 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 #ifndef BFS_QSZ 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; } #else BFS_Slot * bfs_prep_slot(BFS_Trail *f, BFS_Slot *t) { if (t->s_data) { memset(t->s_data, 0, sizeof(BFS_State)); } else { t->s_data = (BFS_State *) sh_malloc((ulong) sizeof(BFS_State)); } if (f) { t->s_data->t_info = f; } else { t->s_data->t_info = bfs_grab_trail(); } return t; } #endif 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 BFS_Slot * bfs_pack_state(Trail *f, BFS_Trail *g, int search_depth, BFS_Slot *t) { #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) && !defined(NOREDUCE) 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) && t->ostate) { 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 (!(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) { 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) { 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 { 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(" log[%d] %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) { 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) { int unused = system("rm -fr .spin"); if (mkdir(".spin", 0777) != 0) { perror("mkdir"); Uerror("aborting"); } } void bfs_disk_stop(void) { if (system("rm -fr .spin") < 0) { perror("rm -fr .spin/"); } } void bfs_disk_inp(void) { 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) { 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:%lu: %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; } void bfs_Uerror(char *str) { /* bfs_uerror(str); */ bfs_printf("pan:%lu: %s (at depth %ld)\n", ++errors, str, ((depthfound == -1)?depth:depthfound)); bfs_shutdown("bfs_Uerror"); }