src/cuBdd/cuddCache.c

Go to the documentation of this file.

#include "util.h"
#include "cuddInt.h"

/*---------------------------------------------------------------------------*/
/* Constant declarations                                                     */
/*---------------------------------------------------------------------------*/

#ifdef DD_CACHE_PROFILE
#define DD_HYSTO_BINS 8
#endif

/*---------------------------------------------------------------------------*/
/* Stucture declarations                                                     */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Type declarations                                                         */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Variable declarations                                                     */
/*---------------------------------------------------------------------------*/

#ifndef lint
static char rcsid[] DD_UNUSED = "$Id: cuddCache.c,v 1.34 2009/02/19 16:17:50 fabio Exp $";
#endif

/*---------------------------------------------------------------------------*/
/* Macro declarations                                                        */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Static function prototypes                                                */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Definition of exported functions                                          */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Definition of internal functions                                          */
/*---------------------------------------------------------------------------*/


int
cuddInitCache(
  DdManager * unique /* unique table */,
  unsigned int cacheSize /* initial size of the cache */,
  unsigned int maxCacheSize /* cache size beyond which no resizing occurs */)
{
    int i;
    unsigned int logSize;
#ifndef DD_CACHE_PROFILE
    DdNodePtr *mem;
    ptruint offset;
#endif

    /* Round cacheSize to largest power of 2 not greater than the requested
    ** initial cache size. */
    logSize = cuddComputeFloorLog2(ddMax(cacheSize,unique->slots/2));
    cacheSize = 1 << logSize;
    unique->acache = ALLOC(DdCache,cacheSize+1);
    if (unique->acache == NULL) {
        unique->errorCode = CUDD_MEMORY_OUT;
        return(0);
    }
    /* If the size of the cache entry is a power of 2, we want to
    ** enforce alignment to that power of two. This happens when
    ** DD_CACHE_PROFILE is not defined. */
#ifdef DD_CACHE_PROFILE
    unique->cache = unique->acache;
    unique->memused += (cacheSize) * sizeof(DdCache);
#else
    mem = (DdNodePtr *) unique->acache;
    offset = (ptruint) mem & (sizeof(DdCache) - 1);
    mem += (sizeof(DdCache) - offset) / sizeof(DdNodePtr);
    unique->cache = (DdCache *) mem;
    assert(((ptruint) unique->cache & (sizeof(DdCache) - 1)) == 0);
    unique->memused += (cacheSize+1) * sizeof(DdCache);
#endif
    unique->cacheSlots = cacheSize;
    unique->cacheShift = sizeof(int) * 8 - logSize;
    unique->maxCacheHard = maxCacheSize;
    /* If cacheSlack is non-negative, we can resize. */
    unique->cacheSlack = (int) ddMin(maxCacheSize,
        DD_MAX_CACHE_TO_SLOTS_RATIO*unique->slots) -
        2 * (int) cacheSize;
    Cudd_SetMinHit(unique,DD_MIN_HIT);
    /* Initialize to avoid division by 0 and immediate resizing. */
    unique->cacheMisses = (double) (int) (cacheSize * unique->minHit + 1);
    unique->cacheHits = 0;
    unique->totCachehits = 0;
    /* The sum of cacheMisses and totCacheMisses is always correct,
    ** even though cacheMisses is larger than it should for the reasons
    ** explained above. */
    unique->totCacheMisses = -unique->cacheMisses;
    unique->cachecollisions = 0;
    unique->cacheinserts = 0;
    unique->cacheLastInserts = 0;
    unique->cachedeletions = 0;

    /* Initialize the cache */
    for (i = 0; (unsigned) i < cacheSize; i++) {
        unique->cache[i].h = 0; /* unused slots */
        unique->cache[i].data = NULL; /* invalid entry */
#ifdef DD_CACHE_PROFILE
        unique->cache[i].count = 0;
#endif
    }

    return(1);

} /* end of cuddInitCache */


void
cuddCacheInsert(
  DdManager * table,
  ptruint op,
  DdNode * f,
  DdNode * g,
  DdNode * h,
  DdNode * data)
{
    int posn;
    register DdCache *entry;
    ptruint uf, ug, uh;

    uf = (ptruint) f | (op & 0xe);
    ug = (ptruint) g | (op >> 4);
    uh = (ptruint) h;

    posn = ddCHash2(uh,uf,ug,table->cacheShift);
    entry = &table->cache[posn];

    table->cachecollisions += entry->data != NULL;
    table->cacheinserts++;

    entry->f    = (DdNode *) uf;
    entry->g    = (DdNode *) ug;
    entry->h    = uh;
    entry->data = data;
#ifdef DD_CACHE_PROFILE
    entry->count++;
#endif

} /* end of cuddCacheInsert */


