src/main/gov/nasa/jpf/vm/JenkinsStateSet.java

   1 /*
   2  * Copyright (C) 2014, United States Government, as represented by the
   3  * Administrator of the National Aeronautics and Space Administration.
   4  * All rights reserved.
   5  *
   6  * The Java Pathfinder core (jpf-core) platform is licensed under the
   7  * Apache License, Version 2.0 (the "License"); you may not use this file except
   8  * in compliance with the License. You may obtain a copy of the License at
   9  *
  10  *        http://www.apache.org/licenses/LICENSE-2.0.
  11  *
  12  * Unless required by applicable law or agreed to in writing, software
  13  * distributed under the License is distributed on an "AS IS" BASIS,
  14  * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
  15  * See the License for the specific language governing permissions and
  16  * limitations under the License.
  17  */
  18 package gov.nasa.jpf.vm;
  19 //
  20 // Contributed by Peter C. Dillinger and the Georgia Tech Research Corporation
  21 //
  22 // Portions drawn from public domain work by Bob Jenkins, May 2006
  23 //
  24 // Modified by Peter C. Dillinger working under Mission Critical Technologies
  25 //
  26
  27 //import gov.nasa.jpf.util.LongVector;
  28
  29 /**
  30  * Implements StateSet based on Jenkins hashes.
  31  */
  32 public class JenkinsStateSet extends SerializingStateSet {
  33   static final double MAX_LOAD = 0.7;
  34   static final int INIT_SIZE = 65536;
  35
  36
  37   int lastStateId = -1;
  38
  39   //LongVector fingerprints;
  40   long[] fingerprints;
  41
  42   int[] hashtable;
  43
  44   int nextRehash;
  45
  46   public JenkinsStateSet() {
  47     lastStateId = -1;
  48     hashtable = new int[INIT_SIZE];
  49     nextRehash = (int) (MAX_LOAD * INIT_SIZE);
  50
  51     //fingerprints = new LongVector(nextRehash / 2);
  52     fingerprints = new long[nextRehash/2];
  53
  54   }
  55
  56   @Override
  57   public int size () {
  58     return lastStateId + 1;
  59   }
  60
  61   public static long longLookup3Hash(int[] val) {
  62     // Jenkins' LOOKUP3 hash  (May 2006)
  63     int a = 0x510fb60d;
  64     int b = 0xa4cb30d9 + (val.length);
  65     int c = 0x9e3779b9;
  66
  67     int i;
  68     int max = val.length - 2;
  69     for (i = 0; i < max; i += 3) {
  70       a += val[i];
  71       b += val[i + 1];
  72       c += val[i + 2];
  73       a -= c;  a ^= (c << 4) ^ (c >>> 28);  c += b;
  74       b -= a;  b ^= (a << 6) ^ (a >>> 26);  a += c;
  75       c -= b;  c ^= (b << 8) ^ (b >>> 24);  b += a;
  76       a -= c;  a ^= (c << 16)^ (c >>> 16);  c += b;
  77       b -= a;  b ^= (a << 19)^ (a >>> 13);  a += c;
  78       c -= b;  c ^= (b << 4) ^ (b >>> 28);  b += a;
  79     }
  80     switch (val.length - i) {
  81     case 2:
  82       c += val[val.length - 2];
  83       b += val[val.length - 1];
  84       break;
  85     case 1:
  86       b += val[val.length - 1];
  87       break;
  88     }
  89     c ^= b; c -= (b << 14) ^ (b >>> 18);
  90     a ^= c; a -= (c << 11) ^ (c >>> 21);
  91     b ^= a; b -= (a << 25) ^ (a >>>  7);
  92     c ^= b; c -= (b << 16) ^ (b >>> 16);
  93     a ^= c; a -= (c <<  4) ^ (c >>> 28);
  94     b ^= a; b -= (a << 14) ^ (a >>> 18);
  95     c ^= b; c -= (b << 24) ^ (b >>>  8);
  96
  97     return ((long)c << 32) ^ b ^ a;
  98   }
  99
 100
 101   @Override
 102   public int add (int[] val) {
 103     long hash = longLookup3Hash(val); // this is the expensive part
 104     int i;
 105
 106     // hash table lookup & add; open-addressed, double hashing
 107     int mask = hashtable.length - 1;
 108     int idx = (int)(hash >> 32) & mask;
 109     int delta = (int)hash | 1; // must be odd!
 110     int oidx = idx;
 111
 112     while (hashtable[idx] != 0) {
 113       int id = hashtable[idx] - 1; // in table, 1 higher
 114       //if (fingerprints.get(id) == hash) {
 115       if (fingerprints[id] == hash){
 116         return id;
 117       }
 118       idx = (idx + delta) & mask;
 119       assert (idx != oidx); // should never wrap around
 120     }
 121     assert (hashtable[idx] == 0); // should never fill up
 122
 123     if (lastStateId >= nextRehash) { // too full
 124       hashtable = null;
 125       // run GC here?
 126       hashtable = new int[(mask + 1) << 1];
 127       mask = hashtable.length - 1;
 128       nextRehash = (int) (MAX_LOAD * mask);
 129
 130       for (i = 0; i <= lastStateId; i++) {
 131         //long h = fingerprints.get(i);
 132         long h = fingerprints[i];
 133         idx = (int)(h >> 32) & mask;
 134         delta = (int)h | 1;
 135         while (hashtable[idx] != 0) { // we know enough slots exist
 136           idx = (idx + delta) & mask;
 137         }
 138         hashtable[idx] = i + 1; // in table, add 1
 139       }
 140       // done with rehash; now get idx to empty slot
 141       idx = (int)(hash >> 32) & mask;
 142       delta = (int)hash | 1; // must be odd!
 143       while (hashtable[idx] != 0) { // we know enough slots exist and state is
 144                                     // new
 145         idx = (idx + delta) & mask;
 146       }
 147     } else {
 148       // idx already pointing to empty slot
 149     }
 150
 151     //--- only reached if state is new
 152
 153     lastStateId++;
 154     hashtable[idx] = lastStateId + 1; // in table, add 1
 155
 156     //fingerprints.set(lastStateId, hash);
 157     try { // this happens rarely enough to save on nominal branch instructions
 158       fingerprints[lastStateId] = hash;
 159     } catch (ArrayIndexOutOfBoundsException ix){
 160       growFingerprint(lastStateId);
 161       fingerprints[lastStateId] = hash;
 162     }
 163
 164     return lastStateId;
 165   }
 166
 167   void growFingerprint (int minSize){
 168     // we don't try to be fancy here
 169     int newSize = fingerprints.length *2;
 170     if (newSize < minSize) {
 171       newSize = minSize;
 172     }
 173
 174     long[] newFingerprints = new long[newSize];
 175     System.arraycopy( fingerprints, 0, newFingerprints, 0, fingerprints.length);
 176     fingerprints = newFingerprints;
 177   }
 178
 179   /**
 180    * Main for testing speed, mostly.
 181    */
 182   public static void main(String[] args) {
 183     try {
 184       int vlen = Integer.parseInt(args[0]);
 185       int adds = Integer.parseInt(args[1]);
 186       int queries = Integer.parseInt(args[2]);
 187       if (queries > adds) {
 188         queries = adds;
 189         System.err.println("Truncating queries to " + queries);
 190       }
 191
 192       int[] v = new int[vlen];
 193       int i;
 194       for (i = 0; i < vlen; i++) {
 195         v[i] = i - 42;
 196       }
 197
 198       JenkinsStateSet set = new JenkinsStateSet();
 199
 200       long t1 = System.currentTimeMillis();
 201       for (i = 0; i < adds; i++) {
 202         v[0] = i * 3;
 203         set.add(v);
 204         assert set.size() == i+1;
 205       }
 206
 207       for (i = 0; i < queries; i++) {
 208         v[0] = i * 3;
 209         set.add(v);
 210         assert set.size() == adds;
 211       }
 212       long t2 = System.currentTimeMillis();
 213       System.out.println("duration: " + (t2 - t1));
 214
 215
 216     } catch (RuntimeException re) {
 217       re.printStackTrace();
 218       System.err.println("args:  vector_length  #adds  #queries");
 219     }
 220   }
 221 }