From 99dffa731f7be238af64135b182e6ce42b704a59 Mon Sep 17 00:00:00 2001 From: Aman Goel Date: Tue, 18 Jul 2023 16:39:09 -0700 Subject: [PATCH 1/6] [PSym] Upgrades (#621) * [PSym] Bump version * [PChecker] Change buggy schedule to be printed with actor name instead of actor id * [PSym] Cleanup how psym is invoked with p check command Adds timeout tracker for Java process Better checker error reporting Improve memout/timeout tracking * [PSym] Adds first version of printing .schedule that is replayable by bug-finding mode * [PSym] Minor cleanup * [PSym] cleanup * [PSym] Use integer choice as index for choose from composite types * [PSym] Adds receiver queue semantics Adds option to set event queue semantics to sender or receiver. Adds replaying trace from PSym with PChecker C#, even with receive statements Sets receiver queue semantics as default for coverage mode * [PChecker] Support passing both iterations and timeout as limits simultaneously * [PSym] Set timeout/iterations similar to C# backend Also clean up event buffer functions * [PChecker] Adds graceful termination for verification and coverage modes Adds gracefully terminating PSym processes spawned by checker * [PSym] Cleanup unnecessary tracking of globals with object instances * [PSym] Remove hardcoded sync event. Instead use json for specifying sync events * [PSym] Correct .schedule file Corrects .schedule file to support user-defined raise event * [PSym] code gen: fix name collisions Fixes name collisions between receive case payload and receive parent's local variables * [Tst] Fix an incorrect regression test * [Tst] Fix an incorrect regression test Adds a test case and corrects assertion to correctly pass the test * [Tst] Fix an incorrect regression test Adds a test case and corrects assertion to fail the test with a dynamic error * [PSym] code gen: support test defined with Main machines defined as well Add support for relation operations on strings * [PSym] Improve type casting Consider value type for primitive value summary when casting to/from any * [CLI] Set default compiler output to /PGenerated/ folder * [PSym] more corrections Changes project name autodetection to remove suffix Improves type casting to/from any type Experimenting with regression tests * [PSym] Support type casting to/from any for map values * [PSym] Minor update * [PSym] More improvements to type casting * [PSym] Improving comparison with any type * [PSym] Resolve corner cases with any type with null value * [PSym] Minor cleanup * [PCover] improve liveness checking Track cycles in the same iteration Cleanup state cahing * [PSym] codegen: support enum with non-zero default value * [PSym] codegen: support enum with non-zero default value * [PSym] CI: update to symex strategy as default Adds argumenets to pass to mvn test (use symex by default) * [PSym] remove receiver queue, set symex to default * [PSym] Minor * [PSym] correct CI * [PSym] Minor * [PSym] more corrections * [PSym] minor * [PSym] Minor change to printing stats * [PSym] Correct any type with null value * [PSym] improve cex printing * [PSym] improve cex printing * [PSym] CI: reduce amount of non determinism * [PSym] reduce default internal steps, add event name based sync events * [PChecker] Revert printing shceduling choice as actor id instead of actor name * [PSym] Improve sync events interface Support inputting user-provided sync events as in psym-config.json * [CLI] Add stateless option for coverage mode * [PSym] improve logging Improve log4j2 configuration Resolve compile warnings * [PSym] ci: minor * [PSym] improve liveness checking Check for liveness at each depth for guards where no machine can run * [PSym] more improvements to liveness checking * [PSym] Attempt to use symbolic comparison for symbolic state hashing * [PSym] Minor * [PSym] Correct out of range bugs, improve replayer * [PSym] ci: minor * [PSym] cli: add option to disable sync events * [PSym] update replayer Refactoring and updating replayer * [PSym] more cleanup Remove now unnecessary choosing from collection functions Set replayer machine creation same as search scheduler * [PSym] Correct replayer Remove empty choices * [PSym] minor * [PSym] refactor * [PCover] minor correction --------- Co-authored-by: Ankush Desai --- .../PCommandLine/Options/PCheckerOptions.cs | 9 +- Src/PRuntimes/PSymRuntime/pom.xml | 2 + .../src/main/java/META-INF/MANIFEST.MF | 1 + .../src/main/java/psym/EntryPoint.java | 12 +- .../PSymRuntime/src/main/java/psym/PSym.java | 25 ++-- .../psym/commandline/PSymConfiguration.java | 6 +- .../java/psym/commandline/PSymOptions.java | 28 ++-- .../main/java/psym/runtime/PSymGlobal.java | 50 ++++++- .../src/main/java/psym/runtime/Program.java | 1 - .../java/psym/runtime/logger/Log4JConfig.java | 11 +- .../java/psym/runtime/logger/PSymLogger.java | 4 +- .../psym/runtime/logger/ScheduleWriter.java | 9 +- .../psym/runtime/logger/ScratchLogger.java | 4 +- .../psym/runtime/logger/SearchLogger.java | 4 +- .../java/psym/runtime/logger/TraceLogger.java | 4 +- .../java/psym/runtime/machine/Machine.java | 4 +- .../runtime/machine/buffer/DeferQueue.java | 1 - .../runtime/machine/buffer/EventQueue.java | 14 +- .../runtime/machine/buffer/SymbolicQueue.java | 3 +- .../psym/runtime/machine/events/Message.java | 6 +- .../runtime/machine/events/StateEvents.java | 1 - .../java/psym/runtime/scheduler/Schedule.java | 111 +++------------ .../psym/runtime/scheduler/Scheduler.java | 63 ++++++--- .../runtime/scheduler/SearchScheduler.java | 55 +------- .../explicit/ExplicitSearchScheduler.java | 25 ++-- .../explicit/ExplicitSymmetryTracker.java | 2 - .../scheduler/replay/ReplayScheduler.java | 126 +++--------------- .../symbolic/SymbolicSearchScheduler.java | 79 ++++++++++- .../psym/runtime/statistics/SolverStats.java | 4 +- .../psym/utils/monitor/MemoryMonitor.java | 1 - .../main/java/psym/valuesummary/ListVS.java | 30 +++-- .../java/psym/valuesummary/PrimitiveVS.java | 1 - .../java/psym/valuesummary/UnionVStype.java | 10 +- .../java/psym/valuesummary/ValueSummary.java | 1 - .../src/test/java/psym/PSymTestLogger.java | 4 +- .../src/test/java/psym/TestCaseExecutor.java | 15 +-- .../java/psym/TestSymbolicRegression.java | 14 +- 37 files changed, 344 insertions(+), 396 deletions(-) diff --git a/Src/PCompiler/PCommandLine/Options/PCheckerOptions.cs b/Src/PCompiler/PCommandLine/Options/PCheckerOptions.cs index a01fc0f95..c084f3343 100644 --- a/Src/PCompiler/PCommandLine/Options/PCheckerOptions.cs +++ b/Src/PCompiler/PCommandLine/Options/PCheckerOptions.cs @@ -57,8 +57,8 @@ internal PCheckerOptions() schedulingGroup.AddArgument("sch-pct", null, "Choose the PCT scheduling strategy with given maximum number of priority switch points", typeof(uint)); schedulingGroup.AddArgument("sch-fairpct", null, "Choose the fair PCT scheduling strategy with given maximum number of priority switch points", typeof(uint)); schedulingGroup.AddArgument("sch-rl", null, "Choose the reinforcement learning (RL) scheduling strategy", typeof(bool)).IsHidden = true; - var schCoverage = schedulingGroup.AddArgument("sch-coverage", null, "Choose the scheduling strategy for explicit-state search in coverage mode (options: random, dfs, learn). (default: learn)"); - schCoverage.AllowedValues = new List() { "random", "dfs", "learn" }; + var schCoverage = schedulingGroup.AddArgument("sch-coverage", null, "Choose the scheduling strategy for coverage mode (options: learn, random, dfs, stateless). (default: learn)"); + schCoverage.AllowedValues = new List() { "learn", "random", "dfs", "stateless" }; schCoverage.IsHidden = true; var replayOptions = Parser.GetOrCreateGroup("replay", "Replay and debug options"); @@ -282,9 +282,10 @@ private static void SanitizeConfiguration(CheckerConfiguration checkerConfigurat checkerConfiguration.SchedulingStrategy != "fairpct" && checkerConfiguration.SchedulingStrategy != "probabilistic" && checkerConfiguration.SchedulingStrategy != "rl" && - checkerConfiguration.SchedulingStrategy != "dfs" && checkerConfiguration.SchedulingStrategy != "replay" && - checkerConfiguration.SchedulingStrategy != "learn") + checkerConfiguration.SchedulingStrategy != "learn" && + checkerConfiguration.SchedulingStrategy != "dfs" && + checkerConfiguration.SchedulingStrategy != "stateless") { Error.CheckerReportAndExit("Please provide a scheduling strategy (see --sch* options)"); } diff --git a/Src/PRuntimes/PSymRuntime/pom.xml b/Src/PRuntimes/PSymRuntime/pom.xml index 57498f933..1c0697508 100644 --- a/Src/PRuntimes/PSymRuntime/pom.xml +++ b/Src/PRuntimes/PSymRuntime/pom.xml @@ -190,6 +190,8 @@ java.library.path + + diff --git a/Src/PRuntimes/PSymRuntime/src/main/java/META-INF/MANIFEST.MF b/Src/PRuntimes/PSymRuntime/src/main/java/META-INF/MANIFEST.MF index 77fb0ed4c..f936626f2 100644 --- a/Src/PRuntimes/PSymRuntime/src/main/java/META-INF/MANIFEST.MF +++ b/Src/PRuntimes/PSymRuntime/src/main/java/META-INF/MANIFEST.MF @@ -1,2 +1,3 @@ Manifest-Version: 0.1 Main-Class: psym.PSym +Multi-Release: true diff --git a/Src/PRuntimes/PSymRuntime/src/main/java/psym/EntryPoint.java b/Src/PRuntimes/PSymRuntime/src/main/java/psym/EntryPoint.java index ecfd3bc49..538d1c422 100644 --- a/Src/PRuntimes/PSymRuntime/src/main/java/psym/EntryPoint.java +++ b/Src/PRuntimes/PSymRuntime/src/main/java/psym/EntryPoint.java @@ -14,7 +14,6 @@ import psym.runtime.scheduler.symmetry.SymmetryMode; import psym.runtime.scheduler.symmetry.SymmetryTracker; import psym.utils.exception.BugFoundException; -import psym.utils.exception.LivenessException; import psym.utils.exception.MemoutException; import psym.utils.monitor.MemoryMonitor; import psym.utils.monitor.TimeMonitor; @@ -145,7 +144,7 @@ private static void process(boolean resume) throws Exception { postprocess(true); PSymLogger.info(e.toString()); if (PSymGlobal.getConfiguration().getVerbosity() > 0) { - e.printStackTrace(System.out); + PSymGlobal.printStackTrace(e, false); } PSymLogger.setVerbosity(1); @@ -159,11 +158,8 @@ private static void process(boolean resume) throws Exception { scheduler.getProgram(), scheduler.getSchedule(), pc, - scheduler.getDepth(), - (e instanceof LivenessException)); + scheduler.getDepth()); PSymGlobal.setScheduler(replayScheduler); - String writeFileName = PSymGlobal.getConfiguration().getOutputFolder() + "/cex.schedule"; - replayScheduler.writeToFile(writeFileName); replay(replayScheduler); } catch (InterruptedException e) { status = "interrupted"; @@ -212,7 +208,7 @@ private static void replay(ReplayScheduler replayScheduler) throw new RuntimeException("ERROR: Failed to replay counterexample"); } catch (BugFoundException e) { PSymLogger.info(e.toString()); - e.printStackTrace(System.err); + PSymGlobal.printStackTrace(e, true); PSymLogger.info("Checker found a bug."); PSymLogger.info("... Emitting traces:"); PSymLogger.info(String.format("..... Writing %s", ScheduleWriter.getFileName())); @@ -224,7 +220,7 @@ private static void replay(ReplayScheduler replayScheduler) } public static void replayBug(ReplayScheduler replayScheduler) - throws RuntimeException, InterruptedException, TimeoutException { + throws RuntimeException, TimeoutException { SolverEngine.resumeEngine(); if (PSymGlobal.getConfiguration().getVerbosity() == 0) { PSymLogger.setVerbosity(1); diff --git a/Src/PRuntimes/PSymRuntime/src/main/java/psym/PSym.java b/Src/PRuntimes/PSymRuntime/src/main/java/psym/PSym.java index 63037474f..1b53128e9 100644 --- a/Src/PRuntimes/PSymRuntime/src/main/java/psym/PSym.java +++ b/Src/PRuntimes/PSymRuntime/src/main/java/psym/PSym.java @@ -27,7 +27,7 @@ public static void main(String[] args) { PSymLogger.Initialize(PSymGlobal.getConfiguration().getVerbosity()); try { - if (PSymGlobal.getConfiguration().getReadFromFile().equals("") && PSymGlobal.getConfiguration().getReadReplayerFromFile().equals("")) { + if (PSymGlobal.getConfiguration().getReadFromFile().equals("")) { Set> subTypesProgram = reflections.getSubTypesOf(Program.class); if (subTypesProgram.size() == 0) { throw new Exception("No program found."); @@ -46,23 +46,26 @@ public static void main(String[] args) { int exit_code = 0; try { - if (!PSymGlobal.getConfiguration().getReadReplayerFromFile().equals("")) { - ReplayScheduler replayScheduler = - ReplayScheduler.readFromFile(PSymGlobal.getConfiguration().getReadReplayerFromFile()); - EntryPoint.replayBug(replayScheduler); - throw new Exception("ERROR"); - } - if (PSymGlobal.getConfiguration().isWriteToFile()) { BacktrackWriter.Initialize(PSymGlobal.getConfiguration().getProjectName(), PSymGlobal.getConfiguration().getOutputFolder()); } - if (PSymGlobal.getConfiguration().getReadFromFile().equals("")) { + if (!PSymGlobal.getConfiguration().getReadScheduleFromFile().equals("")) { + // replay mode assert (p != null); setTestDriver(p, reflections); - EntryPoint.run(p); - } else { + ReplayScheduler replayScheduler = + ReplayScheduler.readFromFile(PSymGlobal.getConfiguration().getReadScheduleFromFile()); + EntryPoint.replayBug(replayScheduler); + throw new Exception("ERROR"); + } else if(!PSymGlobal.getConfiguration().getReadFromFile().equals("")){ + // resume mode EntryPoint.resume(); + } else { + // default mode + assert (p != null); + setTestDriver(p, reflections); + EntryPoint.run(p); } if (PSymGlobal.getConfiguration().isWriteToFile()) { diff --git a/Src/PRuntimes/PSymRuntime/src/main/java/psym/commandline/PSymConfiguration.java b/Src/PRuntimes/PSymRuntime/src/main/java/psym/commandline/PSymConfiguration.java index fe18b0df8..80cdd4f1c 100644 --- a/Src/PRuntimes/PSymRuntime/src/main/java/psym/commandline/PSymConfiguration.java +++ b/Src/PRuntimes/PSymRuntime/src/main/java/psym/commandline/PSymConfiguration.java @@ -40,14 +40,16 @@ public class PSymConfiguration implements Serializable { @Getter @Setter int maxStepBound = 10000; // fail on reaching the maximum scheduling step bound @Getter @Setter boolean failOnMaxStepBound = false; - // name of the cex file to read the replayer state - @Getter @Setter String readReplayerFromFile = ""; + // name of the .schedule file to read the schedule + @Getter @Setter String readScheduleFromFile = ""; // random seed @Getter @Setter long randomSeed = System.currentTimeMillis(); // name of the psym configuration file @Getter @Setter String configFile = ""; // buffer semantics @Getter @Setter BufferSemantics bufferSemantics = BufferSemantics.SenderQueue; + // whether or not to allow sync events + @Getter @Setter boolean allowSyncEvents = true; // mode of state hashing @Getter @Setter StateCachingMode stateCachingMode = StateCachingMode.None; // symmetry mode diff --git a/Src/PRuntimes/PSymRuntime/src/main/java/psym/commandline/PSymOptions.java b/Src/PRuntimes/PSymRuntime/src/main/java/psym/commandline/PSymOptions.java index 199dfcf86..f94b7e843 100644 --- a/Src/PRuntimes/PSymRuntime/src/main/java/psym/commandline/PSymOptions.java +++ b/Src/PRuntimes/PSymRuntime/src/main/java/psym/commandline/PSymOptions.java @@ -10,7 +10,6 @@ import org.json.JSONObject; import org.json.JSONTokener; import psym.runtime.PSymGlobal; -import psym.runtime.machine.buffer.BufferSemantics; import psym.runtime.scheduler.explicit.StateCachingMode; import psym.runtime.scheduler.explicit.choiceorchestration.ChoiceLearningRewardMode; import psym.runtime.scheduler.explicit.choiceorchestration.ChoiceLearningStateMode; @@ -185,6 +184,11 @@ public class PSymOptions { // Invisible/expert options + // whether or not to disable sync events + Option sync = + Option.builder().longOpt("no-sync").desc("Disable sync events").numberOfArgs(0).build(); + addHiddenOption(sync); + // whether or not to disable state caching Option stateCaching = Option.builder() @@ -452,13 +456,13 @@ public static PSymConfiguration ParseCommandlineArgs(String[] args) { // replay options case "r": case "replay": - config.setReadReplayerFromFile(option.getValue()); - File file = new File(config.getReadReplayerFromFile()); + config.setReadScheduleFromFile(option.getValue()); + File file = new File(config.getReadScheduleFromFile()); try { file.getCanonicalPath(); } catch (IOException e) { optionError( - option, String.format("File %s does not exist", config.getReadReplayerFromFile())); + option, String.format("File %s does not exist", config.getReadScheduleFromFile())); } break; // advanced options @@ -473,6 +477,9 @@ public static PSymConfiguration ParseCommandlineArgs(String[] args) { case "config": readConfigFile(config, option.getValue(), option); break; + case "no-sync": + config.setAllowSyncEvents(false); + break; case "state-caching": switch (option.getValue()) { case "none": @@ -682,10 +689,15 @@ private static void ParseConfigFile(PSymConfiguration config, File configFile) JSONObject value = (JSONObject) jsonObject.get(key); switch (key) { case "sync-events": - JSONArray syncEvents = value.getJSONArray("default"); - for (int i = 0; i < syncEvents.length(); i++) { - String syncEventName = syncEvents.getString(i); - PSymGlobal.getSyncEvents().add(syncEventName); + JSONArray allSyncEvents = value.getJSONArray("default"); + for (int i = 0; i < allSyncEvents.length(); i++) { + JSONObject element = allSyncEvents.getJSONObject(i); + String machineName = element.getString("machine"); + JSONArray syncEvents = element.getJSONArray("events"); + for (int j = 0; j < syncEvents.length(); j++) { + String syncEventName = syncEvents.getString(j); + PSymGlobal.addSyncEvent(machineName, syncEventName); + } } break; case "symmetric-machines": diff --git a/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/PSymGlobal.java b/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/PSymGlobal.java index 108546a71..ce4e50f83 100644 --- a/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/PSymGlobal.java +++ b/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/PSymGlobal.java @@ -1,12 +1,16 @@ package psym.runtime; +import java.io.PrintWriter; import java.io.Serializable; +import java.io.StringWriter; import java.util.HashMap; import java.util.HashSet; import java.util.Map; import java.util.Set; - import psym.commandline.PSymConfiguration; +import psym.runtime.logger.PSymLogger; +import psym.runtime.machine.Machine; +import psym.runtime.machine.events.Event; import psym.runtime.machine.events.StateEvents; import psym.runtime.scheduler.Scheduler; import psym.runtime.scheduler.explicit.ExplicitSymmetryTracker; @@ -42,7 +46,7 @@ public class PSymGlobal implements Serializable { /** * Set of sync event names */ - private final Set syncEvents = new HashSet<>(); + private final Map> syncEvents = new HashMap<>(); /** * Global coverage statistics @@ -102,8 +106,26 @@ public static Map getAllStateEvents() { return getInstance().allStateEvents; } - public static Set getSyncEvents() { - return getInstance().syncEvents; + public static void addSyncEvent(String machineName, String eventName) { + Set syncEvents = + getInstance().syncEvents.computeIfAbsent(machineName, k -> new HashSet<>()); + syncEvents.add(eventName); + getInstance().syncEvents.put(machineName, syncEvents); + } + + public static boolean hasSyncEvent(Machine machine, Event event) { + if (configuration.isAllowSyncEvents()) { + if (event.toString().startsWith("sync_")) { + return true; + } + Set syncEvents = getInstance().syncEvents.get(machine.getName()); + if (syncEvents == null) { + return false; + } + return syncEvents.contains(event.toString()); + } else { + return false; + } } public static CoverageStats getCoverage() { @@ -126,4 +148,24 @@ public static void initializeSymmetryTracker(boolean isSymbolic) { getInstance().symmetryTracker = isSymbolic ? new SymbolicSymmetryTracker() : new ExplicitSymmetryTracker(); } + + public static void printStackTrace(Exception e, boolean stderrOnly) { + if (stderrOnly) { + System.err.println("-----------"); + System.err.println("Stack Trace"); + System.err.println("-----------"); + e.printStackTrace(System.err); + System.err.println("-----------"); + } else { + StringWriter sw = new StringWriter(); + PrintWriter pw = new PrintWriter(sw); + e.printStackTrace(pw); + + PSymLogger.info("-----------"); + PSymLogger.info("Stack Trace"); + PSymLogger.info("-----------"); + PSymLogger.info(sw.toString()); + PSymLogger.info("-----------"); + } + } } diff --git a/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/Program.java b/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/Program.java index 8fb8dc917..009ecdeed 100644 --- a/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/Program.java +++ b/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/Program.java @@ -6,7 +6,6 @@ import psym.runtime.machine.Machine; import psym.runtime.machine.Monitor; import psym.runtime.machine.events.Event; -import psym.runtime.scheduler.Scheduler; public interface Program extends Serializable { Machine getStart(); diff --git a/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/logger/Log4JConfig.java b/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/logger/Log4JConfig.java index 8e6df3c61..e20f5029f 100644 --- a/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/logger/Log4JConfig.java +++ b/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/logger/Log4JConfig.java @@ -8,9 +8,12 @@ import org.apache.logging.log4j.core.config.builder.api.ConfigurationBuilderFactory; import org.apache.logging.log4j.core.config.builder.impl.BuiltConfiguration; import org.apache.logging.log4j.core.layout.PatternLayout; +import org.reflections.Reflections; public class Log4JConfig { + private static final String pattern = "%msg%n"; @Getter private static LoggerContext context = null; + @Getter private static PatternLayout patternLayout = null; public static void configureLog4J() { ConfigurationBuilder builder = @@ -23,12 +26,18 @@ public static void configureLog4J() { .add( builder .newLayout(PatternLayout.class.getSimpleName()) - .addAttribute("pattern", "%msg%n"))); + .addAttribute("pattern", pattern))); // configure the root logger builder.add(builder.newRootLogger(Level.INFO).add(builder.newAppenderRef("stdout"))); // apply the configuration context = Configurator.initialize(builder.build()); + + // set pattern layout + patternLayout = PatternLayout.newBuilder().withPattern(pattern).build(); + + // set level for reflections class + Configurator.setLevel(Reflections.class, Level.ERROR); } } diff --git a/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/logger/PSymLogger.java b/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/logger/PSymLogger.java index 7ce341e51..d0993e49b 100644 --- a/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/logger/PSymLogger.java +++ b/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/logger/PSymLogger.java @@ -6,7 +6,6 @@ import org.apache.logging.log4j.Logger; import org.apache.logging.log4j.core.LoggerContext; import org.apache.logging.log4j.core.appender.ConsoleAppender; -import org.apache.logging.log4j.core.config.Configuration; import org.apache.logging.log4j.core.config.Configurator; import org.apache.logging.log4j.core.layout.PatternLayout; import psym.utils.monitor.MemoryMonitor; @@ -24,8 +23,7 @@ public static void Initialize(int verb) { (org.apache.logging.log4j.core.Logger) LogManager.getLogger(PSymLogger.class.getName()); context = coreLogger.getContext(); - Configuration config = Log4JConfig.getContext().getConfiguration(); - PatternLayout layout = PatternLayout.createDefaultLayout(config); + PatternLayout layout = Log4JConfig.getPatternLayout(); ConsoleAppender consoleAppender = ConsoleAppender.createDefaultAppenderForLayout(layout); consoleAppender.start(); diff --git a/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/logger/ScheduleWriter.java b/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/logger/ScheduleWriter.java index 89a09b755..0a5ef138b 100644 --- a/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/logger/ScheduleWriter.java +++ b/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/logger/ScheduleWriter.java @@ -1,5 +1,9 @@ package psym.runtime.logger; +import java.io.File; +import java.io.IOException; +import java.io.PrintWriter; +import java.util.List; import lombok.Getter; import psym.runtime.PSymGlobal; import psym.runtime.machine.Machine; @@ -10,11 +14,6 @@ import psym.valuesummary.GuardedValue; import psym.valuesummary.PrimitiveVS; -import java.io.File; -import java.io.IOException; -import java.io.PrintWriter; -import java.util.List; - public class ScheduleWriter { static PrintWriter log = null; @Getter static String fileName = ""; diff --git a/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/logger/ScratchLogger.java b/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/logger/ScratchLogger.java index 18622f3e3..625a9d605 100644 --- a/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/logger/ScratchLogger.java +++ b/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/logger/ScratchLogger.java @@ -10,7 +10,6 @@ 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.config.Configuration; import org.apache.logging.log4j.core.layout.PatternLayout; /** Represents the scratch logger */ @@ -38,8 +37,7 @@ public static void Initialize(int verb, String outputFolder) { // Define new file printer FileOutputStream fout = new FileOutputStream(fileName, false); - Configuration config = Log4JConfig.getContext().getConfiguration(); - PatternLayout layout = PatternLayout.createDefaultLayout(config); + PatternLayout layout = Log4JConfig.getPatternLayout(); Appender fileAppender = OutputStreamAppender.createAppender(layout, null, fout, fileName, false, true); fileAppender.start(); diff --git a/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/logger/SearchLogger.java b/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/logger/SearchLogger.java index 7c5d267d3..d59c2f16d 100644 --- a/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/logger/SearchLogger.java +++ b/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/logger/SearchLogger.java @@ -13,7 +13,6 @@ import org.apache.logging.log4j.core.LoggerContext; import org.apache.logging.log4j.core.appender.ConsoleAppender; import org.apache.logging.log4j.core.appender.OutputStreamAppender; -import org.apache.logging.log4j.core.config.Configuration; import org.apache.logging.log4j.core.config.Configurator; import org.apache.logging.log4j.core.layout.PatternLayout; import psym.runtime.statistics.SearchStats; @@ -42,8 +41,7 @@ public static void Initialize(int verb, String outputFolder) { // Define new file printer FileOutputStream fout = new FileOutputStream(fileName, false); - Configuration config = Log4JConfig.getContext().getConfiguration(); - PatternLayout layout = PatternLayout.createDefaultLayout(config); + PatternLayout layout = Log4JConfig.getPatternLayout(); Appender fileAppender = OutputStreamAppender.createAppender(layout, null, fout, fileName, false, true); ConsoleAppender consoleAppender = ConsoleAppender.createDefaultAppenderForLayout(layout); diff --git a/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/logger/TraceLogger.java b/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/logger/TraceLogger.java index 8c5a6e605..273173032 100644 --- a/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/logger/TraceLogger.java +++ b/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/logger/TraceLogger.java @@ -13,7 +13,6 @@ import org.apache.logging.log4j.core.LoggerContext; import org.apache.logging.log4j.core.appender.ConsoleAppender; import org.apache.logging.log4j.core.appender.OutputStreamAppender; -import org.apache.logging.log4j.core.config.Configuration; import org.apache.logging.log4j.core.config.Configurator; import org.apache.logging.log4j.core.layout.PatternLayout; import psym.runtime.machine.Machine; @@ -47,8 +46,7 @@ public static void Initialize(int verb, String outputFolder) { // Define new file printer FileOutputStream fout = new FileOutputStream(fileName, false); - Configuration config = Log4JConfig.getContext().getConfiguration(); - PatternLayout layout = PatternLayout.createDefaultLayout(config); + PatternLayout layout = Log4JConfig.getPatternLayout(); Appender fileAppender = OutputStreamAppender.createAppender(layout, null, fout, fileName, false, true); ConsoleAppender consoleAppender = ConsoleAppender.createDefaultAppenderForLayout(layout); diff --git a/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/machine/Machine.java b/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/machine/Machine.java index b64f374b5..1c9ce7f75 100644 --- a/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/machine/Machine.java +++ b/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/machine/Machine.java @@ -28,9 +28,9 @@ public abstract class Machine implements Serializable, Comparable { continuations = new HashMap<>(); public final Set clearContinuationVars = new HashSet<>(); @Getter protected final String name; - @Getter protected int instanceId; private final State startState; private final Set states; + @Getter protected int instanceId; @Getter private EventQueue sendBuffer; @Getter private DeferQueue deferredQueue; @Getter private transient Scheduler scheduler; @@ -245,7 +245,7 @@ void runOutcomesToCompletion(Guard pc, EventHandlerReturnReason eventHandlerRetu // Inner loop: process sequences of 'goto's and 'raise's. while (eventHandlerReturnReason.isAbnormalReturn()) { - Assert.prop( + Assert.liveness( scheduler.getMaxInternalSteps() < 0 || steps < scheduler.getMaxInternalSteps(), String.format("Possible infinite loop found in machine %s", this), pc.and( diff --git a/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/machine/buffer/DeferQueue.java b/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/machine/buffer/DeferQueue.java index bd484cb69..3b039748c 100644 --- a/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/machine/buffer/DeferQueue.java +++ b/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/machine/buffer/DeferQueue.java @@ -1,7 +1,6 @@ package psym.runtime.machine.buffer; import java.io.Serializable; - import psym.runtime.machine.Machine; /** Implements the Defer Queue used to keep track of the deferred events */ diff --git a/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/machine/buffer/EventQueue.java b/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/machine/buffer/EventQueue.java index 63a0d0d56..b4dcb2c55 100644 --- a/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/machine/buffer/EventQueue.java +++ b/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/machine/buffer/EventQueue.java @@ -2,8 +2,6 @@ import java.io.Serializable; import java.util.function.Function; - -import psym.runtime.PSymGlobal; import psym.runtime.logger.ScheduleWriter; import psym.runtime.logger.TraceLogger; import psym.runtime.machine.Machine; @@ -11,6 +9,7 @@ import psym.runtime.machine.events.Message; import psym.runtime.scheduler.Scheduler; import psym.runtime.scheduler.replay.ReplayScheduler; +import psym.utils.exception.BugFoundException; import psym.valuesummary.*; public class EventQueue extends SymbolicQueue implements EventBuffer, Serializable { @@ -24,12 +23,15 @@ public EventQueue(Machine sender) { public void send( Guard pc, PrimitiveVS dest, PrimitiveVS eventName, UnionVS payload) { - if (eventName.getGuardedValues().size() > 1) { - throw new RuntimeException( - String.format("Handling multiple events together is not supported, in %s", eventName)); + Guard destIsNull = dest.symbolicEquals(null, pc).getGuardFor(true); + if (!destIsNull.isFalse()) { + throw new BugFoundException( + "Machine in send cannot be null", + destIsNull + ); } - TraceLogger.send(new Message(eventName, dest, payload).restrict(pc)); Message event = new Message(eventName, dest, payload).restrict(pc); + TraceLogger.send(event); addEvent(event); sender.getScheduler().runMonitors(event); } diff --git a/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/machine/buffer/SymbolicQueue.java b/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/machine/buffer/SymbolicQueue.java index cb913db7e..3128b04ed 100644 --- a/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/machine/buffer/SymbolicQueue.java +++ b/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/machine/buffer/SymbolicQueue.java @@ -2,7 +2,6 @@ import java.io.Serializable; import java.util.function.Function; - import psym.runtime.PSymGlobal; import psym.runtime.machine.Machine; import psym.runtime.machine.events.Message; @@ -17,10 +16,10 @@ */ public abstract class SymbolicQueue implements Serializable { + private final Machine owner; // elements in the queue protected ListVS elements; private Message peek = null; - private final Machine owner; public SymbolicQueue(Machine m) { this.elements = new ListVS<>(Guard.constTrue()); diff --git a/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/machine/events/Message.java b/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/machine/events/Message.java index b83f13569..24f03e20c 100644 --- a/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/machine/events/Message.java +++ b/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/machine/events/Message.java @@ -107,11 +107,11 @@ public PrimitiveVS isCreateMachine() { public PrimitiveVS isSyncEvent() { Guard cond = Guard.constFalse(); - for (GuardedValue machine : getTarget().getGuardedValues()) { + for (GuardedValue machineGv : getTarget().getGuardedValues()) { + Machine m = machineGv.getValue(); PrimitiveVS events = this.getEvent(); for (GuardedValue event : events.getGuardedValues()) { - if (PSymGlobal.getSyncEvents().contains(event.getValue().name) - || event.getValue().name.startsWith("sync_")) { + if (PSymGlobal.hasSyncEvent(m, event.getValue())) { cond = cond.or(event.getGuard()); } } diff --git a/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/machine/events/StateEvents.java b/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/machine/events/StateEvents.java index 611e6060b..4fb63a4b3 100644 --- a/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/machine/events/StateEvents.java +++ b/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/machine/events/StateEvents.java @@ -2,7 +2,6 @@ import java.io.Serializable; import java.util.*; - import psym.runtime.machine.eventhandlers.EventHandler; public class StateEvents implements Serializable { diff --git a/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/scheduler/Schedule.java b/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/scheduler/Schedule.java index e8f91be9b..3d48b4333 100644 --- a/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/scheduler/Schedule.java +++ b/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/scheduler/Schedule.java @@ -9,10 +9,7 @@ import psym.runtime.machine.Machine; import psym.runtime.machine.MachineLocalState; import psym.runtime.scheduler.symmetry.SymmetryTracker; -import psym.valuesummary.Guard; -import psym.valuesummary.ListVS; -import psym.valuesummary.PrimitiveVS; -import psym.valuesummary.ValueSummary; +import psym.valuesummary.*; public class Schedule implements Serializable { @@ -137,13 +134,6 @@ public void addRepeatInt(PrimitiveVS choice, int depth) { choices.get(depth).addRepeatInt(choice); } - public void addRepeatElement(PrimitiveVS choice, int depth) { - if (depth >= choices.size()) { - choices.add(newChoice()); - } - choices.get(depth).addRepeatElement(choice); - } - public void addBacktrackSchedulingChoice(List> machines, int depth) { if (depth >= choices.size()) { choices.add(newChoice()); @@ -206,27 +196,6 @@ public void addBacktrackInt(List> ints, int depth) { } } - public void addBacktrackElement(List elements, int depth) { - if (depth >= choices.size()) { - choices.add(newChoice()); - } - if (elements.isEmpty()) { - choices - .get(depth) - .storeState(schedulerDepth, schedulerChoiceDepth, null, filter, schedulerSymmetry); - } else { - choices - .get(depth) - .storeState( - schedulerDepth, schedulerChoiceDepth, schedulerState, filter, schedulerSymmetry); - numBacktracks++; - numDataBacktracks++; - } - for (ValueSummary choice : elements) { - choices.get(depth).addBacktrackElement(choice); - } - } - public PrimitiveVS getRepeatSchedulingChoice(int depth) { return choices.get(depth).getRepeatSchedulingChoice(); } @@ -239,10 +208,6 @@ public PrimitiveVS getRepeatInt(int depth) { return choices.get(depth).getRepeatInt(); } - public PrimitiveVS getRepeatElement(int depth) { - return choices.get(depth).getRepeatElement(); - } - public List> getBacktrackSchedulingChoice(int depth) { return choices.get(depth).getBacktrackSchedulingChoice(); } @@ -255,10 +220,6 @@ public List> getBacktrackInt(int depth) { return choices.get(depth).getBacktrackInt(); } - public List getBacktrackElement(int depth) { - return choices.get(depth).getBacktrackElement(); - } - public void clearRepeat(int depth) { choices.get(depth).clearRepeat(); } @@ -290,16 +251,6 @@ public Schedule guard(Guard pc) { return new Schedule(newChoices, createdMachines, machines, pc, schedulerSymmetry); } - public Schedule removeEmptyRepeat() { - List newChoices = new ArrayList<>(); - for (int i = 0; i < size(); i++) { - if (!choices.get(i).isRepeatEmpty()) { - newChoices.add(choices.get(i)); - } - } - return new Schedule(newChoices, createdMachines, machines, pc, schedulerSymmetry); - } - public void makeMachine(Machine m, Guard pc) { PrimitiveVS toAdd = new PrimitiveVS<>(m).restrict(pc); if (createdMachines.containsKey(m.getClass())) { @@ -326,31 +277,42 @@ public PrimitiveVS getMachine(Class type, PrimitiveV } public Schedule getSingleSchedule() { + Schedule result = new Schedule(null); + Guard pc = Guard.constTrue(); pc = pc.and(getFilter()); - for (Choice choice : choices) { + + int dNew = 0; + for (int d = 0; d < choices.size(); d++) { + Choice choice = choices.get(d); Choice guarded = choice.restrict(pc); PrimitiveVS schedulingChoice = guarded.getRepeatSchedulingChoice(); if (schedulingChoice.getGuardedValues().size() > 0) { + // add schedule choice pc = pc.and(schedulingChoice.getGuardedValues().get(0).getGuard()); + result.addRepeatSchedulingChoice(new PrimitiveVS<>(schedulingChoice.getGuardedValues().get(0).getValue()), dNew++); } else { + // add bool choice PrimitiveVS boolChoice = guarded.getRepeatBool(); if (boolChoice.getGuardedValues().size() > 0) { pc = pc.and(boolChoice.getGuardedValues().get(0).getGuard()); + result.addRepeatBool(new PrimitiveVS<>(boolChoice.getGuardedValues().get(0).getValue()), dNew++); } else { + // add int choice PrimitiveVS intChoice = guarded.getRepeatInt(); if (intChoice.getGuardedValues().size() > 0) { pc = pc.and(intChoice.getGuardedValues().get(0).getGuard()); - } else { - PrimitiveVS elementChoice = guarded.getRepeatElement(); - if (elementChoice.getGuardedValues().size() > 0) { - pc = pc.and(elementChoice.getGuardedValues().get(0).getGuard()); - } + result.addRepeatInt(new PrimitiveVS<>(intChoice.getGuardedValues().get(0).getValue()), dNew++); } } } } - return this.guard(pc).removeEmptyRepeat(); + + for (Machine machine : machines) { + result.makeMachine(machine, Guard.constTrue()); + } + + return result; } public Guard getLengthCond(int size) { @@ -385,11 +347,9 @@ public class Choice implements Serializable { @Getter PrimitiveVS repeatSchedulingChoice = new PrimitiveVS<>(); @Getter PrimitiveVS repeatBool = new PrimitiveVS<>(); @Getter PrimitiveVS repeatInt = new PrimitiveVS<>(); - @Getter PrimitiveVS repeatElement = new PrimitiveVS<>(); @Getter List> backtrackSchedulingChoice = new ArrayList<>(); @Getter List> backtrackBool = new ArrayList(); @Getter List> backtrackInt = new ArrayList<>(); - @Getter List backtrackElement = new ArrayList<>(); @Getter Guard handledUniverse = Guard.constFalse(); @Getter int schedulerDepth = 0; @Getter int schedulerChoiceDepth = 0; @@ -408,11 +368,9 @@ public Choice(Choice old) { repeatSchedulingChoice = new PrimitiveVS<>(old.repeatSchedulingChoice); repeatBool = new PrimitiveVS<>(old.repeatBool); repeatInt = new PrimitiveVS<>(old.repeatInt); - repeatElement = new PrimitiveVS<>(old.repeatElement); backtrackSchedulingChoice = new ArrayList<>(old.backtrackSchedulingChoice); backtrackBool = new ArrayList<>(old.backtrackBool); backtrackInt = new ArrayList<>(old.backtrackInt); - backtrackElement = new ArrayList<>(old.backtrackElement); handledUniverse = old.handledUniverse; schedulerDepth = old.schedulerDepth; schedulerChoiceDepth = old.schedulerChoiceDepth; @@ -446,14 +404,13 @@ public void storeState(int depth, int cdepth, ChoiceState state, Guard f, Symmet public int getNumChoicesExplored() { return repeatSchedulingChoice.getValues().size() + repeatBool.getValues().size() - + repeatInt.getValues().size() - + repeatElement.getValues().size(); + + repeatInt.getValues().size(); } public Guard getRepeatUniverse() { return repeatSchedulingChoice .getUniverse() - .or(repeatBool.getUniverse().or(repeatInt.getUniverse().or(repeatElement.getUniverse()))); + .or(repeatBool.getUniverse().or(repeatInt.getUniverse())); } public Guard getBacktrackUniverse() { @@ -467,9 +424,6 @@ public Guard getBacktrackUniverse() { for (PrimitiveVS integer : backtrackInt) { backtrackUniverse = backtrackUniverse.or(integer.getUniverse()); } - for (ValueSummary element : backtrackElement) { - backtrackUniverse = backtrackUniverse.or(element.getUniverse()); - } return backtrackUniverse; } @@ -487,8 +441,7 @@ public boolean isScheduleBacktrackNonEmpty() { public boolean isDataBacktrackNonEmpty() { return !getBacktrackBool().isEmpty() - || !getBacktrackInt().isEmpty() - || !getBacktrackElement().isEmpty(); + || !getBacktrackInt().isEmpty(); } public Choice restrict(Guard pc) { @@ -496,7 +449,6 @@ public Choice restrict(Guard pc) { c.repeatSchedulingChoice = repeatSchedulingChoice.restrict(pc); c.repeatBool = repeatBool.restrict(pc); c.repeatInt = repeatInt.restrict(pc); - c.repeatElement = repeatElement.restrict(pc); c.backtrackSchedulingChoice = backtrackSchedulingChoice.stream() .map(x -> x.restrict(pc)) @@ -512,11 +464,6 @@ public Choice restrict(Guard pc) { .map(x -> x.restrict(pc)) .filter(x -> !x.isEmptyVS()) .collect(Collectors.toList()); - c.backtrackElement = - backtrackElement.stream() - .map(x -> x.restrict(pc)) - .filter(x -> !x.isEmptyVS()) - .collect(Collectors.toList()); c.storeState( this.schedulerDepth, this.schedulerChoiceDepth, @@ -542,19 +489,10 @@ public void addRepeatInt(PrimitiveVS choice) { repeatInt = choice; } - public void addRepeatElement(PrimitiveVS choice) { - repeatElement = choice; - } - - public void clearRepeatSchedulingChoice() { - repeatSchedulingChoice = new PrimitiveVS<>(); - } - public void clearRepeat() { repeatSchedulingChoice = new PrimitiveVS<>(); repeatBool = new PrimitiveVS<>(); repeatInt = new PrimitiveVS<>(); - repeatElement = new PrimitiveVS<>(); } public void addBacktrackSchedulingChoice(PrimitiveVS choice) { @@ -569,15 +507,10 @@ public void addBacktrackInt(PrimitiveVS choice) { if (!choice.isEmptyVS()) backtrackInt.add(choice); } - public void addBacktrackElement(ValueSummary choice) { - if (!choice.isEmptyVS()) backtrackElement.add(choice); - } - public void clearBacktrack() { backtrackSchedulingChoice = new ArrayList<>(); backtrackBool = new ArrayList<>(); backtrackInt = new ArrayList<>(); - backtrackElement = new ArrayList<>(); } public void clear() { diff --git a/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/scheduler/Scheduler.java b/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/scheduler/Scheduler.java index fff531c75..c9d1f3786 100644 --- a/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/scheduler/Scheduler.java +++ b/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/scheduler/Scheduler.java @@ -3,7 +3,6 @@ import java.util.*; import java.util.concurrent.TimeoutException; import java.util.function.Function; - import lombok.Getter; import psym.runtime.*; import psym.runtime.Program; @@ -13,6 +12,7 @@ import psym.runtime.machine.State; import psym.runtime.machine.events.Event; import psym.runtime.machine.events.Message; +import psym.runtime.scheduler.symmetry.SymmetryMode; import psym.runtime.scheduler.symmetry.SymmetryTracker; import psym.runtime.statistics.SearchStats; import psym.utils.Assert; @@ -38,7 +38,7 @@ public abstract class Scheduler implements SchedulerInterface { /** How many instances of each Machine there are */ protected Map, PrimitiveVS> machineCounters; /** Whether or not search is done */ - protected boolean done = false; + protected Guard done = Guard.constFalse(); /** Choice depth */ protected int choiceDepth = 0; @@ -47,7 +47,7 @@ public abstract class Scheduler implements SchedulerInterface { /** Flag whether current step is a create or sync machine step */ protected Boolean stickyStep = true; /** Flag whether current execution finished */ - protected Boolean executionFinished = false; + protected Guard allMachinesHalted = Guard.constFalse(); /** List of monitors instances */ List monitors; /** The machine to start with */ @@ -98,7 +98,7 @@ protected Scheduler(Program p, Machine... machines) { * @return Whether or not there are more steps to run */ public boolean isDone() { - return done || depth == PSymGlobal.getConfiguration().getMaxStepBound(); + return done.isTrue() || depth == PSymGlobal.getConfiguration().getMaxStepBound(); } /** @@ -106,8 +106,12 @@ public boolean isDone() { * * @return Whether or not current execution finished */ - public boolean isFinishedExecution() { - return executionFinished || depth == PSymGlobal.getConfiguration().getMaxStepBound(); + public Guard isFinishedExecution() { + if (depth == PSymGlobal.getConfiguration().getMaxStepBound()) { + return Guard.constTrue(); + } else { + return allMachinesHalted; + } } /** @@ -249,15 +253,15 @@ public void initializeSearch() { start = target; } - protected void checkLiveness(boolean forceCheck) { - if (forceCheck || isFinishedExecution()) { + protected void checkLiveness(Guard finished) { + if (!finished.isFalse()) { for (Monitor m : monitors) { - PrimitiveVS monitorState = m.getCurrentState().restrict(schedule.getFilter()); + PrimitiveVS monitorState = m.getCurrentState().restrict(finished); for (GuardedValue entry : monitorState.getGuardedValues()) { State s = entry.getValue(); if (s.isHotState()) { Guard g = entry.getGuard(); - if (executionFinished) { + if (!allMachinesHalted.isFalse()) { Assert.liveness( g.isFalse(), String.format( @@ -314,20 +318,47 @@ public Machine setupNewMachine( } public PrimitiveVS allocateMachine( - Guard pc, - Class machineType, - Function constructor) { + Guard pc, + Class machineType, + Function constructor) { if (!machineCounters.containsKey(machineType)) { machineCounters.put(machineType, new PrimitiveVS<>(0)); } PrimitiveVS guardedCount = machineCounters.get(machineType).restrict(pc); - Machine newMachine = setupNewMachine(pc, guardedCount, constructor); + + PrimitiveVS allocated; + if (schedule.hasMachine(machineType, guardedCount, pc)) { + allocated = schedule.getMachine(machineType, guardedCount).restrict(pc); + for (GuardedValue gv : allocated.getGuardedValues()) { + Guard g = gv.getGuard(); + Machine m = (Machine) gv.getValue(); + assert (!BooleanVS.isEverTrue(m.hasStarted().restrict(g))); + TraceLogger.onCreateMachine(pc.and(g), m); + if (!machines.contains(m)) { + machines.add(m); + } + currentMachines.add(m); + assert (machines.size() >= currentMachines.size()); + m.setScheduler(this); + if (PSymGlobal.getConfiguration().getSymmetryMode() != SymmetryMode.None) { + PSymGlobal.getSymmetryTracker().createMachine(m, g); + } + } + } else { + Machine newMachine = setupNewMachine(pc, guardedCount, constructor); + + allocated = new PrimitiveVS<>(newMachine).restrict(pc); + if (PSymGlobal.getConfiguration().getSymmetryMode() != SymmetryMode.None) { + PSymGlobal.getSymmetryTracker().createMachine(newMachine, pc); + } + } guardedCount = IntegerVS.add(guardedCount, 1); + PrimitiveVS mergedCount = - machineCounters.get(machineType).updateUnderGuard(pc, guardedCount); + machineCounters.get(machineType).updateUnderGuard(pc, guardedCount); machineCounters.put(machineType, mergedCount); - return new PrimitiveVS<>(newMachine).restrict(pc); + return allocated; } public void runMonitors(Message event) { diff --git a/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/scheduler/SearchScheduler.java b/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/scheduler/SearchScheduler.java index 2daa5a659..4c033e0ea 100644 --- a/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/scheduler/SearchScheduler.java +++ b/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/scheduler/SearchScheduler.java @@ -7,11 +7,9 @@ import java.util.function.Consumer; import java.util.function.Function; import java.util.function.Supplier; -import psym.runtime.PSymGlobal; import psym.runtime.Program; import psym.runtime.logger.*; import psym.runtime.machine.Machine; -import psym.runtime.scheduler.symmetry.SymmetryMode; import psym.runtime.statistics.SearchStats; import psym.utils.monitor.MemoryMonitor; import psym.utils.random.NondetUtil; @@ -60,7 +58,6 @@ public PrimitiveVS getNextSchedulingChoice() { this::getNextSchedulingChoices, this::getNextSchedulingChoiceSummary, false); - choiceDepth = depth + 1; return res; } @@ -101,51 +98,6 @@ public PrimitiveVS getNextInteger(PrimitiveVS bound, Guard pc) return res; } - @Override - public PrimitiveVS allocateMachine( - Guard pc, - Class machineType, - Function constructor) { - if (!machineCounters.containsKey(machineType)) { - machineCounters.put(machineType, new PrimitiveVS<>(0)); - } - PrimitiveVS guardedCount = machineCounters.get(machineType).restrict(pc); - - PrimitiveVS allocated; - if (schedule.hasMachine(machineType, guardedCount, pc)) { - allocated = schedule.getMachine(machineType, guardedCount).restrict(pc); - for (GuardedValue gv : allocated.getGuardedValues()) { - Guard g = gv.getGuard(); - Machine m = (Machine) gv.getValue(); - assert (!BooleanVS.isEverTrue(m.hasStarted().restrict(g))); - TraceLogger.onCreateMachine(pc.and(g), m); - if (!machines.contains(m)) { - machines.add(m); - } - currentMachines.add(m); - assert (machines.size() >= currentMachines.size()); - m.setScheduler(this); - if (PSymGlobal.getConfiguration().getSymmetryMode() != SymmetryMode.None) { - PSymGlobal.getSymmetryTracker().createMachine(m, g); - } - } - } else { - Machine newMachine = setupNewMachine(pc, guardedCount, constructor); - - allocated = new PrimitiveVS<>(newMachine).restrict(pc); - if (PSymGlobal.getConfiguration().getSymmetryMode() != SymmetryMode.None) { - PSymGlobal.getSymmetryTracker().createMachine(newMachine, pc); - } - } - - guardedCount = IntegerVS.add(guardedCount, 1); - - PrimitiveVS mergedCount = - machineCounters.get(machineType).updateUnderGuard(pc, guardedCount); - machineCounters.put(machineType, mergedCount); - return allocated; - } - public void print_stats(SearchStats.TotalStats totalStats, double timeUsed, double memoryUsed) { printProgress(true); if (!isFinalResult) { @@ -203,6 +155,7 @@ protected List getNextSchedulingChoices() { // now there are no create machine and sync event actions remaining List> guardedMachines = new ArrayList<>(); + allMachinesHalted = Guard.constTrue(); for (Machine machine : machines) { if (!machine.getEventBuffer().isEmpty()) { Guard canRun = @@ -210,14 +163,10 @@ protected List getNextSchedulingChoices() { if (!canRun.isFalse()) { guardedMachines.add(new GuardedValue(machine, canRun)); } + allMachinesHalted = allMachinesHalted.and(canRun.not()); } } - executionFinished = - guardedMachines.stream() - .map(x -> x.getGuard().and(schedule.getFilter())) - .allMatch(x -> x.isFalse()); - List candidates = new ArrayList<>(); for (GuardedValue guardedValue : guardedMachines) { candidates.add( diff --git a/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/scheduler/explicit/ExplicitSearchScheduler.java b/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/scheduler/explicit/ExplicitSearchScheduler.java index 23b45dad3..93ef63878 100644 --- a/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/scheduler/explicit/ExplicitSearchScheduler.java +++ b/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/scheduler/explicit/ExplicitSearchScheduler.java @@ -32,7 +32,6 @@ import psym.runtime.statistics.SearchStats; import psym.runtime.statistics.SolverStats; import psym.utils.Assert; -import psym.utils.exception.BugFoundException; import psym.utils.monitor.MemoryMonitor; import psym.utils.monitor.TimeMonitor; import psym.valuesummary.Guard; @@ -141,7 +140,6 @@ public void doSearch() throws TimeoutException, InterruptedException { } searchStats.startNewIteration(iter, backtrackDepth); performSearch(); - checkLiveness(false); summarizeIteration(backtrackDepth); } } @@ -168,7 +166,6 @@ public void resumeSearch() throws TimeoutException, InterruptedException { } searchStats.startNewIteration(iter, backtrackDepth); performSearch(); - checkLiveness(false); summarizeIteration(backtrackDepth); if (resetAfterInitial) { resetAfterInitial = false; @@ -187,13 +184,15 @@ protected void performSearch() throws TimeoutException { "Maximum allowed depth " + PSymGlobal.getConfiguration().getMaxStepBound() + " exceeded", schedule.getLengthCond(schedule.size())); step(); + checkLiveness(allMachinesHalted); } + checkLiveness(Guard.constTrue()); Assert.prop( !PSymGlobal.getConfiguration().isFailOnMaxStepBound() || (getDepth() < PSymGlobal.getConfiguration().getMaxStepBound()), "Scheduling steps bound of " + PSymGlobal.getConfiguration().getMaxStepBound() + " reached.", schedule.getLengthCond(schedule.size())); schedule.setNumBacktracksInSchedule(); - if (done) { + if (done.isTrue()) { searchStats.setIterationCompleted(); } } @@ -201,6 +200,7 @@ protected void performSearch() throws TimeoutException { @Override protected void step() throws TimeoutException { srcState.clear(); + allMachinesHalted = Guard.constFalse(); int numStates = 0; int numStatesDistinct = 0; @@ -217,10 +217,13 @@ protected void step() throws TimeoutException { if (!isDistinctState) { int firstVisitIter = numConcrete[2]; if (firstVisitIter == iter) { - executionFinished = true; -// throw new BugFoundException("Cycle detected: revisited a state multiple times in the same iteration", Guard.constTrue()); + allMachinesHalted = Guard.constTrue(); +// Assert.liveness( +// false, +// String.format("Cycle detected: Possible infinite loop found due to revisiting a state multiple times in the same iteration"), +// Guard.constTrue()); } - done = true; + done = Guard.constTrue(); SearchLogger.finishedExecution(depth); return; } @@ -243,11 +246,11 @@ protected void step() throws TimeoutException { PrimitiveVS schedulingChoices = getNextSchedulingChoice(); if (schedulingChoices.isEmptyVS()) { - done = true; + done = Guard.constTrue(); SearchLogger.finishedExecution(depth); } - if (done) { + if (done.isTrue()) { return; } @@ -903,7 +906,7 @@ private void removePendingTask(BacktrackTask task) { public void reset() { depth = 0; choiceDepth = 0; - done = false; + done = Guard.constFalse(); stickyStep = true; machineCounters.clear(); // machines.clear(); @@ -943,7 +946,7 @@ public void reinitialize() { public void restore(int d, int cd) { depth = d; choiceDepth = cd; - done = false; + done = Guard.constFalse(); } public void restoreState(Schedule.ChoiceState state) { diff --git a/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/scheduler/explicit/ExplicitSymmetryTracker.java b/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/scheduler/explicit/ExplicitSymmetryTracker.java index 91b85790e..0a183cb50 100644 --- a/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/scheduler/explicit/ExplicitSymmetryTracker.java +++ b/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/scheduler/explicit/ExplicitSymmetryTracker.java @@ -6,8 +6,6 @@ import psym.runtime.scheduler.symmetry.SymmetryTracker; import psym.valuesummary.*; -import javax.crypto.Mac; - public class ExplicitSymmetryTracker extends SymmetryTracker { Map>> typeToSymmetryClasses; Set pendingMerges; diff --git a/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/scheduler/replay/ReplayScheduler.java b/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/scheduler/replay/ReplayScheduler.java index 75e0623ff..a1c0281d2 100644 --- a/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/scheduler/replay/ReplayScheduler.java +++ b/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/scheduler/replay/ReplayScheduler.java @@ -1,13 +1,10 @@ package psym.runtime.scheduler.replay; -import java.io.*; -import java.nio.file.Files; -import java.nio.file.Paths; import java.util.ArrayList; import java.util.List; import java.util.concurrent.TimeoutException; -import java.util.function.Function; import lombok.Getter; +import org.apache.commons.lang3.NotImplementedException; import psym.runtime.PSymGlobal; import psym.runtime.Program; import psym.runtime.logger.PSymLogger; @@ -15,7 +12,6 @@ import psym.runtime.logger.SearchLogger; import psym.runtime.logger.TraceLogger; import psym.runtime.machine.Machine; -import psym.runtime.machine.events.Event; import psym.runtime.machine.events.Message; import psym.runtime.scheduler.Schedule; import psym.runtime.scheduler.Scheduler; @@ -26,24 +22,14 @@ public class ReplayScheduler extends Scheduler { @Getter /** Path constraint */ private final Guard pathConstraint; - - @Getter - /** Flag for liveness bug */ - private final boolean isLivenessBug; /** Counterexample length */ private final int cexLength; - public ReplayScheduler( - Program p, Schedule schedule, int length, boolean livenessBug) { - this(p, schedule, Guard.constTrue(), length, livenessBug); - } - public ReplayScheduler( Program p, Schedule schedule, Guard pc, - int length, - boolean livenessBug) { + int length) { super(p); TraceLogger.enable(); this.schedule = schedule.guard(pc).getSingleSchedule(); @@ -53,7 +39,6 @@ public ReplayScheduler( PSymGlobal.getConfiguration().setToReplay(); cexLength = length; pathConstraint = pc; - isLivenessBug = livenessBug; } /** @@ -66,19 +51,14 @@ public ReplayScheduler( public static ReplayScheduler readFromFile(String readFromFile) throws Exception { ReplayScheduler result; try { - PSymLogger.info(".. Reading replayer state from file " + readFromFile); - FileInputStream fis; - fis = new FileInputStream(readFromFile); - ObjectInputStream ois = new ObjectInputStream(fis); - result = (ReplayScheduler) ois.readObject(); - PSymGlobal.setInstance((PSymGlobal) ois.readObject()); - result.reinitialize(); - PSymLogger.info(".. Successfully read."); - } catch (IOException | ClassNotFoundException e) { + PSymLogger.info(".. Reading schedule from file " + readFromFile); + throw new NotImplementedException("Replaying a schedule is currently unsupported."); +// PSymLogger.info(".. Successfully read."); + } catch (NotImplementedException e) { e.printStackTrace(); - throw new RuntimeException(".. Failed to read replayer state from file " + readFromFile, e); + throw new RuntimeException(".. Failed to read schedule from file " + readFromFile, e); } - return result; +// return result; } @Override @@ -87,7 +67,6 @@ public void doSearch() throws TimeoutException { ScheduleWriter.logHeader(); initializeSearch(); performSearch(); - checkLiveness(isLivenessBug); } @Override @@ -103,28 +82,32 @@ protected void performSearch() throws TimeoutException { "Maximum allowed depth " + PSymGlobal.getConfiguration().getMaxStepBound() + " exceeded", schedule.getLengthCond(schedule.size())); step(); + checkLiveness(allMachinesHalted); } + checkLiveness(Guard.constTrue()); Assert.prop( !PSymGlobal.getConfiguration().isFailOnMaxStepBound() || (getDepth() < PSymGlobal.getConfiguration().getMaxStepBound()), "Scheduling steps bound of " + PSymGlobal.getConfiguration().getMaxStepBound() + " reached.", schedule.getLengthCond(schedule.size())); - if (done) { + if (done.isTrue()) { searchStats.setIterationCompleted(); } } @Override public void step() { + allMachinesHalted = Guard.constFalse(); + removeHalted(); PrimitiveVS schedulingChoices = getNextSchedulingChoice(); if (schedulingChoices.isEmptyVS()) { - done = true; + done = Guard.constTrue(); SearchLogger.finishedExecution(depth); } - if (done) { + if (done.isTrue()) { return; } @@ -164,6 +147,9 @@ public void step() { @Override public PrimitiveVS getNextSchedulingChoice() { PrimitiveVS res = schedule.getRepeatSchedulingChoice(choiceDepth); + if (res.isEmptyVS()) { + allMachinesHalted = Guard.constTrue(); + } choiceDepth++; return res; } @@ -184,85 +170,9 @@ public PrimitiveVS getNextInteger(PrimitiveVS bound, Guard pc) return res; } - @Override - public PrimitiveVS allocateMachine( - Guard pc, - Class machineType, - Function constructor) { - if (!machineCounters.containsKey(machineType)) { - machineCounters.put(machineType, new PrimitiveVS<>(0)); - } - PrimitiveVS guardedCount = machineCounters.get(machineType).restrict(pc); - - PrimitiveVS allocated = schedule.getMachine(machineType, guardedCount); - TraceLogger.onCreateMachine(pc, allocated.getValues().iterator().next()); - allocated.getValues().iterator().next().setScheduler(this); - - guardedCount = IntegerVS.add(guardedCount, 1); - - PrimitiveVS mergedCount = - machineCounters.get(machineType).updateUnderGuard(pc, guardedCount); - machineCounters.put(machineType, mergedCount); - return allocated; - } - - @Override - public void startWith(Machine machine) { - PrimitiveVS machineVS; - if (this.machineCounters.containsKey(machine.getClass())) { - machineVS = - schedule.getMachine(machine.getClass(), this.machineCounters.get(machine.getClass())); - this.machineCounters.put( - machine.getClass(), IntegerVS.add(this.machineCounters.get(machine.getClass()), 1)); - } else { - machineVS = schedule.getMachine(machine.getClass(), new PrimitiveVS<>(0)); - this.machineCounters.put(machine.getClass(), new PrimitiveVS<>(1)); - } - - TraceLogger.onCreateMachine(machineVS.getUniverse(), machine); - machine.setScheduler(this); - performEffect(new Message(Event.createMachine, machineVS, null)); - } - @Override public boolean isDone() { return super.isDone() || this.getChoiceDepth() >= schedule.size(); } - @Override - public boolean isFinishedExecution() { - return super.isFinishedExecution() || this.getChoiceDepth() >= schedule.size(); - } - - public void reinitialize() { - for (Machine machine : schedule.getMachines()) { - machine.reset(); - } - for (Machine machine : schedule.getMachines()) { - machine.setScheduler(this); - } - } - - /** - * Write scheduler state to a file - * - * @param writeFileName Output file name - * @throws Exception Throw error if writing fails - */ - public void writeToFile(String writeFileName) throws RuntimeException { - try { - FileOutputStream fos = new FileOutputStream(writeFileName); - ObjectOutputStream oos = new ObjectOutputStream(fos); - oos.writeObject(this); - oos.writeObject(PSymGlobal.getInstance()); - if (PSymGlobal.getConfiguration().getVerbosity() > 0) { - long szBytes = Files.size(Paths.get(writeFileName)); - PSymLogger.info( - String.format(" %,.1f MB written in %s", (szBytes / 1024.0 / 1024.0), writeFileName)); - } - } catch (IOException e) { - // e.printStackTrace(); - throw new RuntimeException("Failed to write replayer in file " + writeFileName, e); - } - } } diff --git a/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/scheduler/symbolic/SymbolicSearchScheduler.java b/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/scheduler/symbolic/SymbolicSearchScheduler.java index 9be144c26..dd5882bc5 100644 --- a/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/scheduler/symbolic/SymbolicSearchScheduler.java +++ b/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/scheduler/symbolic/SymbolicSearchScheduler.java @@ -2,8 +2,7 @@ import java.time.Duration; import java.time.Instant; -import java.util.ArrayList; -import java.util.List; +import java.util.*; import java.util.concurrent.TimeUnit; import java.util.concurrent.TimeoutException; import java.util.function.BiConsumer; @@ -11,13 +10,16 @@ import java.util.function.Function; import java.util.function.Supplier; import java.util.stream.Collectors; +import lombok.Getter; import org.apache.commons.lang3.StringUtils; import psym.runtime.PSymGlobal; import psym.runtime.Program; import psym.runtime.logger.*; import psym.runtime.machine.Machine; +import psym.runtime.machine.MachineLocalState; import psym.runtime.machine.events.Message; import psym.runtime.scheduler.SearchScheduler; +import psym.runtime.scheduler.explicit.StateCachingMode; import psym.runtime.scheduler.symmetry.SymmetryMode; import psym.runtime.statistics.SearchStats; import psym.runtime.statistics.SolverStats; @@ -31,6 +33,7 @@ import psym.valuesummary.solvers.SolverEngine; public class SymbolicSearchScheduler extends SearchScheduler { + private final TreeMap depthToProtocolState = new TreeMap<>(); public SymbolicSearchScheduler(Program p) { super(p); @@ -50,7 +53,6 @@ public void doSearch() throws TimeoutException { } searchStats.startNewIteration(1, 0); performSearch(); - checkLiveness(false); summarizeIteration(0); } @@ -68,18 +70,22 @@ public void performSearch() throws TimeoutException { "Maximum allowed depth " + PSymGlobal.getConfiguration().getMaxStepBound() + " exceeded", schedule.getLengthCond(schedule.size())); step(); + checkLiveness(allMachinesHalted); } + checkLiveness(Guard.constTrue()); Assert.prop( !PSymGlobal.getConfiguration().isFailOnMaxStepBound() || (getDepth() < PSymGlobal.getConfiguration().getMaxStepBound()), "Scheduling steps bound of " + PSymGlobal.getConfiguration().getMaxStepBound() + " reached.", schedule.getLengthCond(schedule.size())); - if (done) { + if (done.isTrue()) { searchStats.setIterationCompleted(); } } @Override protected void step() throws TimeoutException { + allMachinesHalted = Guard.constFalse(); + int numStates = 0; int numMessages = 0; int numMessagesMerged = 0; @@ -94,11 +100,11 @@ protected void step() throws TimeoutException { PrimitiveVS schedulingChoices = getNextSchedulingChoice(); if (schedulingChoices.isEmptyVS()) { - done = true; + done = Guard.constTrue(); SearchLogger.finishedExecution(depth); } - if (done) { + if (done.isTrue()) { return; } @@ -136,6 +142,9 @@ protected void step() throws TimeoutException { } } if (!stickyStep) { + if (PSymGlobal.getConfiguration().getStateCachingMode() == StateCachingMode.Exact) { + effect = effect.restrict(done.not()); + } depth++; } @@ -143,6 +152,18 @@ protected void step() throws TimeoutException { performEffect(effect); + if (!stickyStep) { + if (PSymGlobal.getConfiguration().getStateCachingMode() == StateCachingMode.Exact) { + ProtocolState destProtocolState = new ProtocolState(currentMachines); + for (ProtocolState srcProtocolState : depthToProtocolState.values()) { + Guard areEqual = destProtocolState.symbolicEquals(srcProtocolState); + done = done.or(areEqual); + allMachinesHalted = allMachinesHalted.or(done); + } + depthToProtocolState.put(depth, destProtocolState); + } + } + // simplify engine // SolverEngine.simplifyEngineAuto(); @@ -383,4 +404,50 @@ public void print_search_stats() { "#-events-explored", String.format("%d", totalStats.getDepthStats().getNumOfTransitionsExplored())); } + + public static class ProtocolState { + @Getter + Map stateMap = null; + + public ProtocolState(Collection machines) { + stateMap = new HashMap<>(); + for (Machine m: machines) { + stateMap.put(m, m.getMachineLocalState()); + } + } + + public Guard symbolicEquals(ProtocolState rhs) { + Map rhsStateMap = rhs.getStateMap(); + if (stateMap.size() != rhsStateMap.size()) { + return Guard.constFalse(); + } + + Guard areEqual = Guard.constTrue(); + for (Map.Entry entry: stateMap.entrySet()) { + Machine machine = entry.getKey(); + MachineLocalState lhsMachineState = entry.getValue(); + MachineLocalState rhsMachineState = rhsStateMap.get(machine); + if (rhsMachineState == null) { + return Guard.constFalse(); + } + List lhsLocals = lhsMachineState.getLocals(); + List rhsLocals = rhsMachineState.getLocals(); + assert (lhsLocals.size() == rhsLocals.size()); + + for (int i = 0; i < lhsLocals.size(); i++) { + ValueSummary lhsVs = lhsLocals.get(i).restrict(areEqual); + ValueSummary rhsVs = rhsLocals.get(i).restrict(areEqual); + if (lhsVs.isEmptyVS() && rhsVs.isEmptyVS()) { + continue; + } + areEqual = areEqual.and(lhsVs.symbolicEquals(rhsVs, Guard.constTrue()).getGuardFor(true)); + if (areEqual.isFalse()) { + return Guard.constFalse(); + } + } + } + return areEqual; + } + + } } diff --git a/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/statistics/SolverStats.java b/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/statistics/SolverStats.java index a4de88dcf..6ae7ada0a 100644 --- a/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/statistics/SolverStats.java +++ b/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/statistics/SolverStats.java @@ -1,14 +1,12 @@ package psym.runtime.statistics; -import lombok.Setter; +import java.util.concurrent.TimeoutException; import psym.runtime.logger.SearchLogger; import psym.utils.exception.MemoutException; import psym.utils.monitor.MemoryMonitor; import psym.utils.monitor.TimeMonitor; import psym.valuesummary.solvers.SolverEngine; -import java.util.concurrent.TimeoutException; - public class SolverStats { public static int andOperations = 0; public static int orOperations = 0; diff --git a/Src/PRuntimes/PSymRuntime/src/main/java/psym/utils/monitor/MemoryMonitor.java b/Src/PRuntimes/PSymRuntime/src/main/java/psym/utils/monitor/MemoryMonitor.java index 87ac068ed..9d0fe3fe9 100644 --- a/Src/PRuntimes/PSymRuntime/src/main/java/psym/utils/monitor/MemoryMonitor.java +++ b/Src/PRuntimes/PSymRuntime/src/main/java/psym/utils/monitor/MemoryMonitor.java @@ -3,7 +3,6 @@ import com.sun.management.GarbageCollectionNotificationInfo; import java.lang.management.GarbageCollectorMXBean; import java.lang.management.ManagementFactory; -import java.util.concurrent.TimeoutException; import javax.management.Notification; import javax.management.NotificationEmitter; import javax.management.NotificationListener; diff --git a/Src/PRuntimes/PSymRuntime/src/main/java/psym/valuesummary/ListVS.java b/Src/PRuntimes/PSymRuntime/src/main/java/psym/valuesummary/ListVS.java index 9cba3fbf1..192ad0748 100644 --- a/Src/PRuntimes/PSymRuntime/src/main/java/psym/valuesummary/ListVS.java +++ b/Src/PRuntimes/PSymRuntime/src/main/java/psym/valuesummary/ListVS.java @@ -8,6 +8,7 @@ import java.util.stream.IntStream; import lombok.Getter; import psym.runtime.machine.Machine; +import psym.utils.exception.BugFoundException; /** Represents the list value summaries. */ public class ListVS> implements ValueSummary> { @@ -269,9 +270,12 @@ public T getHelper(PrimitiveVS indexSummary) { // (Checks.sameUniverse(indexSummary.getUniverse(), getUniverse())); final PrimitiveVS inRange = inRange(indexSummary); // make sure it is always in range - if (!inRange.getGuardFor(false).isFalse()) { + Guard outOfRange = inRange.getGuardFor(false); + if (!outOfRange.isFalse()) { // there is a possibility that the index is out-of-bounds - throw new IndexOutOfBoundsException(); + throw new BugFoundException( + "Index was out of range. Must be non-negative and less than the size of the collection.", + outOfRange); } T merger = null; @@ -314,11 +318,13 @@ public ListVS set(PrimitiveVS indexSummary, T itemToSet) { */ private ListVS setHelper(PrimitiveVS indexSummary, T itemToSet) { final PrimitiveVS inRange = inRange(indexSummary); + Guard outOfRange = inRange.getGuardFor(false); // make sure it is always in range - if (!inRange.getGuardFor(false).isFalse()) { + if (!outOfRange.isFalse()) { // there is a possibility that the index is out-of-bounds - throw new IndexOutOfBoundsException( - "Index was out of range. Must be non-negative and less than the size of the collection."); + throw new BugFoundException( + "Index was out of range. Must be non-negative and less than the size of the collection.", + outOfRange); } ListVS merger = null; @@ -371,9 +377,12 @@ public ListVS insert(PrimitiveVS indexSummary, T itemToInsert) { final PrimitiveVS inRange = inRange(indexSummary); // make sure it is always in range - if (!inRange.getGuardFor(false).isFalse()) { + Guard outOfRange = inRange.getGuardFor(false); + if (!outOfRange.isFalse()) { // there is a possibility that the index is out-of-bounds - throw new IndexOutOfBoundsException(); + throw new BugFoundException( + "Index must be within the bounds of the List.", + outOfRange); } // 1. add a new entry (we'll re-add the last entry) @@ -424,9 +433,12 @@ private ListVS removeAtHelper(PrimitiveVS indexSummary) { // assert (Checks.sameUniverse(indexSummary.getUniverse(), getUniverse())); final PrimitiveVS inRange = inRange(indexSummary); // make sure it is always in range - if (!inRange.getGuardFor(false).isFalse()) { + Guard outOfRange = inRange.getGuardFor(false); + if (!outOfRange.isFalse()) { // there is a possibility that the index is out-of-bounds - throw new IndexOutOfBoundsException(); + throw new BugFoundException( + "Index was out of range. Must be non-negative and less than the size of the collection.", + outOfRange); } // new size diff --git a/Src/PRuntimes/PSymRuntime/src/main/java/psym/valuesummary/PrimitiveVS.java b/Src/PRuntimes/PSymRuntime/src/main/java/psym/valuesummary/PrimitiveVS.java index b81b124c1..02e61c43f 100644 --- a/Src/PRuntimes/PSymRuntime/src/main/java/psym/valuesummary/PrimitiveVS.java +++ b/Src/PRuntimes/PSymRuntime/src/main/java/psym/valuesummary/PrimitiveVS.java @@ -6,7 +6,6 @@ import java.util.stream.Collectors; import lombok.Getter; import psym.runtime.machine.Machine; -import psym.runtime.machine.events.Event; /** * Represents a primitive value summary (Boolean, Integer, Float, String) diff --git a/Src/PRuntimes/PSymRuntime/src/main/java/psym/valuesummary/UnionVStype.java b/Src/PRuntimes/PSymRuntime/src/main/java/psym/valuesummary/UnionVStype.java index 376f947e8..f76ce930f 100644 --- a/Src/PRuntimes/PSymRuntime/src/main/java/psym/valuesummary/UnionVStype.java +++ b/Src/PRuntimes/PSymRuntime/src/main/java/psym/valuesummary/UnionVStype.java @@ -35,14 +35,8 @@ public static UnionVStype getUnionVStype(Class tc, Strin @Override public String toString() { - StringBuilder out = new StringBuilder(); - out.append("[type: "); - out.append(typeClass); - out.append(", "); - out.append("names: "); - out.append(names); - out.append("]"); - return out.toString(); + String out = "[type: " + typeClass + ", " + "names: " + names + "]"; + return out; } @Override diff --git a/Src/PRuntimes/PSymRuntime/src/main/java/psym/valuesummary/ValueSummary.java b/Src/PRuntimes/PSymRuntime/src/main/java/psym/valuesummary/ValueSummary.java index 9f7afba19..f16d031c3 100644 --- a/Src/PRuntimes/PSymRuntime/src/main/java/psym/valuesummary/ValueSummary.java +++ b/Src/PRuntimes/PSymRuntime/src/main/java/psym/valuesummary/ValueSummary.java @@ -5,7 +5,6 @@ import java.util.HashMap; import java.util.List; import java.util.Map; - import psym.runtime.machine.Machine; import psym.runtime.machine.events.Message; import psym.utils.exception.BugFoundException; diff --git a/Src/PRuntimes/PSymRuntime/src/test/java/psym/PSymTestLogger.java b/Src/PRuntimes/PSymRuntime/src/test/java/psym/PSymTestLogger.java index 5143396fe..c6b2b64d3 100644 --- a/Src/PRuntimes/PSymRuntime/src/test/java/psym/PSymTestLogger.java +++ b/Src/PRuntimes/PSymRuntime/src/test/java/psym/PSymTestLogger.java @@ -11,7 +11,6 @@ import org.apache.logging.log4j.core.LoggerContext; import org.apache.logging.log4j.core.appender.ConsoleAppender; import org.apache.logging.log4j.core.appender.OutputStreamAppender; -import org.apache.logging.log4j.core.config.Configuration; import org.apache.logging.log4j.core.config.Configurator; import org.apache.logging.log4j.core.layout.PatternLayout; import psym.runtime.logger.Log4JConfig; @@ -38,8 +37,7 @@ public static void Initialize(String outputFolder) { // Define new file printer FileOutputStream fout = new FileOutputStream(fileName, false); - Configuration config = Log4JConfig.getContext().getConfiguration(); - PatternLayout layout = PatternLayout.createDefaultLayout(config); + PatternLayout layout = Log4JConfig.getPatternLayout(); Appender fileAppender = OutputStreamAppender.createAppender(layout, null, fout, fileName, false, true); ConsoleAppender consoleAppender = ConsoleAppender.createDefaultAppenderForLayout(layout); diff --git a/Src/PRuntimes/PSymRuntime/src/test/java/psym/TestCaseExecutor.java b/Src/PRuntimes/PSymRuntime/src/test/java/psym/TestCaseExecutor.java index b9c2e8354..2cb45e050 100644 --- a/Src/PRuntimes/PSymRuntime/src/test/java/psym/TestCaseExecutor.java +++ b/Src/PRuntimes/PSymRuntime/src/test/java/psym/TestCaseExecutor.java @@ -133,23 +133,18 @@ static int runTestCase( StreamGobbler outstreamGobbler = new StreamGobbler(process.getInputStream(), System.out::println); Executors.newSingleThreadExecutor().submit(outstreamGobbler); - int exitCode = process.waitFor(); + resultCode = process.waitFor(); - if (exitCode == 0) { + if (resultCode == 0) { PSymTestLogger.log(" ok"); - resultCode = 0; - } else if (exitCode == 2) { + } else if (resultCode == 2) { PSymTestLogger.log(" bug"); - resultCode = 2; - } else if (exitCode == 3) { + } else if (resultCode == 3) { PSymTestLogger.log(" timeout"); - resultCode = 2; - } else if (exitCode == 4) { + } else if (resultCode == 4) { PSymTestLogger.log(" memout"); - resultCode = 2; } else { PSymTestLogger.log(" error"); - resultCode = 2; } } catch (IOException | InterruptedException e) { PSymTestLogger.error(" fail"); diff --git a/Src/PRuntimes/PSymRuntime/src/test/java/psym/TestSymbolicRegression.java b/Src/PRuntimes/PSymRuntime/src/test/java/psym/TestSymbolicRegression.java index 6be410bd7..747be6edb 100644 --- a/Src/PRuntimes/PSymRuntime/src/test/java/psym/TestSymbolicRegression.java +++ b/Src/PRuntimes/PSymRuntime/src/test/java/psym/TestSymbolicRegression.java @@ -23,11 +23,10 @@ * ../Tst/SymbolicRegressionTests/ */ public class TestSymbolicRegression { - private static String mode = "verification"; - private static String runArgs = "--seed 0 --timeout 60"; private static final String outputDirectory = "output/testCases"; private static final List excluded = new ArrayList<>(); - + private static String mode = "verification"; + private static String runArgs = "--seed 0 --timeout 60 --max-steps 300"; private static boolean initialized = false; private static void setRunArgs() { @@ -35,7 +34,14 @@ private static void setRunArgs() { String psymArgs = System.getProperty("psym.args"); if (md != null && !md.isEmpty()) { - mode = md; + switch (md) { + case "verification": + case "coverage": + mode = md; + break; + default: + break; + } } if (psymArgs != null && !psymArgs.isEmpty()) { runArgs += " --psym-args " + psymArgs; From 795361243ddfae59ffda2eb07f343b841099615f Mon Sep 17 00:00:00 2001 From: Aman Goel Date: Wed, 19 Jul 2023 14:34:04 -0700 Subject: [PATCH 2/6] [PCover] Add CI (#624) * [PSym] updates Correct symbolic set comparison for empty sets [PCover] Correct terminal liveness check with state caching * [CI] Add GitHub action for PCover * [CI] Minor * [PCover] throw detected cycles as bugs * [PCover] Report detected infinite execution due to cycle as error only if --fail-on-maxsteps is enabled * [PCover] minor * [PCover] ci: limit schedules explored * Add badges for new CI in readme * [PSym] ci: remove fixing seed Minor printing changes as well --- .github/workflows/pcover.yml | 40 +++++++++++++++++++ README.md | 2 + .../main/java/psym/runtime/PSymGlobal.java | 10 +---- .../psym/runtime/logger/ScheduleWriter.java | 12 ++++-- .../runtime/machine/buffer/SymbolicQueue.java | 12 +++--- .../psym/runtime/scheduler/Scheduler.java | 2 + .../explicit/ExplicitSearchScheduler.java | 20 +++++++--- .../scheduler/replay/ReplayScheduler.java | 4 ++ .../src/main/java/psym/utils/Assert.java | 26 ++++++++++-- .../main/java/psym/valuesummary/SetVS.java | 6 +++ .../java/psym/TestSymbolicRegression.java | 2 +- 11 files changed, 110 insertions(+), 26 deletions(-) create mode 100644 .github/workflows/pcover.yml diff --git a/.github/workflows/pcover.yml b/.github/workflows/pcover.yml new file mode 100644 index 000000000..9037f6d58 --- /dev/null +++ b/.github/workflows/pcover.yml @@ -0,0 +1,40 @@ +# This workflow will build and test PCover, and cache/restore any dependencies to improve the workflow execution time +# For more information see: https://help.github.com/actions/language-and-framework-guides/building-and-testing-java-with-maven + +name: PCover on Ubuntu + +on: + push: + pull_request: + workflow_dispatch: + inputs: + args: + description: Additional arguments + default: "" + required: false + +jobs: + PCover-Build-And-Test-Ubuntu: + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v1 + - name: Setup .NET Core + uses: actions/setup-dotnet@v1 + with: + dotnet-version: 6.0.x + - name: Set up JDK + uses: actions/setup-java@v1 + with: + java-version: 11 + - name: Cache Maven packages + uses: actions/cache@v2 + with: + path: ~/.m2 + key: ${{ runner.os }}-m2-${{ hashFiles('**/pom.xml') }} + restore-keys: ${{ runner.os }}-m2 + - name: Build PCover + working-directory: Src/PRuntimes/PSymRuntime + run: ./scripts/build.sh + - name: Test PCover + working-directory: Src/PRuntimes/PSymRuntime + run: mvn test -Dmode="coverage" diff --git a/README.md b/README.md index 0d1746bf1..4dbce73f1 100644 --- a/README.md +++ b/README.md @@ -9,6 +9,8 @@ ![GitHub Action (CI on Ubuntu)](https://github.com/p-org/P/workflows/CI%20on%20Ubuntu/badge.svg) ![GitHub Action (CI on MacOS)](https://github.com/p-org/P/workflows/CI%20on%20MacOS/badge.svg) [![Tutorials](https://github.com/p-org/P/actions/workflows/tutorials.yml/badge.svg)](https://github.com/p-org/P/actions/workflows/tutorials.yml) +[![PSym](https://github.com/p-org/P/actions/workflows/psym.yml/badge.svg)](https://github.com/p-org/P/actions/workflows/psym.yml) +[![PCover](https://github.com/p-org/P/actions/workflows/pcover.yml/badge.svg)](https://github.com/p-org/P/actions/workflows/pcover.yml) **Challenge**: Distributed systems are notoriously hard to get right. Programming these systems is challenging because of the need to reason about correctness in the presence of myriad possible interleaving of messages and failures. Unsurprisingly, it is common for service teams to uncover correctness bugs after deployment. Formal methods can play an important role in addressing this challenge! diff --git a/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/PSymGlobal.java b/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/PSymGlobal.java index ce4e50f83..0056e3792 100644 --- a/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/PSymGlobal.java +++ b/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/PSymGlobal.java @@ -151,21 +151,15 @@ public static void initializeSymmetryTracker(boolean isSymbolic) { public static void printStackTrace(Exception e, boolean stderrOnly) { if (stderrOnly) { - System.err.println("-----------"); - System.err.println("Stack Trace"); - System.err.println("-----------"); + System.err.println("... Stack trace:"); e.printStackTrace(System.err); - System.err.println("-----------"); } else { StringWriter sw = new StringWriter(); PrintWriter pw = new PrintWriter(sw); e.printStackTrace(pw); - PSymLogger.info("-----------"); - PSymLogger.info("Stack Trace"); - PSymLogger.info("-----------"); + PSymLogger.info("... Stack trace:"); PSymLogger.info(sw.toString()); - PSymLogger.info("-----------"); } } } diff --git a/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/logger/ScheduleWriter.java b/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/logger/ScheduleWriter.java index 0a5ef138b..8b138fcdf 100644 --- a/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/logger/ScheduleWriter.java +++ b/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/logger/ScheduleWriter.java @@ -11,6 +11,9 @@ import psym.runtime.machine.State; import psym.runtime.machine.events.Event; import psym.runtime.machine.events.Message; +import psym.utils.Assert; +import psym.utils.exception.LivenessException; +import psym.valuesummary.Guard; import psym.valuesummary.GuardedValue; import psym.valuesummary.PrimitiveVS; @@ -115,11 +118,14 @@ public static void logHeader() { if (!PSymGlobal.getConfiguration().getTestDriver().equals(PSymGlobal.getConfiguration().getTestDriverDefault())) { log(String.format("--test-method:%s", PSymGlobal.getConfiguration().getTestDriver())); } + if (Assert.getFailureType().equals("cycle")) { + log(String.format("--cycle-detected: %s", Assert.getFailureMsg())); + } logComment("create GodMachine"); - log("Task(0)"); + log("(0)"); logComment("start GodMachine"); - log("Plang.CSharpRuntime._GodMachine(1)"); + log("(1)"); logComment("create Main(2)"); - log("Plang.CSharpRuntime._GodMachine(1)"); + log("(1)"); } } diff --git a/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/machine/buffer/SymbolicQueue.java b/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/machine/buffer/SymbolicQueue.java index 3128b04ed..7256d7bdc 100644 --- a/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/machine/buffer/SymbolicQueue.java +++ b/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/machine/buffer/SymbolicQueue.java @@ -6,10 +6,7 @@ import psym.runtime.machine.Machine; import psym.runtime.machine.events.Message; import psym.runtime.scheduler.symmetry.SymmetryMode; -import psym.valuesummary.Guard; -import psym.valuesummary.ListVS; -import psym.valuesummary.PrimitiveVS; -import psym.valuesummary.ValueSummary; +import psym.valuesummary.*; /** * Represents a event-queue implementation using value summaries @@ -63,7 +60,12 @@ private Message peekOrDequeueHelper(Guard pc, boolean dequeue) { } Message ret = peek.restrict(pc); if (dequeue) { - elements = elements.removeAt(new PrimitiveVS<>(0).restrict(pc)); + PrimitiveVS idxVs = new PrimitiveVS<>(0, pc); + Guard outOfRange = elements.inRange(idxVs).getGuardFor(false); + if (!outOfRange.isFalse()) { + throw new RuntimeException("Internal error: dequeing from an empty queue"); + } + elements = elements.removeAt(idxVs); resetPeek(); } assert (!pc.isFalse()); diff --git a/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/scheduler/Scheduler.java b/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/scheduler/Scheduler.java index c9d1f3786..220367d63 100644 --- a/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/scheduler/Scheduler.java +++ b/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/scheduler/Scheduler.java @@ -48,6 +48,8 @@ public abstract class Scheduler implements SchedulerInterface { protected Boolean stickyStep = true; /** Flag whether current execution finished */ protected Guard allMachinesHalted = Guard.constFalse(); + /** Flag whether check for liveness at the end */ + protected boolean terminalLivenessEnabled = true; /** List of monitors instances */ List monitors; /** The machine to start with */ diff --git a/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/scheduler/explicit/ExplicitSearchScheduler.java b/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/scheduler/explicit/ExplicitSearchScheduler.java index 93ef63878..aef5ba64f 100644 --- a/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/scheduler/explicit/ExplicitSearchScheduler.java +++ b/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/scheduler/explicit/ExplicitSearchScheduler.java @@ -186,7 +186,9 @@ protected void performSearch() throws TimeoutException { step(); checkLiveness(allMachinesHalted); } - checkLiveness(Guard.constTrue()); + if (terminalLivenessEnabled) { + checkLiveness(Guard.constTrue()); + } Assert.prop( !PSymGlobal.getConfiguration().isFailOnMaxStepBound() || (getDepth() < PSymGlobal.getConfiguration().getMaxStepBound()), "Scheduling steps bound of " + PSymGlobal.getConfiguration().getMaxStepBound() + " reached.", @@ -217,11 +219,15 @@ protected void step() throws TimeoutException { if (!isDistinctState) { int firstVisitIter = numConcrete[2]; if (firstVisitIter == iter) { - allMachinesHalted = Guard.constTrue(); -// Assert.liveness( -// false, -// String.format("Cycle detected: Possible infinite loop found due to revisiting a state multiple times in the same iteration"), -// Guard.constTrue()); + if (PSymGlobal.getConfiguration().isFailOnMaxStepBound()) { + Assert.cycle( + false, + String.format("Cycle detected: Infinite loop found due to revisiting a state multiple times in the same iteration"), + Guard.constTrue()); + } + } else { + // early termination (without cycle) + terminalLivenessEnabled = false; } done = Guard.constTrue(); SearchLogger.finishedExecution(depth); @@ -917,6 +923,7 @@ public void reset() { schedule.setSchedulerChoiceDepth(getChoiceDepth()); schedule.setSchedulerState(srcState, machineCounters); schedule.setSchedulerSymmetry(); + terminalLivenessEnabled = true; } public void reset_stats() { @@ -947,6 +954,7 @@ public void restore(int d, int cd) { depth = d; choiceDepth = cd; done = Guard.constFalse(); + terminalLivenessEnabled = true; } public void restoreState(Schedule.ChoiceState state) { diff --git a/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/scheduler/replay/ReplayScheduler.java b/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/scheduler/replay/ReplayScheduler.java index a1c0281d2..15043aa70 100644 --- a/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/scheduler/replay/ReplayScheduler.java +++ b/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/scheduler/replay/ReplayScheduler.java @@ -16,6 +16,7 @@ import psym.runtime.scheduler.Schedule; import psym.runtime.scheduler.Scheduler; import psym.utils.Assert; +import psym.utils.exception.LivenessException; import psym.valuesummary.*; public class ReplayScheduler extends Scheduler { @@ -85,6 +86,9 @@ protected void performSearch() throws TimeoutException { checkLiveness(allMachinesHalted); } checkLiveness(Guard.constTrue()); + if (Assert.getFailureType().equals("cycle")) { + throw new LivenessException(Assert.getFailureMsg(), Guard.constTrue()); + } Assert.prop( !PSymGlobal.getConfiguration().isFailOnMaxStepBound() || (getDepth() < PSymGlobal.getConfiguration().getMaxStepBound()), "Scheduling steps bound of " + PSymGlobal.getConfiguration().getMaxStepBound() + " reached.", diff --git a/Src/PRuntimes/PSymRuntime/src/main/java/psym/utils/Assert.java b/Src/PRuntimes/PSymRuntime/src/main/java/psym/utils/Assert.java index 795b58578..eb4f4ecd5 100644 --- a/Src/PRuntimes/PSymRuntime/src/main/java/psym/utils/Assert.java +++ b/Src/PRuntimes/PSymRuntime/src/main/java/psym/utils/Assert.java @@ -2,6 +2,8 @@ import java.util.List; import java.util.stream.Collectors; + +import lombok.Getter; import psym.utils.exception.BugFoundException; import psym.utils.exception.LivenessException; import psym.valuesummary.Guard; @@ -9,26 +11,44 @@ import psym.valuesummary.PrimitiveVS; public class Assert { + @Getter + private static String failureType = ""; + @Getter + private static String failureMsg = ""; public static void prop(boolean p, String msg, Guard pc) { if (!p) { - throw new BugFoundException("Property violated: " + msg, pc); + failureType = "prop"; + failureMsg = "Property violated: " + msg; + throw new BugFoundException(failureMsg, pc); } } public static void progProp(boolean p, PrimitiveVS msg, Guard pc) { if (!p) { + failureType = "progProp"; List msgs = msg.restrict(pc).getGuardedValues().stream() .map(GuardedValue::getValue) .collect(Collectors.toList()); - throw new BugFoundException("Properties violated: " + msgs, pc); + failureMsg = "Properties violated: " + msgs; + throw new BugFoundException(failureMsg, pc); } } public static void liveness(boolean p, String msg, Guard pc) { if (!p) { - throw new LivenessException("Property violated: " + msg, pc); + failureType = "liveness"; + failureMsg = "Property violated: " + msg; + throw new LivenessException(failureMsg, pc); + } + } + + public static void cycle(boolean p, String msg, Guard pc) { + if (!p) { + failureType = "cycle"; + failureMsg = "Property violated: " + msg; + throw new LivenessException(failureMsg, pc); } } } diff --git a/Src/PRuntimes/PSymRuntime/src/main/java/psym/valuesummary/SetVS.java b/Src/PRuntimes/PSymRuntime/src/main/java/psym/valuesummary/SetVS.java index 4355c8f0a..e54cd13ad 100644 --- a/Src/PRuntimes/PSymRuntime/src/main/java/psym/valuesummary/SetVS.java +++ b/Src/PRuntimes/PSymRuntime/src/main/java/psym/valuesummary/SetVS.java @@ -122,6 +122,12 @@ public PrimitiveVS symbolicEquals(SetVS cmp, Guard pc) { for (T rhs : cmp.elements.getItems()) { equalCond = equalCond.and(this.contains(rhs).getGuardFor(true)); } + // check case where both empty + Guard thisEmpty = this.elements.size().getGuardFor(0); + if (!thisEmpty.isFalse()) { + Guard cmpEmpty = cmp.elements.size().getGuardFor(0); + equalCond = equalCond.or(thisEmpty.and(cmpEmpty)); + } return BooleanVS.trueUnderGuard(equalCond).restrict(getUniverse().and(cmp.getUniverse())); } diff --git a/Src/PRuntimes/PSymRuntime/src/test/java/psym/TestSymbolicRegression.java b/Src/PRuntimes/PSymRuntime/src/test/java/psym/TestSymbolicRegression.java index 747be6edb..240d056fd 100644 --- a/Src/PRuntimes/PSymRuntime/src/test/java/psym/TestSymbolicRegression.java +++ b/Src/PRuntimes/PSymRuntime/src/test/java/psym/TestSymbolicRegression.java @@ -26,7 +26,7 @@ public class TestSymbolicRegression { private static final String outputDirectory = "output/testCases"; private static final List excluded = new ArrayList<>(); private static String mode = "verification"; - private static String runArgs = "--seed 0 --timeout 60 --max-steps 300"; + private static String runArgs = "--timeout 60 --iterations 100 --max-steps 300"; private static boolean initialized = false; private static void setRunArgs() { From 1bff0755af1cf7e1714083534293d89be45bff42 Mon Sep 17 00:00:00 2001 From: Ankush Desai Date: Wed, 19 Jul 2023 15:56:35 -0700 Subject: [PATCH 3/6] Fixed Minor bug (#625) --- Src/PChecker/CheckerCore/SystematicTesting/TestingEngine.cs | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) diff --git a/Src/PChecker/CheckerCore/SystematicTesting/TestingEngine.cs b/Src/PChecker/CheckerCore/SystematicTesting/TestingEngine.cs index 19c9b61a2..acdc66c39 100644 --- a/Src/PChecker/CheckerCore/SystematicTesting/TestingEngine.cs +++ b/Src/PChecker/CheckerCore/SystematicTesting/TestingEngine.cs @@ -535,7 +535,7 @@ public string GetReport() /// /// Tries to emit the testing traces, if any. /// - public IEnumerable TryEmitTraces(string directory, string file) + public void TryEmitTraces(string directory, string file) { var index = 0; // Find the next available file index. @@ -566,7 +566,6 @@ public IEnumerable TryEmitTraces(string directory, string file) Logger.WriteLine($"..... Writing {readableTracePath}"); File.WriteAllText(readableTracePath, ReadableTrace); - yield return readableTracePath; } } @@ -575,7 +574,6 @@ public IEnumerable TryEmitTraces(string directory, string file) var xmlPath = directory + file + "_" + index + ".trace.xml"; Logger.WriteLine($"..... Writing {xmlPath}"); File.WriteAllText(xmlPath, XmlLog.ToString()); - yield return xmlPath; } if (Graph != null) @@ -583,7 +581,6 @@ public IEnumerable TryEmitTraces(string directory, string file) var graphPath = directory + file + "_" + index + ".dgml"; Graph.SaveDgml(graphPath, true); Logger.WriteLine($"..... Writing {graphPath}"); - yield return graphPath; } if (!_checkerConfiguration.PerformFullExploration) @@ -595,7 +592,6 @@ public IEnumerable TryEmitTraces(string directory, string file) Logger.WriteLine($"..... Writing {reproTracePath}"); File.WriteAllText(reproTracePath, ReproducableTrace); - yield return reproTracePath; } } From 601b778bee0f97be0cf4471af8c1ff8e42a93a5c Mon Sep 17 00:00:00 2001 From: haoran-wen <137958518+haoran-wen@users.noreply.github.com> Date: Wed, 19 Jul 2023 16:43:45 -0700 Subject: [PATCH 4/6] Feature/log json formatter (#623) * functional json formatter that outputs a json format need to decide on the best json schema * added JsonFormatter for JSON error trace, added JsonWriter to help with JsonFormatter * fixed typo in strategyDescription * created PJsonFormatter, restructured code to fix cyclic dependency issue * added vector clock generation in json writer, restructured jsonwriter for better code practices * syntax tweak to keep with original style * PCheckerOptions syntax tweak to keep with original style * fixed xml warnings and possible null input warning * renamed _globalVcMap, removed Timers * removed field jsonPath to accommodate main branch changes --------- Co-authored-by: Aman Goel Co-authored-by: Ankush Desai --- .../CheckerCore/Actors/ActorRuntime.cs | 6 + .../Logging/ActorRuntimeLogJsonFormatter.cs | 182 +++++ .../CheckerCore/Actors/Logging/JsonWriter.cs | 678 ++++++++++++++++++ .../CheckerCore/Actors/Logging/LogWriter.cs | 20 +- .../CheckerCore/CheckerConfiguration.cs | 12 +- .../SystematicTesting/TestingEngine.cs | 19 +- .../Testing/TestingProcessFactory.cs | 5 + .../Backend/CSharp/CSharpCodeGenerator.cs | 1 + .../PCSharpRuntime/PJsonFormatter.cs | 590 +++++++++++++++ 9 files changed, 1509 insertions(+), 4 deletions(-) create mode 100644 Src/PChecker/CheckerCore/Actors/Logging/ActorRuntimeLogJsonFormatter.cs create mode 100644 Src/PChecker/CheckerCore/Actors/Logging/JsonWriter.cs create mode 100644 Src/PRuntimes/PCSharpRuntime/PJsonFormatter.cs diff --git a/Src/PChecker/CheckerCore/Actors/ActorRuntime.cs b/Src/PChecker/CheckerCore/Actors/ActorRuntime.cs index 5ab7f5189..b5ec87f98 100644 --- a/Src/PChecker/CheckerCore/Actors/ActorRuntime.cs +++ b/Src/PChecker/CheckerCore/Actors/ActorRuntime.cs @@ -692,6 +692,12 @@ internal void NotifyMonitorError(Monitor monitor) /// public override TextWriter SetLogger(TextWriter logger) => LogWriter.SetLogger(logger); + + /// + /// Sets the JsonLogger in LogWriter.cs + /// + /// jsonLogger instance + public void SetJsonLogger(JsonWriter jsonLogger) => LogWriter.SetJsonLogger(jsonLogger); /// /// Use this method to register an . diff --git a/Src/PChecker/CheckerCore/Actors/Logging/ActorRuntimeLogJsonFormatter.cs b/Src/PChecker/CheckerCore/Actors/Logging/ActorRuntimeLogJsonFormatter.cs new file mode 100644 index 000000000..0d2495220 --- /dev/null +++ b/Src/PChecker/CheckerCore/Actors/Logging/ActorRuntimeLogJsonFormatter.cs @@ -0,0 +1,182 @@ +// Copyright (c) Microsoft Corporation. +// Licensed under the MIT License. + +using System; +using PChecker.Actors.Events; + +namespace PChecker.Actors.Logging +{ + /// + /// This class implements IActorRuntimeLog and generates log output in an XML format. + /// + public class ActorRuntimeLogJsonFormatter : IActorRuntimeLog + { + /// + /// Get or set the JsonWriter to write to. + /// + public JsonWriter Writer { get; set; } + + /// + /// Initializes a new instance of the class. + /// + protected ActorRuntimeLogJsonFormatter() + { + Writer = new JsonWriter(); + } + + /// + public virtual void OnCompleted() + { + } + + /// + public virtual void OnAssertionFailure(string error) + { + } + + /// + public virtual void OnCreateActor(ActorId id, string creatorName, string creatorType) + { + } + + /// + public virtual void OnCreateStateMachine(ActorId id, string creatorName, string creatorType) + { + } + + /// + public virtual void OnDefaultEventHandler(ActorId id, string stateName) + { + } + + /// + public virtual void OnDequeueEvent(ActorId id, string stateName, Event e) + { + } + + /// + public virtual void OnEnqueueEvent(ActorId id, Event e) + { + } + + /// + public virtual void OnExceptionHandled(ActorId id, string stateName, string actionName, Exception ex) + { + } + + /// + public virtual void OnExceptionThrown(ActorId id, string stateName, string actionName, Exception ex) + { + } + + /// + public virtual void OnExecuteAction(ActorId id, string handlingStateName, string currentStateName, + string actionName) + { + } + + /// + public virtual void OnGotoState(ActorId id, string currentStateName, string newStateName) + { + } + + /// + public virtual void OnHalt(ActorId id, int inboxSize) + { + } + + /// + public virtual void OnHandleRaisedEvent(ActorId id, string stateName, Event e) + { + } + + /// + public virtual void OnPopState(ActorId id, string currentStateName, string restoredStateName) + { + } + + /// + public virtual void OnPopStateUnhandledEvent(ActorId id, string stateName, Event e) + { + } + + /// + public virtual void OnPushState(ActorId id, string currentStateName, string newStateName) + { + } + + /// + public virtual void OnRaiseEvent(ActorId id, string stateName, Event e) + { + } + + /// + public virtual void OnReceiveEvent(ActorId id, string stateName, Event e, bool wasBlocked) + { + } + + /// + public virtual void OnSendEvent(ActorId targetActorId, string senderName, string senderType, + string senderStateName, + Event e, Guid opGroupId, bool isTargetHalted) + { + } + + /// + public virtual void OnStateTransition(ActorId id, string stateName, bool isEntry) + { + } + + /// + public virtual void OnWaitEvent(ActorId id, string stateName, Type eventType) + { + } + + /// + public virtual void OnWaitEvent(ActorId id, string stateName, params Type[] eventTypes) + { + } + + /// + public virtual void OnCreateMonitor(string monitorType) + { + } + + /// + public virtual void OnMonitorExecuteAction(string monitorType, string stateName, string actionName) + { + } + + /// + public virtual void OnMonitorProcessEvent(string monitorType, string stateName, string senderName, + string senderType, string senderStateName, Event e) + { + } + + /// + public virtual void OnMonitorRaiseEvent(string monitorType, string stateName, Event e) + { + } + + /// + public virtual void OnMonitorStateTransition(string monitorType, string stateName, bool isEntry, + bool? isInHotState) + { + } + + /// + public virtual void OnMonitorError(string monitorType, string stateName, bool? isInHotState) + { + } + + /// + public virtual void OnRandom(object result, string callerName, string callerType) + { + } + + /// + public virtual void OnStrategyDescription(string strategyName, string description) + { + } + } +} \ No newline at end of file diff --git a/Src/PChecker/CheckerCore/Actors/Logging/JsonWriter.cs b/Src/PChecker/CheckerCore/Actors/Logging/JsonWriter.cs new file mode 100644 index 000000000..a13d2cdbe --- /dev/null +++ b/Src/PChecker/CheckerCore/Actors/Logging/JsonWriter.cs @@ -0,0 +1,678 @@ +#nullable enable +using System; +using System.Linq; +using System.Text; +using System.Text.Json; +using System.Collections.Generic; +using System.Security.Cryptography; +using System.Text.Json.Serialization; + +namespace PChecker.Actors.Logging +{ + /// + /// Class for handling generating the vector clock for a log entry + /// + internal class VectorClockGenerator + { + /// + /// Nested class for handling FIFO send receive requests. + /// NOTE: In the case of sending to a the same machine with the same event and same payload. + /// + private class FifoSendReceiveMapping + { + /// + /// Private property for the number of counts of sends of the same machine, event, and payload. + /// + private int _sent { get; set; } + + /// + /// Private property for the number of counts of receives of the same machine, event, and payload. + /// + private int _received { get; set; } + + /// + /// Public getter and setter for _sent. + /// + public int SentCount + { + get => _sent; + set => _sent = value; + } + + /// + /// Public getter and setter for _received. + /// + public int ReceivedCount + { + get => _received; + set => _received = value; + } + + /// + /// Constructor for FifoSendReceiveMapping. + /// Set _sent and _received to 0 initially. + /// + internal FifoSendReceiveMapping() + { + _sent = 0; + _received = 0; + } + } + + /// + /// Field declaration that keeps track of a global vector clock map of all the machines. + /// + private readonly Dictionary> _contextVcMap; + + /// + /// Field declaration that keeps track of unprocessed send requests. I.e., when a send request happened + /// but hasn't had a corresponding receive event of it. + /// + private readonly Dictionary> _unhandledSendRequests; + + /// + /// Hash set to keep track of all unique machines. + /// + private readonly HashSet _machines; + + /// + /// Field declaration to keep track of send requests with the same target machine, event name, and payload. + /// + private readonly Dictionary _sendRequestsCount; + + /// + /// VectorClockGenerator constructor + /// Initialize empty mappings for _contextVcMap, _unhandledSendRequests, _machines, and _sendRequestsCount. + /// + public VectorClockGenerator() + { + _contextVcMap = new Dictionary>(); + _unhandledSendRequests = new Dictionary>(); + _machines = new HashSet(); + _sendRequestsCount = new Dictionary(); + } + + /// + /// Checks to see if machine name is new. + /// + /// Machine name + /// bool: true when machine is new, false otherwise. + private bool MachineIsNew(string machine) => !_machines.Contains(machine); + + /// + /// Get the machine name for appropriate naming of the vector clock map. + /// + /// Of type LogDetails: only names can be extracted from Id, Monitor, or Sender + /// string: the name of the machine for the type among the possible attributes containing the machine name. + private static string GetMachineName(LogDetails logDetails) => + (logDetails.Id ?? logDetails.Monitor ?? logDetails.Sender)!; + + /// + /// Hashes a string. + /// + /// Some string input. + /// string: the hashed string result. + private static string HashString(string input) + { + using var sha256 = SHA256.Create(); + var inputBytes = Encoding.UTF8.GetBytes(input); + var hashBytes = sha256.ComputeHash(inputBytes); + return Convert.ToBase64String(hashBytes); + } + + /// + /// Makes a copy of the vector clock map. + /// + /// Of type Dictionary<string, int>: the original vector clock map needed to be copied. + /// Dictionary<string, int>: the copied vector clock map. + private static Dictionary CopyVcMap(Dictionary vcMap) => + vcMap.ToDictionary(entry => entry.Key, entry => entry.Value); + + /// + /// Converts payload from json to string representation. + /// + /// Of type Dictionary<string, string>: JSON representation of payload. + /// string: string representation of payload. + private static string ConvertPayloadToString(Dictionary? eventPayload) + { + // If no payload, return empty string. + if (eventPayload is null) + { + return string.Empty; + } + + // Construct the string payload in the format as follows: { key: val, key2: val2, ... } + var stringBuilder = new StringBuilder(); + foreach (var kvp in eventPayload) + { + stringBuilder.Append($"{kvp.Key}: {kvp.Value}, "); + } + + // Remove the last ", " + if (stringBuilder.Length >= 2) + { + stringBuilder.Length -= 2; + } + + return $"{{ {stringBuilder} }}"; + } + + /// + /// Gets the unique string to be hashed that contain information regarding a send/receive event. + /// In the case of a send, machineName will be the target machine that's to be sent to. + /// In the case of a receive, machineName will simply be the machine that receives it. + /// + /// of type string: name of the machine. + /// Of type string: name of the event. + /// Of type Dictionary<string, string>: payload of the event, if there is any. + /// string: the string containing all information. + private static string GetSendReceiveId(string? machineName, string? eventName, + Dictionary? eventPayload) => + $"_{machineName}:_{eventName}:_{ConvertPayloadToString(eventPayload)}"; + + /// + /// Main method to update the vector clock mappings. + /// + /// Of type LogEntry: the log entry information. Directly modifies the logEntry with the vector clock + public void HandleLogEntry(LogEntry logEntry) + { + // Get the type, and details of the log and get the machine name associated with it. + var logType = logEntry.Type; + var logDetails = logEntry.Details; + var machine = GetMachineName(logDetails); + + // If new machine, create a new mapping for it in the _contextVcMap and add it to _machines. + if (MachineIsNew(machine)) + { + _machines.Add(machine); + _contextVcMap.Add(machine, new Dictionary { { machine, 0 } }); + } + + // Always update the local machine count by one on any event. + _contextVcMap[machine][machine] += 1; + + switch (logType) + { + // On send event, hash the string containing information about the target machine to be sent to, the event name, and payload + // This is used as an unique id necessary to correctly update the vector clock for the right machine-event-payload combo that + // receives it later. + case "SendEvent": + var targetMachine = logDetails.Target; + var sendReqId = GetSendReceiveId(targetMachine, logDetails.Event, logDetails.Payload); + var hashedGeneralSendReqId = HashString(sendReqId); + + // If we have seen this sendReqId before, increment the sent count of it in _sendRequestsCount + if (_sendRequestsCount.TryGetValue(hashedGeneralSendReqId, out var generalSendReqIdValue)) + { + generalSendReqIdValue.SentCount += 1; + } + // Else, create an instance of FifoSendReceiveMapping corresponding to the sendReqId in _sendRequestsCount. + else + { + _sendRequestsCount.Add(hashedGeneralSendReqId, new FifoSendReceiveMapping()); + } + + // Update the sendReqId with the send count of it. + sendReqId += $":_{_sendRequestsCount[hashedGeneralSendReqId].SentCount}"; + var hashedSendReqId = HashString(sendReqId); + _unhandledSendRequests.Add(hashedSendReqId, CopyVcMap(_contextVcMap[machine])); + break; + + // On dequeue event, has the string containing information about the current machine that dequeued (i.e. received the event), + // the event name, and payload. This is used to find the corresponding SendReqId from the machine that sent it in order to retrieve + // the vector clock of the sender machine during that time when it was sent. + case "DequeueEvent": + var correspondingSendReqId = GetSendReceiveId(machine, logDetails.Event, logDetails.Payload); + var hashedGeneralCorrespondingSendReqId = HashString(correspondingSendReqId); + var correspondingSendReqIdReceiveCount = + _sendRequestsCount[hashedGeneralCorrespondingSendReqId].ReceivedCount; + + // If we have handled all sent requests (i.e. received count is the same as sent count for the general sendReqId), + // remove it from _sendRequestsCount. + if (correspondingSendReqIdReceiveCount == + _sendRequestsCount[hashedGeneralCorrespondingSendReqId].SentCount) + { + _sendRequestsCount.Remove(hashedGeneralCorrespondingSendReqId); + } + // If not, increment received count. + else + { + _sendRequestsCount[hashedGeneralCorrespondingSendReqId].ReceivedCount += 1; + } + + correspondingSendReqId += $":_{correspondingSendReqIdReceiveCount}"; + var hashedCorrespondingSendReqId = HashString(correspondingSendReqId); + var senderVcMap = _unhandledSendRequests[hashedCorrespondingSendReqId]; + + // Get a set of all machine names to update between the sender vc map and the current machine vc map (minus the current machine) + var machinesToUpdateInVc = + new HashSet( + _contextVcMap[machine].Keys.Union(senderVcMap.Keys).Except(new[] { machine })); + + // Update local machine's vector clock in _contextVcMap, outside of itself, since it was already updated (incremented) from above + // right before the switch case. + // The rule for the remaining machines to be updated is taking the max between the sender machine's vector clock at that time and + // the current machine's vector clock. Details can be found here: https://en.wikipedia.org/wiki/Vector_clock + foreach (var machineToUpdate in machinesToUpdateInVc) + { + if (_contextVcMap[machine].TryGetValue(machineToUpdate, out var localMachineToUpdateValue)) + { + if (senderVcMap.TryGetValue(machineToUpdate, out var senderMachineToUpdateValue)) + { + _contextVcMap[machine][machineToUpdate] = + Math.Max(senderMachineToUpdateValue, localMachineToUpdateValue); + } + } + else + { + _contextVcMap[machine].Add(machineToUpdate, senderVcMap[machineToUpdate]); + } + } + + // Remove the SendReqId because we've processed it. + _unhandledSendRequests.Remove(hashedCorrespondingSendReqId); + break; + } + + // Update the log entry with the vector clock. + logEntry.Details.Clock = CopyVcMap(_contextVcMap[machine]); + } + } + + /// + /// + /// + public class LogEntry + { + /// + /// The log type of the log entry. + /// + public string? Type { get; set; } + + /// + /// The details of the log entry. + /// + public LogDetails Details { get; set; } + + /// + /// LogEntry constructor. + /// + public LogEntry() + { + Details = new LogDetails(); + } + } + + /// + /// Enum representing the possible attributes in the details dictionary, + /// which represents the data associated with a specific log type. All of + /// the following are available or expanded parameters associated with an + /// IActorRuntime method. Naming for them is mostly the same except some + /// are changed for simplicity. + /// I.e., for OnRaiseEvent(ActorId id, string, stateName, Event e), it + /// will have attributes id, state (simplified from stateName, event + /// (simplified from eventName within Event e), and payload (in Event e). + /// + public class LogDetails + { + /// + /// The text log from PLogFormatter. Removes the log tags. + /// I.e., no <SomeLog> in the beginning. + /// Available for all log types. + /// + public string? Log { get; set; } + + /// + /// The actor id. + /// + public string? Id { get; set; } + + /// + /// The error message if an error occurs. + /// + public string? Error { get; set; } + + /// + /// The event name. I.e. eWithDrawReq, etc... + /// + public string? Event { get; set; } + + /// + /// Name of creator. + /// + public string? CreatorName { get; set; } + + /// + /// Type of creator. + /// + public string? CreatorType { get; set; } + + /// + /// The state associated with an event, machine, etc... + /// + public string? State { get; set; } + + /// + /// The initial state associated with an event, machine, etc... + /// Available for log types GotoState, PopState, PushState + /// + public string? StartState { get; set; } + + /// + /// The initial state associated with an event, machine, etc... + /// Available for log types GotoState, PopState, PushState + /// + public string? EndState { get; set; } + + /// + /// Payload of an event. Represented in dictionary object. + /// I.e. + /// { + /// "source": "Client(4)", + /// "accountId": "0", + /// "amount": "52", + /// "rId": "1" + /// } + /// + public Dictionary? Payload { get; set; } + + /// + /// The action being executed. + /// Available for log type ExceptionHandled and ExceptionThrown. + /// + public string? Action { get; set; } + + /// + /// The name of the exception. + /// Available for log type ExceptionHandled and ExceptionThrown. + /// + public string? Exception { get; set; } + + /// + /// Approximate size of the inbox. + /// Available for log type Halt. + /// + public int? HaltInboxSize { get; set; } + + /// + /// Boolean representing whether an actor was waiting for one or more events + /// Available for log type ReceiveEvent. + /// + public bool? WasBlocked { get; set; } + + /// + /// Name of sender. + /// Available for log type SendEvent. + /// + public string? Sender { get; set; } + + /// + /// Id of target actor. + /// Available for log type SendEvent. + /// + public string? Target { get; set; } + + /// + /// The id for the send operation. + /// Available for log type SendEvent. + /// + public string? OpGroupId { get; set; } + + /// + /// Boolean representing whether the target actor was halted. + /// Available for log type SendEvent. + /// + public bool? IsTargetHalted { get; set; } + + /// + /// Boolean representing whether it's a state entry to exit. + /// Available for log types StateTransition and MonitorStateTransition. + /// + public bool? IsEntry { get; set; } + + /// + /// Boolean representing whether monitor is in hot or cold state. + /// Available for log type MonitorStateTransition. + /// + public bool? IsInHotState { get; set; } + + /// + /// The type of the event being waited for. + /// Available for log type WaitEvent. + /// + public string? EventType { get; set; } + + /// + /// The type of events being waited for. + /// Available for log type WaitMultipleEvents. + /// + public List? EventTypes { get; set; } + + /// + /// Name of monitor. + /// Available for log types CreateMonitor, MonitorProcessEvent, + /// MonitorRaiseEvent, and MonitorStateTransition + /// + public string? Monitor { get; set; } + + /// + /// Name of strategy used. + /// Available for log type StrategyDescription. + /// + public string? Strategy { get; set; } + + /// + /// Information about the scheduling strategy. + /// Available for log type StrategyDescription. + /// + public string? StrategyDescription { get; set; } + + /// + /// Vector map of the machine associated with the log entry + /// + public Dictionary? Clock { get; set; } + } + + /// + /// JsonWriter to write the Json output. + /// + public class JsonWriter + { + /// + /// List of LogEntry. + /// + private readonly List _logs; + + /// + /// LogEntry with fields Type and Details. Represents an individual log. + /// + private LogEntry _log; + + /// + /// Vector clock generator instance to help with vector clock generation. + /// + private readonly VectorClockGenerator _vcGenerator; + + /// + /// Getter for accessing log entry details. + /// + public LogDetails LogDetails => _log.Details; + + /// + /// Initializes the Writer. Create empty _logs, _log, and _details objects. + /// + public JsonWriter() + { + _logs = new List(); + _log = new LogEntry(); + _vcGenerator = new VectorClockGenerator(); + } + + /// + /// Enum representing the different log types the JSON error trace logs. + /// Referenced from PLogFormatter.cs and ActorRuntimeLogTextFormatter.cs + /// to see what those formatter logs. Check IActorRuntimeLog.cs to see + /// each log types' description and when they are invoked. + /// + public enum LogType + { + /// + /// Invoked when the specified assertion failure has occurred. + /// + AssertionFailure, + + /// + /// Invoked when the specified actor has been created. + /// + CreateActor, + + /// + /// Invoked when the specified state machine has been created. + /// + CreateStateMachine, + + /// + /// Invoked when the specified monitor has been created. + /// + CreateMonitor, + + /// + /// Invoked when the specified actor is idle (there is nothing to dequeue) and the default + /// event handler is about to be executed. + /// + DefaultEventHandler, + + /// + /// Invoked when the specified event is dequeued by an actor. + /// + DequeueEvent, + + /// + /// Invoked when the specified OnException method is used to handle a thrown exception. + /// + ExceptionHandled, + + /// + /// Invoked when the specified actor throws an exception. + /// + ExceptionThrown, + + /// + /// Invoked when the specified state machine performs a goto transition to the specified state. + /// + GotoState, + + /// + /// Invoked when the specified actor has been halted. + /// + Halt, + + /// + /// Invoked when the specified monitor is about to process an event. + /// + MonitorProcessEvent, + + /// + /// Invoked when the specified monitor raised an event. + /// + MonitorRaiseEvent, + + /// + /// Invoked when the specified monitor enters or exits a state. + /// + MonitorStateTransition, + + /// + /// Invoked when the specified state machine has popped its current state. + /// + PopState, + + /// + /// Invoked when the specified event cannot be handled in the current state, its exit + /// handler is executed and then the state is popped and any previous "current state" + /// is reentered. This handler is called when that pop has been done. + /// + PopStateUnhandledEvent, + + /// + /// Invoked when the specified state machine is being pushed to a state. + /// + PushState, + + /// + /// Invoked when the specified state machine raises an event. + /// + RaiseEvent, + + /// + /// Invoked when the specified event is received by an actor. + /// + ReceiveEvent, + + /// + /// Invoked when the specified event is sent to a target actor. + /// + SendEvent, + + /// + /// Invoked when the specified state machine enters or exits a state. + /// + StateTransition, + + /// + /// Invoked to describe the specified scheduling strategy. + /// + StrategyDescription, + + /// + /// Invoked when the specified actor waits to receive an event of a specified type. + /// + WaitEvent, + + /// + /// Invoked when the specified actor waits to receive multiple events of a specified type. + /// + WaitMultipleEvents + } + + /// + /// Adds log text to details dictionary. + /// + /// The log text. + public void AddLog(string log) => _log.Details.Log = log; + + + /// + /// Add the log type to _log dictionary. + /// + /// The log type + public void AddLogType(LogType type) => _log.Type = type.ToString(); + + + /// + /// Add _log to _logs and resets the Writer for next available logging. + /// + /// Of type Bool: If true, run HandleLogEntry to get vector clock. Else, don't. + public void AddToLogs(bool updateVcMap = false) + { + if (updateVcMap) + { + _vcGenerator.HandleLogEntry(_log); + } + + _logs.Add(_log); + _log = new LogEntry(); + } + + /// + /// Serializes the _logs to be exported as a JSON file. + /// + /// + public string ToJsonString() => JsonSerializer.Serialize(_logs, + new JsonSerializerOptions + { + DefaultIgnoreCondition = JsonIgnoreCondition.WhenWritingNull, + PropertyNamingPolicy = JsonNamingPolicy.CamelCase, WriteIndented = true + }); + } +} \ No newline at end of file diff --git a/Src/PChecker/CheckerCore/Actors/Logging/LogWriter.cs b/Src/PChecker/CheckerCore/Actors/Logging/LogWriter.cs index 6ca7dc5e5..c7d5957cc 100644 --- a/Src/PChecker/CheckerCore/Actors/Logging/LogWriter.cs +++ b/Src/PChecker/CheckerCore/Actors/Logging/LogWriter.cs @@ -25,6 +25,11 @@ internal sealed class LogWriter /// Used to log messages. /// internal TextWriter Logger { get; private set; } + + /// + /// Used to log json messages. + /// + private JsonWriter JsonLogger { get; set; } /// /// Initializes a new instance of the class. @@ -561,6 +566,12 @@ internal TextWriter SetLogger(TextWriter logger) return prevLogger; } + + /// + /// Sets the JsonLogger to an instance created on runtime. + /// + /// The jsonLogger instance created from runtime before running tests. + internal void SetJsonLogger(JsonWriter jsonLogger) => JsonLogger = jsonLogger; private ActorRuntimeLogTextFormatter GetOrCreateTextLog() { @@ -607,7 +618,14 @@ internal void RegisterLog(IActorRuntimeLog log) a.Logger = Logger; } } - + + // If log is or of subclass ActorRuntimeLogJsonFormatter (i.e. when log is PJsonFormatter), + // update the Writer reference to the JsonLogger instance defined within LogWriter.cs + if (log is ActorRuntimeLogJsonFormatter tempJsonFormatter) + { + tempJsonFormatter.Writer = JsonLogger; + } + Logs.Add(log); } diff --git a/Src/PChecker/CheckerCore/CheckerConfiguration.cs b/Src/PChecker/CheckerCore/CheckerConfiguration.cs index 323a270b8..e6aa50cb6 100644 --- a/Src/PChecker/CheckerCore/CheckerConfiguration.cs +++ b/Src/PChecker/CheckerCore/CheckerConfiguration.cs @@ -5,6 +5,7 @@ using System.Collections.Generic; using System.IO; using System.Runtime.Serialization; +using PChecker.Actors.Logging; using PChecker.Utilities; namespace PChecker @@ -211,7 +212,14 @@ public int MaxSchedulingSteps /// [DataMember] public bool IsXmlLogEnabled { get; set; } - + + /// + /// Produce a JSON formatted runtime log file. + /// Defaults to true. + /// + [DataMember] + public bool IsJsonLogEnabled { get; set; } = true; + /// /// If specified, requests a custom runtime log to be used instead of the default. /// This is the AssemblyQualifiedName of the type to load. @@ -310,7 +318,7 @@ protected CheckerConfiguration() EnableDebugging = false; AdditionalCodeCoverageAssemblies = new Dictionary(); - + EnableColoredConsoleOutput = false; DisableEnvironmentExit = true; diff --git a/Src/PChecker/CheckerCore/SystematicTesting/TestingEngine.cs b/Src/PChecker/CheckerCore/SystematicTesting/TestingEngine.cs index acdc66c39..bb8bf7e81 100644 --- a/Src/PChecker/CheckerCore/SystematicTesting/TestingEngine.cs +++ b/Src/PChecker/CheckerCore/SystematicTesting/TestingEngine.cs @@ -75,6 +75,12 @@ public class TestingEngine /// private TextWriter Logger; + /// + /// Contains a single iteration of JSON log output in the case where the IsJsonLogEnabled + /// checkerConfiguration is specified. + /// + private JsonWriter JsonLogger; + /// /// The profiler. /// @@ -101,7 +107,7 @@ public class TestingEngine /// checkerConfiguration is specified. /// private StringBuilder XmlLog; - + /// /// The readable trace, if any. /// @@ -430,6 +436,10 @@ private void RunNextIteration(int iteration) // Creates a new instance of the controlled runtime. runtime = new ControlledRuntime(_checkerConfiguration, Strategy, RandomValueGenerator); + // Always output a json log of the error + JsonLogger = new JsonWriter(); + runtime.SetJsonLogger(JsonLogger); + // If verbosity is turned off, then intercept the program log, and also redirect // the standard output and error streams to a nul logger. if (!_checkerConfiguration.IsVerbose) @@ -575,6 +585,13 @@ public void TryEmitTraces(string directory, string file) Logger.WriteLine($"..... Writing {xmlPath}"); File.WriteAllText(xmlPath, XmlLog.ToString()); } + + if (_checkerConfiguration.IsJsonLogEnabled) + { + var jsonPath = directory + file + "_" + index + ".trace.json"; + Logger.WriteLine($"..... Writing {jsonPath}"); + File.WriteAllText(jsonPath, JsonLogger.ToJsonString()); + } if (Graph != null) { diff --git a/Src/PChecker/CheckerCore/Testing/TestingProcessFactory.cs b/Src/PChecker/CheckerCore/Testing/TestingProcessFactory.cs index 5f0d112a7..4c3d8001a 100644 --- a/Src/PChecker/CheckerCore/Testing/TestingProcessFactory.cs +++ b/Src/PChecker/CheckerCore/Testing/TestingProcessFactory.cs @@ -113,6 +113,11 @@ checkerConfiguration.SchedulingStrategy is "probabilistic" || arguments.Append("--xml-trace "); } + if (checkerConfiguration.IsJsonLogEnabled) + { + arguments.Append("--json-trace "); + } + if (!string.IsNullOrEmpty(checkerConfiguration.CustomActorRuntimeLogType)) { arguments.Append($"--actor-runtime-log {checkerConfiguration.CustomActorRuntimeLogType} "); diff --git a/Src/PCompiler/CompilerCore/Backend/CSharp/CSharpCodeGenerator.cs b/Src/PCompiler/CompilerCore/Backend/CSharp/CSharpCodeGenerator.cs index e5e99664e..de7f7f658 100644 --- a/Src/PCompiler/CompilerCore/Backend/CSharp/CSharpCodeGenerator.cs +++ b/Src/PCompiler/CompilerCore/Backend/CSharp/CSharpCodeGenerator.cs @@ -387,6 +387,7 @@ private void WriteTestFunction(CompilationContext context, StringWriter output, context.WriteLine(output, "[PChecker.SystematicTesting.Test]"); context.WriteLine(output, "public static void Execute(IActorRuntime runtime) {"); context.WriteLine(output, "runtime.RegisterLog(new PLogFormatter());"); + context.WriteLine(output, "runtime.RegisterLog(new PJsonFormatter());"); context.WriteLine(output, "PModule.runtime = runtime;"); context.WriteLine(output, "PHelper.InitializeInterfaces();"); context.WriteLine(output, "PHelper.InitializeEnums();"); diff --git a/Src/PRuntimes/PCSharpRuntime/PJsonFormatter.cs b/Src/PRuntimes/PCSharpRuntime/PJsonFormatter.cs new file mode 100644 index 000000000..435704b67 --- /dev/null +++ b/Src/PRuntimes/PCSharpRuntime/PJsonFormatter.cs @@ -0,0 +1,590 @@ +// Copyright (c) Microsoft Corporation. +// Licensed under the MIT License. + +using System; +using System.Linq; +using System.Threading.Tasks; +using PChecker.Actors; +using PChecker.Actors.Logging; +using PChecker.Actors.Events; +using System.Collections.Generic; +using Plang.CSharpRuntime.Exceptions; + +namespace Plang.CSharpRuntime +{ + /// + /// This class implements IActorRuntimeLog and generates log output in an XML format. + /// + public class PJsonFormatter : ActorRuntimeLogJsonFormatter + { + public PJsonFormatter() : base() + { + } + + /// + /// Removes the '<' and '>' tags for a log text. + /// I.e., ' Some error log...' becomes 'Some error log...' + /// + /// The text log + /// New string with the tag removed or just the string itself if there is no tag. + private static string RemoveLogTag(string log) + { + var openingTagIndex = log.IndexOf("<"); + var closingTagIndex = log.IndexOf(">"); + var potentialTagExists = openingTagIndex != -1 && closingTagIndex != -1; + var validOpeningTag = openingTagIndex == 0 && closingTagIndex > openingTagIndex; + + if (potentialTagExists && validOpeningTag) + { + return log[(closingTagIndex + 1)..].Trim(); + } + + return log; + } + + /// + /// Parse payload input to dictionary format. + /// I.e. + /// Input: () + /// Parsed Output: { + /// "source": "Client(4)", + /// "accountId": "0", + /// "amount": "8", + /// "rId": "19", + /// } + /// + /// String representing the payload. + /// The dictionary object representation of the payload. + private static Dictionary ParsePayloadToDictionary(string payload) + { + var parsedPayload = new Dictionary(); + var trimmedPayload = payload.Trim('(', ')', '<', '>'); + var payloadKeyValuePairs = trimmedPayload.Split(','); + + foreach (var payloadPair in payloadKeyValuePairs) + { + var payloadKeyValue = payloadPair.Split(':'); + + if (payloadKeyValue.Length != 2) continue; + var key = payloadKeyValue[0].Trim(); + var value = payloadKeyValue[1].Trim(); + + parsedPayload[key] = value; + } + + return parsedPayload; + } + + /// + /// Method taken from PLogFormatter.cs file. Takes in a string and only get the + /// last element of the string separated by a period. + /// I.e. + /// Input: PImplementation.TestWithSingleClient(2) + /// Output: TestWithSingleClient(2) + /// + /// String representing the name to be parsed. + /// The split string. + private static string GetShortName(string name) => name?.Split('.').Last(); + + /// TODO: What other forms can the payload be in? Have the method implemented in IPrtValue? + /// + /// Cleans the payload string to remove "<" and "/>" and replacing ':' with '=' + /// I.e. + /// Input: () + /// Output: (source=Client(4), accountId=0, amount=4, rId=18) + /// + /// String representation of the payload. + /// The cleaned payload. + private static string CleanPayloadString(string payload) + { + var output = payload.Replace("<", string.Empty); + output = output.Replace(':', '='); + output = output.Replace(", >", string.Empty); + return output; + } + + /// + /// Method taken from PLogFormatter.cs file. Takes in Event e and returns string + /// with details about the event such as event name and its payload. Slightly modified + /// from the method in PLogFormatter.cs in that payload is parsed with the CleanPayloadString + /// method right above. + /// + /// Event input. + /// String with the event description. + private static string GetEventNameWithPayload(Event e) + { + if (e.GetType().Name.Contains("GotoStateEvent")) + { + return e.GetType().Name; + } + + var pe = (PEvent)(e); + var payload = pe.Payload == null ? "null" : pe.Payload.ToEscapedString(); + var msg = pe.Payload == null ? "" : $" with payload ({CleanPayloadString(payload)})"; + return $"{GetShortName(e.GetType().Name)}{msg}"; + } + + /// + /// Takes in Event e and returns the dictionary representation of the payload of the event. + /// + /// Event input. + /// Dictionary representation of the payload for the event, if any. + private static Dictionary GetEventPayloadInJson(Event e) + { + if (e.GetType().Name.Contains("GotoStateEvent")) + { + return null; + } + + var pe = (PEvent)(e); + return pe.Payload != null ? ParsePayloadToDictionary(pe.Payload.ToEscapedString()) : null; + } + + public override void OnCompleted() + { + } + + public override void OnAssertionFailure(string error) + { + error = RemoveLogTag(error); + + Writer.AddLogType(JsonWriter.LogType.AssertionFailure); + Writer.LogDetails.Error = error; + Writer.AddLog(error); + Writer.AddToLogs(); + } + + public override void OnCreateActor(ActorId id, string creatorName, string creatorType) + { + if (id.Name.Contains("GodMachine") || creatorName.Contains("GodMachine")) + { + return; + } + + var source = creatorName ?? $"task '{Task.CurrentId}'"; + var log = $"{id} was created by {source}."; + + Writer.AddLogType(JsonWriter.LogType.CreateActor); + Writer.LogDetails.Id = id.ToString(); + Writer.LogDetails.CreatorName = source; + Writer.LogDetails.CreatorType = creatorType; + Writer.AddLog(log); + Writer.AddToLogs(updateVcMap: true); + } + + /// + public override void OnCreateStateMachine(ActorId id, string creatorName, string creatorType) + { + if (id.Name.Contains("GodMachine") || creatorName.Contains("GodMachine")) + { + return; + } + + var source = creatorName ?? $"task '{Task.CurrentId}'"; + var log = $"{id} was created by {source}."; + + Writer.AddLogType(JsonWriter.LogType.CreateStateMachine); + Writer.LogDetails.Id = id.ToString(); + Writer.LogDetails.CreatorName = creatorName; + Writer.LogDetails.CreatorType = creatorType; + Writer.AddLog(log); + Writer.AddToLogs(updateVcMap: true); + } + + public override void OnDefaultEventHandler(ActorId id, string stateName) + { + stateName = GetShortName(stateName); + + var log = stateName is null + ? $"{id} is executing the default handler." + : $"{id} is executing the default handler in state '{stateName}'."; + + Writer.AddLogType(JsonWriter.LogType.DefaultEventHandler); + Writer.LogDetails.Id = id.ToString(); + Writer.LogDetails.State = stateName; + Writer.AddLog(log); + Writer.AddToLogs(updateVcMap: true); + } + + public override void OnDequeueEvent(ActorId id, string stateName, Event e) + { + if (stateName.Contains("__InitState__") || id.Name.Contains("GodMachine")) + { + return; + } + + var eventName = GetEventNameWithPayload(e); + var log = stateName is null + ? $"'{id}' dequeued event '{eventName}'." + : $"'{id}' dequeued event '{eventName}' in state '{stateName}'."; + + Writer.AddLogType(JsonWriter.LogType.DequeueEvent); + Writer.LogDetails.Id = id.ToString(); + Writer.LogDetails.Event = GetShortName(e.GetType().Name); + Writer.LogDetails.State = GetShortName(stateName); + Writer.LogDetails.Payload = GetEventPayloadInJson(e); + Writer.AddLog(log); + Writer.AddToLogs(updateVcMap: true); + } + + public override void OnEnqueueEvent(ActorId id, Event e) + { + } + + public override void OnExceptionHandled(ActorId id, string stateName, string actionName, Exception ex) + { + if (ex is PNonStandardReturnException) + { + return; + } + + var log = stateName is null + ? $"{id} running action '{actionName}' chose to handle exception '{ex.GetType().Name}'." + : $"{id} running action '{actionName}' in state '{stateName}' chose to handle exception '{ex.GetType().Name}'."; + + Writer.AddLogType(JsonWriter.LogType.ExceptionHandled); + Writer.LogDetails.Id = id.ToString(); + Writer.LogDetails.State = GetShortName(stateName); + Writer.LogDetails.Action = actionName; + Writer.LogDetails.Exception = ex.GetType().Name; + Writer.AddLog(log); + Writer.AddToLogs(updateVcMap: true); + } + + public override void OnExceptionThrown(ActorId id, string stateName, string actionName, Exception ex) + { + if (ex is PNonStandardReturnException) + { + return; + } + + var log = stateName is null + ? $"{id} running action '{actionName}' chose to handle exception '{ex.GetType().Name}'." + : $"{id} running action '{actionName}' in state '{stateName}' threw exception '{ex.GetType().Name}'."; + + Writer.AddLogType(JsonWriter.LogType.ExceptionThrown); + Writer.LogDetails.Id = id.ToString(); + Writer.LogDetails.State = GetShortName(stateName); + Writer.LogDetails.Action = actionName; + Writer.LogDetails.Exception = ex.GetType().Name; + Writer.AddLog(log); + Writer.AddToLogs(updateVcMap: true); + } + + public override void OnExecuteAction(ActorId id, string handlingStateName, string currentStateName, string actionName) + { + } + + public override void OnGotoState(ActorId id, string currentStateName, string newStateName) + { + if (currentStateName.Contains("__InitState__") || id.Name.Contains("GodMachine")) + { + return; + } + + currentStateName = GetShortName(currentStateName); + newStateName = GetShortName(newStateName); + + var log = + $"{id} is transitioning from state '{currentStateName}' to state '{newStateName}'."; + + Writer.AddLogType(JsonWriter.LogType.GotoState); + Writer.LogDetails.Id = id.ToString(); + Writer.LogDetails.StartState = currentStateName; + Writer.LogDetails.EndState = newStateName; + Writer.AddLog(log); + Writer.AddToLogs(updateVcMap: true); + } + + public override void OnHalt(ActorId id, int inboxSize) + { + var log = $"{id} halted with {inboxSize} events in its inbox."; + + Writer.AddLogType(JsonWriter.LogType.Halt); + Writer.LogDetails.Id = id.ToString(); + Writer.LogDetails.HaltInboxSize = inboxSize; + Writer.AddLog(log); + Writer.AddToLogs(updateVcMap: true); + } + + public override void OnHandleRaisedEvent(ActorId id, string stateName, Event e) + { + } + + public override void OnPopState(ActorId id, string currentStateName, string restoredStateName) + { + currentStateName = string.IsNullOrEmpty(currentStateName) ? "[not recorded]" : currentStateName; + var reenteredStateName = restoredStateName ?? string.Empty; + var log = $"{id} popped state '{currentStateName}' and reentered state '{reenteredStateName}'."; + + Writer.AddLogType(JsonWriter.LogType.PopState); + Writer.LogDetails.Id = id.ToString(); + Writer.LogDetails.StartState = currentStateName; + Writer.LogDetails.EndState = reenteredStateName; + Writer.AddLog(log); + Writer.AddToLogs(updateVcMap: true); + } + + public override void OnPopStateUnhandledEvent(ActorId id, string stateName, Event e) + { + var log = $"{id} popped state {stateName} due to unhandled event '{e.GetType().Name}'."; + + Writer.AddLogType(JsonWriter.LogType.PopStateUnhandledEvent); + Writer.LogDetails.Id = id.ToString(); + Writer.LogDetails.State = stateName; + Writer.LogDetails.Event = e.GetType().Name; + Writer.AddLog(log); + Writer.AddToLogs(updateVcMap: true); + } + + public override void OnPushState(ActorId id, string currentStateName, string newStateName) + { + var log = $"{id} pushed from state '{currentStateName}' to state '{newStateName}'."; + + Writer.AddLogType(JsonWriter.LogType.PushState); + Writer.LogDetails.Id = id.ToString(); + Writer.LogDetails.StartState = currentStateName; + Writer.LogDetails.EndState = newStateName; + Writer.AddLog(log); + Writer.AddToLogs(updateVcMap: true); + } + + public override void OnRaiseEvent(ActorId id, string stateName, Event e) + { + stateName = GetShortName(stateName); + string eventName = GetEventNameWithPayload(e); + + if (stateName.Contains("__InitState__") || id.Name.Contains("GodMachine") || + eventName.Contains("GotoStateEvent")) + { + return; + } + + var log = stateName is null + ? $"'{id}' raised event '{eventName}'." + : $"'{id}' raised event '{eventName}' in state '{stateName}'."; + + Writer.AddLogType(JsonWriter.LogType.RaiseEvent); + Writer.LogDetails.Id = id.ToString(); + Writer.LogDetails.Event = GetShortName(e.GetType().Name); + Writer.LogDetails.State = stateName; + Writer.LogDetails.Payload = GetEventPayloadInJson(e); + Writer.AddLog(log); + Writer.AddToLogs(updateVcMap: true); + } + + public override void OnReceiveEvent(ActorId id, string stateName, Event e, bool wasBlocked) + { + stateName = GetShortName(stateName); + string eventName = GetEventNameWithPayload(e); + var unblocked = wasBlocked ? " and unblocked" : string.Empty; + var log = stateName is null + ? $"'{id}' dequeued event '{eventName}'{unblocked}." + : $"'{id}' dequeued event '{eventName}'{unblocked} in state '{stateName}'."; + + Writer.AddLogType(JsonWriter.LogType.ReceiveEvent); + Writer.LogDetails.Id = id.ToString(); + Writer.LogDetails.State = stateName; + Writer.LogDetails.Event = GetShortName(e.GetType().Name); + Writer.LogDetails.WasBlocked = wasBlocked; + Writer.LogDetails.Payload = GetEventPayloadInJson(e); + Writer.AddLog(log); + Writer.AddToLogs(updateVcMap: true); + } + + public override void OnSendEvent(ActorId targetActorId, string senderName, string senderType, string senderStateName, + Event e, Guid opGroupId, bool isTargetHalted) + { + senderStateName = GetShortName(senderStateName); + string eventName = GetEventNameWithPayload(e); + var opGroupIdMsg = opGroupId != Guid.Empty ? $" (operation group '{opGroupId}')" : string.Empty; + var isHalted = isTargetHalted ? $" which has halted" : string.Empty; + var sender = !string.IsNullOrEmpty(senderName) + ? $"'{senderName}' in state '{senderStateName}'" + : $"The runtime"; + var log = $"{sender} sent event '{eventName}' to '{targetActorId}'{isHalted}{opGroupIdMsg}."; + + Writer.AddLogType(JsonWriter.LogType.SendEvent); + Writer.LogDetails.Sender = !string.IsNullOrEmpty(senderName) ? senderName : "Runtime"; + Writer.LogDetails.State = senderStateName; + Writer.LogDetails.Event = GetShortName(e.GetType().Name); + Writer.LogDetails.Target = targetActorId.ToString(); + Writer.LogDetails.OpGroupId = opGroupId.ToString(); + Writer.LogDetails.IsTargetHalted = isTargetHalted; + Writer.LogDetails.Payload = GetEventPayloadInJson(e); + Writer.AddLog(log); + Writer.AddToLogs(updateVcMap: true); + } + + public override void OnStateTransition(ActorId id, string stateName, bool isEntry) + { + if (stateName.Contains("__InitState__") || id.Name.Contains("GodMachine")) + { + return; + } + + stateName = GetShortName(stateName); + var direction = isEntry ? "enters" : "exits"; + var log = $"{id} {direction} state '{stateName}'."; + + Writer.AddLogType(JsonWriter.LogType.StateTransition); + Writer.LogDetails.Id = id.ToString(); + Writer.LogDetails.State = stateName; + Writer.LogDetails.IsEntry = isEntry; + Writer.AddLog(log); + Writer.AddToLogs(updateVcMap: true); + } + + public override void OnWaitEvent(ActorId id, string stateName, Type eventType) + { + stateName = GetShortName(stateName); + + var log = stateName is null + ? $"{id} is waiting to dequeue an event of type '{eventType.FullName}'." + : $"{id} is waiting to dequeue an event of type '{eventType.FullName}' in state '{stateName}'."; + + Writer.AddLogType(JsonWriter.LogType.WaitEvent); + Writer.LogDetails.Id = id.ToString(); + Writer.LogDetails.EventType = eventType.FullName; + Writer.LogDetails.State = stateName; + Writer.AddLog(log); + Writer.AddToLogs(updateVcMap: true); + } + + public override void OnWaitEvent(ActorId id, string stateName, params Type[] eventTypes) + { + stateName = GetShortName(stateName); + string eventNames; + + switch (eventTypes.Length) + { + case 0: + eventNames = "''"; + break; + case 1: + eventNames = "'" + eventTypes[0].Name + "'"; + break; + case 2: + eventNames = "'" + eventTypes[0].Name + "' or '" + eventTypes[1].Name + "'"; + break; + case 3: + eventNames = "'" + eventTypes[0].Name + "', '" + eventTypes[1].Name + "' or '" + + eventTypes[2].Name + + "'"; + break; + default: + { + var eventNameArray = new string[eventTypes.Length - 1]; + for (var i = 0; i < eventTypes.Length - 2; i++) + { + eventNameArray[i] = eventTypes[i].Name; + } + + eventNames = "'" + string.Join("', '", eventNameArray) + "' or '" + + eventTypes[^1].Name + "'"; + break; + } + } + + var log = stateName is null + ? $"{id} is waiting to dequeue an event of type {eventNames}." + : $"{id} is waiting to dequeue an event of type {eventNames} in state '{stateName}'."; + + var eventTypesNames = eventTypes.Select(eventType => eventType.Name).ToList(); + + Writer.AddLogType(JsonWriter.LogType.WaitMultipleEvents); + Writer.LogDetails.Id = id.ToString(); + Writer.LogDetails.EventTypes = eventTypesNames; + Writer.AddLog(log); + Writer.AddToLogs(updateVcMap: true); + } + + public override void OnCreateMonitor(string monitorType) + { + monitorType = GetShortName(monitorType); + var log = $"{monitorType} was created."; + + Writer.AddLogType(JsonWriter.LogType.CreateMonitor); + Writer.LogDetails.Monitor = monitorType; + Writer.AddLog(log); + Writer.AddToLogs(updateVcMap: true); + } + + public override void OnMonitorExecuteAction(string monitorType, string stateName, string actionName) + { + } + + public override void OnMonitorProcessEvent(string monitorType, string stateName, string senderName, + string senderType, string senderStateName, Event e) + { + monitorType = GetShortName(monitorType); + var log = $"{monitorType} is processing event '{GetEventNameWithPayload(e)}' in state '{stateName}'."; + + Writer.AddLogType(JsonWriter.LogType.MonitorProcessEvent); + Writer.LogDetails.Monitor = monitorType; + Writer.LogDetails.Event = GetShortName(e.GetType().Name); + Writer.LogDetails.State = stateName; + Writer.LogDetails.Payload = GetEventPayloadInJson(e); + Writer.AddLog(log); + Writer.AddToLogs(updateVcMap: true); + } + + public override void OnMonitorRaiseEvent(string monitorType, string stateName, Event e) + { + stateName = GetShortName(stateName); + string eventName = GetEventNameWithPayload(e); + var log = $"Monitor '{GetShortName(monitorType)}' raised event '{eventName}' in state '{stateName}'."; + + Writer.AddLogType(JsonWriter.LogType.MonitorRaiseEvent); + Writer.LogDetails.Monitor = monitorType; + Writer.LogDetails.Event = GetShortName(e.GetType().Name); + Writer.LogDetails.State = stateName; + Writer.LogDetails.Payload = GetEventPayloadInJson(e); + Writer.AddLog(log); + Writer.AddToLogs(updateVcMap: true); + } + + public override void OnMonitorStateTransition(string monitorType, string stateName, bool isEntry, bool? isInHotState) + { + monitorType = GetShortName(monitorType); + + if (stateName.Contains("__InitState__")) + { + return; + } + + stateName = GetShortName(stateName); + var liveness = isInHotState.HasValue ? (isInHotState.Value ? "hot " : "cold ") : string.Empty; + var direction = isEntry ? "enters" : "exits"; + var log = $"{monitorType} {direction} {liveness}state '{stateName}'."; + + Writer.AddLogType(JsonWriter.LogType.MonitorStateTransition); + Writer.LogDetails.Monitor = monitorType; + Writer.LogDetails.State = stateName; + Writer.LogDetails.IsEntry = isEntry; + Writer.LogDetails.IsInHotState = isInHotState; + Writer.AddLog(log); + Writer.AddToLogs(updateVcMap: true); + } + + public override void OnMonitorError(string monitorType, string stateName, bool? isInHotState) + { + } + + public override void OnRandom(object result, string callerName, string callerType) + { + } + + public override void OnStrategyDescription(string strategyName, string description) + { + var desc = string.IsNullOrEmpty(description) ? $" Description: {description}" : string.Empty; + var log = $"Found bug using '{strategyName}' strategy.{desc}"; + + Writer.AddLogType(JsonWriter.LogType.StrategyDescription); + Writer.LogDetails.Strategy = strategyName; + Writer.LogDetails.StrategyDescription = description; + Writer.AddLog(log); + Writer.AddToLogs(); + } + } +} \ No newline at end of file From 58f51cfacf077f653ea554dafffc96112300f789 Mon Sep 17 00:00:00 2001 From: haoran-wen <137958518+haoran-wen@users.noreply.github.com> Date: Thu, 20 Jul 2023 15:49:03 -0700 Subject: [PATCH 5/6] outputs json verbose logs if testing in verbose mode, stream to json file while serializing (#626) --- .../CheckerCore/Actors/Logging/JsonWriter.cs | 18 ++----- .../SystematicTesting/TestingEngine.cs | 54 ++++++++++++++++++- 2 files changed, 58 insertions(+), 14 deletions(-) diff --git a/Src/PChecker/CheckerCore/Actors/Logging/JsonWriter.cs b/Src/PChecker/CheckerCore/Actors/Logging/JsonWriter.cs index a13d2cdbe..916d57691 100644 --- a/Src/PChecker/CheckerCore/Actors/Logging/JsonWriter.cs +++ b/Src/PChecker/CheckerCore/Actors/Logging/JsonWriter.cs @@ -2,10 +2,8 @@ using System; using System.Linq; using System.Text; -using System.Text.Json; using System.Collections.Generic; using System.Security.Cryptography; -using System.Text.Json.Serialization; namespace PChecker.Actors.Logging { @@ -497,6 +495,11 @@ public class JsonWriter /// Getter for accessing log entry details. /// public LogDetails LogDetails => _log.Details; + + /// + /// Getter for accessing logs. + /// + public List Logs => _logs; /// /// Initializes the Writer. Create empty _logs, _log, and _details objects. @@ -663,16 +666,5 @@ public void AddToLogs(bool updateVcMap = false) _logs.Add(_log); _log = new LogEntry(); } - - /// - /// Serializes the _logs to be exported as a JSON file. - /// - /// - public string ToJsonString() => JsonSerializer.Serialize(_logs, - new JsonSerializerOptions - { - DefaultIgnoreCondition = JsonIgnoreCondition.WhenWritingNull, - PropertyNamingPolicy = JsonNamingPolicy.CamelCase, WriteIndented = true - }); } } \ No newline at end of file diff --git a/Src/PChecker/CheckerCore/SystematicTesting/TestingEngine.cs b/Src/PChecker/CheckerCore/SystematicTesting/TestingEngine.cs index bb8bf7e81..f0f5e98cf 100644 --- a/Src/PChecker/CheckerCore/SystematicTesting/TestingEngine.cs +++ b/Src/PChecker/CheckerCore/SystematicTesting/TestingEngine.cs @@ -8,6 +8,8 @@ using System.Reflection; using System.Runtime.ExceptionServices; using System.Text; +using System.Text.Json; +using System.Text.Json.Serialization; using System.Text.RegularExpressions; using System.Threading; using System.Threading.Tasks; @@ -81,6 +83,23 @@ public class TestingEngine /// private JsonWriter JsonLogger; + /// + /// Field declaration for the JsonVerboseLogs + /// Structure representation is a list of the JsonWriter logs. + /// [log iter 1, log iter 2, log iter 3, ...] + /// + private readonly List> JsonVerboseLogs; + + /// + /// Field declaration with default JSON serializer options + /// + private JsonSerializerOptions jsonSerializerConfig = new() + { + DefaultIgnoreCondition = JsonIgnoreCondition.WhenWritingNull, + PropertyNamingPolicy = JsonNamingPolicy.CamelCase, + WriteIndented = true + }; + /// /// The profiler. /// @@ -221,6 +240,12 @@ private TestingEngine(CheckerConfiguration checkerConfiguration, TestMethodInfo CancellationTokenSource = new CancellationTokenSource(); PrintGuard = 1; + // Initialize a new instance of JsonVerboseLogs if running in verbose mode. + if (checkerConfiguration.IsVerbose) + { + JsonVerboseLogs = new List>(); + } + if (checkerConfiguration.SchedulingStrategy is "replay") { var scheduleDump = GetScheduleForReplay(out var isFair); @@ -401,6 +426,24 @@ _checkerConfiguration.SchedulingStrategy is "probabilistic" || ExceptionDispatchInfo.Capture(innerException).Throw(); } } + + // Output JSON verbose logs at the end of Task + if (_checkerConfiguration.IsVerbose) + { + // Get the file path to output the json verbose logs file + var directory = _checkerConfiguration.OutputDirectory; + var file = Path.GetFileNameWithoutExtension(_checkerConfiguration.AssemblyToBeAnalyzed); + file += "_" + _checkerConfiguration.TestingProcessId; + var jsonVerbosePath = directory + file + "_verbose.trace.json"; + + Logger.WriteLine("... Emitting verbose logs:"); + Logger.WriteLine($"..... Writing {jsonVerbosePath}"); + + // Stream directly to the output file while serializing the JSON + using var jsonStreamFile = File.Create(jsonVerbosePath); + JsonSerializer.Serialize(jsonStreamFile, JsonVerboseLogs, jsonSerializerConfig); + } + }, CancellationTokenSource.Token); } @@ -479,6 +522,12 @@ private void RunNextIteration(int iteration) ErrorReporter.WriteErrorLine(runtime.Scheduler.BugReport); } + // Only add the current iteration of JsonLogger logs to JsonVerboseLogs if in verbose mode + if (_checkerConfiguration.IsVerbose) + { + JsonVerboseLogs.Add(JsonLogger.Logs); + } + runtime.LogWriter.LogCompletion(); GatherTestingStatistics(runtime); @@ -590,7 +639,10 @@ public void TryEmitTraces(string directory, string file) { var jsonPath = directory + file + "_" + index + ".trace.json"; Logger.WriteLine($"..... Writing {jsonPath}"); - File.WriteAllText(jsonPath, JsonLogger.ToJsonString()); + + // Stream directly to the output file while serializing the JSON + using var jsonStreamFile = File.Create(jsonPath); + JsonSerializer.Serialize(jsonStreamFile, JsonLogger.Logs, jsonSerializerConfig); } if (Graph != null) From 5a21eef1a189978a8eb8fcf4f485dcdc0142d582 Mon Sep 17 00:00:00 2001 From: Aman Goel Date: Fri, 21 Jul 2023 19:35:56 -0700 Subject: [PATCH 6/6] [CI] Update Tutorials CI (#628) Increase number of iterations for Tutorials CI --- Src/Scripts/TutorialsChecker/check.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Src/Scripts/TutorialsChecker/check.sh b/Src/Scripts/TutorialsChecker/check.sh index e625422c6..a25041fe1 100755 --- a/Src/Scripts/TutorialsChecker/check.sh +++ b/Src/Scripts/TutorialsChecker/check.sh @@ -1,6 +1,6 @@ #!/bin/bash -ITERATIONS=10000 +ITERATIONS=25000 cd $1