void
cuddCacheInsert2(
  DdManager * table,
  DD_CTFP op,
  DdNode * f,
  DdNode * g,
  DdNode * data)
{
    int posn;
    register DdCache *entry;

    posn = ddCHash2(op,f,g,table->cacheShift);
    entry = &table->cache[posn];

    if (entry->data != NULL) {
        table->cachecollisions++;
    }
    table->cacheinserts++;

    entry->f = f;
    entry->g = g;
    entry->h = (ptruint) op;
    entry->data = data;
#ifdef DD_CACHE_PROFILE
    entry->count++;
#endif

} /* end of cuddCacheInsert2 */


void
cuddCacheInsert1(
  DdManager * table,
  DD_CTFP1 op,
  DdNode * f,
  DdNode * data)
{
    int posn;
    register DdCache *entry;

    posn = ddCHash2(op,f,f,table->cacheShift);
    entry = &table->cache[posn];

    if (entry->data != NULL) {
        table->cachecollisions++;
    }
    table->cacheinserts++;

    entry->f = f;
    entry->g = f;
    entry->h = (ptruint) op;
    entry->data = data;
#ifdef DD_CACHE_PROFILE
    entry->count++;
#endif

} /* end of cuddCacheInsert1 */


DdNode *
cuddCacheLookup(
  DdManager * table,
  ptruint op,
  DdNode * f,
  DdNode * g,
  DdNode * h)
{
    int posn;
    DdCache *en,*cache;
    DdNode *data;
    ptruint uf, ug, uh;

    uf = (ptruint) f | (op & 0xe);
    ug = (ptruint) g | (op >> 4);
    uh = (ptruint) h;

    cache = table->cache;
#ifdef DD_DEBUG
    if (cache == NULL) {
        return(NULL);
    }
#endif

    posn = ddCHash2(uh,uf,ug,table->cacheShift);
    en = &cache[posn];
    if (en->data != NULL && en->f==(DdNodePtr)uf && en->g==(DdNodePtr)ug &&
        en->h==uh) {
        data = Cudd_Regular(en->data);
        table->cacheHits++;
        if (data->ref == 0) {
            cuddReclaim(table,data);
        }
        return(en->data);
    }

    /* Cache miss: decide whether to resize. */
    table->cacheMisses++;

    if (table->cacheSlack >= 0 &&
        table->cacheHits > table->cacheMisses * table->minHit) {
        cuddCacheResize(table);
    }

    return(NULL);

} /* end of cuddCacheLookup */


DdNode *
cuddCacheLookupZdd(
  DdManager * table,
  ptruint op,
  DdNode * f,
  DdNode * g,
  DdNode * h)
{
    int posn;
    DdCache *en,*cache;
    DdNode *data;
    ptruint uf, ug, uh;

    uf = (ptruint) f | (op & 0xe);
    ug = (ptruint) g | (op >> 4);
    uh = (ptruint) h;

    cache = table->cache;
#ifdef DD_DEBUG
    if (cache == NULL) {
        return(NULL);
    }
#endif

    posn = ddCHash2(uh,uf,ug,table->cacheShift);
    en = &cache[posn];
    if (en->data != NULL && en->f==(DdNodePtr)uf && en->g==(DdNodePtr)ug &&
        en->h==uh) {
        data = Cudd_Regular(en->data);
        table->cacheHits++;
        if (data->ref == 0) {
            cuddReclaimZdd(table,data);
        }
        return(en->data);
    }

    /* Cache miss: decide whether to resize. */
    table->cacheMisses++;

    if (table->cacheSlack >= 0 &&
        table->cacheHits > table->cacheMisses * table->minHit) {
        cuddCacheResize(table);
    }

    return(NULL);

} /* end of cuddCacheLookupZdd */


DdNode *
cuddCacheLookup2(
  DdManager * table,
  DD_CTFP op,
  DdNode * f,
  DdNode * g)
{
    int posn;
    DdCache *en,*cache;
    DdNode *data;

    cache = table->cache;
#ifdef DD_DEBUG
    if (cache == NULL) {
        return(NULL);
    }
#endif

    posn = ddCHash2(op,f,g,table->cacheShift);
    en = &cache[posn];
    if (en->data != NULL && en->f==f && en->g==g && en->h==(ptruint)op) {
        data = Cudd_Regular(en->data);
        table->cacheHits++;
        if (data->ref == 0) {
            cuddReclaim(table,data);
        }
        return(en->data);
    }

    /* Cache miss: decide whether to resize. */
    table->cacheMisses++;

    if (table->cacheSlack >= 0 &&
        table->cacheHits > table->cacheMisses * table->minHit) {
        cuddCacheResize(table);
    }

    return(NULL);

} /* end of cuddCacheLookup2 */


