From 90551644b7f91bea28ce3a94768e8fc197597e23 Mon Sep 17 00:00:00 2001 From: Aman Goel Date: Tue, 18 Jun 2024 23:37:22 +0000 Subject: [PATCH] [PEx] Store temporary changes --- .../main/java/pexplicit/RuntimeExecutor.java | 40 ++++-- .../runtime/logger/PExplicitLogger.java | 20 ++- .../runtime/logger/ScheduleWriter.java | 15 +- .../pexplicit/runtime/logger/TraceLogger.java | 134 ------------------ .../pexplicit/runtime/machine/PMachine.java | 44 ++++-- .../machine/buffer/BufferSemantics.java | 3 +- .../runtime/machine/buffer/EventBuffer.java | 19 --- .../runtime/machine/buffer/FifoQueue.java | 20 +++ .../runtime/machine/buffer/SenderQueue.java | 35 ----- .../pexplicit/runtime/scheduler/Schedule.java | 1 - .../runtime/scheduler/Scheduler.java | 22 +-- .../explicit/ExplicitSearchScheduler.java | 25 ++-- ...eduler.java => ReceiverQueueReplayer.java} | 23 ++- .../scheduler/replay/SenderQueueReplayer.java | 123 ++++++++++++++++ .../main/java/pexplicit/values/PMessage.java | 8 +- 15 files changed, 263 insertions(+), 269 deletions(-) delete mode 100644 Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/logger/TraceLogger.java delete mode 100644 Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/machine/buffer/EventBuffer.java create mode 100644 Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/machine/buffer/FifoQueue.java delete mode 100644 Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/machine/buffer/SenderQueue.java rename Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/replay/{ReplayScheduler.java => ReceiverQueueReplayer.java} (84%) create mode 100644 Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/replay/SenderQueueReplayer.java diff --git a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/RuntimeExecutor.java b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/RuntimeExecutor.java index 3c5e3ecdb..a88959b3f 100644 --- a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/RuntimeExecutor.java +++ b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/RuntimeExecutor.java @@ -4,8 +4,10 @@ import pexplicit.runtime.STATUS; import pexplicit.runtime.logger.PExplicitLogger; import pexplicit.runtime.logger.StatWriter; +import pexplicit.runtime.scheduler.Schedule; import pexplicit.runtime.scheduler.explicit.ExplicitSearchScheduler; -import pexplicit.runtime.scheduler.replay.ReplayScheduler; +import pexplicit.runtime.scheduler.replay.ReceiverQueueReplayer; +import pexplicit.runtime.scheduler.replay.SenderQueueReplayer; import pexplicit.utils.exceptions.BugFoundException; import pexplicit.utils.exceptions.MemoutException; import pexplicit.utils.monitor.MemoryMonitor; @@ -99,21 +101,31 @@ private static void process(boolean resume) throws Exception { PExplicitGlobal.setResult(String.format("found cex of length %d", scheduler.getStepNumber())); PExplicitLogger.logStackTrace(e); - ReplayScheduler replayer = new ReplayScheduler(scheduler.schedule); - PExplicitGlobal.setScheduler(replayer); + SenderQueueReplayer senderQueueReplayer = new SenderQueueReplayer(scheduler.schedule); + PExplicitGlobal.setScheduler(senderQueueReplayer); try { - replayer.run(); - } catch (NullPointerException | StackOverflowError | ClassCastException replayException) { - PExplicitLogger.logStackTrace((Exception) replayException); - throw new BugFoundException(replayException.getMessage(), replayException); - } catch (BugFoundException replayException) { - PExplicitLogger.logStackTrace(replayException); - throw replayException; - } catch (Exception replayException) { - PExplicitLogger.logStackTrace(replayException); - throw new Exception("Error when replaying the bug", replayException); + senderQueueReplayer.run(); + } catch (NullPointerException | StackOverflowError | ClassCastException | BugFoundException senderQueueException) { + ReceiverQueueReplayer receiverQueueReplayer = new ReceiverQueueReplayer(senderQueueReplayer.getReceiverSemanticsSchedule()); + PExplicitGlobal.setScheduler(receiverQueueReplayer); + try { + receiverQueueReplayer.run(); + } catch (NullPointerException | StackOverflowError | ClassCastException receiverQueueException) { + PExplicitLogger.logStackTrace((Exception) receiverQueueException); + throw new BugFoundException(receiverQueueException.getMessage(), receiverQueueException); + } catch (BugFoundException receiverQueueException) { + PExplicitLogger.logStackTrace(receiverQueueException); + throw receiverQueueException; + } catch (Exception receiverQueueException) { + PExplicitLogger.logStackTrace(receiverQueueException); + throw new Exception("Error when replaying the bug in receiver queue semantics", receiverQueueException); + } + throw new Exception("Failed to replay bug in receiver queue semantics", e); + } catch (Exception senderQueueException) { + PExplicitLogger.logStackTrace(senderQueueException); + throw new Exception("Error when replaying the bug in sender queue semantics", senderQueueException); } - throw new Exception("Failed to replay bug", e); + throw new Exception("Failed to replay bug in sender queue semantics", e); } catch (InterruptedException e) { PExplicitGlobal.setStatus(STATUS.INTERRUPTED); throw new Exception("INTERRUPTED", e); diff --git a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/logger/PExplicitLogger.java b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/logger/PExplicitLogger.java index f0dbf439c..bdfa9489b 100644 --- a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/logger/PExplicitLogger.java +++ b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/logger/PExplicitLogger.java @@ -21,7 +21,8 @@ import pexplicit.runtime.scheduler.explicit.SearchStatistics; import pexplicit.runtime.scheduler.explicit.StateCachingMode; import pexplicit.runtime.scheduler.explicit.strategy.SearchTask; -import pexplicit.runtime.scheduler.replay.ReplayScheduler; +import pexplicit.runtime.scheduler.replay.ReceiverQueueReplayer; +import pexplicit.runtime.scheduler.replay.SenderQueueReplayer; import pexplicit.utils.monitor.MemoryMonitor; import pexplicit.values.ComputeHash; import pexplicit.values.PEvent; @@ -184,11 +185,11 @@ public static void logStartIteration(SearchTask task, int iter, int step) { } } - public static void logStartStep(int step, PMachine sender, PMessage msg) { + public static void logStartStep(int step, PMessage msg) { if (verbosity > 0) { log.info(String.format( " Step %d: %s sent %s to %s", - step, sender, msg.getEvent(), msg.getTarget())); + step, msg.getSender(), msg.getEvent(), msg.getTarget())); if (verbosity > 5) { log.info(String.format(" payload: %s", msg.getPayload())); } @@ -267,7 +268,8 @@ public static void logNewState(int step, int idx, Object stateKey, SortedSet 0) { log.info("--------------------"); - log.info("Replaying schedule"); + switch(PExplicitGlobal.getConfig().getBufferSemantics()) { + case SenderQueue -> log.info("Replaying schedule: sender queue semantics"); + case ReceiverQueue -> log.info("Replaying schedule: receiver queue semantics"); + } + } } } diff --git a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/logger/ScheduleWriter.java b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/logger/ScheduleWriter.java index 548486ac5..5fd13c353 100644 --- a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/logger/ScheduleWriter.java +++ b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/logger/ScheduleWriter.java @@ -6,6 +6,7 @@ import pexplicit.utils.misc.Assert; import pexplicit.values.PBool; import pexplicit.values.PInt; +import pexplicit.values.PMessage; import pexplicit.values.PValue; import java.io.File; @@ -56,8 +57,8 @@ public static void logDataChoice(PValue choice) { } public static void logScheduleChoice(PMachine choice) { - logComment("schedule choice"); - log(String.format("(%d)", choice.getInstanceId())); + logComment(String.format("schedule choice: %s", choice)); +// log(String.format("(%d)", choice.getInstanceId())); } public static void logHeader() { @@ -74,4 +75,14 @@ public static void logHeader() { logComment("create Main(2)"); log("(1)"); } + + public static void logSend(PMessage msg) { + log(String.format("// send %s from %s to %s", msg.getEvent(), msg.getSender(), msg.getTarget())); + log(String.format("(%d)", msg.getSender().getInstanceId())); + } + + public static void logReceive(PMessage msg) { + log(String.format("// receive %s at %s", msg.getEvent(), msg.getTarget())); + log(String.format("(%d)", msg.getTarget().getInstanceId())); + } } diff --git a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/logger/TraceLogger.java b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/logger/TraceLogger.java deleted file mode 100644 index 67eeb64de..000000000 --- a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/logger/TraceLogger.java +++ /dev/null @@ -1,134 +0,0 @@ -package pexplicit.runtime.logger; - -import lombok.Getter; -import lombok.Setter; -import org.apache.logging.log4j.Level; -import org.apache.logging.log4j.LogManager; -import org.apache.logging.log4j.Logger; -import org.apache.logging.log4j.core.Appender; -import org.apache.logging.log4j.core.LoggerContext; -import org.apache.logging.log4j.core.appender.ConsoleAppender; -import org.apache.logging.log4j.core.appender.OutputStreamAppender; -import org.apache.logging.log4j.core.config.Configurator; -import org.apache.logging.log4j.core.layout.PatternLayout; -import pexplicit.runtime.machine.PMachine; -import pexplicit.values.PMessage; - -import java.io.File; -import java.io.FileOutputStream; -import java.io.IOException; -import java.util.Date; - -/** - * Represents the trace logger that logs on every schedule step. - */ -public class TraceLogger { - static Logger log = null; - static LoggerContext context = null; - - @Getter - @Setter - static int verbosity; - - /** - * Initialize the logger - * - * @param verb Verbosity level - * @param outputFolder Output folder where trace log file resides - */ - public static void Initialize(int verb, String outputFolder) { - verbosity = verb; - log = Log4JConfig.getContext().getLogger(TraceLogger.class.getName()); - org.apache.logging.log4j.core.Logger coreLogger = - (org.apache.logging.log4j.core.Logger) LogManager.getLogger(TraceLogger.class.getName()); - context = coreLogger.getContext(); - - try { - // get new file name - Date date = new Date(); - String fileName = outputFolder + "/trace-" + date + ".log"; - File file = new File(fileName); - file.getParentFile().mkdirs(); - file.createNewFile(); - - // Define new file printer - FileOutputStream fout = new FileOutputStream(fileName, false); - - PatternLayout layout = Log4JConfig.getPatternLayout(); - Appender fileAppender = - OutputStreamAppender.createAppender(layout, null, fout, fileName, false, true); - ConsoleAppender consoleAppender = ConsoleAppender.createDefaultAppenderForLayout(layout); - fileAppender.start(); - consoleAppender.start(); - - context.getConfiguration().addLoggerAppender(coreLogger, fileAppender); - context.getConfiguration().addLoggerAppender(coreLogger, consoleAppender); - } catch (IOException e) { - System.out.println("Failed to set printer to the TraceLogger!!"); - } - } - - /** - * Disable the logger - */ - public static void disable() { - Configurator.setLevel(TraceLogger.class.getName(), Level.OFF); - } - - /** - * Enable the logger - */ - public static void enable() { - Configurator.setLevel(TraceLogger.class.getName(), Level.INFO); - } - - /** - * Log when a machine sends an event to another machine. - * - * @param message Message that is sent - */ - - public static void send(PMessage message) { - if (verbosity > 3) { - String msg = String.format("Send %s to %s", message.getEvent(), message.getTarget()); - log.info(msg); - } - } - - /** - * Log when a machine unblocks on receiving an event - * - * @param message - */ - public static void unblock(PMessage message) { - if (verbosity > 3) { - String msg = String.format("Unblock %s on receiving %s", message.getTarget(), message.getEvent()); - log.info(msg); - } - } - - /** - * Log when a machine schedules an event. - * - * @param depth Schedule depth - * @param message Message that is scheduled - * @param sender Sender machine - */ - - public static void schedule(int depth, PMessage message, PMachine sender) { - if (verbosity > 0) { - String msg = - String.format(" Depth %d: %s sent %s to %s", depth, sender, message.getEvent(), message.getTarget()); - log.info(msg); - } - } - - /** - * Log at the start of replaying a counterexample - */ - public static void logStartReplayCex() { - log.info("------------------------"); - log.info("Replaying Counterexample"); - log.info("-----------------------"); - } -} diff --git a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/machine/PMachine.java b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/machine/PMachine.java index dff212214..abc8f104f 100644 --- a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/machine/PMachine.java +++ b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/machine/PMachine.java @@ -3,10 +3,12 @@ import lombok.Getter; import pexplicit.runtime.PExplicitGlobal; import pexplicit.runtime.logger.PExplicitLogger; +import pexplicit.runtime.logger.ScheduleWriter; import pexplicit.runtime.machine.buffer.DeferQueue; -import pexplicit.runtime.machine.buffer.SenderQueue; +import pexplicit.runtime.machine.buffer.FifoQueue; import pexplicit.runtime.machine.eventhandlers.EventHandler; import pexplicit.runtime.machine.events.PContinuation; +import pexplicit.runtime.scheduler.replay.ReceiverQueueReplayer; import pexplicit.utils.exceptions.BugFoundException; import pexplicit.utils.misc.Assert; import pexplicit.utils.serialize.SerializableBiFunction; @@ -34,7 +36,7 @@ public abstract class PMachine implements Serializable, Comparable { private final Set states; private final State startState; @Getter - private final SenderQueue sendBuffer; + private final FifoQueue eventBuffer; private final DeferQueue deferQueue; @Getter private final Map continuationMap = new TreeMap<>(); @@ -93,7 +95,7 @@ public void handleEvent(PMachine target, PValue payload) { }); // initialize send buffer - this.sendBuffer = new SenderQueue(this); + this.eventBuffer = new FifoQueue(this); this.deferQueue = new DeferQueue(this); } @@ -122,7 +124,7 @@ public boolean canRun() { public void reset() { this.currentState = startState; - this.sendBuffer.clear(); + this.eventBuffer.clear(); this.deferQueue.clear(); this.started = false; @@ -168,7 +170,7 @@ public List getLocalVarValues() { result.add(currentState); - result.add(sendBuffer.getElements()); + result.add(eventBuffer.getElements()); result.add(deferQueue.getElements()); result.add(started); @@ -192,7 +194,7 @@ public List copyLocalVarValues() { result.add(currentState); - result.add(new ArrayList<>(sendBuffer.getElements())); + result.add(new ArrayList<>(eventBuffer.getElements())); result.add(new ArrayList<>(deferQueue.getElements())); result.add(started); @@ -217,7 +219,7 @@ protected int setLocalVarValues(List values) { currentState = (State) values.get(idx++); - sendBuffer.setElements(new ArrayList<>((List) values.get(idx++))); + eventBuffer.setElements(new ArrayList<>((List) values.get(idx++))); deferQueue.setElements(new ArrayList<>((List) values.get(idx++))); started = (boolean) values.get(idx++); @@ -239,6 +241,17 @@ public void setMachineState(MachineLocalState input) { setLocalVarValues(input.getLocals()); } + private void addMessage(PMessage msg) { + if (PExplicitGlobal.getScheduler() instanceof ReceiverQueueReplayer) { + ScheduleWriter.logSend(msg); + } + + switch(PExplicitGlobal.getConfig().getBufferSemantics()) { + case SenderQueue -> this.eventBuffer.add(msg); + case ReceiverQueue -> msg.getTarget().eventBuffer.add(msg); + } + } + /** * Create a new machine instance * @@ -252,8 +265,8 @@ public PMachineValue create( PValue payload, Function constructor) { PMachine machine = PExplicitGlobal.getScheduler().allocateMachine(machineType, constructor); - PMessage msg = new PMessage(PEvent.createMachine, machine, payload); - sendBuffer.add(msg); + PMessage msg = new PMessage(PEvent.createMachine, machine, payload, this); + addMessage(msg); return new PMachineValue(machine); } @@ -282,12 +295,13 @@ public void sendEvent(PMachineValue target, PEvent event, PValue payload) { throw new BugFoundException("Machine in send event cannot be null."); } - PMessage msg = new PMessage(event, target.getValue(), payload); + PMessage msg = new PMessage(event, target.getValue(), payload, this); // log send event - PExplicitLogger.logSendEvent(this, msg); + PExplicitLogger.logSendEvent(msg); + + addMessage(msg); - sendBuffer.add(msg); PExplicitGlobal.getScheduler().runMonitors(msg); } @@ -408,6 +422,10 @@ void processEvent(PMessage message) { * @param message Message to process */ void runEvent(PMessage message) { + if (PExplicitGlobal.getScheduler() instanceof ReceiverQueueReplayer) { + ScheduleWriter.logReceive(message); + } + if (isBlocked()) { PContinuation currBlockedBy = this.blockedBy; PEvent event = message.getEvent(); @@ -448,7 +466,7 @@ public void raiseEvent(PEvent event, PValue payload) { return; } - PMessage msg = new PMessage(event, this, payload); + PMessage msg = new PMessage(event, this, payload, this); // log raise event PExplicitLogger.logRaiseEvent(this, event); diff --git a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/machine/buffer/BufferSemantics.java b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/machine/buffer/BufferSemantics.java index 4a991d13e..2dba4060f 100644 --- a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/machine/buffer/BufferSemantics.java +++ b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/machine/buffer/BufferSemantics.java @@ -4,5 +4,6 @@ * Supported event buffer semantics */ public enum BufferSemantics { - SenderQueue + SenderQueue, + ReceiverQueue } diff --git a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/machine/buffer/EventBuffer.java b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/machine/buffer/EventBuffer.java deleted file mode 100644 index dbcc25bc5..000000000 --- a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/machine/buffer/EventBuffer.java +++ /dev/null @@ -1,19 +0,0 @@ -package pexplicit.runtime.machine.buffer; - -import pexplicit.runtime.machine.PMachine; -import pexplicit.values.PEvent; -import pexplicit.values.PValue; - -/** - * Represents an interface implemented by a machine event buffer - */ -public interface EventBuffer { - /** - * Send an event - * - * @param target Target machine - * @param event Event - * @param payload Event payload - */ - void send(PMachine target, PEvent event, PValue payload); -} diff --git a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/machine/buffer/FifoQueue.java b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/machine/buffer/FifoQueue.java new file mode 100644 index 000000000..8c39d938f --- /dev/null +++ b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/machine/buffer/FifoQueue.java @@ -0,0 +1,20 @@ +package pexplicit.runtime.machine.buffer; + +import pexplicit.runtime.machine.PMachine; + +import java.io.Serializable; + +/** + * Represents a FIFO event queue + */ +public class FifoQueue extends MessageQueue implements Serializable { + + /** + * Constructor + * + * @param owner Machine (owner of the queue) + */ + public FifoQueue(PMachine owner) { + super(owner); + } +} diff --git a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/machine/buffer/SenderQueue.java b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/machine/buffer/SenderQueue.java deleted file mode 100644 index b84aee732..000000000 --- a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/machine/buffer/SenderQueue.java +++ /dev/null @@ -1,35 +0,0 @@ -package pexplicit.runtime.machine.buffer; - -import pexplicit.runtime.machine.PMachine; -import pexplicit.utils.exceptions.NotImplementedException; -import pexplicit.values.PEvent; -import pexplicit.values.PValue; - -import java.io.Serializable; - -/** - * Represents a FIFO sender event queue - */ -public class SenderQueue extends MessageQueue implements EventBuffer, Serializable { - - /** - * Constructor - * - * @param owner Sender machine (owner of the queue) - */ - public SenderQueue(PMachine owner) { - super(owner); - } - - /** - * TODO - * - * @param target Target machine - * @param eventName Event - * @param payload Event payload - */ - public void send(PMachine target, PEvent eventName, PValue payload) { - throw new NotImplementedException(); - } - -} diff --git a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/Schedule.java b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/Schedule.java index 3591e725f..747203d9e 100644 --- a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/Schedule.java +++ b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/Schedule.java @@ -73,7 +73,6 @@ public void setScheduleChoice(int stepNum, int choiceNum, PMachineId current) { assert (choiceNum < choices.size()); if (PExplicitGlobal.getConfig().isStatefulBacktrackEnabled() && stepNum != 0) { - assert (stepBeginState != null); choices.set(choiceNum, new ScheduleChoice(stepNum, choiceNum, current, stepBeginState)); } else { choices.set(choiceNum, new ScheduleChoice(stepNum, choiceNum, current, null)); diff --git a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/Scheduler.java b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/Scheduler.java index 163b0ef86..c88fbde29 100644 --- a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/Scheduler.java +++ b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/Scheduler.java @@ -229,17 +229,17 @@ public void startMachine(PMachine machine) { stepState.makeMachine(machine); // run create machine event - processCreateEvent(new PMessage(PEvent.createMachine, machine, null)); + processCreateEvent(new PMessage(PEvent.createMachine, machine, null, machine)); } /** - * Execute a step by popping a message from the sender FIFO buffer and handling it + * Execute a step by popping a message from the machine's FIFO buffer and handling it * - * @param sender Sender machine + * @param schChoice Machine */ - public void executeStep(PMachine sender) { - // pop message from sender queue - PMessage msg = sender.getSendBuffer().remove(); + public void executeStep(PMachine schChoice) { + // pop message from machine queue + PMessage msg = schChoice.getEventBuffer().remove(); isStickyStep = msg.getEvent().isCreateMachineEvent(); if (!isStickyStep) { @@ -251,10 +251,10 @@ public void executeStep(PMachine sender) { stepNumLogs = 0; // log start step - PExplicitLogger.logStartStep(stepNumber, sender, msg); + PExplicitLogger.logStartStep(stepNumber, msg); // process message - processDequeueEvent(sender, msg); + processDequeueEvent(schChoice, msg); // update done stepping flag isDoneStepping = (stepNumber >= PExplicitGlobal.getConfig().getMaxStepBound()); @@ -316,10 +316,10 @@ public void processCreateEvent(PMessage message) { * * @param message Message to process */ - public void processDequeueEvent(PMachine sender, PMessage message) { + public void processDequeueEvent(PMachine schChoice, PMessage message) { if (message.getEvent().isCreateMachineEvent()) { // log create machine - PExplicitLogger.logCreateMachine(message.getTarget(), sender); + PExplicitLogger.logCreateMachine(message.getTarget(), message.getSender()); } else { // log monitor process event PExplicitLogger.logDequeueEvent(message.getTarget(), message); @@ -338,7 +338,7 @@ public void announce(PEvent event, PValue payload) { if (event == null) { throw new NotImplementedException("Machine cannot announce a null event"); } - PMessage message = new PMessage(event, null, payload); + PMessage message = new PMessage(event, null, payload, null); runMonitors(message); } diff --git a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/explicit/ExplicitSearchScheduler.java b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/explicit/ExplicitSearchScheduler.java index c233ca8d8..bd8aa9da2 100644 --- a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/explicit/ExplicitSearchScheduler.java +++ b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/explicit/ExplicitSearchScheduler.java @@ -12,7 +12,6 @@ import pexplicit.runtime.machine.PMachine; import pexplicit.runtime.machine.PMachineId; import pexplicit.runtime.scheduler.Scheduler; -import pexplicit.runtime.scheduler.choice.Choice; import pexplicit.runtime.scheduler.choice.ScheduleChoice; import pexplicit.runtime.scheduler.choice.SearchUnit; import pexplicit.runtime.scheduler.explicit.strategy.*; @@ -198,10 +197,10 @@ protected void runStep() throws TimeoutException { schedule.setStepBeginState(stepState.copyState()); } - // get a scheduling choice as sender machine - PMachine sender = getNextScheduleChoice(); + // get a scheduling choice as a machine + PMachine schChoice = getNextScheduleChoice(); - if (sender == null) { + if (schChoice == null) { // done with this schedule scheduleTerminated = true; skipLiveness = false; @@ -210,8 +209,8 @@ protected void runStep() throws TimeoutException { return; } - // execute a step from message in the sender queue - executeStep(sender); + // execute a step from message in the event queue + executeStep(schChoice); } /** @@ -284,14 +283,6 @@ Object getCurrentStateKey() { return stateKey; } - /** - * Reset the scheduler. - */ - @Override - protected void reset() { - super.reset(); - } - /** * Get the next schedule choice. * @@ -541,7 +532,7 @@ private void postIterationCleanup() { stepNumber = newStepNumber; choiceNumber = scheduleChoice.getChoiceNumber(); stepState.setTo(scheduleChoice.getChoiceState()); - assert (!PExplicitGlobal.getGlobalMachine(scheduleChoice.getCurrent()).getSendBuffer().isEmpty()); + assert (!PExplicitGlobal.getGlobalMachine(scheduleChoice.getCurrent()).getEventBuffer().isEmpty()); } schedule.removeChoicesAfter(backtrackChoiceNumber); PExplicitLogger.logBacktrack(newStepNumber, cIdx, unit); @@ -554,7 +545,7 @@ private void postIterationCleanup() { private List getNewScheduleChoices() { // prioritize create machine events for (PMachine machine : stepState.getMachineSet()) { - if (machine.getSendBuffer().nextIsCreateMachineMsg()) { + if (machine.getEventBuffer().nextIsCreateMachineMsg()) { return new ArrayList<>(Collections.singletonList(machine.getPid())); } } @@ -563,7 +554,7 @@ private List getNewScheduleChoices() { List choices = new ArrayList<>(); for (PMachine machine : stepState.getMachineSet()) { - if (machine.getSendBuffer().nextHasTargetRunning()) { + if (machine.getEventBuffer().nextHasTargetRunning()) { choices.add(machine.getPid()); } } diff --git a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/replay/ReplayScheduler.java b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/replay/ReceiverQueueReplayer.java similarity index 84% rename from Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/replay/ReplayScheduler.java rename to Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/replay/ReceiverQueueReplayer.java index 2b5b48764..8ad9b41d3 100644 --- a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/replay/ReplayScheduler.java +++ b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/replay/ReceiverQueueReplayer.java @@ -5,6 +5,7 @@ import pexplicit.runtime.logger.ScheduleWriter; import pexplicit.runtime.machine.PMachine; import pexplicit.runtime.machine.PMachineId; +import pexplicit.runtime.machine.buffer.BufferSemantics; import pexplicit.runtime.scheduler.Schedule; import pexplicit.runtime.scheduler.Scheduler; import pexplicit.utils.misc.Assert; @@ -13,9 +14,11 @@ import java.util.List; import java.util.concurrent.TimeoutException; -public class ReplayScheduler extends Scheduler { - public ReplayScheduler(Schedule sch) { +public class ReceiverQueueReplayer extends Scheduler { + + public ReceiverQueueReplayer(Schedule sch) { super(sch); + PExplicitGlobal.getConfig().setBufferSemantics(BufferSemantics.ReceiverQueue); } @Override @@ -61,10 +64,10 @@ protected void runIteration() throws TimeoutException { @Override protected void runStep() throws TimeoutException { - // get a scheduling choice as sender machine - PMachine sender = getNextScheduleChoice(); + // get a scheduling choice as a machine + PMachine schChoice = getNextScheduleChoice(); - if (sender == null) { + if (schChoice == null) { // done with this schedule scheduleTerminated = true; isDoneStepping = true; @@ -72,13 +75,10 @@ protected void runStep() throws TimeoutException { return; } - // execute a step from message in the sender queue - executeStep(sender); - } + ScheduleWriter.logScheduleChoice(schChoice.getEventBuffer().peek().getTarget()); - @Override - protected void reset() { - super.reset(); + // execute a step from message in the machine queue + executeStep(schChoice); } @Override @@ -94,7 +94,6 @@ protected PMachine getNextScheduleChoice() { } PMachine result = PExplicitGlobal.getGlobalMachine(pid); - ScheduleWriter.logScheduleChoice(result); PExplicitLogger.logRepeatScheduleChoice(result, stepNumber, choiceNumber); choiceNumber++; diff --git a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/replay/SenderQueueReplayer.java b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/replay/SenderQueueReplayer.java new file mode 100644 index 000000000..169f9cfa9 --- /dev/null +++ b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/replay/SenderQueueReplayer.java @@ -0,0 +1,123 @@ +package pexplicit.runtime.scheduler.replay; + +import lombok.Getter; +import pexplicit.runtime.PExplicitGlobal; +import pexplicit.runtime.logger.PExplicitLogger; +import pexplicit.runtime.machine.PMachine; +import pexplicit.runtime.machine.PMachineId; +import pexplicit.runtime.machine.buffer.BufferSemantics; +import pexplicit.runtime.scheduler.Schedule; +import pexplicit.runtime.scheduler.Scheduler; +import pexplicit.utils.misc.Assert; +import pexplicit.values.PValue; + +import java.util.List; +import java.util.concurrent.TimeoutException; + +public class SenderQueueReplayer extends Scheduler { + @Getter + Schedule receiverSemanticsSchedule; + + public SenderQueueReplayer(Schedule sch) { + super(sch); + PExplicitGlobal.getConfig().setBufferSemantics(BufferSemantics.SenderQueue); + receiverSemanticsSchedule = new Schedule(); + } + + @Override + public void run() throws TimeoutException, InterruptedException { + PExplicitLogger.logStartReplay(); + + // log run test + PExplicitLogger.logRunTest(); + + stepState.resetToZero(); + start(); + runIteration(); + } + + @Override + protected void runIteration() throws TimeoutException { + isDoneStepping = false; + scheduleTerminated = false; + while (!isDoneStepping) { + runStep(); + } + + // check if cycle detected error + if (Assert.getFailureType().equals("cycle")) { + Assert.cycle("Cycle detected: Infinite loop found due to revisiting a state multiple times in the same schedule"); + } + + if (Assert.getFailureType().equals("deadlock") && scheduleTerminated) { + // schedule terminated, check for deadlock + checkDeadlock(); + } + + if (Assert.getFailureType().equals("liveness")) { + // check for liveness + checkLiveness(scheduleTerminated); + } + + Assert.fromModel( + !PExplicitGlobal.getConfig().isFailOnMaxStepBound() || (stepNumber < PExplicitGlobal.getConfig().getMaxStepBound()), + "Step bound of " + PExplicitGlobal.getConfig().getMaxStepBound() + " reached."); + } + + @Override + protected void runStep() throws TimeoutException { + // get a scheduling choice as a machine + PMachine schChoice = getNextScheduleChoice(); + + if (schChoice == null) { + // done with this schedule + scheduleTerminated = true; + isDoneStepping = true; + PExplicitLogger.logFinishedIteration(stepNumber); + return; + } + + // execute a step from message in the machine queue + executeStep(schChoice); + } + + @Override + protected PMachine getNextScheduleChoice() { + if (choiceNumber >= schedule.size()) { + return null; + } + + // pick the current schedule choice + PMachineId pid = schedule.getCurrentScheduleChoice(choiceNumber); + if (pid == null) { + return null; + } + + PMachine result = PExplicitGlobal.getGlobalMachine(pid); + PExplicitLogger.logRepeatScheduleChoice(result, stepNumber, choiceNumber); + + if (result != null) { + receiverSemanticsSchedule.setScheduleChoice(stepNumber, choiceNumber, result.getEventBuffer().peek().getTarget().getPid()); + } + + choiceNumber++; + return result; + } + + @Override + protected PValue getNextDataChoice(List> input_choices) { + if (choiceNumber >= schedule.size()) { + return null; + } + + // pick the current data choice + PValue result = schedule.getCurrentDataChoice(choiceNumber); + assert (input_choices.contains(result)); + PExplicitLogger.logRepeatDataChoice(result, stepNumber, choiceNumber); + + receiverSemanticsSchedule.setDataChoice(stepNumber, choiceNumber, result); + + choiceNumber++; + return result; + } +} diff --git a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/values/PMessage.java b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/values/PMessage.java index b72710948..143a3a46a 100644 --- a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/values/PMessage.java +++ b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/values/PMessage.java @@ -11,6 +11,7 @@ public class PMessage extends PValue { private final PEvent event; private final PMachine target; private final PValue payload; + private final PMachine sender; /** * Constructor @@ -19,20 +20,21 @@ public class PMessage extends PValue { * @param target Target machine * @param payload Event payload */ - public PMessage(PEvent event, PMachine target, PValue payload) { + public PMessage(PEvent event, PMachine target, PValue payload, PMachine sender) { this.event = event; this.target = target; this.payload = payload; + this.sender = sender; initialize(); } public PMessage setTarget(PMachine target) { - return new PMessage(event, target, payload); + return new PMessage(event, target, payload, sender); } @Override public PMessage clone() { - return new PMessage(this.event, this.target, this.payload); + return new PMessage(this.event, this.target, this.payload, this.sender); } @Override