Skip to content

Commit

Permalink
[PEx] Adds option --replay <.schedule file> to replay a buggy trace
Browse files Browse the repository at this point in the history
  • Loading branch information
@aman-goel
aman-goel committed Jul 19, 2024
1 parent dbe1887 commit 9d02686
Show file tree
Hide file tree
Showing 9 changed files with 147 additions and 65 deletions.
2 changes: 0 additions & 2 deletions Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/PExplicit.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,6 @@
import pexplicit.runtime.logger.PExplicitLogger;
import pexplicit.runtime.logger.StatWriter;
import pexplicit.runtime.machine.PTestDriver;
import pexplicit.runtime.scheduler.explicit.strategy.SearchTask;
import pexplicit.utils.exceptions.BugFoundException;
import pexplicit.utils.monitor.MemoryMonitor;
import pexplicit.utils.monitor.TimeMonitor;
Expand All @@ -35,7 +34,6 @@ public static void main(String[] args) {
PExplicitGlobal.setConfig(PExplicitOptions.ParseCommandlineArgs(args));
PExplicitLogger.Initialize(PExplicitGlobal.getConfig().getVerbosity());
ComputeHash.Initialize();
SearchTask.Initialize();

// get reflections corresponding to the model
Reflections reflections = new Reflections("pexplicit.model");
Expand Down
79 changes: 65 additions & 14 deletions Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/RuntimeExecutor.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,8 +3,12 @@
import pexplicit.runtime.PExplicitGlobal;
import pexplicit.runtime.STATUS;
import pexplicit.runtime.logger.PExplicitLogger;
import pexplicit.runtime.logger.ScratchLogger;
import pexplicit.runtime.logger.StatWriter;
import pexplicit.runtime.scheduler.Schedule;
import pexplicit.runtime.scheduler.explicit.ExplicitSearchScheduler;
import pexplicit.runtime.scheduler.explicit.SearchStatistics;
import pexplicit.runtime.scheduler.explicit.strategy.SearchStrategyMode;
import pexplicit.runtime.scheduler.explicit.strategy.SearchTask;
import pexplicit.runtime.scheduler.replay.ReplayScheduler;
import pexplicit.utils.exceptions.BugFoundException;
Expand Down Expand Up @@ -55,39 +59,42 @@ private static void runWithTimeout(long timeLimit)
}

private static void printStats() {
double searchTime = TimeMonitor.stopInterval();
scheduler.recordStats();
if (PExplicitGlobal.getResult().equals("correct for any depth")) {
PExplicitGlobal.setStatus(STATUS.VERIFIED);
} else if (PExplicitGlobal.getResult().startsWith("correct up to step")) {
PExplicitGlobal.setStatus(STATUS.VERIFIED_UPTO_MAX_STEPS);
double timeUsed = (Duration.between(TimeMonitor.getStart(), Instant.now()).toMillis() / 1000.0);
double memoryUsed = MemoryMonitor.getMemSpent();

StatWriter.log("time-seconds", String.format("%.1f", timeUsed));
StatWriter.log("memory-max-MB", String.format("%.1f", MemoryMonitor.getMaxMemSpent()));
StatWriter.log("memory-current-MB", String.format("%.1f", memoryUsed));

if (PExplicitGlobal.getConfig().getSearchStrategyMode() != SearchStrategyMode.Replay) {
StatWriter.log("max-depth-explored", String.format("%d", SearchStatistics.maxSteps));
scheduler.recordStats();
if (PExplicitGlobal.getResult().equals("correct for any depth")) {
PExplicitGlobal.setStatus(STATUS.VERIFIED);
} else if (PExplicitGlobal.getResult().startsWith("correct up to step")) {
PExplicitGlobal.setStatus(STATUS.VERIFIED_UPTO_MAX_STEPS);
}
}
StatWriter.log("time-search-seconds", String.format("%.1f", searchTime));
}

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().getSearchStrategyMode(), PExplicitGlobal.getConfig().getRandomSeed()));

executor = Executors.newSingleThreadExecutor();

PExplicitGlobal.setResult("error");

double preSearchTime =
TimeMonitor.findInterval(TimeMonitor.getStart());
StatWriter.log("project-name", String.format("%s", PExplicitGlobal.getConfig().getProjectName()));
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));
}

