Skip to content

Commit

Permalink
[PExplicit] Add non-chronological search
Browse files Browse the repository at this point in the history 
Adds non-chronological search that implements search beyond DFS.

New search modes include random, astar

Each run is executed over search tasks, with each task tracking the set of unexplored choices it is assigned to explore

Each search task can create new children sub-tasks
  • Loading branch information
@aman-goel
aman-goel committed Apr 25, 2024
1 parent 242fc6e commit e21ae0f
Show file tree
Hide file tree
Showing 15 changed files with 612 additions and 80 deletions.
4 changes: 2 additions & 2 deletions Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/RuntimeExecutor.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -65,7 +65,7 @@ private static void printStats() {
private static void preprocess() {
PExplicitLogger.logInfo(String.format(".. Test case :: " + PExplicitGlobal.getConfig().getTestDriver()));
PExplicitLogger.logInfo(String.format("... Checker is using '%s' strategy (seed:%s)",
PExplicitGlobal.getConfig().getStrategy(), PExplicitGlobal.getConfig().getRandomSeed()));
PExplicitGlobal.getConfig().getSearchStrategyMode(), PExplicitGlobal.getConfig().getRandomSeed()));

executor = Executors.newSingleThreadExecutor();

Expand All @@ -74,7 +74,7 @@ private static void preprocess() {
double preSearchTime =
TimeMonitor.findInterval(TimeMonitor.getStart());
StatWriter.log("project-name", String.format("%s", PExplicitGlobal.getConfig().getProjectName()));
StatWriter.log("strategy", String.format("%s", PExplicitGlobal.getConfig().getStrategy()));
StatWriter.log("strategy", String.format("%s", PExplicitGlobal.getConfig().getSearchStrategyMode()));
StatWriter.log("time-limit-seconds", String.format("%.1f", PExplicitGlobal.getConfig().getTimeLimit()));
StatWriter.log("memory-limit-MB", String.format("%.1f", PExplicitGlobal.getConfig().getMemLimit()));
StatWriter.log("time-pre-seconds", String.format("%.1f", preSearchTime));
Expand Down
21 changes: 10 additions & 11 deletions Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/commandline/PExplicitConfig.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,7 @@
import lombok.Setter;
import pexplicit.runtime.machine.buffer.BufferSemantics;
import pexplicit.runtime.scheduler.explicit.StateCachingMode;
import pexplicit.runtime.scheduler.explicit.strategy.SearchStrategyMode;

/**
* Represents the configuration for PExplicit runtime.
Expand Down Expand Up @@ -32,9 +33,6 @@ public class PExplicitConfig {
// level of verbosity for the logging
@Setter
int verbosity = 0;
// strategy of exploration
@Setter
String strategy = "dfs";
// max number of schedules bound provided by the user
@Setter
int maxSchedules = 1;
Expand All @@ -59,12 +57,13 @@ public class PExplicitConfig {
// use stateful backtracking
@Setter
boolean statefulBacktrackEnabled = true;

public void setToDfs() {
this.setStrategy("dfs");
}

public void setToReplay() {
this.setStrategy("replay");
}
// search strategy mode
@Setter
SearchStrategyMode searchStrategyMode = SearchStrategyMode.Random;
// max number of schedules per search task
@Setter
int maxSchedulesPerTask = 100;
//max number of children search tasks
@Setter
int maxChildrenPerTask = 2;
}
54 changes: 52 additions & 2 deletions Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/commandline/PExplicitOptions.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,7 @@

import org.apache.commons.cli.*;
import pexplicit.runtime.scheduler.explicit.StateCachingMode;
import pexplicit.runtime.scheduler.explicit.strategy.SearchStrategyMode;

import java.io.PrintWriter;

Expand Down Expand Up @@ -98,7 +99,7 @@ public class PExplicitOptions {
Option strategy =
Option.builder("st")
.longOpt("strategy")
.desc("Exploration strategy: dfs (default: dfs)")
.desc("Exploration strategy: dfs, random, astar (default: dfs)")
.numberOfArgs(1)
.hasArg()
.argName("Strategy (string)")
Expand Down Expand Up @@ -147,6 +148,7 @@ public class PExplicitOptions {
.build();
addOption(randomSeed);


/*
* Invisible/expert options
*/
Expand All @@ -171,6 +173,28 @@ public class PExplicitOptions {
.build();
addHiddenOption(backtrack);

// max number of schedules to explore per search task
Option maxSchedulesPerTask =
Option.builder()
.longOpt("schedules-per-task")
.desc("Max number of schedules to explore per search task (default: 100)")
.numberOfArgs(1)
.hasArg()
.argName("(integer)")
.build();
addHiddenOption(maxSchedulesPerTask);

// max number of children per search task
Option maxChildrenPerTask =
Option.builder()
.longOpt("children-per-task")
.desc("Max number of children to generate per search task (default: 2)")
.numberOfArgs(1)
.hasArg()
.argName("(integer)")
.build();
addHiddenOption(maxChildrenPerTask);

/*
* Help menu options
*/
Expand Down Expand Up @@ -267,7 +291,13 @@ public static PExplicitConfig ParseCommandlineArgs(String[] args) {
case "strategy":
switch (option.getValue()) {
case "dfs":
config.setToDfs();
config.setSearchStrategyMode(SearchStrategyMode.DepthFirst);
break;
case "random":
config.setSearchStrategyMode(SearchStrategyMode.Random);
break;
case "astar":
config.setSearchStrategyMode (SearchStrategyMode.AStar);
break;
default:
optionError(
Expand Down Expand Up @@ -336,6 +366,22 @@ public static PExplicitConfig ParseCommandlineArgs(String[] args) {
case "no-backtrack":
config.setStatefulBacktrackEnabled(false);
break;
case "schedules-per-task":
try {
config.setMaxSchedulesPerTask(Integer.parseInt(option.getValue()));
} catch (NumberFormatException ex) {
optionError(
option, String.format("Expected an integer value, got %s", option.getValue()));
}
break;
case "children-per-task":
try {
config.setMaxChildrenPerTask(Integer.parseInt(option.getValue()));
} catch (NumberFormatException ex) {
optionError(
option, String.format("Expected an integer value, got %s", option.getValue()));
}
break;
case "h":
case "help":
formatter.printHelp(
Expand All @@ -360,6 +406,10 @@ public static PExplicitConfig ParseCommandlineArgs(String[] args) {
}
}

if (config.getSearchStrategyMode() == SearchStrategyMode.DepthFirst) {
config.setMaxSchedulesPerTask(0);
}

return config;
}

Expand Down
5 changes: 5 additions & 0 deletions Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/PExplicitGlobal.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,8 @@
import pexplicit.commandline.PExplicitConfig;
import pexplicit.runtime.machine.PMachine;
import pexplicit.runtime.scheduler.Scheduler;
import pexplicit.runtime.scheduler.explicit.strategy.SearchStrategy;
import pexplicit.runtime.scheduler.explicit.strategy.SearchStrategyMode;

import java.util.*;

Expand Down Expand Up @@ -40,6 +42,9 @@ public class PExplicitGlobal {
@Getter
@Setter
private static Scheduler scheduler = null;
@Getter
@Setter
private static SearchStrategyMode searchStrategyMode;
/**
* Status of the run
**/
Expand Down
49 changes: 46 additions & 3 deletions Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/logger/PExplicitLogger.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,7 @@
import pexplicit.runtime.scheduler.explicit.ExplicitSearchScheduler;
import pexplicit.runtime.scheduler.explicit.SearchStatistics;
import pexplicit.runtime.scheduler.explicit.StateCachingMode;
import pexplicit.runtime.scheduler.explicit.strategy.SearchTask;
import pexplicit.runtime.scheduler.replay.ReplayScheduler;
import pexplicit.utils.monitor.MemoryMonitor;
import pexplicit.values.PEvent;
Expand Down Expand Up @@ -96,6 +97,8 @@ public static void logEndOfRun(ExplicitSearchScheduler scheduler, long timeSpent
log.info(String.format("..... Explored %d distinct states", SearchStatistics.totalDistinctStates));
}
log.info(String.format("..... Explored %d distinct schedules", SearchStatistics.iteration));
log.info(String.format("..... Finished %d search tasks (%d pending)",
scheduler.getSearchStrategy().getFinishedTasks().size(), scheduler.getSearchStrategy().getPendingTasks().size()));
log.info(String.format("..... Number of steps explored: %d (min), %d (avg), %d (max).",
SearchStatistics.minSteps, (SearchStatistics.totalSteps / SearchStatistics.iteration), SearchStatistics.maxSteps));
log.info(String.format("... Elapsed %d seconds and used %.1f GB", timeSpent, MemoryMonitor.getMaxMemSpent() / 1000.0));
Expand All @@ -116,16 +119,56 @@ public static void logStackTrace(Exception e) {
log.info(sw.toString());
}

/**
* Log at the start of a search task
*
* @param task Search task
*/
public static void logStartTask(SearchTask task) {
if (verbosity > 0) {
log.info("=====================");
log.info(String.format("Starting %s", task.toStringDetailed()));
}
}

/**
* Log at the end of a search task
*
* @param task Search task
*/
public static void logEndTask(SearchTask task, int numSchedules) {
if (verbosity > 0) {
log.info(String.format(" Finished %s after exploring %d schedules", task, numSchedules));
}
}

public static void logNewTasks(List<SearchTask> tasks) {
if (verbosity > 0) {
log.info(String.format(" Added %d new tasks", tasks.size()));
}
if (verbosity > 1) {
for (SearchTask task : tasks) {
log.info(String.format(" %s", task.toStringDetailed()));
}
}
}

public static void logNextTask(SearchTask task) {
if (verbosity > 1) {
log.info(String.format(" Next task is %s", task.toStringDetailed()));
}
}

/**
* Log at the start of an iteration
*
* @param iter Iteration number
* @param step Starting step number
*/
public static void logStartIteration(int iter, int step) {
public static void logStartIteration(SearchTask task, int iter, int step) {
if (verbosity > 0) {
log.info("--------------------");
log.info("Starting Schedule: " + iter + " from step: " + step);
log.info(String.format("[%s] Starting schedule %s from step %s", task, iter, step));
}
}

Expand Down Expand Up @@ -233,7 +276,7 @@ public static void logModel(String message) {
public static void logBugFound(String message) {
if (typedLogEnabled()) {
typedLog(LogType.ErrorLog, message);
typedLog(LogType.StrategyLog, String.format("Found bug using '%s' strategy.", PExplicitGlobal.getConfig().getStrategy()));
typedLog(LogType.StrategyLog, String.format("Found bug using '%s' strategy.", PExplicitGlobal.getConfig().getSearchStrategyMode()));
typedLog(LogType.StrategyLog, "Checking statistics:");
typedLog(LogType.StrategyLog, "Found 1 bug.");
}
Expand Down
28 changes: 19 additions & 9 deletions Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/Choice.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -32,6 +32,22 @@ public class Choice implements Serializable {
public Choice() {
}

public Choice transferUnexplored() {
Choice newChoice = new Choice();
newChoice.currentScheduleChoice = this.currentScheduleChoice;
newChoice.currentDataChoice = this.currentDataChoice;

newChoice.unexploredScheduleChoices = this.unexploredScheduleChoices;
newChoice.unexploredDataChoices = this.unexploredDataChoices;
newChoice.choiceStep = this.choiceStep;

this.unexploredScheduleChoices = new ArrayList<>();
this.unexploredDataChoices = new ArrayList<>();
this.choiceStep = null;

return newChoice;
}

/**
* Check if this choice has an unexplored choice remaining.
*
Expand Down Expand Up @@ -73,15 +89,9 @@ public void clearCurrent() {
public void clearUnexplored() {
unexploredScheduleChoices.clear();
unexploredDataChoices.clear();
choiceStep = null;
}

/**
* Clear this choice
*/
public void clear() {
clearCurrent();
clearUnexplored();
if (choiceStep != null) {
choiceStep.clear();
}
}

@Override
Expand Down
48 changes: 10 additions & 38 deletions Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/Schedule.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -27,7 +27,7 @@ public class Schedule implements Serializable {
* Used in stateful backtracking
*/
@Setter
private StepState stepBeginState = null;
private transient StepState stepBeginState = null;

/**
* Constructor
Expand All @@ -54,23 +54,14 @@ public Choice getChoice(int idx) {
return choices.get(idx);
}

/**
* Set the choice at a choice depth.
*
* @param idx Choice depth
* @param choice Choice object
*/
public void setChoice(int idx, Choice choice) {
choices.set(idx, choice);
}

/**
* Clear choice at a choice depth
*
* @param idx Choice depth
*/
public void clearChoice(int idx) {
choices.get(idx).clear();
choices.get(idx).clearCurrent();
choices.get(idx).clearUnexplored();
}

/**
Expand All @@ -81,32 +72,22 @@ public void clearChoice(int idx) {
public int getNumUnexploredChoices() {
int numUnexplored = 0;
for (Choice c : choices) {
if (c.isUnexploredNonEmpty()) {
numUnexplored += c.unexploredScheduleChoices.size() + c.unexploredDataChoices.size();
}
numUnexplored += c.unexploredScheduleChoices.size() + c.unexploredDataChoices.size();
}
return numUnexplored;
}

/**
* Get the percentage of unexplored choices in this schedule that are data choices
* Get the number of unexplored data choices in this schedule
*
* @return Percentage of unexplored choices that are data choices
* @return Number of unexplored data choices
*/
public double getUnexploredDataChoicesPercent() {
int totalUnexplored = getNumUnexploredChoices();
if (totalUnexplored == 0) {
return 0;
}

int numUnexploredData = 0;
public int getNumUnexploredDataChoices() {
int numUnexplored = 0;
for (Choice c : choices) {
if (c.isUnexploredDataChoicesNonEmpty()) {
numUnexploredData += c.unexploredDataChoices.size();
}
numUnexplored += c.unexploredDataChoices.size();
}

return (numUnexploredData * 100.0) / totalUnexplored;
return numUnexplored;
}

/**
Expand Down Expand Up @@ -230,15 +211,6 @@ public void clearCurrent(int idx) {
choices.get(idx).clearCurrent();
}

/**
* Clear unexplored choices at a choice depth
*
* @param idx Choice depth
*/
public void clearUnexplored(int idx) {
choices.get(idx).clearUnexplored();
}

/**
* Get the number of choices in the schedule
*
Expand Down
Loading

0 comments on commit e21ae0f

Please sign in to comment.