diff --git a/Src/PCompiler/CompilerCore/Backend/PEx/PExCodeGenerator.cs b/Src/PCompiler/CompilerCore/Backend/PEx/PExCodeGenerator.cs index e40617650a..e017af243d 100644 --- a/Src/PCompiler/CompilerCore/Backend/PEx/PExCodeGenerator.cs +++ b/Src/PCompiler/CompilerCore/Backend/PEx/PExCodeGenerator.cs @@ -127,15 +127,6 @@ private CompiledFile GenerateSource(CompilationContext context, Scope globalScop context.WriteLine(source.Stream, "public void setTestDriver(PTestDriver input) { testDriver = input; }"); context.WriteLine(source.Stream); - context.WriteLine(source.Stream, "@Generated"); - context.WriteLine(source.Stream, "public PMachine getStart() { return testDriver.getStart(); }"); - context.WriteLine(source.Stream, "@Generated"); - context.WriteLine(source.Stream, "public List getMonitors() { return testDriver.getMonitors(); }"); - context.WriteLine(source.Stream, "@Generated"); - context.WriteLine(source.Stream, - "public Map> getListeners() { return testDriver.getListeners(); }"); - context.WriteLine(source.Stream); - WriteSourceEpilogue(context, source.Stream); return source; @@ -155,7 +146,7 @@ private void WriteDriverConfigure(CompilationContext context, StringWriter outpu context.WriteLine(output, "@Generated"); context.WriteLine(output, "public void configure() {"); - context.WriteLine(output, $" mainMachine = new {startMachine}(0);"); + context.WriteLine(output, $" mainMachine = {startMachine}.class;"); context.WriteLine(output); context.WriteLine(output, " interfaceMap.clear();"); @@ -175,13 +166,13 @@ private void WriteDriverConfigure(CompilationContext context, StringWriter outpu { context.WriteLine(output); var declName = context.GetNameForDecl(machine); - context.WriteLine(output, $" PMonitor instance_{declName} = new {declName}(0);"); - context.WriteLine(output, $" monitorList.add(instance_{declName});"); + context.WriteLine(output, $" Class cls_{declName} = {declName}.class;"); + context.WriteLine(output, $" monitorList.add(cls_{declName});"); foreach (var pEvent in machine.Observes.Events) { context.WriteLine(output, $" if(!observerMap.containsKey({pEvent.Name}))"); context.WriteLine(output, $" observerMap.put({pEvent.Name}, new ArrayList<>());"); - context.WriteLine(output, $" observerMap.get({pEvent.Name}).add(instance_{declName});"); + context.WriteLine(output, $" observerMap.get({pEvent.Name}).add(cls_{declName});"); } } @@ -732,7 +723,7 @@ private bool WriteStmt(Function function, CompilationContext context, StringWrit break; case PrintStmt printStmt: - context.Write(output, "PExLogger.logModel("); + context.Write(output, $"{CompilationContext.SchedulerVar}.getLogger().logModel("); WriteExpr(context, output, printStmt.Message); context.WriteLine(output, ".toString());"); break; diff --git a/Src/PRuntimes/PExRuntime/pom.xml b/Src/PRuntimes/PExRuntime/pom.xml index 8da504c5c2..1d08c68488 100644 --- a/Src/PRuntimes/PExRuntime/pom.xml +++ b/Src/PRuntimes/PExRuntime/pom.xml @@ -274,7 +274,7 @@ ${java.version} ${project.basedir}/src/main/resources/log4j2.xml UTF-8 - 0.0.1 + 0.1.0 diff --git a/Src/PRuntimes/PExRuntime/src/main/java/pex/RuntimeExecutor.java b/Src/PRuntimes/PExRuntime/src/main/java/pex/RuntimeExecutor.java index 3e3b861673..8d23217ec8 100644 --- a/Src/PRuntimes/PExRuntime/src/main/java/pex/RuntimeExecutor.java +++ b/Src/PRuntimes/PExRuntime/src/main/java/pex/RuntimeExecutor.java @@ -7,7 +7,6 @@ import pex.runtime.logger.StatWriter; import pex.runtime.scheduler.Schedule; import pex.runtime.scheduler.explicit.ExplicitSearchScheduler; -import pex.runtime.scheduler.explicit.SearchStatistics; import pex.runtime.scheduler.explicit.strategy.SearchStrategyMode; import pex.runtime.scheduler.explicit.strategy.SearchTask; import pex.runtime.scheduler.replay.ReplayScheduler; @@ -19,6 +18,10 @@ import java.time.Duration; import java.time.Instant; +import java.util.ArrayList; +import java.util.HashSet; +import java.util.List; +import java.util.Set; import java.util.concurrent.*; /** @@ -26,35 +29,85 @@ */ public class RuntimeExecutor { private static ExecutorService executor; - private static Future future; - private static ExplicitSearchScheduler scheduler; + private static List> futures = new ArrayList<>(); - private static void runWithTimeout(long timeLimit) - throws TimeoutException, - InterruptedException, - RuntimeException { - try { + private static void cancelAllThreads() { + for (int i = 0; i < futures.size(); i++) { + Future f = futures.get(i); + if (!f.isDone() && !f.isCancelled()) { + f.cancel(true); + } + } + } + + private static void runWithTimeout() throws Exception { + PExGlobal.setResult("incomplete"); + PExGlobal.printProgressHeader(); + + double timeLimit = PExGlobal.getConfig().getTimeLimit(); + Set done = new HashSet<>(); + Exception resultException = null; + + PExGlobal.getSearchSchedulers().get(1).getSearchStrategy().createFirstTask(); + + for (int i = 0; i < PExGlobal.getConfig().getNumThreads(); i++) { + TimedCall timedCall = new TimedCall(PExGlobal.getSearchSchedulers().get(i + 1)); + Future f = executor.submit(timedCall); + futures.add(f); + } + + while (true) { if (timeLimit > 0) { - future.get(timeLimit, TimeUnit.SECONDS); - } else { - future.get(); + double elapsedTime = TimeMonitor.getRuntime(); + if (elapsedTime > timeLimit) { + cancelAllThreads(); + resultException = new TimeoutException(String.format("Max time limit reached. Runtime: %.1f seconds", elapsedTime)); + } + } + + for (int i = 0; i < futures.size(); i++) { + if (!done.contains(i)) { + Future f = futures.get(i); + if (f.isDone() || f.isCancelled()) { + done.add(i); + try { + f.get(); + } catch (InterruptedException | CancellationException e) { + cancelAllThreads(); + } catch (OutOfMemoryError e) { + cancelAllThreads(); + resultException = new MemoutException(e.getMessage(), MemoryMonitor.getMemSpent(), e); + } catch (ExecutionException e) { + if (e.getCause() instanceof MemoutException) { + cancelAllThreads(); + resultException = (MemoutException) e.getCause(); + } else if (e.getCause() instanceof BugFoundException) { + cancelAllThreads(); + resultException = (BugFoundException) e.getCause(); + } else if (e.getCause() instanceof TimeoutException) { + cancelAllThreads(); + resultException = (TimeoutException) e.getCause(); + } else { + cancelAllThreads(); + resultException = new RuntimeException("RuntimeException", e); + } + } + } + } } - } catch (TimeoutException | BugFoundException e) { - throw e; - } catch (OutOfMemoryError e) { - throw new MemoutException(e.getMessage(), MemoryMonitor.getMemSpent(), e); - } catch (ExecutionException e) { - if (e.getCause() instanceof MemoutException) { - throw (MemoutException) e.getCause(); - } else if (e.getCause() instanceof BugFoundException) { - throw (BugFoundException) e.getCause(); - } else if (e.getCause() instanceof TimeoutException) { - throw (TimeoutException) e.getCause(); - } else { - throw new RuntimeException("RuntimeException", e); + + if (done.size() == PExGlobal.getConfig().getNumThreads()) { + break; } - } catch (InterruptedException e) { - throw e; + + TimeUnit.MILLISECONDS.sleep(100); + PExGlobal.printProgress(false); + } + PExGlobal.printProgress(true); + PExGlobal.printProgressFooter(); + + if (resultException != null) { + throw resultException; } } @@ -67,8 +120,8 @@ private static void printStats() { StatWriter.log("memory-current-MB", String.format("%.1f", memoryUsed)); if (PExGlobal.getConfig().getSearchStrategyMode() != SearchStrategyMode.Replay) { - StatWriter.log("max-depth-explored", String.format("%d", SearchStatistics.maxSteps)); - scheduler.recordStats(); + StatWriter.log("max-depth-explored", String.format("%d", PExGlobal.getMaxSteps())); + PExGlobal.recordStats(); if (PExGlobal.getResult().equals("correct for any depth")) { PExGlobal.setStatus(STATUS.VERIFIED); } else if (PExGlobal.getResult().startsWith("correct up to step")) { @@ -82,8 +135,8 @@ private static void printStats() { private static void preprocess() { PExLogger.logInfo(String.format(".. Test case :: " + PExGlobal.getConfig().getTestDriver())); - PExLogger.logInfo(String.format("... Checker is using '%s' strategy (seed:%s)", - PExGlobal.getConfig().getSearchStrategyMode(), PExGlobal.getConfig().getRandomSeed())); + PExLogger.logInfo(String.format("... Checker is using '%s' strategy with %d threads (seed:%s)", + PExGlobal.getConfig().getSearchStrategyMode(), PExGlobal.getConfig().getNumThreads(), PExGlobal.getConfig().getRandomSeed())); PExGlobal.setResult("error"); @@ -94,11 +147,8 @@ private static void preprocess() { } private static void process(boolean resume) throws Exception { - executor = Executors.newSingleThreadExecutor(); try { - TimedCall timedCall = new TimedCall(scheduler, resume); - future = executor.submit(timedCall); - runWithTimeout((long) PExGlobal.getConfig().getTimeLimit()); + runWithTimeout(); } catch (TimeoutException e) { PExGlobal.setStatus(STATUS.TIMEOUT); throw new Exception("TIMEOUT", e); @@ -107,15 +157,15 @@ private static void process(boolean resume) throws Exception { throw new Exception("MEMOUT", e); } catch (BugFoundException e) { PExGlobal.setStatus(STATUS.BUG_FOUND); - PExGlobal.setResult(String.format("found cex of length %d", scheduler.getStepNumber())); - PExLogger.logStackTrace(e); + PExGlobal.setResult(String.format("found cex of length %d", e.getScheduler().getStepNumber())); + e.getScheduler().getLogger().logStackTrace(e); String schFile = PExGlobal.getConfig().getOutputFolder() + "/" + PExGlobal.getConfig().getProjectName() + "_0_0.schedule"; PExLogger.logInfo(String.format("Writing buggy trace in %s", schFile)); - scheduler.getSchedule().writeToFile(schFile); + e.getScheduler().getSchedule().writeToFile(schFile); - ReplayScheduler replayer = new ReplayScheduler(scheduler.getSchedule()); - PExGlobal.setScheduler(replayer); + ReplayScheduler replayer = new ReplayScheduler(e.getScheduler().getSchedule()); + PExGlobal.setReplayScheduler(replayer); try { replayer.run(); } catch (NullPointerException | StackOverflowError | ClassCastException replayException) { @@ -136,11 +186,11 @@ private static void process(boolean resume) throws Exception { PExGlobal.setStatus(STATUS.ERROR); throw new Exception("ERROR", e); } finally { - future.cancel(true); + cancelAllThreads(); executor.shutdownNow(); - scheduler.updateResult(); + PExGlobal.updateResult(); printStats(); - PExLogger.logEndOfRun(scheduler, Duration.between(TimeMonitor.getStart(), Instant.now()).getSeconds()); + PExLogger.logEndOfRun(Duration.between(TimeMonitor.getStart(), Instant.now()).getSeconds()); SearchTask.Cleanup(); } } @@ -149,10 +199,15 @@ public static void runSearch() throws Exception { SearchTask.Initialize(); ScratchLogger.Initialize(); - scheduler = new ExplicitSearchScheduler(); - PExGlobal.setScheduler(scheduler); - preprocess(); + + executor = Executors.newFixedThreadPool(PExGlobal.getConfig().getNumThreads()); + + for (int i = 0; i < PExGlobal.getConfig().getNumThreads(); i++) { + ExplicitSearchScheduler scheduler = new ExplicitSearchScheduler(i + 1); + PExGlobal.addSearchScheduler(scheduler); + } + process(false); } @@ -160,7 +215,7 @@ private static void replaySchedule(String fileName) throws Exception { PExLogger.logInfo(String.format("... Reading buggy trace from %s", fileName)); ReplayScheduler replayer = new ReplayScheduler(Schedule.readFromFile(fileName)); - PExGlobal.setScheduler(replayer); + PExGlobal.setReplayScheduler(replayer); try { replayer.run(); } catch (NullPointerException | StackOverflowError | ClassCastException replayException) { @@ -178,7 +233,7 @@ private static void replaySchedule(String fileName) throws Exception { throw new Exception("Error when replaying the bug", replayException); } finally { printStats(); - PExLogger.logEndOfRun(null, Duration.between(TimeMonitor.getStart(), Instant.now()).getSeconds()); + PExLogger.logEndOfRun(Duration.between(TimeMonitor.getStart(), Instant.now()).getSeconds()); } } diff --git a/Src/PRuntimes/PExRuntime/src/main/java/pex/commandline/PExConfig.java b/Src/PRuntimes/PExRuntime/src/main/java/pex/commandline/PExConfig.java index ccfd1f873a..38e6c3d9e8 100644 --- a/Src/PRuntimes/PExRuntime/src/main/java/pex/commandline/PExConfig.java +++ b/Src/PRuntimes/PExRuntime/src/main/java/pex/commandline/PExConfig.java @@ -24,6 +24,9 @@ public class PExConfig { // name of the output folder @Setter String outputFolder = "output"; + // number of threads + @Setter + int numThreads = 1; // time limit in seconds (0 means infinite) @Setter double timeLimit = 0; diff --git a/Src/PRuntimes/PExRuntime/src/main/java/pex/commandline/PExOptions.java b/Src/PRuntimes/PExRuntime/src/main/java/pex/commandline/PExOptions.java index 768cde2817..7b7ebd430b 100644 --- a/Src/PRuntimes/PExRuntime/src/main/java/pex/commandline/PExOptions.java +++ b/Src/PRuntimes/PExRuntime/src/main/java/pex/commandline/PExOptions.java @@ -60,6 +60,17 @@ public class PExOptions { .build(); addOption(outputDir); + // number of threads + Option numThreads = + Option.builder("n") + .longOpt("nproc") + .desc("Number of threads (default: 1)") + .numberOfArgs(1) + .hasArg() + .argName("No. of Threads (integer)") + .build(); + addOption(numThreads); + // time limit Option timeLimit = Option.builder("t") @@ -288,6 +299,19 @@ public static PExConfig ParseCommandlineArgs(String[] args) { case "outdir": config.setOutputFolder(option.getValue()); break; + case "n": + case "nproc": + try { + config.setNumThreads(Integer.parseInt(option.getValue())); + if (config.getNumThreads() < 1) { + optionError( + option, String.format("Expected a positive integer value, got %s", option.getValue())); + } + } catch (NumberFormatException ex) { + optionError( + option, String.format("Expected an integer value, got %s", option.getValue())); + } + break; case "t": case "timeout": try { @@ -473,10 +497,12 @@ public static PExConfig ParseCommandlineArgs(String[] args) { if (config.getSearchStrategyMode() == SearchStrategyMode.DepthFirst) { config.setMaxSchedulesPerTask(0); + config.setNumThreads(1); } if (config.getReplayFile() != "") { config.setSearchStrategyMode(SearchStrategyMode.Replay); + config.setNumThreads(1); if (config.getVerbosity() == 0) { config.setVerbosity(1); } diff --git a/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/PExGlobal.java b/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/PExGlobal.java index 003e23a1fb..71e8d095fa 100644 --- a/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/PExGlobal.java +++ b/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/PExGlobal.java @@ -2,31 +2,61 @@ import lombok.Getter; import lombok.Setter; +import org.apache.commons.lang3.StringUtils; import pex.commandline.PExConfig; -import pex.runtime.machine.PMachine; -import pex.runtime.machine.PMachineId; +import pex.runtime.logger.ScratchLogger; +import pex.runtime.logger.StatWriter; import pex.runtime.scheduler.Scheduler; +import pex.runtime.scheduler.explicit.ExplicitSearchScheduler; +import pex.runtime.scheduler.explicit.StateCachingMode; import pex.runtime.scheduler.explicit.choiceselector.ChoiceSelector; import pex.runtime.scheduler.explicit.choiceselector.ChoiceSelectorQL; import pex.runtime.scheduler.explicit.choiceselector.ChoiceSelectorRandom; -import pex.runtime.scheduler.explicit.strategy.SearchStrategyMode; +import pex.runtime.scheduler.explicit.strategy.SearchTask; +import pex.runtime.scheduler.replay.ReplayScheduler; +import pex.utils.monitor.MemoryMonitor; +import pex.utils.monitor.TimeMonitor; -import java.util.*; +import java.time.Instant; +import java.util.Map; +import java.util.Set; +import java.util.concurrent.ConcurrentHashMap; +import java.util.concurrent.TimeUnit; /** * Represents global data structures represented with a singleton class */ public class PExGlobal { /** - * Mapping from machine type to list of all machine instances + * Map from state hash to schedulerId-iteration when first visited */ @Getter - private static final Map, List> machineListByType = new HashMap<>(); + private static final Map stateCache = new ConcurrentHashMap<>(); /** - * Set of machines + * Set of timelines */ @Getter - private static final SortedSet machineSet = new TreeSet<>(); + private static final Set timelines = ConcurrentHashMap.newKeySet(); + /** + * List of all search tasks + */ + @Getter + private static final Map allTasks = new ConcurrentHashMap<>(); + /** + * Set of all search tasks that are pending + */ + @Getter + private static final Set pendingTasks = ConcurrentHashMap.newKeySet(); + /** + * List of all search tasks that finished + */ + @Getter + private static final Set finishedTasks = ConcurrentHashMap.newKeySet(); + /** + * Set of all search tasks that are currently running + */ + @Getter + private static final Set runningTasks = ConcurrentHashMap.newKeySet(); /** * PModel **/ @@ -40,14 +70,25 @@ public class PExGlobal { @Setter private static PExConfig config = null; /** - * Scheduler + * Replay scheduler + */ + @Setter + private static ReplayScheduler replayScheduler = null; + /** + * Explicit search schedulers **/ @Getter - @Setter - private static Scheduler scheduler = null; + private static Map searchSchedulers = new ConcurrentHashMap<>(); @Getter - @Setter - private static SearchStrategyMode searchStrategyMode; + private static Map threadToSchedulerId = new ConcurrentHashMap<>(); + /** + * Map from scheduler to global machine id + */ + private static Map globalMachineId = new ConcurrentHashMap<>(); + /** + * Map from scheduler to global monitor id + */ + private static Map globalMonitorId = new ConcurrentHashMap<>(); /** * Status of the run **/ @@ -65,40 +106,58 @@ public class PExGlobal { */ @Getter private static ChoiceSelector choiceSelector = null; - /** - * Get a machine of a given type and index if exists, else return null. - * - * @param pid Machine pid - * @return Machine + * Time of last status report */ - public static PMachine getGlobalMachine(PMachineId pid) { - List machinesOfType = machineListByType.get(pid.getType()); - if (machinesOfType == null) { - return null; + private static Instant lastReportTime = Instant.now(); + + public static void addSearchScheduler(ExplicitSearchScheduler sch) { + searchSchedulers.put(sch.getSchedulerId(), sch); + } + + public static void registerSearchScheduler(int schId) { + assert (searchSchedulers.containsKey(schId)); + + long threadId = Thread.currentThread().getId(); + assert (!threadToSchedulerId.containsKey(threadId)); + threadToSchedulerId.put(threadId, schId); + } + + public static Scheduler getScheduler() { + if (replayScheduler == null) { + long threadId = Thread.currentThread().getId(); + Integer schId = threadToSchedulerId.get(threadId); + assert (schId != null); + return searchSchedulers.get(schId); + } else { + return replayScheduler; } - if (pid.getTypeId() >= machinesOfType.size()) { - return null; + } + + public static int getGlobalMachineId() { + Scheduler sch = getScheduler(); + if (!globalMachineId.containsKey(sch)) { + globalMachineId.put(sch, 1); } - PMachine result = machineListByType.get(pid.getType()).get(pid.getTypeId()); - assert (machineSet.contains(result)); - return result; + return globalMachineId.get(sch); } - /** - * Add a machine. - * - * @param machine Machine to add - * @param machineCount Machine type count - */ - public static void addGlobalMachine(PMachine machine, int machineCount) { - if (!machineListByType.containsKey(machine.getClass())) { - machineListByType.put(machine.getClass(), new ArrayList<>()); + public static void setGlobalMachineId(int id) { + Scheduler sch = getScheduler(); + globalMachineId.put(sch, id); + } + + public static int getGlobalMonitorId() { + Scheduler sch = getScheduler(); + if (!globalMonitorId.containsKey(sch)) { + globalMonitorId.put(sch, -1); } - assert (machineCount == machineListByType.get(machine.getClass()).size()); - machineListByType.get(machine.getClass()).add(machine); - machineSet.add(machine); - assert (machineListByType.get(machine.getClass()).get(machineCount) == machine); + return globalMonitorId.get(sch); + } + + public static void setGlobalMonitorId(int id) { + Scheduler sch = getScheduler(); + globalMonitorId.put(sch, id); } /** @@ -116,4 +175,224 @@ public static void setChoiceSelector() { throw new RuntimeException("Unrecognized choice orchestrator: " + config.getChoiceSelectorMode()); } } + + /** + * Get the number of unexplored choices in the pending tasks + * + * @return Number of unexplored choices + */ + static int getNumPendingChoices() { + int numUnexplored = 0; + for (SearchTask task : pendingTasks) { + numUnexplored += task.getTotalUnexploredChoices(); + } + return numUnexplored; + } + + /** + * Get the number of unexplored data choices in the pending tasks + * + * @return Number of unexplored data choices + */ + static int getNumPendingDataChoices() { + int numUnexplored = 0; + for (SearchTask task : pendingTasks) { + numUnexplored += task.getTotalUnexploredDataChoices(); + } + return numUnexplored; + } + + static int getNumUnexploredChoices() { + int result = getNumPendingChoices(); + for (ExplicitSearchScheduler sch : searchSchedulers.values()) { + result += sch.getSearchStrategy().getCurrTask().getCurrentNumUnexploredChoices(); + } + return result; + } + + static int getNumUnexploredDataChoices() { + int result = getNumPendingDataChoices(); + for (ExplicitSearchScheduler sch : searchSchedulers.values()) { + result += sch.getSearchStrategy().getCurrTask().getCurrentNumUnexploredDataChoices(); + } + return result; + } + + /** + * Get the percentage of unexplored choices that are data choices + * + * @return Percentage of unexplored choices that are data choices + */ + static double getUnexploredDataChoicesPercent() { + int totalUnexplored = getNumUnexploredChoices(); + if (totalUnexplored == 0) { + return 0; + } + + int numUnexploredData = getNumUnexploredDataChoices(); + return (numUnexploredData * 100.0) / totalUnexplored; + } + + public static void updateResult() { + if (status == STATUS.BUG_FOUND) { + return; + } + + String resultString = ""; + int maxStepBound = config.getMaxStepBound(); + int numUnexplored = getNumUnexploredChoices(); + if (getMaxSteps() < maxStepBound) { + if (numUnexplored == 0) { + resultString += "correct for any depth"; + } else { + resultString += String.format("partially correct with %d choices remaining", numUnexplored); + } + } else { + if (numUnexplored == 0) { + resultString += String.format("correct up to step %d", getMaxSteps()); + } else { + resultString += String.format("partially correct up to step %d with %d choices remaining", getMaxSteps(), numUnexplored); + } + } + result = resultString; + } + + public static void recordStats() { + // print basic statistics + StatWriter.log("#-schedules", String.format("%d", getTotalSchedules())); + StatWriter.log("#-timelines", String.format("%d", timelines.size())); + if (config.getStateCachingMode() != StateCachingMode.None) { + StatWriter.log("#-states", String.format("%d", getTotalStates())); + StatWriter.log("#-distinct-states", String.format("%d", stateCache.size())); + } + StatWriter.log("steps-min", String.format("%d", getMinSteps())); + StatWriter.log("steps-avg", String.format("%d", getTotalSteps() / getTotalSchedules())); + StatWriter.log("#-choices-unexplored", String.format("%d", getNumUnexploredChoices())); + StatWriter.log("%-choices-unexplored-data", String.format("%.1f", getUnexploredDataChoicesPercent())); + StatWriter.log("#-tasks-finished", String.format("%d", finishedTasks.size())); + StatWriter.log("#-tasks-pending", String.format("%d", pendingTasks.size())); + StatWriter.log("ql-#-states", String.format("%d", ChoiceSelectorQL.getChoiceQL().getNumStates())); + StatWriter.log("ql-#-actions", String.format("%d", ChoiceSelectorQL.getChoiceQL().getNumActions())); + } + + static void printCurrentStatus(double newRuntime) { + StringBuilder s = new StringBuilder("--------------------"); + s.append(String.format("\n Status after %.2f seconds:", newRuntime)); + s.append(String.format("\n Memory: %.2f MB", MemoryMonitor.getMemSpent())); + s.append(String.format("\n Schedules: %d", getTotalSchedules())); +// s.append(String.format("\n Unexplored: %d", getNumUnexploredChoices())); + s.append(String.format("\n RunningTasks: %d", runningTasks.size())); + s.append(String.format("\n FinishedTasks: %d", finishedTasks.size())); + s.append(String.format("\n PendingTasks: %d", pendingTasks.size())); + s.append(String.format("\n Timelines: %d", timelines.size())); + if (config.getStateCachingMode() != StateCachingMode.None) { + s.append(String.format("\n States: %d", getTotalStates())); + s.append(String.format("\n DistinctStates: %d", stateCache.size())); + } + ScratchLogger.log(s.toString()); + } + + public static void printProgressHeader() { + StringBuilder s = new StringBuilder(100); + s.append(StringUtils.center("Time", 11)); + s.append(StringUtils.center("Memory", 9)); + + s.append(StringUtils.center("Schedules", 12)); + s.append(StringUtils.center("Timelines", 12)); + s.append(StringUtils.center("Tasks (run/fin/pen)", 24)); +// s.append(StringUtils.center("Unexplored", 24)); + + if (config.getStateCachingMode() != StateCachingMode.None) { + s.append(StringUtils.center("States", 12)); + } + + System.out.println("--------------------"); + System.out.println(s); + } + + public static void printProgressFooter() { + System.out.println(); + } + + public static void printProgress(boolean forcePrint) { + if (forcePrint || (TimeMonitor.findInterval(lastReportTime) > 10)) { + lastReportTime = Instant.now(); + double newRuntime = TimeMonitor.getRuntime(); + printCurrentStatus(newRuntime); + long runtime = (long) (newRuntime * 1000); + String runtimeHms = + String.format( + "%02d:%02d:%02d", + TimeUnit.MILLISECONDS.toHours(runtime), + TimeUnit.MILLISECONDS.toMinutes(runtime) % TimeUnit.HOURS.toMinutes(1), + TimeUnit.MILLISECONDS.toSeconds(runtime) % TimeUnit.MINUTES.toSeconds(1)); + + StringBuilder s = new StringBuilder(100); + s.append('\r'); + s.append(StringUtils.center(String.format("%s", runtimeHms), 11)); + s.append( + StringUtils.center(String.format("%.1f GB", MemoryMonitor.getMemSpent() / 1024), 9)); + + s.append(StringUtils.center(String.format("%d", getTotalSchedules()), 12)); + s.append(StringUtils.center(String.format("%d", timelines.size()), 12)); + s.append(StringUtils.center(String.format("%d / %d / %d", + runningTasks.size(), finishedTasks.size(), pendingTasks.size()), + 24)); +// s.append( +// StringUtils.center( +// String.format( +// "%d (%.0f %% data)", getNumUnexploredChoices(), getUnexploredDataChoicesPercent()), +// 24)); + + if (config.getStateCachingMode() != StateCachingMode.None) { + s.append(StringUtils.center(String.format("%d", stateCache.size()), 12)); + } + + System.out.print(s); + } + } + + public static int getTotalSchedules() { + int result = 0; + for (ExplicitSearchScheduler sch : searchSchedulers.values()) { + result += sch.getStats().numSchedules; + } + return result; + } + + public static int getMinSteps() { + int result = -1; + for (ExplicitSearchScheduler sch : searchSchedulers.values()) { + if (result == -1 || result > sch.getStats().minSteps) { + result = sch.getStats().minSteps; + } + } + return result; + } + + public static int getMaxSteps() { + int result = -1; + for (ExplicitSearchScheduler sch : searchSchedulers.values()) { + if (result == -1 || result < sch.getStats().maxSteps) { + result = sch.getStats().maxSteps; + } + } + return result; + } + + public static int getTotalSteps() { + int result = 0; + for (ExplicitSearchScheduler sch : searchSchedulers.values()) { + result += sch.getStats().totalSteps; + } + return result; + } + + public static int getTotalStates() { + int result = 0; + for (ExplicitSearchScheduler sch : searchSchedulers.values()) { + result += sch.getStats().totalStates; + } + return result; + } } \ No newline at end of file diff --git a/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/PModel.java b/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/PModel.java index 7cc11025bf..e9c5b02f3a 100644 --- a/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/PModel.java +++ b/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/PModel.java @@ -1,39 +1,13 @@ package pex.runtime; -import pex.runtime.machine.PMachine; -import pex.runtime.machine.PMonitor; import pex.runtime.machine.PTestDriver; -import pex.values.PEvent; import java.io.Serializable; -import java.util.List; -import java.util.Map; /** * Interface of a PEx IR model/program. */ public interface PModel extends Serializable { - /** - * Get the start/main machine - * - * @return Machine - */ - PMachine getStart(); - - /** - * Get the mapping from events to monitors listening/observing an event - * - * @return - */ - Map> getListeners(); - - /** - * Get the list of monitors - * - * @return List of monitors - */ - List getMonitors(); - /** * Get the test driver * diff --git a/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/logger/PExLogger.java b/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/logger/PExLogger.java index 3ef8de20f2..c6f21c8a41 100644 --- a/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/logger/PExLogger.java +++ b/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/logger/PExLogger.java @@ -8,28 +8,12 @@ import org.apache.logging.log4j.core.layout.PatternLayout; import pex.runtime.PExGlobal; import pex.runtime.STATUS; -import pex.runtime.machine.PMachine; -import pex.runtime.machine.PMachineId; -import pex.runtime.machine.PMonitor; -import pex.runtime.machine.State; -import pex.runtime.machine.events.PContinuation; -import pex.runtime.scheduler.choice.ScheduleSearchUnit; -import pex.runtime.scheduler.choice.SearchUnit; -import pex.runtime.scheduler.explicit.ExplicitSearchScheduler; -import pex.runtime.scheduler.explicit.SearchStatistics; import pex.runtime.scheduler.explicit.StateCachingMode; -import pex.runtime.scheduler.explicit.strategy.SearchTask; -import pex.runtime.scheduler.replay.ReplayScheduler; +import pex.runtime.scheduler.explicit.strategy.SearchStrategyMode; import pex.utils.monitor.MemoryMonitor; -import pex.values.ComputeHash; -import pex.values.PEvent; -import pex.values.PMessage; -import pex.values.PValue; import java.io.PrintWriter; import java.io.StringWriter; -import java.util.List; -import java.util.SortedSet; /** * Represents the main PEx logger @@ -80,7 +64,7 @@ public static void logVerbose(String message) { * @param scheduler Explicit state search scheduler * @param timeSpent Time spent in seconds */ - public static void logEndOfRun(ExplicitSearchScheduler scheduler, long timeSpent) { + public static void logEndOfRun(long timeSpent) { if (verbosity == 0) { log.info(""); } @@ -91,17 +75,17 @@ public static void logEndOfRun(ExplicitSearchScheduler scheduler, long timeSpent } else { log.info("..... Found 0 bugs."); } - if (scheduler != null) { - log.info("... Scheduling statistics:"); + if (PExGlobal.getConfig().getSearchStrategyMode() != SearchStrategyMode.Replay) { + log.info("... Search statistics:"); if (PExGlobal.getConfig().getStateCachingMode() != StateCachingMode.None) { log.info(String.format("..... Explored %d distinct states over %d timelines", - SearchStatistics.totalDistinctStates, scheduler.getTimelines().size())); + PExGlobal.getStateCache().size(), PExGlobal.getTimelines().size())); } - log.info(String.format("..... Explored %d distinct schedules", SearchStatistics.iteration)); + log.info(String.format("..... Explored %d distinct schedules", PExGlobal.getTotalSchedules())); log.info(String.format("..... Finished %d search tasks (%d pending)", - scheduler.getSearchStrategy().getFinishedTasks().size(), scheduler.getSearchStrategy().getPendingTasks().size())); + PExGlobal.getFinishedTasks().size(), PExGlobal.getPendingTasks().size())); log.info(String.format("..... Number of steps explored: %d (min), %d (avg), %d (max).", - SearchStatistics.minSteps, (SearchStatistics.totalSteps / SearchStatistics.iteration), SearchStatistics.maxSteps)); + PExGlobal.getMinSteps(), (PExGlobal.getTotalSteps() / PExGlobal.getTotalSchedules()), PExGlobal.getMaxSteps())); } log.info(String.format("... Elapsed %d seconds and used %.1f GB", timeSpent, MemoryMonitor.getMaxMemSpent() / 1000.0)); log.info(String.format(".. Result: " + PExGlobal.getResult())); @@ -120,320 +104,4 @@ public static void logStackTrace(Exception e) { log.info("--------------------"); 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)); - } - } - - /** - * Log when the next task is selected - * - * @param task Next search task - */ - public static void logNextTask(SearchTask task) { - if (verbosity > 0) { - log.info(String.format(" Next task: %s", task.toStringDetailed())); - } - } - - public static void logNewTasks(List 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())); - } - } - } - - /** - * Log when serializing a task - * - * @param task Task to serialize - * @param szBytes Bytes written - */ - public static void logSerializeTask(SearchTask task, long szBytes) { - if (verbosity > 1) { - log.info(String.format(" %,.1f MB written in %s", (szBytes / 1024.0 / 1024.0), task.getSerializeFile())); - } - } - - /** - * Log when deserializing a task - * - * @param task Task that is deserialized - */ - public static void logDeserializeTask(SearchTask task) { - if (verbosity > 1) { - log.info(String.format(" Reading %s from %s", task, task.getSerializeFile())); - } - } - - /** - * Log at the start of an iteration - * - * @param iter Iteration number - * @param step Starting step number - */ - public static void logStartIteration(SearchTask task, int iter, int step) { - if (verbosity > 0) { - log.info("--------------------"); - log.info(String.format("[%s] Starting schedule %s from step %s", task, iter, step)); - } - } - - public static void logStartStep(int step, PMachine sender, PMessage msg) { - if (verbosity > 0) { - log.info(String.format( - " Step %d: %s sent %s to %s", - step, sender, msg.getEvent(), msg.getTarget())); - if (verbosity > 5) { - log.info(String.format(" payload: %s", msg.getPayload())); - } - } - } - - /** - * Log at the end of an iteration - * - * @param step Step number - */ - public static void logFinishedIteration(int step) { - if (verbosity > 0) { - log.info(String.format(" Schedule finished at step %d", step)); - } - } - - /** - * Log when backtracking to a search unit - * - * @param stepNum Step number - * @param choiceNum Choice number - * @param unit Search unit to which backtracking to - */ - public static void logBacktrack(int stepNum, int choiceNum, SearchUnit unit) { - if (verbosity > 1) { - log.info(String.format(" Backtracking to %s choice @%d::%d", - ((unit instanceof ScheduleSearchUnit) ? "schedule" : "data"), - stepNum, choiceNum)); - } - } - - public static void logNewScheduleChoice(List choices, int step, int idx) { - if (verbosity > 1) { - log.info(String.format(" @%d::%d new schedule choice: %s", step, idx, choices)); - } - } - - public static void logNewDataChoice(List> choices, int step, int idx) { - if (verbosity > 1) { - log.info(String.format(" @%d::%d new data choice: %s", step, idx, choices)); - } - } - - public static void logRepeatScheduleChoice(PMachine choice, int step, int idx) { - if (verbosity > 2) { - log.info(String.format(" @%d::%d %s (repeat)", step, idx, choice)); - } - } - - public static void logCurrentScheduleChoice(PMachine choice, int step, int idx) { - if (verbosity > 2) { - log.info(String.format(" @%d::%d %s", step, idx, choice)); - } - } - - public static void logRepeatDataChoice(PValue choice, int step, int idx) { - if (verbosity > 2) { - log.info(String.format(" @%d::%d %s (repeat)", step, idx, choice)); - } - } - - public static void logCurrentDataChoice(PValue choice, int step, int idx) { - if (verbosity > 2) { - log.info(String.format(" @%d::%d %s", step, idx, choice)); - } - } - - public static void logNewState(int step, int idx, Object stateKey, SortedSet machines) { - if (verbosity > 3) { - log.info(String.format(" @%d::%d new state with key %s", step, idx, stateKey)); - if (verbosity > 6) { - log.info(String.format(" %s", ComputeHash.getExactString(machines))); - } - } - } - - /** - * Log a new timeline - * - * @param sch Scheduler - */ - public static void logNewTimeline(ExplicitSearchScheduler sch) { - if (verbosity > 2) { - log.info(String.format(" new timeline %d", sch.getTimelines().size())); - if (verbosity > 4) { - log.info(String.format(" %s", sch.getStepState().getTimelineString())); - } - } - } - - private static boolean isReplaying() { - return (PExGlobal.getScheduler() instanceof ReplayScheduler); - } - - private static boolean typedLogEnabled() { - return (verbosity > 5) || isReplaying(); - } - - private static void typedLog(LogType type, String message) { - if (isReplaying()) { - TextWriter.typedLog(type, message); - } else { - log.info(String.format(" <%s> %s", type, message)); - } - } - - public static void logRunTest() { - if (typedLogEnabled()) { - typedLog(LogType.TestLog, String.format("Running test %s.", - PExGlobal.getConfig().getTestDriver())); - } - } - - public static void logModel(String message) { - if (verbosity > 0) { - log.info(message); - } - if (typedLogEnabled()) { - typedLog(LogType.PrintLog, message); - } - } - - public static void logBugFound(String message) { - if (typedLogEnabled()) { - typedLog(LogType.ErrorLog, message); - typedLog(LogType.StrategyLog, String.format("Found bug using '%s' strategy.", PExGlobal.getConfig().getSearchStrategyMode())); - typedLog(LogType.StrategyLog, "Checking statistics:"); - typedLog(LogType.StrategyLog, "Found 1 bug."); - } - } - - /** - * Log when a machine is created - * - * @param machine Machine that is created - * @param creator Machine that created this machine - */ - public static void logCreateMachine(PMachine machine, PMachine creator) { - PExGlobal.getScheduler().updateLogNumber(); - if (typedLogEnabled()) { - typedLog(LogType.CreateLog, String.format("%s was created by %s.", machine, creator)); - } - } - - public static void logSendEvent(PMachine sender, PMessage message) { - PExGlobal.getScheduler().updateLogNumber(); - if (typedLogEnabled()) { - String payloadMsg = ""; - if (message.getPayload() != null) { - payloadMsg = String.format(" with payload %s", message.getPayload()); - } - typedLog(LogType.SendLog, String.format("%s in state %s sent event %s%s to %s.", - sender, sender.getCurrentState(), message.getEvent(), payloadMsg, message.getTarget())); - } - } - - /** - * Log when a machine enters a new state - * - * @param machine Machine that is entering the state - */ - public static void logStateEntry(PMachine machine) { - PExGlobal.getScheduler().updateLogNumber(); - if (typedLogEnabled()) { - typedLog(LogType.StateLog, String.format("%s enters state %s.", machine, machine.getCurrentState())); - } - } - - /** - * Log when a machine exits the current state - * - * @param machine Machine that is exiting the state - */ - public static void logStateExit(PMachine machine) { - PExGlobal.getScheduler().updateLogNumber(); - if (typedLogEnabled()) { - typedLog(LogType.StateLog, String.format("%s exits state %s.", machine, machine.getCurrentState())); - } - } - - public static void logRaiseEvent(PMachine machine, PEvent event) { - PExGlobal.getScheduler().updateLogNumber(); - if (typedLogEnabled()) { - typedLog(LogType.RaiseLog, String.format("%s raised event %s in state %s.", machine, event, machine.getCurrentState())); - } - } - - public static void logStateTransition(PMachine machine, State newState) { - PExGlobal.getScheduler().updateLogNumber(); - if (typedLogEnabled()) { - typedLog(LogType.GotoLog, String.format("%s is transitioning from state %s to state %s.", machine, machine.getCurrentState(), newState)); - } - } - - public static void logReceive(PMachine machine, PContinuation continuation) { - PExGlobal.getScheduler().updateLogNumber(); - if (typedLogEnabled()) { - typedLog(LogType.ReceiveLog, String.format("%s is waiting to dequeue an event of type %s or %s in state %s.", - machine, continuation.getCaseEvents(), PEvent.haltEvent, machine.getCurrentState())); - } - } - - public static void logMonitorProcessEvent(PMonitor monitor, PMessage message) { - PExGlobal.getScheduler().updateLogNumber(); - if (typedLogEnabled()) { - typedLog(LogType.MonitorLog, String.format("%s is processing event %s in state %s.", - monitor, message.getEvent(), monitor.getCurrentState())); - } - } - - public static void logDequeueEvent(PMachine machine, PMessage message) { - PExGlobal.getScheduler().updateLogNumber(); - if (typedLogEnabled()) { - String payloadMsg = ""; - if (message.getPayload() != null) { - payloadMsg = String.format(" with payload %s", message.getPayload()); - } - typedLog(LogType.DequeueLog, String.format("%s dequeued event %s%s in state %s.", - machine, message.getEvent(), payloadMsg, machine.getCurrentState())); - } - } - - public static void logStartReplay() { - if (verbosity > 0) { - log.info("--------------------"); - log.info("Replaying schedule"); - } - } } diff --git a/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/logger/SchedulerLogger.java b/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/logger/SchedulerLogger.java new file mode 100644 index 0000000000..0bf0c662be --- /dev/null +++ b/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/logger/SchedulerLogger.java @@ -0,0 +1,411 @@ +package pex.runtime.logger; + +import lombok.Setter; +import org.apache.logging.log4j.LogManager; +import org.apache.logging.log4j.Logger; +import org.apache.logging.log4j.core.Appender; +import org.apache.logging.log4j.core.LoggerContext; +import org.apache.logging.log4j.core.appender.OutputStreamAppender; +import org.apache.logging.log4j.core.layout.PatternLayout; +import pex.runtime.PExGlobal; +import pex.runtime.machine.PMachine; +import pex.runtime.machine.PMachineId; +import pex.runtime.machine.PMonitor; +import pex.runtime.machine.State; +import pex.runtime.machine.events.PContinuation; +import pex.runtime.scheduler.choice.ScheduleSearchUnit; +import pex.runtime.scheduler.choice.SearchUnit; +import pex.runtime.scheduler.explicit.ExplicitSearchScheduler; +import pex.runtime.scheduler.explicit.strategy.SearchTask; +import pex.runtime.scheduler.replay.ReplayScheduler; +import pex.values.ComputeHash; +import pex.values.PEvent; +import pex.values.PMessage; +import pex.values.PValue; + +import java.io.*; +import java.util.List; +import java.util.SortedSet; + +/** + * Represents the logger for scheduler + */ +public class SchedulerLogger { + Logger log = null; + LoggerContext context = null; + @Setter + int verbosity; + + /** + * Initializes the logger with the given verbosity level. + */ + public SchedulerLogger(int schId) { + verbosity = PExGlobal.getConfig().getVerbosity(); + log = Log4JConfig.getContext().getLogger(SchedulerLogger.class.getName() + schId); + org.apache.logging.log4j.core.Logger coreLogger = + (org.apache.logging.log4j.core.Logger) LogManager.getLogger(SchedulerLogger.class.getName() + schId); + context = coreLogger.getContext(); + + try { + // get new file name + String fileName = PExGlobal.getConfig().getOutputFolder() + "/threads/" + schId + ".log"; + File file = new File(fileName); + file.getParentFile().mkdirs(); + file.createNewFile(); + + // Define new file printer + FileOutputStream fout = new FileOutputStream(fileName, false); + + PatternLayout layout = Log4JConfig.getPatternLayout(); + Appender fileAppender = + OutputStreamAppender.createAppender(layout, null, fout, fileName, false, true); + fileAppender.start(); + + context.getConfiguration().addLoggerAppender(coreLogger, fileAppender); + } catch (IOException e) { + System.out.println("Failed to set printer to the SchedulerLogger!!"); + } + } + + /** + * Logs the given message based on the current verbosity level. + * + * @param message Message to print + */ + public void logVerbose(String message) { + if (verbosity > 3) { + log.info(message); + } + } + + /** + * Log at the start of a search task + * + * @param task Search task + */ + public 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 void logEndTask(SearchTask task, int numSchedules) { + if (verbosity > 0) { + log.info(String.format(" Finished %s after exploring %d schedules", task, numSchedules)); + } + } + + /** + * Log when the next task is selected + * + * @param task Next search task + */ + public void logNextTask(SearchTask task) { + if (verbosity > 0) { + log.info(String.format(" Next task: %s", task.toStringDetailed())); + } + } + + public void logNewTasks(List 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())); + } + } + } + + /** + * Log when serializing a task + * + * @param task Task to serialize + * @param szBytes Bytes written + */ + public void logSerializeTask(SearchTask task, long szBytes) { + if (verbosity > 1) { + log.info(String.format(" %,.1f MB written in %s", (szBytes / 1024.0 / 1024.0), task.getSerializeFile())); + } + } + + /** + * Log when deserializing a task + * + * @param task Task that is deserialized + */ + public void logDeserializeTask(SearchTask task) { + if (verbosity > 1) { + log.info(String.format(" Reading %s from %s", task, task.getSerializeFile())); + } + } + + /** + * Log at the start of an iteration + * + * @param task Search task + * @param schId Scheduler id + * @param iter Schedule number + * @param step Starting step number + */ + public void logStartIteration(SearchTask task, int schId, int iter, int step) { + if (verbosity > 0) { + log.info("--------------------"); + log.info(String.format("[%d::%s] Starting schedule %s from step %s", schId, task, iter, step)); + } + } + + public void logStartStep(int step, PMachine sender, PMessage msg) { + if (verbosity > 0) { + log.info(String.format( + " Step %d: %s sent %s to %s", + step, sender, msg.getEvent(), msg.getTarget())); + if (verbosity > 5) { + log.info(String.format(" payload: %s", msg.getPayload())); + } + } + } + + /** + * Log at the end of an iteration + * + * @param step Step number + */ + public void logFinishedIteration(int step) { + if (verbosity > 0) { + log.info(String.format(" Schedule finished at step %d", step)); + } + } + + /** + * Log when backtracking to a search unit + * + * @param stepNum Step number + * @param choiceNum Choice number + * @param unit Search unit to which backtracking to + */ + public void logBacktrack(int stepNum, int choiceNum, SearchUnit unit) { + if (verbosity > 1) { + log.info(String.format(" Backtracking to %s choice @%d::%d", + ((unit instanceof ScheduleSearchUnit) ? "schedule" : "data"), + stepNum, choiceNum)); + } + } + + public void logNewScheduleChoice(List choices, int step, int idx) { + if (verbosity > 1) { + log.info(String.format(" @%d::%d new schedule choice: %s", step, idx, choices)); + } + } + + public void logNewDataChoice(List> choices, int step, int idx) { + if (verbosity > 1) { + log.info(String.format(" @%d::%d new data choice: %s", step, idx, choices)); + } + } + + public void logRepeatScheduleChoice(PMachine choice, int step, int idx) { + if (verbosity > 2) { + log.info(String.format(" @%d::%d %s (repeat)", step, idx, choice)); + } + } + + public void logCurrentScheduleChoice(PMachine choice, int step, int idx) { + if (verbosity > 2) { + log.info(String.format(" @%d::%d %s", step, idx, choice)); + } + } + + public void logRepeatDataChoice(PValue choice, int step, int idx) { + if (verbosity > 2) { + log.info(String.format(" @%d::%d %s (repeat)", step, idx, choice)); + } + } + + public void logCurrentDataChoice(PValue choice, int step, int idx) { + if (verbosity > 2) { + log.info(String.format(" @%d::%d %s", step, idx, choice)); + } + } + + public void logNewState(int step, int idx, Object stateKey, SortedSet machines) { + if (verbosity > 3) { + log.info(String.format(" @%d::%d new state with key %s", step, idx, stateKey)); + if (verbosity > 6) { + log.info(String.format(" %s", ComputeHash.getExactString(machines))); + } + } + } + + /** + * Log a new timeline + * + * @param sch Scheduler + */ + public void logNewTimeline(ExplicitSearchScheduler sch) { + if (verbosity > 2) { + log.info(String.format(" new timeline %d", PExGlobal.getTimelines().size())); + if (verbosity > 4) { + log.info(String.format(" %s", sch.getStepState().getTimelineString())); + } + } + } + + private boolean isReplaying() { + return (PExGlobal.getScheduler() instanceof ReplayScheduler); + } + + private boolean typedLogEnabled() { + return (verbosity > 5) || isReplaying(); + } + + private void typedLog(LogType type, String message) { + if (isReplaying()) { + TextWriter.typedLog(type, message); + } else { + log.info(String.format(" <%s> %s", type, message)); + } + } + + public void logRunTest() { + if (typedLogEnabled()) { + typedLog(LogType.TestLog, String.format("Running test %s.", + PExGlobal.getConfig().getTestDriver())); + } + } + + public void logModel(String message) { + if (verbosity > 0) { + log.info(message); + } + if (typedLogEnabled()) { + typedLog(LogType.PrintLog, message); + } + } + + public void logBugFound(String message) { + if (typedLogEnabled()) { + typedLog(LogType.ErrorLog, message); + typedLog(LogType.StrategyLog, String.format("Found bug using '%s' strategy.", PExGlobal.getConfig().getSearchStrategyMode())); + typedLog(LogType.StrategyLog, "Checking statistics:"); + typedLog(LogType.StrategyLog, "Found 1 bug."); + } + } + + /** + * Log when a machine is created + * + * @param machine Machine that is created + * @param creator Machine that created this machine + */ + public void logCreateMachine(PMachine machine, PMachine creator) { + PExGlobal.getScheduler().updateLogNumber(); + if (typedLogEnabled()) { + typedLog(LogType.CreateLog, String.format("%s was created by %s.", machine, creator)); + } + } + + public void logSendEvent(PMachine sender, PMessage message) { + PExGlobal.getScheduler().updateLogNumber(); + if (typedLogEnabled()) { + String payloadMsg = ""; + if (message.getPayload() != null) { + payloadMsg = String.format(" with payload %s", message.getPayload()); + } + typedLog(LogType.SendLog, String.format("%s in state %s sent event %s%s to %s.", + sender, sender.getCurrentState(), message.getEvent(), payloadMsg, message.getTarget())); + } + } + + /** + * Log when a machine enters a new state + * + * @param machine Machine that is entering the state + */ + public void logStateEntry(PMachine machine) { + PExGlobal.getScheduler().updateLogNumber(); + if (typedLogEnabled()) { + typedLog(LogType.StateLog, String.format("%s enters state %s.", machine, machine.getCurrentState())); + } + } + + /** + * Log when a machine exits the current state + * + * @param machine Machine that is exiting the state + */ + public void logStateExit(PMachine machine) { + PExGlobal.getScheduler().updateLogNumber(); + if (typedLogEnabled()) { + typedLog(LogType.StateLog, String.format("%s exits state %s.", machine, machine.getCurrentState())); + } + } + + public void logRaiseEvent(PMachine machine, PEvent event) { + PExGlobal.getScheduler().updateLogNumber(); + if (typedLogEnabled()) { + typedLog(LogType.RaiseLog, String.format("%s raised event %s in state %s.", machine, event, machine.getCurrentState())); + } + } + + public void logStateTransition(PMachine machine, State newState) { + PExGlobal.getScheduler().updateLogNumber(); + if (typedLogEnabled()) { + typedLog(LogType.GotoLog, String.format("%s is transitioning from state %s to state %s.", machine, machine.getCurrentState(), newState)); + } + } + + public void logReceive(PMachine machine, PContinuation continuation) { + PExGlobal.getScheduler().updateLogNumber(); + if (typedLogEnabled()) { + typedLog(LogType.ReceiveLog, String.format("%s is waiting to dequeue an event of type %s or %s in state %s.", + machine, continuation.getCaseEvents(), PEvent.haltEvent, machine.getCurrentState())); + } + } + + public void logMonitorProcessEvent(PMonitor monitor, PMessage message) { + PExGlobal.getScheduler().updateLogNumber(); + if (typedLogEnabled()) { + typedLog(LogType.MonitorLog, String.format("%s is processing event %s in state %s.", + monitor, message.getEvent(), monitor.getCurrentState())); + } + } + + public void logDequeueEvent(PMachine machine, PMessage message) { + PExGlobal.getScheduler().updateLogNumber(); + if (typedLogEnabled()) { + String payloadMsg = ""; + if (message.getPayload() != null) { + payloadMsg = String.format(" with payload %s", message.getPayload()); + } + typedLog(LogType.DequeueLog, String.format("%s dequeued event %s%s in state %s.", + machine, message.getEvent(), payloadMsg, machine.getCurrentState())); + } + } + + public void logStartReplay() { + if (verbosity > 0) { + log.info("--------------------"); + log.info("Replaying schedule"); + } + } + + /** + * Print error trace + * + * @param e Exception object + */ + public void logStackTrace(Exception e) { + StringWriter sw = new StringWriter(); + PrintWriter pw = new PrintWriter(sw); + e.printStackTrace(pw); + log.info("--------------------"); + log.info(sw.toString()); + } +} diff --git a/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/machine/PMachine.java b/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/machine/PMachine.java index 1e5a939e8d..96a9ddccac 100644 --- a/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/machine/PMachine.java +++ b/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/machine/PMachine.java @@ -2,7 +2,6 @@ import lombok.Getter; import pex.runtime.PExGlobal; -import pex.runtime.logger.PExLogger; import pex.runtime.machine.buffer.DeferQueue; import pex.runtime.machine.buffer.SenderQueue; import pex.runtime.machine.eventhandlers.EventHandler; @@ -23,9 +22,6 @@ * Represents the base class for all P machines. */ public abstract class PMachine implements Serializable, Comparable { - @Getter - private static final Map nameToMachine = new HashMap<>(); - protected static int globalMachineId = 1; @Getter protected final PMachineId pid; @Getter @@ -73,10 +69,12 @@ public abstract class PMachine implements Serializable, Comparable { public PMachine(String name, int id, State startState, State... states) { // initialize name, ids this.name = name; - this.instanceId = ++globalMachineId; + if (!(this instanceof PMonitor)) { + PExGlobal.setGlobalMachineId(PExGlobal.getGlobalMachineId() + 1); + } + this.instanceId = PExGlobal.getGlobalMachineId(); this.pid = new PMachineId(this.getClass(), id); this.pid.setName(this.toString()); - nameToMachine.put(toString(), this); // initialize states this.states = new HashSet<>(); @@ -352,7 +350,6 @@ public PMachineValue create( * Create a new machine instance * * @param machineType Machine type - * @param constructor Machine constructor * @return New machine as a PMachineValue */ public PMachineValue create( @@ -375,7 +372,7 @@ public void sendEvent(PMachineValue target, PEvent event, PValue payload) { PMessage msg = new PMessage(event, target.getValue(), payload); // log send event - PExLogger.logSendEvent(this, msg); + PExGlobal.getScheduler().getLogger().logSendEvent(this, msg); sendBuffer.add(msg); PExGlobal.getScheduler().runMonitors(msg); @@ -402,7 +399,7 @@ protected PContinuation registerContinuation( String name, SerializableBiFunction handleFun, String... caseEvents) { - PContinuation continuation = new PContinuation(handleFun, caseEvents); + PContinuation continuation = new PContinuation(name, handleFun, caseEvents); continuationMap.put(name, continuation); return continuation; } @@ -427,7 +424,7 @@ public void blockUntil(String continuationName) { blockedBy = continuationMap.get(continuationName); // log receive - PExLogger.logReceive(this, blockedBy); + PExGlobal.getScheduler().getLogger().logReceive(this, blockedBy); } public boolean isBlocked() { @@ -554,7 +551,7 @@ public void raiseEvent(PEvent event, PValue payload) { PMessage msg = new PMessage(event, this, payload); // log raise event - PExLogger.logRaiseEvent(this, event); + PExGlobal.getScheduler().getLogger().logRaiseEvent(this, event); // run the event (even if deferred) runEvent(msg); @@ -586,7 +583,7 @@ public void processStateTransition(State newState, PValue payload) { } // log state transition - PExLogger.logStateTransition(this, newState); + PExGlobal.getScheduler().getLogger().logStateTransition(this, newState); if (currentState != null) { // execute exit function of current state @@ -611,7 +608,7 @@ public void exitCurrentState() { blockedStateExit = null; - PExLogger.logStateExit(this); + PExGlobal.getScheduler().getLogger().logStateExit(this); currentState.exit(this); } @@ -627,7 +624,7 @@ public void enterNewState(State newState, PValue payload) { // change current state to new state currentState = newState; - PExLogger.logStateEntry(this); + PExGlobal.getScheduler().getLogger().logStateEntry(this); // change current state to new state newState.entry(this, payload); diff --git a/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/machine/PMonitor.java b/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/machine/PMonitor.java index 8fd85eba44..ff5d372efb 100644 --- a/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/machine/PMonitor.java +++ b/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/machine/PMonitor.java @@ -1,15 +1,11 @@ package pex.runtime.machine; +import pex.runtime.PExGlobal; + /** * Represents a P monitor. */ public class PMonitor extends PMachine { - /** - * Global monitor id - * Runs from -(#Monitors) to 0 - */ - protected static int globalMonitorId = 0; - /** * Monitor constructor * @@ -20,8 +16,8 @@ public class PMonitor extends PMachine { */ public PMonitor(String name, int id, State startState, State... states) { super(name, id, startState, states); - globalMachineId--; - this.instanceId = --globalMonitorId; + PExGlobal.setGlobalMonitorId(PExGlobal.getGlobalMonitorId() - 1); + this.instanceId = PExGlobal.getGlobalMonitorId(); } @Override diff --git a/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/machine/PTestDriver.java b/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/machine/PTestDriver.java index 6a337ba4b4..d9056e34ba 100644 --- a/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/machine/PTestDriver.java +++ b/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/machine/PTestDriver.java @@ -12,10 +12,11 @@ * Represents the base class for a P test driver. */ public abstract class PTestDriver implements Serializable { + // TODO: pex parallel - make fields thread safe public final Map, Class> interfaceMap; - public final List monitorList; - public final Map> observerMap; - public PMachine mainMachine; + public final List> monitorList; + public final Map>> observerMap; + public Class mainMachine; /** * Test driver constructor @@ -33,7 +34,7 @@ public PTestDriver() { * * @return the start/main machine of this test driver. */ - public PMachine getStart() { + public Class getStart() { return mainMachine; } @@ -42,7 +43,7 @@ public PMachine getStart() { * * @return List of monitors */ - public List getMonitors() { + public List> getMonitors() { return monitorList; } @@ -51,7 +52,7 @@ public List getMonitors() { * * @return Map from event to list of monitors listening/observing that event */ - public Map> getListeners() { + public Map>> getListeners() { return observerMap; } diff --git a/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/machine/events/PContinuation.java b/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/machine/events/PContinuation.java index 2c3447fb06..87ac74b9f5 100644 --- a/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/machine/events/PContinuation.java +++ b/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/machine/events/PContinuation.java @@ -16,12 +16,14 @@ @Getter public class PContinuation implements Serializable { + private final String name; private final Set caseEvents; private final SerializableBiFunction handleFun; @Getter private final Map> vars; - public PContinuation(SerializableBiFunction handleFun, String... ev) { + public PContinuation(String name, SerializableBiFunction handleFun, String... ev) { + this.name = name; this.handleFun = handleFun; this.caseEvents = new HashSet<>(Set.of(ev)); this.vars = new HashMap<>(); @@ -114,4 +116,26 @@ public void runAfter(PMachine machine) { } } + @Override + public int hashCode() { + return this.name.hashCode(); + } + + @Override + public boolean equals(Object obj) { + if (obj == this) return true; + else if (!(obj instanceof PContinuation)) { + return false; + } + if (this.name == null) { + return (((PContinuation) obj).name == null); + } + return this.name.equals(((PContinuation) obj).name); + } + + @Override + public String toString() { + return this.name; + } + } diff --git a/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/scheduler/Scheduler.java b/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/scheduler/Scheduler.java index 5163377e17..4b8e2bde87 100644 --- a/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/scheduler/Scheduler.java +++ b/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/scheduler/Scheduler.java @@ -3,7 +3,7 @@ import lombok.Getter; import lombok.Setter; import pex.runtime.PExGlobal; -import pex.runtime.logger.PExLogger; +import pex.runtime.logger.SchedulerLogger; import pex.runtime.machine.PMachine; import pex.runtime.machine.PMachineId; import pex.runtime.machine.PMonitor; @@ -14,8 +14,7 @@ import pex.values.*; import java.lang.reflect.InvocationTargetException; -import java.util.ArrayList; -import java.util.List; +import java.util.*; import java.util.concurrent.TimeoutException; /** @@ -27,6 +26,19 @@ public abstract class Scheduler implements SchedulerInterface { */ @Getter protected final Schedule schedule; + @Getter + protected final int schedulerId; + @Getter + protected final SchedulerLogger logger; + /** + * Mapping from machine type to list of all machine instances + */ + private final Map, List> machineListByType = new HashMap<>(); + /** + * Set of machines + */ + @Getter + private final SortedSet machineSet = new TreeSet<>(); /** * Step number */ @@ -48,12 +60,10 @@ public abstract class Scheduler implements SchedulerInterface { * Whether done with current iteration */ protected transient boolean isDoneStepping = false; - /** * Whether schedule terminated */ protected transient boolean scheduleTerminated = false; - @Getter @Setter protected transient int stepNumLogs = 0; @@ -65,15 +75,17 @@ public abstract class Scheduler implements SchedulerInterface { /** * Constructor */ - protected Scheduler(Schedule sch) { + protected Scheduler(int schedulerId, Schedule sch) { + this.schedulerId = schedulerId; this.schedule = sch; + this.logger = new SchedulerLogger(schedulerId); } /** * Constructor */ - protected Scheduler() { - this(new Schedule()); + protected Scheduler(int schedulerId) { + this(schedulerId, new Schedule()); } /** @@ -208,26 +220,20 @@ public PValue getRandomEntry(PMap map) { */ protected void start() { // start monitors first - for (PMonitor monitor : PExGlobal.getModel().getMonitors()) { - startMachine(monitor); + for (Class monitorType : PExGlobal.getModel().getTestDriver().getMonitors()) { + startMachine(monitorType); } // start main machine - startMachine(PExGlobal.getModel().getStart()); + startMachine(PExGlobal.getModel().getTestDriver().getStart()); } /** * Start a machine. * Runs the constructor of this machine. */ - public void startMachine(PMachine machine) { - if (!PExGlobal.getMachineSet().contains(machine)) { - // add machine to global context - PExGlobal.addGlobalMachine(machine, 0); - } - - // add machine to schedule - stepState.makeMachine(machine); + public void startMachine(Class machineType) { + PMachine machine = allocateMachine(machineType); // run create machine event processCreateEvent(new PMessage(PEvent.createMachine, machine, null)); @@ -252,7 +258,7 @@ public void executeStep(PMachine sender) { stepNumLogs = 0; // log start step - PExLogger.logStartStep(stepNumber, sender, msg); + logger.logStartStep(stepNumber, sender, msg); // process message processDequeueEvent(sender, msg); @@ -261,6 +267,41 @@ public void executeStep(PMachine sender) { isDoneStepping = (stepNumber >= PExGlobal.getConfig().getMaxStepBound()); } + /** + * Get a machine of a given type and index if exists, else return null. + * + * @param pid Machine pid + * @return Machine + */ + public PMachine getMachine(PMachineId pid) { + List machinesOfType = machineListByType.get(pid.getType()); + if (machinesOfType == null) { + return null; + } + if (pid.getTypeId() >= machinesOfType.size()) { + return null; + } + PMachine result = machineListByType.get(pid.getType()).get(pid.getTypeId()); + assert (machineSet.contains(result)); + return result; + } + + /** + * Add a machine. + * + * @param machine Machine to add + * @param machineCount Machine type count + */ + public void addMachine(PMachine machine, int machineCount) { + if (!machineListByType.containsKey(machine.getClass())) { + machineListByType.put(machine.getClass(), new ArrayList<>()); + } + assert (machineCount == machineListByType.get(machine.getClass()).size()); + machineListByType.get(machine.getClass()).add(machine); + machineSet.add(machine); + assert (machineListByType.get(machine.getClass()).get(machineCount) == machine); + } + /** * Allocate a machine * @@ -271,7 +312,7 @@ public PMachine allocateMachine(Class machineType) { // get machine count for given type from schedule int machineCount = stepState.getMachineCount(machineType); PMachineId pid = new PMachineId(machineType, machineCount); - PMachine machine = PExGlobal.getGlobalMachine(pid); + PMachine machine = getMachine(pid); if (machine == null) { // create a new machine try { @@ -280,7 +321,7 @@ public PMachine allocateMachine(Class machineType) { NoSuchMethodException e) { throw new RuntimeException(e); } - PExGlobal.addGlobalMachine(machine, machineCount); + addMachine(machine, machineCount); } // add machine to schedule @@ -294,11 +335,13 @@ public PMachine allocateMachine(Class machineType) { * @param message Message */ public void runMonitors(PMessage message) { - List listenersForEvent = PExGlobal.getModel().getListeners().get(message.getEvent()); + List> listenersForEvent = PExGlobal.getModel().getTestDriver().getListeners().get(message.getEvent()); if (listenersForEvent != null) { - for (PMonitor m : listenersForEvent) { + for (Class machineType : listenersForEvent) { + PMonitor m = (PMonitor) getMachine(new PMachineId(machineType, 0)); + // log monitor process event - PExLogger.logMonitorProcessEvent(m, message); + logger.logMonitorProcessEvent(m, message); m.processEventToCompletion(message.setTarget(m)); } @@ -322,10 +365,10 @@ public void processCreateEvent(PMessage message) { public void processDequeueEvent(PMachine sender, PMessage message) { if (message.getEvent().isCreateMachineEvent()) { // log create machine - PExLogger.logCreateMachine(message.getTarget(), sender); + logger.logCreateMachine(message.getTarget(), sender); } else { // log monitor process event - PExLogger.logDequeueEvent(message.getTarget(), message); + logger.logDequeueEvent(message.getTarget(), message); } message.getTarget().processEventToCompletion(message); @@ -349,7 +392,7 @@ public void announce(PEvent event, PValue payload) { * Check for deadlock at the end of a completed schedule */ public void checkDeadlock() { - for (PMachine machine : stepState.getMachineSet()) { + for (PMachine machine : stepState.getMachines()) { if (machine.canRun() && machine.isBlocked()) { Assert.deadlock(String.format("Deadlock detected. %s is waiting to receive an event, but no other controlled tasks are enabled.", machine)); } @@ -361,7 +404,9 @@ public void checkDeadlock() { */ public void checkLiveness(boolean terminated) { if (terminated) { - for (PMachine monitor : PExGlobal.getModel().getMonitors()) { + for (Class machineType : PExGlobal.getModel().getTestDriver().getMonitors()) { + PMonitor monitor = (PMonitor) getMachine(new PMachineId(machineType, 0)); + 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())); } diff --git a/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/scheduler/explicit/ExplicitSearchScheduler.java b/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/scheduler/explicit/ExplicitSearchScheduler.java index bb3fa7d80a..47d8d96e5c 100644 --- a/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/scheduler/explicit/ExplicitSearchScheduler.java +++ b/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/scheduler/explicit/ExplicitSearchScheduler.java @@ -2,19 +2,13 @@ import com.google.common.hash.Hashing; import lombok.Getter; -import lombok.Setter; -import org.apache.commons.lang3.StringUtils; import pex.runtime.PExGlobal; import pex.runtime.STATUS; -import pex.runtime.logger.PExLogger; -import pex.runtime.logger.ScratchLogger; -import pex.runtime.logger.StatWriter; import pex.runtime.machine.PMachine; import pex.runtime.machine.PMachineId; import pex.runtime.scheduler.Scheduler; import pex.runtime.scheduler.choice.ScheduleChoice; import pex.runtime.scheduler.choice.SearchUnit; -import pex.runtime.scheduler.explicit.choiceselector.ChoiceSelectorQL; import pex.runtime.scheduler.explicit.strategy.*; import pex.utils.exceptions.PExRuntimeException; import pex.utils.misc.Assert; @@ -23,8 +17,9 @@ import pex.values.ComputeHash; import pex.values.PValue; -import java.time.Instant; -import java.util.*; +import java.util.ArrayList; +import java.util.Collections; +import java.util.List; import java.util.concurrent.TimeUnit; import java.util.concurrent.TimeoutException; @@ -32,21 +27,13 @@ * Represents the scheduler for performing explicit-state model checking */ public class ExplicitSearchScheduler extends Scheduler { - /** - * Map from state hash to iteration when first visited - */ - private final transient Map stateCache = new HashMap<>(); - /** - * Set of timelines - */ - @Getter - private final transient Set timelines = new HashSet<>(); /** * Search strategy orchestrator */ @Getter - @Setter private final transient SearchStrategy searchStrategy; + @Getter + private final SchedulerStatistics stats = new SchedulerStatistics(); /** * Backtrack choice number */ @@ -60,19 +47,13 @@ public class ExplicitSearchScheduler extends Scheduler { * Whether to skip liveness check (because of early schedule termination due to state caching) */ private transient boolean skipLiveness = false; - /** - * Time of last status report - */ - @Getter - @Setter - private transient Instant lastReportTime = Instant.now(); /** * Constructor. */ - public ExplicitSearchScheduler() { - super(); + public ExplicitSearchScheduler(int schedulerId) { + super(schedulerId); switch (PExGlobal.getConfig().getSearchStrategyMode()) { case DepthFirst: searchStrategy = new SearchStrategyDfs(); @@ -88,47 +69,83 @@ public ExplicitSearchScheduler() { } } + /** + * Set next backtrack task with given orchestration mode + */ + public SearchTask waitForNextTask() throws InterruptedException { + SearchTask nextTask = null; + + while (true) { + if (PExGlobal.getRunningTasks().isEmpty() && PExGlobal.getPendingTasks().isEmpty()) { + // nothing running and no pending tasks, done + break; + } + + // try getting a next task + nextTask = searchStrategy.setNextTask(); + if (nextTask != null) { + // got a new next task + searchStrategy.setCurrTask(nextTask); + + // add next task to running task + assert (!PExGlobal.getRunningTasks().contains(nextTask)); + PExGlobal.getRunningTasks().add(nextTask); + + // setup for next task + logger.logNextTask(nextTask); + schedule.setChoices(nextTask.getPrefixChoices()); + postIterationCleanup(); + break; + } + + // no next task but there are running tasks, sleep and retry + TimeUnit.MILLISECONDS.sleep(100); + } + + return nextTask; + } + /** * Run the scheduler to perform explicit-state search. * * @throws TimeoutException Throws timeout exception if timeout is reached */ @Override - public void run() throws TimeoutException { - // log run test - PExLogger.logRunTest(); + public void run() throws TimeoutException, InterruptedException { + PExGlobal.registerSearchScheduler(schedulerId); - PExGlobal.setResult("incomplete"); - if (PExGlobal.getConfig().getVerbosity() == 0) { - printProgressHeader(true); - } - searchStrategy.createFirstTask(); + // log run test + logger.logRunTest(); while (true) { - PExLogger.logStartTask(searchStrategy.getCurrTask()); + if (PExGlobal.getStatus() == STATUS.SCHEDULEOUT) { + // schedule limit reached, done + break; + } + + // wait for the next task + SearchTask nextTask = waitForNextTask(); + if (nextTask == null) { + // nothing running and no pending tasks, done + break; + } + + // run the task + logger.logStartTask(searchStrategy.getCurrTask()); isDoneIterating = false; while (!isDoneIterating) { - SearchStatistics.iteration++; - PExLogger.logStartIteration(searchStrategy.getCurrTask(), SearchStatistics.iteration, stepNumber); + stats.numSchedules++; + searchStrategy.incrementCurrTaskNumSchedules(); + logger.logStartIteration(searchStrategy.getCurrTask(), schedulerId, stats.numSchedules, stepNumber); if (stepNumber == 0) { start(); } runIteration(); postProcessIteration(); } - PExLogger.logEndTask(searchStrategy.getCurrTask(), searchStrategy.getNumSchedulesInCurrTask()); + logger.logEndTask(searchStrategy.getCurrTask(), searchStrategy.getCurrTaskNumSchedules()); addRemainingChoicesAsChildrenTasks(); endCurrTask(); - - if (searchStrategy.getPendingTasks().isEmpty() || PExGlobal.getStatus() == STATUS.SCHEDULEOUT) { - // all tasks completed or schedule limit reached - break; - } - - // schedule limit not reached and there are pending tasks - // set the next task - SearchTask nextTask = setNextTask(); - assert (nextTask != null); } } @@ -143,17 +160,15 @@ protected void runIteration() throws TimeoutException { scheduleTerminated = false; skipLiveness = false; while (!isDoneStepping) { - printProgress(false); runStep(); } - printProgress(false); - SearchStatistics.totalSteps += stepNumber; - if (SearchStatistics.minSteps == -1 || stepNumber < SearchStatistics.minSteps) { - SearchStatistics.minSteps = stepNumber; + stats.totalSteps += stepNumber; + if (stats.minSteps == -1 || stepNumber < stats.minSteps) { + stats.minSteps = stepNumber; } - if (SearchStatistics.maxSteps == -1 || stepNumber > SearchStatistics.maxSteps) { - SearchStatistics.maxSteps = stepNumber; + if (stats.maxSteps == -1 || stepNumber > stats.maxSteps) { + stats.maxSteps = stepNumber; } if (scheduleTerminated) { @@ -170,7 +185,7 @@ protected void runIteration() throws TimeoutException { "Step bound of " + PExGlobal.getConfig().getMaxStepBound() + " reached."); if (PExGlobal.getConfig().getMaxSchedules() > 0) { - if (SearchStatistics.iteration >= PExGlobal.getConfig().getMaxSchedules()) { + if (PExGlobal.getTotalSchedules() >= PExGlobal.getConfig().getMaxSchedules()) { isDoneIterating = true; PExGlobal.setStatus(STATUS.SCHEDULEOUT); } @@ -193,7 +208,7 @@ protected void runStep() throws TimeoutException { scheduleTerminated = false; skipLiveness = true; isDoneStepping = true; - PExLogger.logFinishedIteration(stepNumber); + logger.logFinishedIteration(stepNumber); return; } @@ -204,10 +219,10 @@ protected void runStep() throws TimeoutException { // update timeline Object timeline = stepState.getTimeline(); - if (!timelines.contains(timeline)) { + if (!PExGlobal.getTimelines().contains(timeline)) { // add new timeline - PExLogger.logNewTimeline(this); - timelines.add(timeline); + logger.logNewTimeline(this); + PExGlobal.getTimelines().add(timeline); } // get a scheduling choice as sender machine @@ -218,7 +233,7 @@ protected void runStep() throws TimeoutException { scheduleTerminated = true; skipLiveness = false; isDoneStepping = true; - PExLogger.logFinishedIteration(stepNumber); + logger.logFinishedIteration(stepNumber); return; } @@ -242,26 +257,25 @@ boolean skipRemainingSchedule() { } // increment state count - SearchStatistics.totalStates++; + stats.totalStates++; // get state key Object stateKey = getCurrentStateKey(); // check if state key is present in state cache - Integer visitedAtIteration = stateCache.get(stateKey); + String visitedAt = PExGlobal.getStateCache().get(stateKey); + String stateVal = String.format("%d-%d", schedulerId, stats.numSchedules); - if (visitedAtIteration == null) { + if (visitedAt == null) { // not present, add to state cache - stateCache.put(stateKey, SearchStatistics.iteration); - // increment distinct state count - SearchStatistics.totalDistinctStates++; + PExGlobal.getStateCache().put(stateKey, stateVal); // log new state - PExLogger.logNewState(stepNumber, choiceNumber, stateKey, stepState.getMachineSet()); + logger.logNewState(stepNumber, choiceNumber, stateKey, stepState.getMachines()); } else { // present in state cache // check if possible cycle - if (visitedAtIteration == SearchStatistics.iteration) { + if (visitedAt == stateVal) { if (PExGlobal.getConfig().isFailOnMaxStepBound()) { // cycle detected since revisited same state at a different step in the same schedule Assert.cycle("Cycle detected: Infinite loop found due to revisiting a state multiple times in the same schedule"); @@ -284,12 +298,12 @@ boolean skipRemainingSchedule() { Object getCurrentStateKey() { Object stateKey; switch (PExGlobal.getConfig().getStateCachingMode()) { - case HashCode -> stateKey = ComputeHash.getHashCode(stepState.getMachineSet()); - case SipHash24 -> stateKey = ComputeHash.getHashCode(stepState.getMachineSet(), Hashing.sipHash24()); + case HashCode -> stateKey = ComputeHash.getHashCode(stepState.getMachines()); + case SipHash24 -> stateKey = ComputeHash.getHashCode(stepState.getMachines(), Hashing.sipHash24()); case Murmur3_128 -> - stateKey = ComputeHash.getHashCode(stepState.getMachineSet(), Hashing.murmur3_128((int) PExGlobal.getConfig().getRandomSeed())); - case Sha256 -> stateKey = ComputeHash.getHashCode(stepState.getMachineSet(), Hashing.sha256()); - case Exact -> stateKey = ComputeHash.getExactString(stepState.getMachineSet()); + stateKey = ComputeHash.getHashCode(stepState.getMachines(), Hashing.murmur3_128((int) PExGlobal.getConfig().getRandomSeed())); + case Sha256 -> stateKey = ComputeHash.getHashCode(stepState.getMachines(), Hashing.sha256()); + case Exact -> stateKey = ComputeHash.getExactString(stepState.getMachines()); default -> throw new PExRuntimeException(String.format("Unexpected state caching mode: %s", PExGlobal.getConfig().getStateCachingMode())); } @@ -316,8 +330,8 @@ public PMachine getNextScheduleChoice() { if (choiceNumber < backtrackChoiceNumber) { // pick the current schedule choice PMachineId pid = schedule.getCurrentScheduleChoice(choiceNumber); - result = PExGlobal.getGlobalMachine(pid); - PExLogger.logRepeatScheduleChoice(result, stepNumber, choiceNumber); + result = getMachine(pid); + logger.logRepeatScheduleChoice(result, stepNumber, choiceNumber); // increment choice number choiceNumber++; @@ -332,7 +346,7 @@ public PMachine getNextScheduleChoice() { choices = getNewScheduleChoices(); if (choices.size() > 1) { // log new choice - PExLogger.logNewScheduleChoice(choices, stepNumber, choiceNumber); + logger.logNewScheduleChoice(choices, stepNumber, choiceNumber); } if (choices.isEmpty()) { @@ -346,8 +360,8 @@ public PMachine getNextScheduleChoice() { // pick a choice int selected = PExGlobal.getChoiceSelector().selectChoice(this, choices); - result = PExGlobal.getGlobalMachine(choices.get(selected)); - PExLogger.logCurrentScheduleChoice(result, stepNumber, choiceNumber); + result = getMachine(choices.get(selected)); + logger.logCurrentScheduleChoice(result, stepNumber, choiceNumber); // remove the selected choice from unexplored choices choices.remove(selected); @@ -380,7 +394,7 @@ public PValue getNextDataChoice(List> input_choices) { // pick the current data choice result = schedule.getCurrentDataChoice(choiceNumber); assert (input_choices.contains(result)); - PExLogger.logRepeatDataChoice(result, stepNumber, choiceNumber); + logger.logRepeatDataChoice(result, stepNumber, choiceNumber); // increment choice number choiceNumber++; @@ -396,7 +410,7 @@ public PValue getNextDataChoice(List> input_choices) { choices = input_choices; if (choices.size() > 1) { // log new choice - PExLogger.logNewDataChoice(choices, stepNumber, choiceNumber); + logger.logNewDataChoice(choices, stepNumber, choiceNumber); } if (choices.isEmpty()) { @@ -411,7 +425,7 @@ public PValue getNextDataChoice(List> input_choices) { // pick a choice int selected = PExGlobal.getChoiceSelector().selectChoice(this, choices); result = choices.get(selected); - PExLogger.logCurrentDataChoice(result, stepNumber, choiceNumber); + logger.logCurrentDataChoice(result, stepNumber, choiceNumber); // remove the selected choice from unexplored choices choices.remove(selected); @@ -433,7 +447,10 @@ public PValue getNextDataChoice(List> input_choices) { private void postProcessIteration() { int maxSchedulesPerTask = PExGlobal.getConfig().getMaxSchedulesPerTask(); - if (maxSchedulesPerTask > 0 && searchStrategy.getNumSchedulesInCurrTask() >= maxSchedulesPerTask) { + if (PExGlobal.getConfig().getNumThreads() > 1 && searchStrategy.getCurrTaskId() == 0) { + // multi-threaded run, and this is the very first task + isDoneIterating = true; + } else if (maxSchedulesPerTask > 0 && searchStrategy.getCurrTaskNumSchedules() >= maxSchedulesPerTask) { isDoneIterating = true; } @@ -442,7 +459,7 @@ private void postProcessIteration() { } } - private void addRemainingChoicesAsChildrenTasks() { + private void addRemainingChoicesAsChildrenTasks() throws InterruptedException { SearchTask parentTask = searchStrategy.getCurrTask(); int numChildrenAdded = 0; for (int i : parentTask.getSearchUnitKeys(false)) { @@ -459,16 +476,17 @@ private void addRemainingChoicesAsChildrenTasks() { } } - PExLogger.logNewTasks(parentTask.getChildren()); + logger.logNewTasks(parentTask.getChildren()); } private void endCurrTask() { SearchTask currTask = searchStrategy.getCurrTask(); currTask.cleanup(); - searchStrategy.getFinishedTasks().add(currTask.getId()); + PExGlobal.getFinishedTasks().add(currTask); + PExGlobal.getRunningTasks().remove(currTask); } - private void setChildTask(SearchUnit unit, int choiceNum, SearchTask parentTask, boolean isExact) { + private void setChildTask(SearchUnit unit, int choiceNum, SearchTask parentTask, boolean isExact) throws InterruptedException { SearchTask newTask = searchStrategy.createTask(parentTask); int maxChoiceNum = choiceNum; @@ -492,46 +510,9 @@ private void setChildTask(SearchUnit unit, int choiceNum, SearchTask parentTask, newTask.writeToFile(); parentTask.addChild(newTask); - searchStrategy.getPendingTasks().add(newTask.getId()); searchStrategy.addNewTask(newTask); } - /** - * Set next backtrack task with given orchestration mode - */ - public SearchTask setNextTask() { - SearchTask nextTask = searchStrategy.setNextTask(); - if (nextTask != null) { - PExLogger.logNextTask(nextTask); - schedule.setChoices(nextTask.getPrefixChoices()); - postIterationCleanup(); - } - return nextTask; - } - - public int getNumUnexploredChoices() { - return searchStrategy.getCurrTask().getCurrentNumUnexploredChoices() + searchStrategy.getNumPendingChoices(); - } - - public int getNumUnexploredDataChoices() { - return searchStrategy.getCurrTask().getCurrentNumUnexploredDataChoices() + searchStrategy.getNumPendingDataChoices(); - } - - /** - * Get the percentage of unexplored choices that are data choices - * - * @return Percentage of unexplored choices that are data choices - */ - public double getUnexploredDataChoicesPercent() { - int totalUnexplored = getNumUnexploredChoices(); - if (totalUnexplored == 0) { - return 0; - } - - int numUnexploredData = getNumUnexploredDataChoices(); - return (numUnexploredData * 100.0) / totalUnexplored; - } - private void postIterationCleanup() { SearchTask task = searchStrategy.getCurrTask(); for (int cIdx : task.getSearchUnitKeys(true)) { @@ -552,15 +533,15 @@ private void postIterationCleanup() { } if (newStepNumber == 0) { reset(); - stepState.resetToZero(); + stepState.resetToZero(getMachineSet()); } else { stepNumber = newStepNumber; choiceNumber = scheduleChoice.getChoiceNumber(); - stepState.setTo(scheduleChoice.getChoiceState()); - assert (!PExGlobal.getGlobalMachine(scheduleChoice.getCurrent()).getSendBuffer().isEmpty()); + stepState.setTo(getMachineSet(), scheduleChoice.getChoiceState()); + assert (!getMachine(scheduleChoice.getCurrent()).getSendBuffer().isEmpty()); } schedule.removeChoicesAfter(backtrackChoiceNumber); - PExLogger.logBacktrack(newStepNumber, cIdx, unit); + logger.logBacktrack(newStepNumber, cIdx, unit); return; } schedule.clear(); @@ -569,7 +550,7 @@ private void postIterationCleanup() { private List getNewScheduleChoices() { // prioritize create machine events - for (PMachine machine : stepState.getMachineSet()) { + for (PMachine machine : stepState.getMachines()) { if (machine.getSendBuffer().nextIsCreateMachineMsg()) { return new ArrayList<>(Collections.singletonList(machine.getPid())); } @@ -578,7 +559,7 @@ private List getNewScheduleChoices() { // now there are no create machine events remaining List choices = new ArrayList<>(); - for (PMachine machine : stepState.getMachineSet()) { + for (PMachine machine : stepState.getMachines()) { if (machine.getSendBuffer().nextHasTargetRunning()) { choices.add(machine.getPid()); } @@ -586,136 +567,4 @@ private List getNewScheduleChoices() { return choices; } - - public void updateResult() { - if (PExGlobal.getStatus() == STATUS.BUG_FOUND) { - return; - } - - String result = ""; - int maxStepBound = PExGlobal.getConfig().getMaxStepBound(); - int numUnexplored = getNumUnexploredChoices(); - if (SearchStatistics.maxSteps < maxStepBound) { - if (numUnexplored == 0) { - result += "correct for any depth"; - } else { - result += String.format("partially correct with %d choices remaining", numUnexplored); - } - } else { - if (numUnexplored == 0) { - result += String.format("correct up to step %d", SearchStatistics.maxSteps); - } else { - result += String.format("partially correct up to step %d with %d choices remaining", SearchStatistics.maxSteps, numUnexplored); - } - - } - PExGlobal.setResult(result); - } - - public void recordStats() { - printProgress(true); - - // print basic statistics - StatWriter.log("#-schedules", String.format("%d", SearchStatistics.iteration)); - StatWriter.log("#-timelines", String.format("%d", timelines.size())); - if (PExGlobal.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("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())); - 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) { - StringBuilder s = new StringBuilder("--------------------"); - s.append(String.format("\n Status after %.2f seconds:", newRuntime)); - s.append(String.format("\n Memory: %.2f MB", MemoryMonitor.getMemSpent())); - s.append(String.format("\n Step: %d", stepNumber)); - s.append(String.format("\n Schedules: %d", SearchStatistics.iteration)); - 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 (PExGlobal.getConfig().getStateCachingMode() != StateCachingMode.None) { - s.append(String.format("\n States: %d", SearchStatistics.totalStates)); - s.append(String.format("\n DistinctStates: %d", SearchStatistics.totalDistinctStates)); - } - ScratchLogger.log(s.toString()); - } - - private void printProgressHeader(boolean consolePrint) { - StringBuilder s = new StringBuilder(100); - s.append(StringUtils.center("Time", 11)); - s.append(StringUtils.center("Memory", 9)); - 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 (PExGlobal.getConfig().getStateCachingMode() != StateCachingMode.None) { - s.append(StringUtils.center("States", 12)); - } - - if (consolePrint) { - System.out.println("--------------------"); - System.out.println(s); - } else { - PExLogger.logVerbose("--------------------"); - PExLogger.logVerbose(s.toString()); - } - } - - protected void printProgress(boolean forcePrint) { - if (forcePrint || (TimeMonitor.findInterval(getLastReportTime()) > 10)) { - setLastReportTime(Instant.now()); - double newRuntime = TimeMonitor.getRuntime(); - printCurrentStatus(newRuntime); - boolean consolePrint = (PExGlobal.getConfig().getVerbosity() == 0); - if (consolePrint || forcePrint) { - long runtime = (long) (newRuntime * 1000); - String runtimeHms = - String.format( - "%02d:%02d:%02d", - TimeUnit.MILLISECONDS.toHours(runtime), - TimeUnit.MILLISECONDS.toMinutes(runtime) % TimeUnit.HOURS.toMinutes(1), - TimeUnit.MILLISECONDS.toSeconds(runtime) % TimeUnit.MINUTES.toSeconds(1)); - - StringBuilder s = new StringBuilder(100); - if (consolePrint) { - s.append('\r'); - } else { - printProgressHeader(false); - } - s.append(StringUtils.center(String.format("%s", runtimeHms), 11)); - s.append( - StringUtils.center(String.format("%.1f GB", MemoryMonitor.getMemSpent() / 1024), 9)); - 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( - "%d (%.0f %% data)", getNumUnexploredChoices(), getUnexploredDataChoicesPercent()), - 24)); - - if (PExGlobal.getConfig().getStateCachingMode() != StateCachingMode.None) { - s.append(StringUtils.center(String.format("%d", SearchStatistics.totalDistinctStates), 12)); - } - - if (consolePrint) { - System.out.print(s); - } else { - PExLogger.logVerbose(s.toString()); - } - } - } - } } diff --git a/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/scheduler/explicit/SchedulerStatistics.java b/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/scheduler/explicit/SchedulerStatistics.java new file mode 100644 index 0000000000..658ca3768c --- /dev/null +++ b/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/scheduler/explicit/SchedulerStatistics.java @@ -0,0 +1,31 @@ +package pex.runtime.scheduler.explicit; + +public class SchedulerStatistics { + /** + * Number of schedules + */ + public int numSchedules = 0; + + /** + * Min steps + */ + public int minSteps = 0; + + /** + * Max steps + */ + public int maxSteps = 0; + + /** + * Total steps + */ + public int totalSteps = 0; + + /** + * Total number of states visited + */ + public int totalStates = 0; + + public SchedulerStatistics() { + } +} diff --git a/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/scheduler/explicit/SearchStatistics.java b/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/scheduler/explicit/SearchStatistics.java deleted file mode 100644 index e1068e1218..0000000000 --- a/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/scheduler/explicit/SearchStatistics.java +++ /dev/null @@ -1,33 +0,0 @@ -package pex.runtime.scheduler.explicit; - -public class SearchStatistics { - /** - * Current iteration - */ - public static int iteration = 0; - - /** - * Min steps - */ - public static int minSteps = 0; - - /** - * Max steps - */ - public static int maxSteps = 0; - - /** - * Total steps - */ - public static int totalSteps = 0; - - /** - * Total number of states visited - */ - public static int totalStates = 0; - - /** - * Total number of distinct states visited - */ - public static int totalDistinctStates = 0; -} diff --git a/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/scheduler/explicit/StepState.java b/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/scheduler/explicit/StepState.java index 2774644c8d..8fad8dadf7 100644 --- a/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/scheduler/explicit/StepState.java +++ b/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/scheduler/explicit/StepState.java @@ -1,7 +1,6 @@ package pex.runtime.scheduler.explicit; import lombok.Getter; -import pex.runtime.PExGlobal; import pex.runtime.machine.MachineLocalState; import pex.runtime.machine.PMachine; @@ -16,7 +15,7 @@ public class StepState implements Serializable { * Set of machines */ @Getter - private SortedSet machineSet = new TreeSet<>(); + private SortedSet machines = new TreeSet<>(); /** * Local state of each machine (if present in machineSet) @@ -26,36 +25,36 @@ public class StepState implements Serializable { public StepState copyState() { StepState stepState = new StepState(); - stepState.machineSet = new TreeSet<>(this.machineSet); + stepState.machines = new TreeSet<>(this.machines); stepState.machineLocalStates = new HashMap<>(); - for (PMachine machine : this.machineSet) { + for (PMachine machine : this.machines) { stepState.machineLocalStates.put(machine, machine.copyMachineState()); } - assert (stepState.machineSet.size() == stepState.machineLocalStates.size()); + assert (stepState.machines.size() == stepState.machineLocalStates.size()); return stepState; } public void clear() { - machineSet.clear(); + machines.clear(); machineLocalStates.clear(); } - public void resetToZero() { - for (PMachine machine : PExGlobal.getMachineSet()) { + public void resetToZero(SortedSet allMachines) { + for (PMachine machine : allMachines) { machine.reset(); } - machineSet.clear(); + machines.clear(); } - public void setTo(StepState input) { - machineSet = new TreeSet<>(input.machineSet); + public void setTo(SortedSet allMachines, StepState input) { + machines = new TreeSet<>(input.machines); machineLocalStates = new HashMap<>(input.machineLocalStates); - assert (machineSet.size() == machineLocalStates.size()); + assert (machines.size() == machineLocalStates.size()); - for (PMachine machine : PExGlobal.getMachineSet()) { + for (PMachine machine : allMachines) { MachineLocalState ms = machineLocalStates.get(machine); if (ms == null) { machine.reset(); @@ -71,7 +70,7 @@ public void setTo(StepState input) { * @param machine Machine to add */ public void makeMachine(PMachine machine) { - machineSet.add(machine); + machines.add(machine); } /** @@ -82,7 +81,7 @@ public void makeMachine(PMachine machine) { */ public int getMachineCount(Class type) { int result = 0; - for (PMachine m : machineSet) { + for (PMachine m : machines) { if (type.isInstance(m)) { result++; } @@ -97,7 +96,7 @@ public Object getTimeline() { public String getTimelineString() { StringBuilder s = new StringBuilder(); - for (PMachine m : machineSet) { + for (PMachine m : machines) { MachineLocalState ms = machineLocalStates.get(m); if (ms != null) { s.append(String.format("%s -> %s, ", m, ms.getHappensBeforePairs())); @@ -113,7 +112,7 @@ public String toString() { } StringBuilder s = new StringBuilder(); - for (PMachine machine : machineSet) { + for (PMachine machine : machines) { s.append(String.format("%s:\n", machine)); List fields = machine.getLocalVarNames(); List values = machineLocalStates.get(machine).getLocals(); diff --git a/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/scheduler/explicit/choiceselector/ChoiceQL.java b/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/scheduler/explicit/choiceselector/ChoiceQL.java index 6d330f98eb..69b8f934d5 100644 --- a/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/scheduler/explicit/choiceselector/ChoiceQL.java +++ b/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/scheduler/explicit/choiceselector/ChoiceQL.java @@ -1,7 +1,7 @@ package pex.runtime.scheduler.explicit.choiceselector; import lombok.Getter; -import pex.runtime.logger.PExLogger; +import pex.runtime.PExGlobal; import pex.utils.random.RandomNumberGenerator; import java.io.Serializable; @@ -81,10 +81,10 @@ public int getNumActions() { public void printQTable() { - PExLogger.logVerbose("--------------------"); - PExLogger.logVerbose("Q Table"); - PExLogger.logVerbose("--------------------"); - PExLogger.logVerbose(String.format(" #QStates = %d", qValues.size())); + PExGlobal.getScheduler().getLogger().logVerbose("--------------------"); + PExGlobal.getScheduler().getLogger().logVerbose("Q Table"); + PExGlobal.getScheduler().getLogger().logVerbose("--------------------"); + PExGlobal.getScheduler().getLogger().logVerbose(String.format(" #QStates = %d", qValues.size())); for (S state : qValues.getStates()) { ChoiceQTable.ChoiceQStateEntry stateEntry = qValues.get(state); String stateStr = String.valueOf(state); @@ -101,7 +101,7 @@ public void printQTable() { Object bestAction = classEntry.getBestAction(); if (bestAction != null) { double maxQ = classEntry.get(bestAction); - PExLogger.logVerbose( + PExGlobal.getScheduler().getLogger().logVerbose( String.format( " %s [%s] -> %s -> %.2f\t%s", stateStr, cls.getSimpleName(), bestAction, maxQ, classEntry)); diff --git a/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/scheduler/explicit/choiceselector/ChoiceSelectorQL.java b/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/scheduler/explicit/choiceselector/ChoiceSelectorQL.java index f23a3feede..92410420ed 100644 --- a/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/scheduler/explicit/choiceselector/ChoiceSelectorQL.java +++ b/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/scheduler/explicit/choiceselector/ChoiceSelectorQL.java @@ -2,6 +2,7 @@ import lombok.Getter; import lombok.Setter; +import pex.runtime.PExGlobal; import pex.runtime.scheduler.explicit.ExplicitSearchScheduler; import pex.utils.random.RandomNumberGenerator; @@ -36,7 +37,7 @@ protected int select(ExplicitSearchScheduler sch, List choices) { } Object timeline = sch.getStepState().getTimeline(); - if (!sch.getTimelines().contains(timeline)) { + if (!PExGlobal.getTimelines().contains(timeline)) { // reward new timeline choiceQL.rewardNewTimeline(state, choices.get(selected)); } else { diff --git a/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/scheduler/explicit/strategy/SearchStrategy.java b/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/scheduler/explicit/strategy/SearchStrategy.java index 85f31e0321..d199b82bac 100644 --- a/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/scheduler/explicit/strategy/SearchStrategy.java +++ b/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/scheduler/explicit/strategy/SearchStrategy.java @@ -1,116 +1,90 @@ package pex.runtime.scheduler.explicit.strategy; import lombok.Getter; -import pex.runtime.scheduler.explicit.SearchStatistics; +import pex.runtime.PExGlobal; import java.io.Serializable; -import java.util.ArrayList; -import java.util.HashSet; -import java.util.List; -import java.util.Set; +import java.util.concurrent.Semaphore; @Getter public abstract class SearchStrategy implements Serializable { - /** - * List of all search tasks - */ - final List allTasks = new ArrayList<>(); - /** - * Set of all search tasks that are pending - */ - final Set pendingTasks = new HashSet<>(); - /** - * List of all search tasks that finished - */ - final List finishedTasks = new ArrayList<>(); + private static final Semaphore sem = new Semaphore(1); + /** * Task id of the latest search task */ int currTaskId = 0; /** - * Starting iteration number for the current task + * Number of schedules for the current task */ - int currTaskStartIteration = 0; + int currTaskNumSchedules = 0; - public SearchTask createTask(SearchTask parentTask) { - SearchTask newTask = new SearchTask(allTasks.size(), parentTask); - allTasks.add(newTask); - return newTask; + public SearchTask getCurrTask() { + return getTask(currTaskId); } - public void createFirstTask() { - assert (allTasks.size() == 0); - SearchTask firstTask = createTask(null); - pendingTasks.add(firstTask.getId()); - setCurrTask(firstTask); + public void setCurrTask(SearchTask task) { + currTaskId = task.getId(); + currTaskNumSchedules = 0; } - public SearchTask getCurrTask() { - return getTask(currTaskId); + public void incrementCurrTaskNumSchedules() { + currTaskNumSchedules++; } - private void setCurrTask(SearchTask task) { - assert (pendingTasks.contains(task.getId())); - pendingTasks.remove(task.getId()); - currTaskId = task.getId(); - currTaskStartIteration = SearchStatistics.iteration; + public SearchTask setNextTask() throws InterruptedException { + SearchTask nextTask = popNextTask(); + if (nextTask != null) { + if (nextTask.getId() != 0) { + // not the very first task, read from file + nextTask.readFromFile(); + } + } + return nextTask; } - public int getNumSchedulesInCurrTask() { - return SearchStatistics.iteration - currTaskStartIteration; + public SearchTask createTask(SearchTask parentTask) throws InterruptedException { + sem.acquire(); + SearchTask newTask = new SearchTask(PExGlobal.getAllTasks().size(), parentTask); + PExGlobal.getAllTasks().put(newTask.getId(), newTask); + sem.release(); + return newTask; } + public void createFirstTask() throws InterruptedException { + assert (PExGlobal.getAllTasks().size() == 0); + SearchTask firstTask = createTask(null); + addNewTask(firstTask); + } private boolean isValidTaskId(int id) { - return (id < allTasks.size()); + return (id < PExGlobal.getAllTasks().size()) && (PExGlobal.getAllTasks().containsKey(id)); } protected SearchTask getTask(int id) { assert (isValidTaskId(id)); - return allTasks.get(id); - } - - public SearchTask setNextTask() { - if (pendingTasks.isEmpty()) { - return null; - } - - SearchTask nextTask = popNextTask(); - nextTask.readFromFile(); - setCurrTask(nextTask); - - return nextTask; + return PExGlobal.getAllTasks().get(id); } - /** - * Get the number of unexplored choices in the pending tasks - * - * @return Number of unexplored choices - */ - public int getNumPendingChoices() { - int numUnexplored = 0; - for (Integer tid : pendingTasks) { - SearchTask task = getTask(tid); - numUnexplored += task.getTotalUnexploredChoices(); - } - return numUnexplored; + public void addNewTask(SearchTask task) throws InterruptedException { + sem.acquire(); + addTask(task); + sem.release(); } - /** - * Get the number of unexplored data choices in the pending tasks - * - * @return Number of unexplored data choices - */ - public int getNumPendingDataChoices() { - int numUnexplored = 0; - for (Integer tid : pendingTasks) { - SearchTask task = getTask(tid); - numUnexplored += task.getTotalUnexploredDataChoices(); + SearchTask popNextTask() throws InterruptedException { + sem.acquire(); + SearchTask task; + if (PExGlobal.getPendingTasks().isEmpty()) { + task = null; + } else { + task = popTask(); } - return numUnexplored; + sem.release(); + return task; } - abstract SearchTask popNextTask(); + abstract SearchTask popTask(); - public abstract void addNewTask(SearchTask task); + abstract void addTask(SearchTask task); } diff --git a/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/scheduler/explicit/strategy/SearchStrategyAStar.java b/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/scheduler/explicit/strategy/SearchStrategyAStar.java index 5ecb0027ca..8ffb8c4a6a 100644 --- a/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/scheduler/explicit/strategy/SearchStrategyAStar.java +++ b/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/scheduler/explicit/strategy/SearchStrategyAStar.java @@ -1,28 +1,32 @@ package pex.runtime.scheduler.explicit.strategy; +import pex.runtime.PExGlobal; + import java.util.Comparator; import java.util.concurrent.PriorityBlockingQueue; public class SearchStrategyAStar extends SearchStrategy { - private final PriorityBlockingQueue elements; + private static final PriorityBlockingQueue elements = + new PriorityBlockingQueue( + 100, + new Comparator() { + public int compare(SearchTask a, SearchTask b) { + return Integer.compare(a.getCurrChoiceNumber(), b.getCurrChoiceNumber()); + } + }); public SearchStrategyAStar() { - elements = - new PriorityBlockingQueue( - 100, - new Comparator() { - public int compare(SearchTask a, SearchTask b) { - return Integer.compare(a.getCurrChoiceNumber(), b.getCurrChoiceNumber()); - } - }); } - public void addNewTask(SearchTask task) { + public void addTask(SearchTask task) { + PExGlobal.getPendingTasks().add(task); elements.offer(task); } - public SearchTask popNextTask() { + public SearchTask popTask() { assert (!elements.isEmpty()); - return elements.poll(); + SearchTask task = elements.poll(); + PExGlobal.getPendingTasks().remove(task); + return task; } } diff --git a/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/scheduler/explicit/strategy/SearchStrategyDfs.java b/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/scheduler/explicit/strategy/SearchStrategyDfs.java index 1e577ef8a4..19319160c6 100644 --- a/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/scheduler/explicit/strategy/SearchStrategyDfs.java +++ b/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/scheduler/explicit/strategy/SearchStrategyDfs.java @@ -1,14 +1,19 @@ package pex.runtime.scheduler.explicit.strategy; +import pex.runtime.PExGlobal; + public class SearchStrategyDfs extends SearchStrategy { public SearchStrategyDfs() { } - public void addNewTask(SearchTask task) { + public void addTask(SearchTask task) { + PExGlobal.getPendingTasks().add(task); } - public SearchTask popNextTask() { - assert (pendingTasks.size() == 1); - return getTask(pendingTasks.iterator().next()); + public SearchTask popTask() { + assert (PExGlobal.getPendingTasks().size() == 1); + SearchTask task = PExGlobal.getPendingTasks().iterator().next(); + PExGlobal.getPendingTasks().remove(task); + return task; } } diff --git a/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/scheduler/explicit/strategy/SearchStrategyRandom.java b/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/scheduler/explicit/strategy/SearchStrategyRandom.java index 9c43decb6e..72ba9825e9 100644 --- a/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/scheduler/explicit/strategy/SearchStrategyRandom.java +++ b/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/scheduler/explicit/strategy/SearchStrategyRandom.java @@ -1,31 +1,31 @@ package pex.runtime.scheduler.explicit.strategy; +import pex.runtime.PExGlobal; import pex.utils.random.RandomNumberGenerator; -import java.util.*; +import java.util.ArrayList; +import java.util.Collections; +import java.util.List; +import java.util.Random; public class SearchStrategyRandom extends SearchStrategy { - private final List elementList; - private final Set elementSet; + private static final List elementList = new ArrayList<>(); public SearchStrategyRandom() { - elementList = new ArrayList<>(); - elementSet = new HashSet<>(); } - public void addNewTask(SearchTask task) { - assert (!elementSet.contains(task)); + public void addTask(SearchTask task) { + PExGlobal.getPendingTasks().add(task); elementList.add(task); - elementSet.add(task); } - public SearchTask popNextTask() { + public SearchTask popTask() { assert (!elementList.isEmpty()); Collections.shuffle( elementList, new Random(RandomNumberGenerator.getInstance().getRandomLong())); SearchTask result = elementList.get(0); elementList.remove(0); - elementSet.remove(result); + PExGlobal.getPendingTasks().remove(result); return result; } } diff --git a/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/scheduler/explicit/strategy/SearchTask.java b/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/scheduler/explicit/strategy/SearchTask.java index 8ea5110160..5c8ace3766 100644 --- a/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/scheduler/explicit/strategy/SearchTask.java +++ b/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/scheduler/explicit/strategy/SearchTask.java @@ -2,7 +2,6 @@ import lombok.Getter; import pex.runtime.PExGlobal; -import pex.runtime.logger.PExLogger; import pex.runtime.machine.PMachineId; import pex.runtime.scheduler.choice.Choice; import pex.runtime.scheduler.choice.DataSearchUnit; @@ -250,7 +249,7 @@ public void writeToFile() { oos.writeObject(this.prefixChoices); oos.writeObject(this.searchUnits); long szBytes = Files.size(Paths.get(serializeFile)); - PExLogger.logSerializeTask(this, szBytes); + PExGlobal.getScheduler().getLogger().logSerializeTask(this, szBytes); } catch (IOException e) { throw new RuntimeException("Failed to write task in file " + serializeFile, e); } @@ -265,7 +264,7 @@ public void readFromFile() { assert (searchUnits == null); try { - PExLogger.logDeserializeTask(this); + PExGlobal.getScheduler().getLogger().logDeserializeTask(this); FileInputStream fis; fis = new FileInputStream(serializeFile); ObjectInputStream ois = new ObjectInputStream(fis); diff --git a/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/scheduler/replay/ReplayScheduler.java b/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/scheduler/replay/ReplayScheduler.java index fc53b5294e..4ac7a13d6d 100644 --- a/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/scheduler/replay/ReplayScheduler.java +++ b/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/scheduler/replay/ReplayScheduler.java @@ -1,7 +1,6 @@ package pex.runtime.scheduler.replay; import pex.runtime.PExGlobal; -import pex.runtime.logger.PExLogger; import pex.runtime.logger.ScheduleWriter; import pex.runtime.logger.TextWriter; import pex.runtime.machine.PMachine; @@ -16,12 +15,12 @@ public class ReplayScheduler extends Scheduler { public ReplayScheduler(Schedule sch) { - super(sch); + super(0, sch); } @Override public void run() throws TimeoutException, InterruptedException { - PExLogger.logStartReplay(); + logger.logStartReplay(); ScheduleWriter.Initialize(); TextWriter.Initialize(); @@ -29,9 +28,8 @@ public void run() throws TimeoutException, InterruptedException { ScheduleWriter.logHeader(); // log run test - PExLogger.logRunTest(); + logger.logRunTest(); - stepState.resetToZero(); start(); runIteration(); } @@ -73,7 +71,7 @@ protected void runStep() throws TimeoutException { // done with this schedule scheduleTerminated = true; isDoneStepping = true; - PExLogger.logFinishedIteration(stepNumber); + logger.logFinishedIteration(stepNumber); return; } @@ -98,9 +96,9 @@ protected PMachine getNextScheduleChoice() { return null; } - PMachine result = PExGlobal.getGlobalMachine(pid); + PMachine result = getMachine(pid); ScheduleWriter.logScheduleChoice(result); - PExLogger.logRepeatScheduleChoice(result, stepNumber, choiceNumber); + logger.logRepeatScheduleChoice(result, stepNumber, choiceNumber); choiceNumber++; return result; @@ -116,7 +114,7 @@ protected PValue getNextDataChoice(List> input_choices) { PValue result = schedule.getCurrentDataChoice(choiceNumber); assert (input_choices.contains(result)); ScheduleWriter.logDataChoice(result); - PExLogger.logRepeatDataChoice(result, stepNumber, choiceNumber); + logger.logRepeatDataChoice(result, stepNumber, choiceNumber); choiceNumber++; return result; diff --git a/Src/PRuntimes/PExRuntime/src/main/java/pex/utils/exceptions/BugFoundException.java b/Src/PRuntimes/PExRuntime/src/main/java/pex/utils/exceptions/BugFoundException.java index 5478dc2bd5..3249c41b1b 100644 --- a/Src/PRuntimes/PExRuntime/src/main/java/pex/utils/exceptions/BugFoundException.java +++ b/Src/PRuntimes/PExRuntime/src/main/java/pex/utils/exceptions/BugFoundException.java @@ -1,15 +1,22 @@ package pex.utils.exceptions; -import pex.runtime.logger.PExLogger; +import lombok.Getter; +import pex.runtime.PExGlobal; +import pex.runtime.scheduler.Scheduler; public class BugFoundException extends RuntimeException { + @Getter + Scheduler scheduler; + public BugFoundException(String message) { super(message); - PExLogger.logBugFound(message); + this.scheduler = PExGlobal.getScheduler(); + this.scheduler.getLogger().logBugFound(message); } public BugFoundException(String message, Throwable cause) { super(message, cause); - PExLogger.logBugFound(message); + this.scheduler = PExGlobal.getScheduler(); + this.scheduler.getLogger().logBugFound(message); } } diff --git a/Src/PRuntimes/PExRuntime/src/main/java/pex/utils/monitor/TimedCall.java b/Src/PRuntimes/PExRuntime/src/main/java/pex/utils/monitor/TimedCall.java index ed8ee6f9e1..1dd133b3cd 100644 --- a/Src/PRuntimes/PExRuntime/src/main/java/pex/utils/monitor/TimedCall.java +++ b/Src/PRuntimes/PExRuntime/src/main/java/pex/utils/monitor/TimedCall.java @@ -10,7 +10,7 @@ public class TimedCall implements Callable { private final Scheduler scheduler; - public TimedCall(Scheduler scheduler, boolean resume) { + public TimedCall(Scheduler scheduler) { this.scheduler = scheduler; } diff --git a/Src/PRuntimes/PExRuntime/src/test/java/pex/TestPEx.java b/Src/PRuntimes/PExRuntime/src/test/java/pex/TestPEx.java index a73467b7ae..6a3f9d37be 100644 --- a/Src/PRuntimes/PExRuntime/src/test/java/pex/TestPEx.java +++ b/Src/PRuntimes/PExRuntime/src/test/java/pex/TestPEx.java @@ -27,7 +27,7 @@ public class TestPEx { private static String timeout = "30"; private static String schedules = "100"; private static String maxSteps = "10000"; - private static String runArgs = "--checker-args :--schedules-per-task:10"; + private static String runArgs = "--checker-args :--schedules-per-task:10:--nproc:3"; private static boolean initialized = false; private static void setRunArgs() {