[PEx] Add first version of RL-based choice selection

p-org · Aug 7, 2024 · 0174966 · 0174966
1 parent ad40c1c
commit 0174966
Show file tree

Hide file tree

Showing 17 changed files with 560 additions and 13 deletions.
diff --git a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/PExplicit.java b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/PExplicit.java
@@ -32,6 +32,7 @@ public static void main(String[] args) {
 
         // parse the commandline arguments to create the configuration
         PExplicitGlobal.setConfig(PExplicitOptions.ParseCommandlineArgs(args));
+        PExplicitGlobal.setChoiceSelector();
         PExplicitLogger.Initialize(PExplicitGlobal.getConfig().getVerbosity());
         ComputeHash.Initialize();
 

diff --git a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/commandline/PExplicitConfig.java b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/commandline/PExplicitConfig.java
@@ -5,6 +5,7 @@
 import pexplicit.runtime.machine.buffer.BufferSemantics;
 import pexplicit.runtime.scheduler.explicit.StateCachingMode;
 import pexplicit.runtime.scheduler.explicit.StatefulBacktrackingMode;
+import pexplicit.runtime.scheduler.explicit.choiceselector.ChoiceSelectorMode;
 import pexplicit.runtime.scheduler.explicit.strategy.SearchStrategyMode;
 
 /**
@@ -62,6 +63,9 @@ public class PExplicitConfig {
     // search strategy mode
     @Setter
     SearchStrategyMode searchStrategyMode = SearchStrategyMode.Random;
+    // choice selector mode
+    @Setter
+    ChoiceSelectorMode choiceSelectorMode = ChoiceSelectorMode.Random;
     // max number of schedules per search task
     @Setter
     int maxSchedulesPerTask = 500;

diff --git a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/commandline/PExplicitOptions.java b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/commandline/PExplicitOptions.java
@@ -3,6 +3,7 @@
 import org.apache.commons.cli.*;
 import pexplicit.runtime.scheduler.explicit.StateCachingMode;
 import pexplicit.runtime.scheduler.explicit.StatefulBacktrackingMode;
+import pexplicit.runtime.scheduler.explicit.choiceselector.ChoiceSelectorMode;
 import pexplicit.runtime.scheduler.explicit.strategy.SearchStrategyMode;
 
 import java.io.PrintWriter;
@@ -214,6 +215,17 @@ public class PExplicitOptions {
                         .build();
         addHiddenOption(maxChildrenPerTask);
 
+        // choice selection mode
+        Option choiceSelect =
+                Option.builder("cs")
+                        .longOpt("choice-selection")
+                        .desc("Choice selection mode: random, ql (default: random)")
+                        .numberOfArgs(1)
+                        .hasArg()
+                        .argName("Mode (string)")
+                        .build();
+        addOption(choiceSelect);
+
         /*
          * Help menu options
          */
@@ -420,6 +432,21 @@ public static PExplicitConfig ParseCommandlineArgs(String[] args) {
                                 option, String.format("Expected an integer value, got %s", option.getValue()));
                     }
                     break;
