[PExplicit] Correct backtracking

p-org · Apr 19, 2024 · a10f249 · a10f249
1 parent e1e1464
commit a10f249
Show file tree

Hide file tree

Showing 9 changed files with 142 additions and 98 deletions.
diff --git a/Src/PCompiler/CompilerCore/Backend/PExplicit/PExplicitCodeGenerator.cs b/Src/PCompiler/CompilerCore/Backend/PExplicit/PExplicitCodeGenerator.cs
@@ -344,6 +344,18 @@ private void WriteMachineFields(CompilationContext context, StringWriter output,
             context.WriteLine(output, "}");
             context.WriteLine(output);
 
+            context.WriteLine(output, "@Generated");
+            context.WriteLine(output, "@Override");
+            context.WriteLine(output, "public List<Object> copyLocalVarValues() {");
+            context.WriteLine(output, "    List<Object> result = super.copyLocalVarValues();");
+            foreach (var field in machine.Fields)
+            {
+                context.WriteLine(output, $"    result.add({CompilationContext.GetVar(field.Name)});");
+            }
+            context.WriteLine(output, "    return result;");
+            context.WriteLine(output, "}");
+            context.WriteLine(output);
+
             context.WriteLine(output, "@Generated");
             context.WriteLine(output, "@Override");
             context.WriteLine(output, "protected int setLocalVarValues(List<Object> values) {");

diff --git a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/RuntimeExecutor.java b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/RuntimeExecutor.java
@@ -94,7 +94,7 @@ private static void process(boolean resume) throws Exception {
             throw new Exception("MEMOUT", e);
         } catch (BugFoundException e) {
             PExplicitGlobal.setStatus(STATUS.BUG_FOUND);
-            PExplicitGlobal.setResult(String.format("found cex of length %d", scheduler.currentStep.getStepNumber()));
+            PExplicitGlobal.setResult(String.format("found cex of length %d", scheduler.getStepState().getStepNumber()));
             PExplicitLogger.logStackTrace(e);
 
             ReplayScheduler replayer = new ReplayScheduler(scheduler.schedule);

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
@@ -171,6 +171,30 @@ public List<Object> getLocalVarValues() {
 
         result.add(currentState);
 
+        result.add(sendBuffer.getElements());
+        result.add(deferQueue.getElements());
+
+        result.add(started);
+        result.add(halted);
+
+        result.add(blockedBy);
+        result.add(blockedStateExit);
+        result.add(blockedNewStateEntry);
+        result.add(blockedNewStateEntryPayload);
+
+        return result;
+    }
+
+    /**
+     * Copy values of local variables as an ordered list
+     *
+     * @return List of values
+     */
+    public List<Object> copyLocalVarValues() {
+        List<Object> result = new ArrayList<>();
+
+        result.add(currentState);
+
         result.add(new ArrayList<>(sendBuffer.getElements()));
         result.add(new ArrayList<>(deferQueue.getElements()));
 
@@ -210,8 +234,8 @@ protected int setLocalVarValues(List<Object> values) {
         return idx;
     }
 
-    public MachineState getMachineState() {
-        return new MachineState(getLocalVarValues());
+    public MachineState copyMachineState() {
+        return new MachineState(copyLocalVarValues());
     }
 
     public void setMachineState(MachineState input) {

diff --git a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/Choice.java b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/Choice.java
@@ -32,28 +32,6 @@ public class Choice implements Serializable {
     public Choice() {
     }
 
-    /**
-     * Copy-constructor for Choice
-     *
-     * @param old The choice to copy
-     */
-    private Choice(Choice old) {
-        currentScheduleChoice = old.currentScheduleChoice;
-        currentDataChoice = old.currentDataChoice;
-        unexploredScheduleChoices = new ArrayList<>(old.unexploredScheduleChoices);
-        unexploredDataChoices = new ArrayList<>(old.unexploredDataChoices);
-        choiceStep = old.choiceStep;
-    }
-
-    /**
-     * Copy the Choice
-     *
-     * @return A new cloned copy of the Choice
-     */
-    public Choice getCopy() {
-        return new Choice(this);
-    }
-
     /**
      * Check if this choice has an unexplored choice remaining.
      *

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
@@ -21,6 +21,13 @@ public class Schedule implements Serializable {
     @Setter
     private List<Choice> choices = new ArrayList<>();
 
+    /**
+     * Step state at the start of a scheduler step.
+     * Used in stateful backtracking
+     */
+    @Setter
+    private StepState stepBeginState = null;
+
     /**
      * Constructor
      */
@@ -140,9 +147,9 @@ public void setUnexploredScheduleChoices(List<PMachine> machines, int idx) {
         choices.get(idx).setUnexploredScheduleChoices(machines);
         if (PExplicitGlobal.getConfig().isBacktrackingEnabled()
                 && !machines.isEmpty()
-                && PExplicitGlobal.getScheduler().currentStep != null
-                && PExplicitGlobal.getScheduler().currentStep.getStepNumber() != 0) {
-            choices.get(idx).setChoiceStep(PExplicitGlobal.getScheduler().currentStep.copy());
+                && stepBeginState != null
+                && stepBeginState.getStepNumber() != 0) {
+            choices.get(idx).setChoiceStep(stepBeginState.copy());
         }
     }
 
@@ -159,9 +166,9 @@ public void setUnexploredDataChoices(List<PValue<?>> values, int idx) {
         choices.get(idx).setUnexploredDataChoices(values);
         if (PExplicitGlobal.getConfig().isBacktrackingEnabled()
                 && !values.isEmpty()
-                && PExplicitGlobal.getScheduler().currentStep != null
-                && PExplicitGlobal.getScheduler().currentStep.getStepNumber() != 0) {
-            choices.get(idx).setChoiceStep(PExplicitGlobal.getScheduler().currentStep.copy());
+                && stepBeginState != null
+                && stepBeginState.getStepNumber() != 0) {
+            choices.get(idx).setChoiceStep(stepBeginState.copy());
         }
     }
 

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
@@ -25,7 +25,8 @@ public abstract class Scheduler implements SchedulerInterface {
     /**
      * Current step state
      */
-    public StepState currentStep = new StepState();
+    @Getter
+    protected StepState stepState = new StepState();
 
     /**
      * Current schedule
@@ -205,7 +206,7 @@ public void startMachine(PMachine machine) {
         }
 
         // add machine to schedule
-        currentStep.makeMachine(machine);
+        stepState.makeMachine(machine);
 
         // run create machine event
         processCreateEvent(new PMessage(PEvent.createMachine, machine, null));
@@ -222,20 +223,20 @@ public void executeStep(PMachine sender) {
 
         if (!msg.getEvent().isCreateMachineEvent()) {
             // update step number
-            currentStep.setStepNumber(currentStep.getStepNumber() + 1);
+            stepState.setStepNumber(stepState.getStepNumber() + 1);
         }
 
         // reset number of logs in current step
         stepNumLogs = 0;
 
         // log start step
-        PExplicitLogger.logStartStep(currentStep.getStepNumber(), sender, msg);
+        PExplicitLogger.logStartStep(stepState.getStepNumber(), sender, msg);
 
         // process message
         processDequeueEvent(sender, msg);
 
         // update done stepping flag
-        isDoneStepping = (currentStep.getStepNumber() >= PExplicitGlobal.getConfig().getMaxStepBound());
+        isDoneStepping = (stepState.getStepNumber() >= PExplicitGlobal.getConfig().getMaxStepBound());
     }
 
     /**
@@ -249,7 +250,7 @@ public PMachine allocateMachine(
             Class<? extends PMachine> machineType,
             Function<Integer, ? extends PMachine> constructor) {
         // get machine count for given type from schedule
-        int machineCount = currentStep.getMachineCount(machineType);
+        int machineCount = stepState.getMachineCount(machineType);
 
         PMachine machine = PExplicitGlobal.getGlobalMachine(machineType, machineCount);
         if (machine == null) {
@@ -259,7 +260,7 @@ public PMachine allocateMachine(
         }
 
         // add machine to schedule
-        currentStep.makeMachine(machine);
+        stepState.makeMachine(machine);
         return machine;
     }
 
@@ -324,7 +325,7 @@ public void announce(PEvent event, PValue<?> payload) {
      * Check for deadlock at the end of a completed schedule
      */
     public void checkDeadlock() {
-        for (PMachine machine: currentStep.getMachineSet()) {
+        for (PMachine machine: stepState.getMachineSet()) {
             if (machine.canRun() && machine.isBlocked()) {
                 throw new DeadlockException(String.format("Deadlock detected. %s is waiting to receive an event, but no other controlled tasks are enabled.", machine));
             }