[PExplicit] Improve state caching

Adds storing hashcode and string representation during PValue initialization Adds new state caching modes using hash functions from guava library New state caching modes include: hashcode (java built in, 32-bit), siphash24 (64-bit), murmur3_128 (128-bit, default), sha256 (256-bit), or exact (using exact string representation)
p-org · Apr 23, 2024 · 242fc6e · 242fc6e
1 parent e290af6
commit 242fc6e
Show file tree

Hide file tree

Showing 27 changed files with 304 additions and 195 deletions.
diff --git a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/PExplicit.java b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/PExplicit.java
@@ -12,6 +12,7 @@
 import pexplicit.utils.monitor.MemoryMonitor;
 import pexplicit.utils.monitor.TimeMonitor;
 import pexplicit.utils.random.RandomNumberGenerator;
+import pexplicit.values.ComputeHash;
 
 import java.lang.reflect.InvocationTargetException;
 import java.util.Optional;
@@ -32,6 +33,7 @@ public static void main(String[] args) {
         // parse the commandline arguments to create the configuration
         PExplicitGlobal.setConfig(PExplicitOptions.ParseCommandlineArgs(args));
         PExplicitLogger.Initialize(PExplicitGlobal.getConfig().getVerbosity());
+        ComputeHash.Initialize();
 
         // get reflections corresponding to the model
         Reflections reflections = new Reflections("pexplicit.model");

diff --git a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/commandline/PExplicitConfig.java b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/commandline/PExplicitConfig.java
@@ -55,7 +55,7 @@ public class PExplicitConfig {
     BufferSemantics bufferSemantics = BufferSemantics.SenderQueue;
     // state caching mode
     @Setter
-    StateCachingMode stateCachingMode = StateCachingMode.Fingerprint;
+    StateCachingMode stateCachingMode = StateCachingMode.Murmur3_128;
     // use stateful backtracking
     @Setter
     boolean statefulBacktrackEnabled = true;

diff --git a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/commandline/PExplicitOptions.java b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/commandline/PExplicitOptions.java
@@ -155,7 +155,7 @@ public class PExplicitOptions {
         Option stateCachingMode =
                 Option.builder()
                         .longOpt("state-caching")
-                        .desc("State caching mode: none, fingerprint, exact (default: fingerprint)")
+                        .desc("State caching mode: none, hashcode, siphash24, murmur3_128, sha256, exact (default: murmur3_128)")
                         .numberOfArgs(1)
                         .hasArg()
                         .argName("Caching Mode (string)")
@@ -312,8 +312,17 @@ public static PExplicitConfig ParseCommandlineArgs(String[] args) {
                         case "none":
                             config.setStateCachingMode(StateCachingMode.None);
                             break;
-                        case "fingerprint":
-                            config.setStateCachingMode(StateCachingMode.Fingerprint);
+                        case "hashcode":
+                            config.setStateCachingMode(StateCachingMode.HashCode);
+                            break;
+                        case "siphash24":
+                            config.setStateCachingMode(StateCachingMode.SipHash24);
+                            break;
+                        case "murmur3_128":
+                            config.setStateCachingMode(StateCachingMode.Murmur3_128);
+                            break;
+                        case "sha256":
+                            config.setStateCachingMode(StateCachingMode.Sha256);
                             break;
                         case "exact":
                             config.setStateCachingMode(StateCachingMode.Exact);

diff --git a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/logger/PExplicitLogger.java b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/logger/PExplicitLogger.java
@@ -12,13 +12,13 @@
 import pexplicit.runtime.machine.PMonitor;
 import pexplicit.runtime.machine.State;
 import pexplicit.runtime.machine.events.PContinuation;
-import pexplicit.runtime.machine.events.PMessage;
 import pexplicit.runtime.scheduler.explicit.ExplicitSearchScheduler;
 import pexplicit.runtime.scheduler.explicit.SearchStatistics;
 import pexplicit.runtime.scheduler.explicit.StateCachingMode;
 import pexplicit.runtime.scheduler.replay.ReplayScheduler;
 import pexplicit.utils.monitor.MemoryMonitor;
 import pexplicit.values.PEvent;
+import pexplicit.values.PMessage;
 import pexplicit.values.PValue;
 
 import java.io.PrintWriter;

diff --git a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/logger/TraceLogger.java b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/logger/TraceLogger.java
@@ -12,7 +12,7 @@
 import org.apache.logging.log4j.core.config.Configurator;
 import org.apache.logging.log4j.core.layout.PatternLayout;
 import pexplicit.runtime.machine.PMachine;
-import pexplicit.runtime.machine.events.PMessage;
+import pexplicit.values.PMessage;
 
 import java.io.File;
 import java.io.FileOutputStream;

diff --git a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/machine/PMachine.java b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/machine/PMachine.java
@@ -7,13 +7,13 @@
 import pexplicit.runtime.machine.buffer.SenderQueue;
 import pexplicit.runtime.machine.eventhandlers.EventHandler;
 import pexplicit.runtime.machine.events.PContinuation;
-import pexplicit.runtime.machine.events.PMessage;
 import pexplicit.utils.exceptions.BugFoundException;
 import pexplicit.utils.misc.Assert;
 import pexplicit.utils.serialize.SerializableBiFunction;
 import pexplicit.utils.serialize.SerializableRunnable;
 import pexplicit.values.PEvent;
 import pexplicit.values.PMachineValue;
+import pexplicit.values.PMessage;
 import pexplicit.values.PValue;
 
 import java.io.Serializable;

diff --git a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/machine/State.java b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/machine/State.java
@@ -3,10 +3,10 @@
 import pexplicit.runtime.machine.eventhandlers.DeferEventHandler;
 import pexplicit.runtime.machine.eventhandlers.EventHandler;
 import pexplicit.runtime.machine.eventhandlers.IgnoreEventHandler;
-import pexplicit.runtime.machine.events.PMessage;
 import pexplicit.runtime.machine.events.StateEvents;
 import pexplicit.utils.misc.Assert;
 import pexplicit.values.PEvent;
+import pexplicit.values.PMessage;
 import pexplicit.values.PValue;
 
 import java.io.Serializable;

diff --git a/...untimes/PExplicitRuntime/src/main/java/pexplicit/runtime/machine/buffer/MessageQueue.java b/...untimes/PExplicitRuntime/src/main/java/pexplicit/runtime/machine/buffer/MessageQueue.java
@@ -2,8 +2,8 @@
 
 import lombok.Getter;
 import pexplicit.runtime.machine.PMachine;
-import pexplicit.runtime.machine.events.PMessage;
 import pexplicit.utils.misc.Assert;
+import pexplicit.values.PMessage;
 
 import java.io.Serializable;
 import java.util.ArrayList;

diff --git a/...ntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/machine/events/PContinuation.java b/...ntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/machine/events/PContinuation.java
@@ -6,6 +6,7 @@
 import pexplicit.utils.serialize.SerializableBiFunction;
 import pexplicit.utils.serialize.SerializableRunnable;
 import pexplicit.values.PEvent;
+import pexplicit.values.PMessage;
 
 import java.util.HashSet;
 import java.util.Set;

diff --git a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/Scheduler.java b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/Scheduler.java
@@ -6,7 +6,6 @@
 import pexplicit.runtime.logger.PExplicitLogger;
 import pexplicit.runtime.machine.PMachine;
 import pexplicit.runtime.machine.PMonitor;
-import pexplicit.runtime.machine.events.PMessage;
 import pexplicit.runtime.scheduler.explicit.StepState;
 import pexplicit.utils.exceptions.DeadlockException;
 import pexplicit.utils.exceptions.LivenessException;
@@ -44,6 +43,10 @@ public abstract class Scheduler implements SchedulerInterface {
     @Getter
     @Setter
     protected transient int stepNumLogs = 0;
+    /**
+     * Whether last step was a sticky step (i.e., createMachine step)
+     */
+    protected boolean isStickyStep = true;
 
     /**
      * Constructor
@@ -85,6 +88,7 @@ protected Scheduler() {
      * Reset the scheduler.
      */
     protected void reset() {
+        isStickyStep = true;
     }
 
     /**
@@ -219,7 +223,8 @@ public void executeStep(PMachine sender) {
         // pop message from sender queue
         PMessage msg = sender.getSendBuffer().remove();
 
-        if (!msg.getEvent().isCreateMachineEvent()) {
+        isStickyStep = msg.getEvent().isCreateMachineEvent();
+        if (!isStickyStep) {
             // update step number
             stepState.setStepNumber(stepState.getStepNumber() + 1);
         }

diff --git a/...itRuntime/src/main/java/pexplicit/runtime/scheduler/explicit/ExplicitSearchScheduler.java b/...itRuntime/src/main/java/pexplicit/runtime/scheduler/explicit/ExplicitSearchScheduler.java
@@ -1,5 +1,6 @@
 package pexplicit.runtime.scheduler.explicit;
 
+import com.google.common.hash.Hashing;
 import lombok.Getter;
 import lombok.Setter;
 import org.apache.commons.lang3.StringUtils;
@@ -11,6 +12,7 @@
 import pexplicit.runtime.machine.PMachine;
 import pexplicit.runtime.scheduler.Choice;
 import pexplicit.runtime.scheduler.Scheduler;
+import pexplicit.utils.exceptions.PExplicitRuntimeException;
 import pexplicit.utils.misc.Assert;
 import pexplicit.utils.monitor.MemoryMonitor;
 import pexplicit.utils.monitor.TimeMonitor;
@@ -181,7 +183,7 @@ protected void runStep() throws TimeoutException {
     boolean skipRemainingSchedule() {
         if (PExplicitGlobal.getConfig().getStateCachingMode() != StateCachingMode.None) {
             // perform state caching only if beyond backtrack choice number
-            if (stepState.getChoiceNumber() > backtrackChoiceNumber) {
+            if (!isStickyStep && stepState.getChoiceNumber() > backtrackChoiceNumber) {
                 // increment state count
                 SearchStatistics.totalStates++;
 
@@ -223,18 +225,16 @@ boolean skipRemainingSchedule() {
      * @return
      */
     Object getCurrentStateKey() {
-        Object stateKey = null;
-        if (PExplicitGlobal.getConfig().getStateCachingMode() == StateCachingMode.Fingerprint) {
-            // use fingerprinting by hashing values from each machine vars
-            int fingerprint = ComputeHash.getHashCode(stepState.getMachineSet());
-            stateKey = fingerprint;
-        } else {
-            // use exact values from each machine vars
-            List<List<Object>> machineValues = new ArrayList<>();
-            for (PMachine machine : stepState.getMachineSet()) {
-                machineValues.add(machine.getLocalVarValues());
-            }
-            stateKey = machineValues;
+        Object stateKey;
+        switch (PExplicitGlobal.getConfig().getStateCachingMode()) {
+            case HashCode -> stateKey = ComputeHash.getHashCode(stepState.getMachineSet());
+            case SipHash24 -> stateKey = ComputeHash.getHashCode(stepState.getMachineSet(), Hashing.sipHash24());
+            case Murmur3_128 ->
+                    stateKey = ComputeHash.getHashCode(stepState.getMachineSet(), Hashing.murmur3_128((int) PExplicitGlobal.getConfig().getRandomSeed()));
+            case Sha256 -> stateKey = ComputeHash.getHashCode(stepState.getMachineSet(), Hashing.sha256());
+            case Exact -> stateKey = ComputeHash.getExactString(stepState.getMachineSet());
+            default ->
+                    throw new PExplicitRuntimeException(String.format("Unexpected state caching mode: %s", PExplicitGlobal.getConfig().getStateCachingMode()));
         }
         return stateKey;
     }
@@ -376,6 +376,7 @@ private void postIterationCleanup() {
                 }
                 PExplicitLogger.logBacktrack(cIdx, newStepNumber);
                 if (newStepNumber == 0) {
+                    reset();
                     stepState.resetToZero();
                 } else {
                     stepState.setTo(choice.getChoiceStep());

diff --git a/...PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/explicit/StateCachingMode.java b/...PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/explicit/StateCachingMode.java
@@ -2,6 +2,9 @@
 
 public enum StateCachingMode {
     None,
-    Fingerprint,
+    HashCode,
+    SipHash24,
+    Murmur3_128,
+    Sha256,
     Exact
 }
diff --git a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/values/ComputeHash.java b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/values/ComputeHash.java
@@ -1,7 +1,10 @@
 package pexplicit.values;
 
+import com.google.common.hash.HashCode;
+import com.google.common.hash.HashFunction;
 import pexplicit.runtime.machine.PMachine;
 
+import java.nio.charset.StandardCharsets;
 import java.util.Collection;
 import java.util.List;
 import java.util.Objects;
@@ -11,6 +14,9 @@
  * Static class to compute hash values
  */
 public class ComputeHash {
+    public static void Initialize() {
+    }
+
 
     /**
      * Compute hash value for a collection of PValues.
@@ -47,7 +53,10 @@ public static int getHashCode(PMachine machine, PValue<?>... values) {
     }
 
     /**
-     * Compute hash value for a PMachine local variables.
+     * Get the hash code of the protocol state using Java inbuilt hashCode() function.
+     *
+     * @param machines Sorted set of protocol machines
+     * @return Integer representing hash code corresponding to the protocol state
      */
     public static int getHashCode(SortedSet<PMachine> machines) {
         int hashValue = 0x802CBBDB;
@@ -59,4 +68,33 @@ public static int getHashCode(SortedSet<PMachine> machines) {
         }
         return hashValue;
     }
+
+    /**
+     * Get the hash code of the protocol state given a hash function.
+     *
+     * @param machines     Sorted set of protocol machines
+     * @param hashFunction Hash function to hash with
+     * @return HashCode representing protocol state hashed by the given hash function
+     */
+    public static HashCode getHashCode(SortedSet<PMachine> machines, HashFunction hashFunction) {
+        return hashFunction.hashString(getExactString(machines), StandardCharsets.UTF_8);
+    }
+
+    /**
+     * Get the exact protocol state as a string.
+     *
+     * @param machines Sorted set of protocol machines
+     * @return String representing the exact protocol state
+     */
+    public static String getExactString(SortedSet<PMachine> machines) {
+        StringBuilder sb = new StringBuilder();
+        for (PMachine machine : machines) {
+            sb.append(machine);
+            for (Object value : machine.getLocalVarValues()) {
+                sb.append(value);
+            }
+        }
+        return sb.toString();
+    }
+
 }
diff --git a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/values/PBool.java b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/values/PBool.java
@@ -16,6 +16,7 @@ public class PBool extends PValue<PBool> {
      */
     public PBool(boolean val) {
         value = val;
+        setRep();
     }
 
     /**
@@ -26,6 +27,7 @@ public PBool(boolean val) {
     public PBool(Object val) {
         if (val instanceof PBool) value = ((PBool) val).value;
         else value = (boolean) val;
+        setRep();
     }
 
     /**
@@ -35,6 +37,7 @@ public PBool(Object val) {
      */
     public PBool(PBool val) {
         value = val.value;
+        setRep();
     }
 
     /**
@@ -90,8 +93,13 @@ public PBool clone() {
     }
 
     @Override
-    public int hashCode() {
-        return Boolean.valueOf(value).hashCode();
+    protected void setHashCode() {
+        hashCode = Boolean.valueOf(value).hashCode();
+    }
+
+    @Override
+    protected void setStringRep() {
+        stringRep = Boolean.toString(value);
     }
 
     @Override
@@ -102,9 +110,4 @@ else if (!(obj instanceof PBool)) {
         }
         return this.value == ((PBool) obj).value;
     }
-
-    @Override
-    public String toString() {
-        return Boolean.toString(value);
-    }
 }
diff --git a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/values/PEnum.java b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/values/PEnum.java
@@ -21,6 +21,7 @@ public PEnum(String type, String name, int val) {
         this.type = type;
         this.name = name;
         this.value = val;
+        setRep();
     }
 
     /**
@@ -32,6 +33,7 @@ public PEnum(PEnum val) {
         type = val.type;
         name = val.name;
         value = val.value;
+        setRep();
     }
 
     /**
@@ -49,8 +51,13 @@ public PEnum clone() {
     }
 
     @Override
-    public int hashCode() {
-        return Long.hashCode(value);
+    protected void setHashCode() {
+        hashCode = Long.hashCode(value);
+    }
+
+    @Override
+    protected void setStringRep() {
+        stringRep = name;
     }
 
     @Override
@@ -61,9 +68,4 @@ else if (!(obj instanceof PEnum)) {
         }
         return this.value == ((PEnum) obj).value;
     }
-
-    @Override
-    public String toString() {
-        return name;
-    }
 }