sys/src/cmd/spin/pangen7.h

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