[PEx] Adds modes for stateful backtracking

Adds CLI option --stateful-backtrack none|intra-task|all to limit stateful backtracking to OFF|within-a-task|ON
p-org · Jul 15, 2024 · 9d7199f · 9d7199f
1 parent c150243
commit 9d7199f
Show file tree

Hide file tree

Showing 9 changed files with 51 additions and 17 deletions.
diff --git a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/commandline/PExplicitConfig.java b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/commandline/PExplicitConfig.java
@@ -4,6 +4,7 @@
 import lombok.Setter;
 import pexplicit.runtime.machine.buffer.BufferSemantics;
 import pexplicit.runtime.scheduler.explicit.StateCachingMode;
+import pexplicit.runtime.scheduler.explicit.StatefulBacktrackingMode;
 import pexplicit.runtime.scheduler.explicit.strategy.SearchStrategyMode;
 
 /**
@@ -52,9 +53,9 @@ public class PExplicitConfig {
     // state caching mode
     @Setter
     StateCachingMode stateCachingMode = StateCachingMode.Murmur3_128;
-    // use stateful backtracking
+    // stateful backtracking mode
     @Setter
-    boolean statefulBacktrackEnabled = true;
+    StatefulBacktrackingMode statefulBacktrackingMode = StatefulBacktrackingMode.IntraTask;
     // search strategy mode
     @Setter
     SearchStrategyMode searchStrategyMode = SearchStrategyMode.Random;

diff --git a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/commandline/PExplicitOptions.java b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/commandline/PExplicitOptions.java
@@ -2,6 +2,7 @@
 
 import org.apache.commons.cli.*;
 import pexplicit.runtime.scheduler.explicit.StateCachingMode;
+import pexplicit.runtime.scheduler.explicit.StatefulBacktrackingMode;
 import pexplicit.runtime.scheduler.explicit.strategy.SearchStrategyMode;
 
 import java.io.PrintWriter;
@@ -165,13 +166,15 @@ public class PExplicitOptions {
         addHiddenOption(stateCachingMode);
 
         // whether or not to disable stateful backtracking
-        Option backtrack =
+        Option backtrackMode =
                 Option.builder()
-                        .longOpt("no-backtrack")
-                        .desc("Disable stateful backtracking")
-                        .numberOfArgs(0)
+                        .longOpt("stateful-backtrack")
+                        .desc("Stateful backtracking mode: none, intra-task, all (default: intra-task)")
+                        .numberOfArgs(1)
+                        .hasArg()
+                        .argName("Backtrack Mode (string)")
                         .build();
-        addHiddenOption(backtrack);
+        addHiddenOption(backtrackMode);
 
         // max number of schedules to explore per search task
         Option maxSchedulesPerTask =
@@ -363,8 +366,22 @@ public static PExplicitConfig ParseCommandlineArgs(String[] args) {
                                     String.format("Unrecognized state caching mode, got %s", option.getValue()));
                     }
                     break;
-                case "no-backtrack":
-                    config.setStatefulBacktrackEnabled(false);
+                case "stateful-backtrack":
+                    switch (option.getValue()) {
+                        case "none":
+                            config.setStatefulBacktrackingMode(StatefulBacktrackingMode.None);
+                            break;
+                        case "intra-task":
+                            config.setStatefulBacktrackingMode(StatefulBacktrackingMode.IntraTask);
+                            break;
+                        case "all":
+                            config.setStatefulBacktrackingMode(StatefulBacktrackingMode.All);
+                            break;
+                        default:
+                            optionError(
+                                    option,
+                                    String.format("Unrecognized stateful backtrack mode, got %s", option.getValue()));
+                    }
                     break;
                 case "schedules-per-task":
                     try {

diff --git a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/Schedule.java b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/Schedule.java
@@ -7,6 +7,7 @@
 import pexplicit.runtime.scheduler.choice.Choice;
 import pexplicit.runtime.scheduler.choice.DataChoice;
 import pexplicit.runtime.scheduler.choice.ScheduleChoice;
+import pexplicit.runtime.scheduler.explicit.StatefulBacktrackingMode;
 import pexplicit.runtime.scheduler.explicit.StepState;
 import pexplicit.values.PValue;
 
@@ -71,7 +72,7 @@ public void setScheduleChoice(int stepNum, int choiceNum, PMachineId current) {
             choices.add(null);
         }
         assert (choiceNum < choices.size());
-        if (PExplicitGlobal.getConfig().isStatefulBacktrackEnabled()
+        if (PExplicitGlobal.getConfig().getStatefulBacktrackingMode() != StatefulBacktrackingMode.None
                 && stepNum != 0) {
             assert (stepBeginState != null);
             choices.set(choiceNum, new ScheduleChoice(stepNum, choiceNum, current, stepBeginState));

diff --git a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/choice/Choice.java b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/choice/Choice.java
@@ -29,7 +29,7 @@ public void clearCurrent() {
      *
      * @return Choice object with the copied current choice
      */