DdNode *
cuddCacheLookup1(
  DdManager * table,
  DD_CTFP1 op,
  DdNode * f)
{
    int posn;
    DdCache *en,*cache;
    DdNode *data;

    cache = table->cache;
#ifdef DD_DEBUG
    if (cache == NULL) {
        return(NULL);
    }
#endif

    posn = ddCHash2(op,f,f,table->cacheShift);
    en = &cache[posn];
    if (en->data != NULL && en->f==f && en->h==(ptruint)op) {
        data = Cudd_Regular(en->data);
        table->cacheHits++;
        if (data->ref == 0) {
            cuddReclaim(table,data);
        }
        return(en->data);
    }

    /* Cache miss: decide whether to resize. */
    table->cacheMisses++;

    if (table->cacheSlack >= 0 &&
        table->cacheHits > table->cacheMisses * table->minHit) {
        cuddCacheResize(table);
    }

    return(NULL);

} /* end of cuddCacheLookup1 */


DdNode *
cuddCacheLookup2Zdd(
  DdManager * table,
  DD_CTFP op,
  DdNode * f,
  DdNode * g)
{
    int posn;
    DdCache *en,*cache;
    DdNode *data;

    cache = table->cache;
#ifdef DD_DEBUG
    if (cache == NULL) {
        return(NULL);
    }
#endif

    posn = ddCHash2(op,f,g,table->cacheShift);
    en = &cache[posn];
    if (en->data != NULL && en->f==f && en->g==g && en->h==(ptruint)op) {
        data = Cudd_Regular(en->data);
        table->cacheHits++;
        if (data->ref == 0) {
            cuddReclaimZdd(table,data);
        }
        return(en->data);
    }

    /* Cache miss: decide whether to resize. */
    table->cacheMisses++;

    if (table->cacheSlack >= 0 &&
        table->cacheHits > table->cacheMisses * table->minHit) {
        cuddCacheResize(table);
    }

    return(NULL);

} /* end of cuddCacheLookup2Zdd */


DdNode *
cuddCacheLookup1Zdd(
  DdManager * table,
  DD_CTFP1 op,
  DdNode * f)
{
    int posn;
    DdCache *en,*cache;
    DdNode *data;

    cache = table->cache;
#ifdef DD_DEBUG
    if (cache == NULL) {
        return(NULL);
    }
#endif

    posn = ddCHash2(op,f,f,table->cacheShift);
    en = &cache[posn];
    if (en->data != NULL && en->f==f && en->h==(ptruint)op) {
        data = Cudd_Regular(en->data);
        table->cacheHits++;
        if (data->ref == 0) {
            cuddReclaimZdd(table,data);
        }
        return(en->data);
    }

    /* Cache miss: decide whether to resize. */
    table->cacheMisses++;

    if (table->cacheSlack >= 0  &&
        table->cacheHits > table->cacheMisses * table->minHit) {
        cuddCacheResize(table);
    }

    return(NULL);

} /* end of cuddCacheLookup1Zdd */


DdNode *
cuddConstantLookup(
  DdManager * table,
  ptruint op,
  DdNode * f,
  DdNode * g,
  DdNode * h)
{
    int posn;
    DdCache *en,*cache;
    ptruint uf, ug, uh;

    uf = (ptruint) f | (op & 0xe);
    ug = (ptruint) g | (op >> 4);
    uh = (ptruint) h;

    cache = table->cache;
#ifdef DD_DEBUG
    if (cache == NULL) {
        return(NULL);
    }
#endif
    posn = ddCHash2(uh,uf,ug,table->cacheShift);
    en = &cache[posn];

    /* We do not reclaim here because the result should not be
     * referenced, but only tested for being a constant.
     */
    if (en->data != NULL &&
        en->f == (DdNodePtr)uf && en->g == (DdNodePtr)ug && en->h == uh) {
        table->cacheHits++;
        return(en->data);
    }

    /* Cache miss: decide whether to resize. */
    table->cacheMisses++;

    if (table->cacheSlack >= 0 &&
        table->cacheHits > table->cacheMisses * table->minHit) {
        cuddCacheResize(table);
    }

    return(NULL);

} /* end of cuddConstantLookup */


