2 * Copyright (C) 2014, United States Government, as represented by the
3 * Administrator of the National Aeronautics and Space Administration.
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
10 * http://www.apache.org/licenses/LICENSE-2.0.
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.
18 package gov.nasa.jpf.vm;
20 // Contributed by Peter C. Dillinger and the Georgia Tech Research Corporation
22 // Portions drawn from public domain work by Bob Jenkins, May 2006
24 // Modified by Peter C. Dillinger working under Mission Critical Technologies
27 //import gov.nasa.jpf.util.LongVector;
30 * Implements StateSet based on Jenkins hashes.
32 public class JenkinsStateSet extends SerializingStateSet {
33 static final double MAX_LOAD = 0.7;
34 static final int INIT_SIZE = 65536;
39 //LongVector fingerprints;
46 public JenkinsStateSet() {
48 hashtable = new int[INIT_SIZE];
49 nextRehash = (int) (MAX_LOAD * INIT_SIZE);
51 //fingerprints = new LongVector(nextRehash / 2);
52 fingerprints = new long[nextRehash/2];
58 return lastStateId + 1;
61 public static long longLookup3Hash(int[] val) {
62 // Jenkins' LOOKUP3 hash (May 2006)
64 int b = 0xa4cb30d9 + (val.length);
68 int max = val.length - 2;
69 for (i = 0; i < max; i += 3) {
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;
80 switch (val.length - i) {
82 c += val[val.length - 2];
83 b += val[val.length - 1];
86 b += val[val.length - 1];
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);
97 return ((long)c << 32) ^ b ^ a;
102 public int add (int[] val) {
103 long hash = longLookup3Hash(val); // this is the expensive part
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!
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){
118 idx = (idx + delta) & mask;
119 assert (idx != oidx); // should never wrap around
121 assert (hashtable[idx] == 0); // should never fill up
123 if (lastStateId >= nextRehash) { // too full
126 hashtable = new int[(mask + 1) << 1];
127 mask = hashtable.length - 1;
128 nextRehash = (int) (MAX_LOAD * mask);
130 for (i = 0; i <= lastStateId; i++) {
131 //long h = fingerprints.get(i);
132 long h = fingerprints[i];
133 idx = (int)(h >> 32) & mask;
135 while (hashtable[idx] != 0) { // we know enough slots exist
136 idx = (idx + delta) & mask;
138 hashtable[idx] = i + 1; // in table, add 1
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
145 idx = (idx + delta) & mask;
148 // idx already pointing to empty slot
151 //--- only reached if state is new
154 hashtable[idx] = lastStateId + 1; // in table, add 1
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;
167 void growFingerprint (int minSize){
168 // we don't try to be fancy here
169 int newSize = fingerprints.length *2;
170 if (newSize < minSize) {
174 long[] newFingerprints = new long[newSize];
175 System.arraycopy( fingerprints, 0, newFingerprints, 0, fingerprints.length);
176 fingerprints = newFingerprints;
180 * Main for testing speed, mostly.
182 public static void main(String[] args) {
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) {
189 System.err.println("Truncating queries to " + queries);
192 int[] v = new int[vlen];
194 for (i = 0; i < vlen; i++) {
198 JenkinsStateSet set = new JenkinsStateSet();
200 long t1 = System.currentTimeMillis();
201 for (i = 0; i < adds; i++) {
204 assert set.size() == i+1;
207 for (i = 0; i < queries; i++) {
210 assert set.size() == adds;
212 long t2 = System.currentTimeMillis();
213 System.out.println("duration: " + (t2 - t1));
216 } catch (RuntimeException re) {
217 re.printStackTrace();
218 System.err.println("args: vector_length #adds #queries");