private static void process(boolean resume) throws Exception {
executor = Executors.newSingleThreadExecutor();
try {
TimedCall timedCall = new TimedCall(scheduler, resume);
future = executor.submit(timedCall);
TimeMonitor.startInterval();
runWithTimeout((long) PExplicitGlobal.getConfig().getTimeLimit());
} catch (TimeoutException e) {
PExplicitGlobal.setStatus(STATUS.TIMEOUT);
Expand Down Expand Up @@ -135,12 +142,56 @@ private static void process(boolean resume) throws Exception {
}
}

public static void run() throws Exception {
public static void runSearch() throws Exception {
SearchTask.Initialize();
ScratchLogger.Initialize();

scheduler = new ExplicitSearchScheduler();
PExplicitGlobal.setScheduler(scheduler);

preprocess();
process(false);
}

private static void replaySchedule(String fileName) throws Exception {
PExplicitLogger.logInfo(String.format("... Reading buggy trace from %s", fileName));

ReplayScheduler replayer = new ReplayScheduler(Schedule.readFromFile(fileName));
PExplicitGlobal.setScheduler(replayer);
try {
replayer.run();
} catch (NullPointerException | StackOverflowError | ClassCastException replayException) {
PExplicitGlobal.setStatus(STATUS.BUG_FOUND);
PExplicitGlobal.setResult(String.format("found cex of length %d", replayer.getStepNumber()));
PExplicitLogger.logStackTrace((Exception) replayException);
throw new BugFoundException(replayException.getMessage(), replayException);
} catch (BugFoundException replayException) {
PExplicitGlobal.setStatus(STATUS.BUG_FOUND);
PExplicitGlobal.setResult(String.format("found cex of length %d", replayer.getStepNumber()));
PExplicitLogger.logStackTrace(replayException);
throw replayException;
} catch (Exception replayException) {
PExplicitLogger.logStackTrace(replayException);
throw new Exception("Error when replaying the bug", replayException);
} finally {
printStats();
PExplicitLogger.logEndOfRun(null, Duration.between(TimeMonitor.getStart(), Instant.now()).getSeconds());
}
}

public static void replay() throws Exception {
preprocess();
replaySchedule(PExplicitGlobal.getConfig().getReplayFile());
}

public static void run() throws Exception {
// initialize stats writer
StatWriter.Initialize();

if (PExplicitGlobal.getConfig().getSearchStrategyMode() == SearchStrategyMode.Replay) {
replay();
} else {
runSearch();
}
}
}
3 changes: 3 additions & 0 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 @@ -44,6 +44,9 @@ public class PExplicitConfig {
// random seed
@Setter
long randomSeed = System.currentTimeMillis();
// name of the replay file
@Setter
String replayFile = "";
// max number of logs (i.e., internal steps) within a single schedule step
@Setter
int maxStepLogBound = 1000;
Expand Down
31 changes: 31 additions & 0 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 @@ -149,6 +149,22 @@ public class PExplicitOptions {
.build();
addOption(randomSeed);

/*
* Replay options
*/

// replay file
Option replayFile =
Option.builder("r")
.longOpt("replay")
.desc("Schedule file to replay")
.numberOfArgs(1)
.hasArg()
.argName("File Name (string)")
.build();
addOption(replayFile);



/*
* Invisible/expert options
Expand Down Expand Up @@ -339,6 +355,12 @@ public static PExplicitConfig ParseCommandlineArgs(String[] args) {
option, String.format("Expected an integer value, got %s", option.getValue()));
}
break;
// replay options
case "r":
case "replay":
config.setReplayFile(option.getValue());
config.setSearchStrategyMode(SearchStrategyMode.Replay);
break;
// invisible expert options
case "state-caching":
switch (option.getValue()) {
Expand Down Expand Up @@ -427,6 +449,15 @@ public static PExplicitConfig ParseCommandlineArgs(String[] args) {
config.setMaxSchedulesPerTask(0);
}

if (config.getSearchStrategyMode() == SearchStrategyMode.Replay) {
if (config.getVerbosity() == 0) {
config.setVerbosity(1);
}
if (config.getReplayFile().startsWith(config.getOutputFolder())) {
config.setOutputFolder(config.getOutputFolder() + "Replay");
}
}

return config;
}

Expand Down
24 changes: 11 additions & 13 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 @@ -58,10 +58,6 @@ public static void Initialize(int verb) {
consoleAppender.start();

context.getConfiguration().addLoggerAppender(coreLogger, consoleAppender);

// initialize all loggers and writers
StatWriter.Initialize();
ScratchLogger.Initialize();
}

public static void logInfo(String message) {
Expand Down Expand Up @@ -96,15 +92,17 @@ public static void logEndOfRun(ExplicitSearchScheduler scheduler, long timeSpent
} else {
log.info("..... Found 0 bugs.");
}
log.info("... Scheduling statistics:");
if (PExplicitGlobal.getConfig().getStateCachingMode() != StateCachingMode.None) {
log.info(String.format("..... Explored %d distinct states", SearchStatistics.totalDistinctStates));
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 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("..... 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));
log.info(String.format(".. Result: " + PExplicitGlobal.getResult()));
log.info(". Done");
Expand Down Expand Up @@ -172,7 +170,7 @@ public static void logNewTasks(List<SearchTask> tasks) {
* Log when serializing a schedule
*
* @param schedule Schedule to serialize
* @param szBytes Bytes written
* @param szBytes Bytes written
*/
public static void logSerializeSchedule(Schedule schedule, String fileName, long szBytes) {
if (verbosity > 1) {
Expand Down
24 changes: 17 additions & 7 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 @@ -3,7 +3,6 @@
import lombok.Getter;
import lombok.Setter;
import pexplicit.runtime.PExplicitGlobal;
import pexplicit.runtime.logger.PExplicitLogger;
import pexplicit.runtime.machine.PMachineId;
import pexplicit.runtime.scheduler.choice.Choice;
import pexplicit.runtime.scheduler.choice.DataChoice;
Expand All @@ -12,12 +11,7 @@
import pexplicit.runtime.scheduler.explicit.StepState;
import pexplicit.values.PValue;

import java.io.FileOutputStream;
import java.io.IOException;
import java.io.ObjectOutputStream;
import java.io.Serializable;
import java.nio.file.Files;
import java.nio.file.Paths;
import java.io.*;
import java.util.ArrayList;
import java.util.List;

Expand Down Expand Up @@ -45,6 +39,22 @@ public class Schedule implements Serializable {
public Schedule() {
}

public static Schedule readFromFile(String fileName) {
assert (fileName != null);
Schedule result = null;

try {
FileInputStream fis;
fis = new FileInputStream(fileName);
ObjectInputStream ois = new ObjectInputStream(fis);
result = (Schedule) ois.readObject();
} catch (IOException | ClassNotFoundException e) {
throw new RuntimeException("Failed to read schedule from file " + fileName, e);
}

return result;
}

/**
* Get the choice at a choice depth
*
Expand Down
8 changes: 0 additions & 8 deletions ...itRuntime/src/main/java/pexplicit/runtime/scheduler/explicit/ExplicitSearchScheduler.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,6 @@
import pexplicit.values.ComputeHash;
import pexplicit.values.PValue;

import java.time.Duration;
import java.time.Instant;
import java.util.*;
import java.util.concurrent.TimeUnit;
Expand Down Expand Up @@ -597,22 +596,15 @@ public void updateResult() {
}

public void recordStats() {
double timeUsed = (Duration.between(TimeMonitor.getStart(), Instant.now()).toMillis() / 1000.0);
double memoryUsed = MemoryMonitor.getMemSpent();

printProgress(true);

// print basic statistics
StatWriter.log("time-seconds", String.format("%.1f", timeUsed));
StatWriter.log("memory-max-MB", String.format("%.1f", MemoryMonitor.getMaxMemSpent()));
StatWriter.log("memory-current-MB", String.format("%.1f", memoryUsed));
StatWriter.log("#-executions", String.format("%d", SearchStatistics.iteration));
if (PExplicitGlobal.getConfig().getStateCachingMode() != StateCachingMode.None) {
StatWriter.log("#-states", String.format("%d", SearchStatistics.totalStates));
StatWriter.log("#-distinct-states", String.format("%d", SearchStatistics.totalDistinctStates));
}
StatWriter.log("steps-min", String.format("%d", SearchStatistics.minSteps));
StatWriter.log("max-depth-explored", String.format("%d", SearchStatistics.maxSteps));
StatWriter.log("steps-avg", String.format("%d", SearchStatistics.totalSteps / SearchStatistics.iteration));
StatWriter.log("#-choices-unexplored", String.format("%d", getNumUnexploredChoices()));
StatWriter.log("%-choices-unexplored-data", String.format("%.1f", getUnexploredDataChoicesPercent()));
Expand Down
3 changes: 2 additions & 1 deletion ...ntime/src/main/java/pexplicit/runtime/scheduler/explicit/strategy/SearchStrategyMode.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,8 @@
public enum SearchStrategyMode {
DepthFirst("dfs"),
Random("random"),
Astar("astar");
Astar("astar"),
Replay("replay");

private String name;

Expand Down
Loading

0 comments on commit 9d02686

Please sign in to comment.