int
cuddCacheProfile(
  DdManager * table,
  FILE * fp)
{
    DdCache *cache = table->cache;
    int slots = table->cacheSlots;
    int nzeroes = 0;
    int i, retval;
    double exUsed;

#ifdef DD_CACHE_PROFILE
    double count, mean, meansq, stddev, expected;
    long max, min;
    int imax, imin;
    double *hystogramQ, *hystogramR; /* histograms by quotient and remainder */
    int nbins = DD_HYSTO_BINS;
    int bin;
    long thiscount;
    double totalcount, exStddev;

    meansq = mean = expected = 0.0;
    max = min = (long) cache[0].count;
    imax = imin = 0;
    totalcount = 0.0;

    hystogramQ = ALLOC(double, nbins);
    if (hystogramQ == NULL) {
        table->errorCode = CUDD_MEMORY_OUT;
        return(0);
    }
    hystogramR = ALLOC(double, nbins);
    if (hystogramR == NULL) {
        FREE(hystogramQ);
        table->errorCode = CUDD_MEMORY_OUT;
        return(0);
    }
    for (i = 0; i < nbins; i++) {
        hystogramQ[i] = 0;
        hystogramR[i] = 0;
    }

    for (i = 0; i < slots; i++) {
        thiscount = (long) cache[i].count;
        if (thiscount > max) {
            max = thiscount;
            imax = i;
        }
        if (thiscount < min) {
            min = thiscount;
            imin = i;
        }
        if (thiscount == 0) {
            nzeroes++;
        }
        count = (double) thiscount;
        mean += count;
        meansq += count * count;
        totalcount += count;
        expected += count * (double) i;
        bin = (i * nbins) / slots;
        hystogramQ[bin] += (double) thiscount;
        bin = i % nbins;
        hystogramR[bin] += (double) thiscount;
    }
    mean /= (double) slots;
    meansq /= (double) slots;

    /* Compute the standard deviation from both the data and the
    ** theoretical model for a random distribution. */
    stddev = sqrt(meansq - mean*mean);
    exStddev = sqrt((1 - 1/(double) slots) * totalcount / (double) slots);

    retval = fprintf(fp,"Cache average accesses = %g\n",  mean);
    if (retval == EOF) return(0);
    retval = fprintf(fp,"Cache access standard deviation = %g ", stddev);
    if (retval == EOF) return(0);
    retval = fprintf(fp,"(expected = %g)\n", exStddev);
    if (retval == EOF) return(0);
    retval = fprintf(fp,"Cache max accesses = %ld for slot %d\n", max, imax);
    if (retval == EOF) return(0);
    retval = fprintf(fp,"Cache min accesses = %ld for slot %d\n", min, imin);
    if (retval == EOF) return(0);
    exUsed = 100.0 * (1.0 - exp(-totalcount / (double) slots));
    retval = fprintf(fp,"Cache used slots = %.2f%% (expected %.2f%%)\n",
                     100.0 - (double) nzeroes * 100.0 / (double) slots,
                     exUsed);
    if (retval == EOF) return(0);

    if (totalcount > 0) {
        expected /= totalcount;
        retval = fprintf(fp,"Cache access hystogram for %d bins", nbins);
        if (retval == EOF) return(0);
        retval = fprintf(fp," (expected bin value = %g)\nBy quotient:",
                         expected);
        if (retval == EOF) return(0);
        for (i = nbins - 1; i>=0; i--) {
            retval = fprintf(fp," %.0f", hystogramQ[i]);
            if (retval == EOF) return(0);
        }
        retval = fprintf(fp,"\nBy residue: ");
        if (retval == EOF) return(0);
        for (i = nbins - 1; i>=0; i--) {
            retval = fprintf(fp," %.0f", hystogramR[i]);
            if (retval == EOF) return(0);
        }
        retval = fprintf(fp,"\n");
        if (retval == EOF) return(0);
    }

    FREE(hystogramQ);
    FREE(hystogramR);
#else
    for (i = 0; i < slots; i++) {
        nzeroes += cache[i].h == 0;
    }
    exUsed = 100.0 *
        (1.0 - exp(-(table->cacheinserts - table->cacheLastInserts) /
                   (double) slots));
    retval = fprintf(fp,"Cache used slots = %.2f%% (expected %.2f%%)\n",
                     100.0 - (double) nzeroes * 100.0 / (double) slots,
                     exUsed);
    if (retval == EOF) return(0);
#endif
    return(1);

} /* end of cuddCacheProfile */