-    abstract public Choice copyCurrent();
+    abstract public Choice copyCurrent(boolean copyState);
 
     abstract public String toString();
 }
diff --git a/...untimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/choice/DataChoice.java b/...untimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/choice/DataChoice.java
@@ -14,7 +14,7 @@ public DataChoice(PValue<?> c) {
         super(c);
     }
 
-    public Choice copyCurrent() {
+    public Choice copyCurrent(boolean copyState) {
         return new DataChoice(this.current);
     }
 

diff --git a/...mes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/choice/ScheduleChoice.java b/...mes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/choice/ScheduleChoice.java
@@ -2,6 +2,7 @@
 
 import lombok.Getter;
 import lombok.Setter;
+import pexplicit.commandline.PExplicitConfig;
 import pexplicit.runtime.machine.PMachineId;
 import pexplicit.runtime.scheduler.explicit.StepState;
 
@@ -32,8 +33,12 @@ public ScheduleChoice(int stepNum, int choiceNum, PMachineId c, StepState s) {
         this.choiceState = s;
     }
 
-    public Choice copyCurrent() {
-        return new ScheduleChoice(this.stepNumber, this.choiceNumber, this.current, this.choiceState);
+    public Choice copyCurrent(boolean copyState) {
+        if (copyState) {
+            return new ScheduleChoice(this.stepNumber, this.choiceNumber, this.current, this.choiceState);
+        } else {
+            return new ScheduleChoice(this.stepNumber, this.choiceNumber, this.current, null);
+        }
     }
 
     @Override

diff --git a/...itRuntime/src/main/java/pexplicit/runtime/scheduler/explicit/ExplicitSearchScheduler.java b/...itRuntime/src/main/java/pexplicit/runtime/scheduler/explicit/ExplicitSearchScheduler.java
@@ -193,7 +193,7 @@ protected void runStep() throws TimeoutException {
             return;
         }
 
-        if (PExplicitGlobal.getConfig().isStatefulBacktrackEnabled()
+        if (PExplicitGlobal.getConfig().getStatefulBacktrackingMode() != StatefulBacktrackingMode.None
                 && stepNumber != 0) {
             schedule.setStepBeginState(stepState.copyState());
         }
@@ -528,7 +528,7 @@ private void postIterationCleanup() {
             backtrackChoiceNumber = cIdx;
             int newStepNumber = 0;
             ScheduleChoice scheduleChoice = null;
-            if (PExplicitGlobal.getConfig().isStatefulBacktrackEnabled()) {
+            if (PExplicitGlobal.getConfig().getStatefulBacktrackingMode() != StatefulBacktrackingMode.None) {
                 scheduleChoice = schedule.getScheduleChoiceAt(cIdx);
                 if (scheduleChoice != null && scheduleChoice.getChoiceState() != null) {
                     newStepNumber = scheduleChoice.getStepNumber();

diff --git a/...tRuntime/src/main/java/pexplicit/runtime/scheduler/explicit/StatefulBacktrackingMode.java b/...tRuntime/src/main/java/pexplicit/runtime/scheduler/explicit/StatefulBacktrackingMode.java
@@ -0,0 +1,7 @@
+package pexplicit.runtime.scheduler.explicit;
+
+public enum StatefulBacktrackingMode {
+    None,
+    IntraTask,
+    All
+}
diff --git a/...plicitRuntime/src/main/java/pexplicit/runtime/scheduler/explicit/strategy/SearchTask.java b/...plicitRuntime/src/main/java/pexplicit/runtime/scheduler/explicit/strategy/SearchTask.java
@@ -1,8 +1,10 @@
 package pexplicit.runtime.scheduler.explicit.strategy;
 
 import lombok.Getter;
+import pexplicit.runtime.PExplicitGlobal;
 import pexplicit.runtime.machine.PMachineId;
 import pexplicit.runtime.scheduler.choice.*;
+import pexplicit.runtime.scheduler.explicit.StatefulBacktrackingMode;
 import pexplicit.values.PValue;
 
 import java.io.Serializable;
@@ -41,7 +43,8 @@ public void cleanup() {
     }
 
     public void addPrefixChoice(Choice choice) {
-        prefixChoices.add(choice.copyCurrent());
+        boolean copyState = (PExplicitGlobal.getConfig().getStatefulBacktrackingMode() == StatefulBacktrackingMode.All);
+        prefixChoices.add(choice.copyCurrent(copyState));
     }
 
     public void addSuffixSearchUnit(int choiceNum, SearchUnit unit) {