+                case "cs":
+                case "choice-selection":
+                    switch (option.getValue()) {
+                        case "random":
+                            config.setChoiceSelectorMode(ChoiceSelectorMode.Random);
+                            break;
+                        case "ql":
+                            config.setChoiceSelectorMode(ChoiceSelectorMode.QL);
+                            break;
+                        default:
+                            optionError(
+                                    option,
+                                    String.format("Unrecognized choice selection mode, got %s", option.getValue()));
+                    }
+                    break;
                 case "h":
                 case "help":
                     formatter.printHelp(

diff --git a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/PExplicitGlobal.java b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/PExplicitGlobal.java
@@ -6,6 +6,9 @@
 import pexplicit.runtime.machine.PMachine;
 import pexplicit.runtime.machine.PMachineId;
 import pexplicit.runtime.scheduler.Scheduler;
+import pexplicit.runtime.scheduler.explicit.choiceselector.ChoiceSelector;
+import pexplicit.runtime.scheduler.explicit.choiceselector.ChoiceSelectorQL;
+import pexplicit.runtime.scheduler.explicit.choiceselector.ChoiceSelectorRandom;
 import pexplicit.runtime.scheduler.explicit.strategy.SearchStrategyMode;
 
 import java.util.*;
@@ -57,6 +60,11 @@ public class PExplicitGlobal {
     @Getter
     @Setter
     private static String result = "error";
+    /**
+     * Choice orchestrator
+     */
+    @Getter
+    private static ChoiceSelector choiceSelector = null;
 
     /**
      * Get a machine of a given type and index if exists, else return null.
@@ -92,4 +100,20 @@ public static void addGlobalMachine(PMachine machine, int machineCount) {
         machineSet.add(machine);
         assert (machineListByType.get(machine.getClass()).get(machineCount) == machine);
     }
+
+    /**
+     * Set choice orchestrator
+     */
+    public static void setChoiceSelector() {
+        switch (config.getChoiceSelectorMode()) {
+            case Random:
+                choiceSelector = new ChoiceSelectorRandom();
+                break;
+            case QL:
+                choiceSelector = new ChoiceSelectorQL();
+                break;
+            default:
+                throw new RuntimeException("Unrecognized choice orchestrator: " + config.getChoiceSelectorMode());
+        }
+    }
 }
diff --git a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/STATUS.java b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/STATUS.java
@@ -11,7 +11,7 @@ public enum STATUS {
     INTERRUPTED("interrupted"),                         // interrupted by user
     ERROR("error");                                     // unexpected error encountered
 
-    private String name;
+    private final String name;
 
     /**
      * Constructor

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
@@ -94,7 +94,8 @@ public static void logEndOfRun(ExplicitSearchScheduler scheduler, long timeSpent
         if (scheduler != null) {
             log.info("... Scheduling statistics:");
             if (PExplicitGlobal.getConfig().getStateCachingMode() != StateCachingMode.None) {
-                log.info(String.format("..... Explored %d distinct states", SearchStatistics.totalDistinctStates));
+                log.info(String.format("..... Explored %d distinct states over %d timelines",
+                        SearchStatistics.totalDistinctStates, scheduler.getTimelines().size()));
             }
             log.info(String.format("..... Explored %d distinct schedules", SearchStatistics.iteration));
             log.info(String.format("..... Finished %d search tasks (%d pending)",

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
@@ -1,6 +1,7 @@
 package pexplicit.runtime.machine;
 
 import lombok.Getter;
+import org.apache.commons.lang3.tuple.ImmutablePair;
 import pexplicit.runtime.PExplicitGlobal;
 import pexplicit.runtime.logger.PExplicitLogger;
 import pexplicit.runtime.machine.buffer.DeferQueue;
@@ -51,6 +52,9 @@ public abstract class PMachine implements Serializable, Comparable<PMachine> {
     private boolean started = false;
     @Getter
     private boolean halted = false;
+    private Set<PEvent> observedEvents;
+    @Getter
+    private Set<ImmutablePair<PEvent, PEvent>> happensBeforePairs;
     private PContinuation blockedBy = null;
     @Getter
     private State blockedStateExit;
@@ -95,6 +99,9 @@ public void handleEvent(PMachine target, PValue<?> payload) {
         // initialize send buffer
         this.sendBuffer = new SenderQueue(this);
         this.deferQueue = new DeferQueue(this);
+        // initialize happens-before
+        this.observedEvents = new HashSet<>();
+        this.happensBeforePairs = new HashSet<>();
     }
 
     public void start(PValue<?> payload) {
@@ -128,6 +135,9 @@ public void reset() {
         this.started = false;
         this.halted = false;
 
+        this.observedEvents.clear();
+        this.happensBeforePairs.clear();
+
         this.blockedBy = null;
         this.blockedStateExit = null;
         this.blockedNewStateEntry = null;
@@ -168,6 +178,9 @@ public List<String> getLocalVarNames() {
         result.add("_started");
         result.add("_halted");
 
+        result.add("_observedEvents");
+        result.add("_happensBefore");
+
         result.add("_blockedBy");
         result.add("_blockedStateExit");
         result.add("_blockedNewStateEntry");
@@ -205,6 +218,9 @@ public List<Object> getLocalVarValues() {
         result.add(started);
         result.add(halted);
 
+        result.add(observedEvents);
+        result.add(happensBeforePairs);
+
         result.add(blockedBy);
         result.add(blockedStateExit);
         result.add(blockedNewStateEntry);
@@ -246,6 +262,9 @@ public List<Object> copyLocalVarValues() {
         result.add(started);
         result.add(halted);
 
+        result.add(new HashSet<>(observedEvents));
+        result.add(new HashSet<>(happensBeforePairs));
+
         result.add(blockedBy);
         result.add(blockedStateExit);
         result.add(blockedNewStateEntry);
@@ -288,6 +307,9 @@ protected int setLocalVarValues(List<Object> values) {
         started = (boolean) values.get(idx++);
         halted = (boolean) values.get(idx++);
 
+        observedEvents = (Set<PEvent>) values.get(idx++);
+        happensBeforePairs = (Set<ImmutablePair<PEvent, PEvent>>) values.get(idx++);
+
         blockedBy = (PContinuation) values.get(idx++);
         blockedStateExit = (State) values.get(idx++);
         blockedNewStateEntry = (State) values.get(idx++);
@@ -502,9 +524,9 @@ void processEvent(PMessage message) {
      * @param message Message to process
      */
     void runEvent(PMessage message) {
+        PEvent event = message.getEvent();
         if (isBlocked()) {
             PContinuation currBlockedBy = this.blockedBy;
-            PEvent event = message.getEvent();
             clearBlocked();
 
             // make sure event is handled (or is halt event)
@@ -521,6 +543,7 @@ void runEvent(PMessage message) {
                                 event, this, this.currentState));
             }
         } else {
+            addObservedEvent(event);
             currentState.handleEvent(message, this);
         }
     }