void
cuddCacheResize(
  DdManager * table)
{
    DdCache *cache, *oldcache, *oldacache, *entry, *old;
    int i;
    int posn, shift;
    unsigned int slots, oldslots;
    double offset;
    int moved = 0;
    extern DD_OOMFP MMoutOfMemory;
    DD_OOMFP saveHandler;
#ifndef DD_CACHE_PROFILE
    ptruint misalignment;
    DdNodePtr *mem;
#endif

    oldcache = table->cache;
    oldacache = table->acache;
    oldslots = table->cacheSlots;
    slots = table->cacheSlots = oldslots << 1;

#ifdef DD_VERBOSE
    (void) fprintf(table->err,"Resizing the cache from %d to %d entries\n",
                   oldslots, slots);
    (void) fprintf(table->err,
                   "\thits = %g\tmisses = %g\thit ratio = %5.3f\n",
                   table->cacheHits, table->cacheMisses,
                   table->cacheHits / (table->cacheHits + table->cacheMisses));
#endif

    saveHandler = MMoutOfMemory;
    MMoutOfMemory = Cudd_OutOfMem;
    table->acache = cache = ALLOC(DdCache,slots+1);
    MMoutOfMemory = saveHandler;
    /* If we fail to allocate the new table we just give up. */
    if (cache == NULL) {
#ifdef DD_VERBOSE
        (void) fprintf(table->err,"Resizing failed. Giving up.\n");
#endif
        table->cacheSlots = oldslots;
        table->acache = oldacache;
        /* Do not try to resize again. */
        table->maxCacheHard = oldslots - 1;
        table->cacheSlack = - (int) (oldslots + 1);
        return;
    }
    /* If the size of the cache entry is a power of 2, we want to
    ** enforce alignment to that power of two. This happens when
    ** DD_CACHE_PROFILE is not defined. */
#ifdef DD_CACHE_PROFILE
    table->cache = cache;
#else
    mem = (DdNodePtr *) cache;
    misalignment = (ptruint) mem & (sizeof(DdCache) - 1);
    mem += (sizeof(DdCache) - misalignment) / sizeof(DdNodePtr);
    table->cache = cache = (DdCache *) mem;
    assert(((ptruint) table->cache & (sizeof(DdCache) - 1)) == 0);
#endif
    shift = --(table->cacheShift);
    table->memused += (slots - oldslots) * sizeof(DdCache);
    table->cacheSlack -= slots; /* need these many slots to double again */

    /* Clear new cache. */
    for (i = 0; (unsigned) i < slots; i++) {
        cache[i].data = NULL;
        cache[i].h = 0;
#ifdef DD_CACHE_PROFILE
        cache[i].count = 0;
#endif
    }

    /* Copy from old cache to new one. */
    for (i = 0; (unsigned) i < oldslots; i++) {
        old = &oldcache[i];
        if (old->data != NULL) {
            posn = ddCHash2(old->h,old->f,old->g,shift);
            entry = &cache[posn];
            entry->f = old->f;
            entry->g = old->g;
            entry->h = old->h;
            entry->data = old->data;
#ifdef DD_CACHE_PROFILE
            entry->count = 1;
#endif
            moved++;
        }
    }

    FREE(oldacache);

    /* Reinitialize measurements so as to avoid division by 0 and
    ** immediate resizing.
    */
    offset = (double) (int) (slots * table->minHit + 1);
    table->totCacheMisses += table->cacheMisses - offset;
    table->cacheMisses = offset;
    table->totCachehits += table->cacheHits;
    table->cacheHits = 0;
    table->cacheLastInserts = table->cacheinserts - (double) moved;

} /* end of cuddCacheResize */


void
cuddCacheFlush(
  DdManager * table)
{
    int i, slots;
    DdCache *cache;

    slots = table->cacheSlots;
    cache = table->cache;
    for (i = 0; i < slots; i++) {
        table->cachedeletions += cache[i].data != NULL;
        cache[i].data = NULL;
    }
    table->cacheLastInserts = table->cacheinserts;

    return;

} /* end of cuddCacheFlush */


int
cuddComputeFloorLog2(
  unsigned int value)
{
    int floorLog = 0;
#ifdef DD_DEBUG
    assert(value > 0);
#endif
    while (value > 1) {
        floorLog++;
        value >>= 1;
    }
    return(floorLog);

} /* end of cuddComputeFloorLog2 */

/*---------------------------------------------------------------------------*/
/* Definition of static functions                                            */
/*---------------------------------------------------------------------------*/

---