@@ -624,6 +647,13 @@ public void enterNewState(State newState, PValue<?> payload) {
         newState.entry(this, payload);
     }
 
+    private void addObservedEvent(PEvent newEvent) {
+        for (PEvent happenedBeforeEvent : observedEvents) {
+            happensBeforePairs.add(new ImmutablePair<>(happenedBeforeEvent, newEvent));
+        }
+        observedEvents.add(newEvent);
+    }
+
     @Override
     public int compareTo(PMachine rhs) {
         if (rhs == null) {

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
@@ -360,7 +360,7 @@ public void checkLiveness(boolean terminated) {
         if (terminated) {
             for (PMachine monitor : PExplicitGlobal.getModel().getMonitors()) {
                 if (monitor.getCurrentState().isHotState()) {
-                        Assert.liveness(String.format("Monitor %s detected liveness bug in hot state %s at the end of program execution", monitor, monitor.getCurrentState()));
+                    Assert.liveness(String.format("Monitor %s detected liveness bug in hot state %s at the end of program execution", monitor, monitor.getCurrentState()));
                 }
             }
         }

diff --git a/...itRuntime/src/main/java/pexplicit/runtime/scheduler/explicit/ExplicitSearchScheduler.java b/...itRuntime/src/main/java/pexplicit/runtime/scheduler/explicit/ExplicitSearchScheduler.java
@@ -14,6 +14,8 @@
 import pexplicit.runtime.scheduler.Scheduler;
 import pexplicit.runtime.scheduler.choice.ScheduleChoice;
 import pexplicit.runtime.scheduler.choice.SearchUnit;
+import pexplicit.runtime.scheduler.explicit.choiceselector.ChoiceSelectorMode;
+import pexplicit.runtime.scheduler.explicit.choiceselector.ChoiceSelectorQL;
 import pexplicit.runtime.scheduler.explicit.strategy.*;
 import pexplicit.utils.exceptions.PExplicitRuntimeException;
 import pexplicit.utils.misc.Assert;
@@ -35,6 +37,11 @@ public class ExplicitSearchScheduler extends Scheduler {
      * Map from state hash to iteration when first visited
      */
     private final transient Map<Object, Integer> stateCache = new HashMap<>();
+    /**
+     * Set of timelines
+     */
+    @Getter
+    private final transient Set<Integer> timelines = new HashSet<>();
     /**
      * Search strategy orchestrator
      */
@@ -191,6 +198,16 @@ protected void runStep() throws TimeoutException {
             return;
         }
 
+        // update timeline
+        Integer timelineHash = stepState.getTimelineHash();
+        if (!timelines.contains(timelineHash)) {
+//            stepState.printTimeline(timelineHash, timelines.size());
+            timelines.add(timelineHash);
+        }
+        if (PExplicitGlobal.getConfig().getChoiceSelectorMode() == ChoiceSelectorMode.QL) {
+            PExplicitGlobal.getChoiceSelector().startStep(this);
+        }
+
         if (PExplicitGlobal.getConfig().getStatefulBacktrackingMode() != StatefulBacktrackingMode.None
                 && stepNumber != 0) {
             schedule.setStepBeginState(stepState.copyState());
@@ -330,12 +347,13 @@ public PMachine getNextScheduleChoice() {
             }
         }
 
-        // pick the first choice
-        result = PExplicitGlobal.getGlobalMachine(choices.get(0));
+        // pick a choice
+        int selected = PExplicitGlobal.getChoiceSelector().selectChoice(choices);
+        result = PExplicitGlobal.getGlobalMachine(choices.get(selected));
         PExplicitLogger.logCurrentScheduleChoice(result, stepNumber, choiceNumber);
 
-        // remove the first choice from unexplored choices
-        choices.remove(0);
+        // remove the selected choice from unexplored choices
+        choices.remove(selected);
 
         // add choice to schedule
         schedule.setScheduleChoice(stepNumber, choiceNumber, result.getPid());
@@ -393,12 +411,13 @@ public PValue<?> getNextDataChoice(List<PValue<?>> input_choices) {
             }
         }
 
-        // pick the first choice
-        result = choices.get(0);
+        // pick a choice
+        int selected = PExplicitGlobal.getChoiceSelector().selectChoice(choices);
+        result = choices.get(selected);
         PExplicitLogger.logCurrentDataChoice(result, stepNumber, choiceNumber);
 
-        // remove the first choice from unexplored choices
-        choices.remove(0);
+        // remove the selected choice from unexplored choices
+        choices.remove(selected);
 
         // add choice to schedule
         schedule.setDataChoice(stepNumber, choiceNumber, result);
@@ -600,6 +619,7 @@ public void recordStats() {
 
         // print basic statistics
         StatWriter.log("#-schedules", String.format("%d", SearchStatistics.iteration));
+        StatWriter.log("#-timelines", String.format("%d", timelines.size()));
         if (PExplicitGlobal.getConfig().getStateCachingMode() != StateCachingMode.None) {
             StatWriter.log("#-states", String.format("%d", SearchStatistics.totalStates));
             StatWriter.log("#-distinct-states", String.format("%d", SearchStatistics.totalDistinctStates));
@@ -610,6 +630,8 @@ public void recordStats() {
         StatWriter.log("%-choices-unexplored-data", String.format("%.1f", getUnexploredDataChoicesPercent()));
         StatWriter.log("#-tasks-finished", String.format("%d", searchStrategy.getFinishedTasks().size()));
         StatWriter.log("#-tasks-pending", String.format("%d", searchStrategy.getPendingTasks().size()));
+        StatWriter.log("ql-#-states", String.format("%d", ChoiceSelectorQL.getChoiceQL().getNumStates()));
+        StatWriter.log("ql-#-actions", String.format("%d", ChoiceSelectorQL.getChoiceQL().getNumActions()));
     }
 
     private void printCurrentStatus(double newRuntime) {
@@ -621,6 +643,7 @@ private void printCurrentStatus(double newRuntime) {
         s.append(String.format("\n      Unexplored:       %d", getNumUnexploredChoices()));
         s.append(String.format("\n      FinishedTasks:    %d", searchStrategy.getFinishedTasks().size()));
         s.append(String.format("\n      PendingTasks:     %d", searchStrategy.getPendingTasks().size()));
+        s.append(String.format("\n      Timelines:        %d", timelines.size()));
         if (PExplicitGlobal.getConfig().getStateCachingMode() != StateCachingMode.None) {
             s.append(String.format("\n      States:           %d", SearchStatistics.totalStates));
             s.append(String.format("\n      DistinctStates:   %d", SearchStatistics.totalDistinctStates));
@@ -635,6 +658,7 @@ private void printProgressHeader(boolean consolePrint) {
         s.append(StringUtils.center("Step", 7));
 
         s.append(StringUtils.center("Schedule", 12));
+        s.append(StringUtils.center("Timelines", 12));
         s.append(StringUtils.center("Unexplored", 24));
 
         if (PExplicitGlobal.getConfig().getStateCachingMode() != StateCachingMode.None) {
@@ -677,6 +701,7 @@ protected void printProgress(boolean forcePrint) {
                 s.append(StringUtils.center(String.format("%d", stepNumber), 7));
 
                 s.append(StringUtils.center(String.format("%d", SearchStatistics.iteration), 12));
+                s.append(StringUtils.center(String.format("%d", timelines.size()), 12));
                 s.append(
                         StringUtils.center(
                                 String.format(