Skip to content

Commit

Permalink
[PEx] Store temporary changes
Browse files Browse the repository at this point in the history
  • Loading branch information
@aman-goel
aman-goel committed Jun 18, 2024
1 parent 82b298c commit 9055164
Show file tree
Hide file tree
Showing 15 changed files with 263 additions and 269 deletions.
40 changes: 26 additions & 14 deletions Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/RuntimeExecutor.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -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);
Expand Down
20 changes: 13 additions & 7 deletions Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/logger/PExplicitLogger.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -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()));
}
Expand Down Expand Up @@ -267,7 +268,8 @@ public static void logNewState(int step, int idx, Object stateKey, SortedSet<PMa
}

private static boolean isReplaying() {
return (PExplicitGlobal.getScheduler() instanceof ReplayScheduler);
return (PExplicitGlobal.getScheduler() instanceof SenderQueueReplayer ||
PExplicitGlobal.getScheduler() instanceof ReceiverQueueReplayer);
}

private static boolean typedLogEnabled() {
Expand Down Expand Up @@ -320,15 +322,15 @@ public static void logCreateMachine(PMachine machine, PMachine creator) {
}
}

public static void logSendEvent(PMachine sender, PMessage message) {
public static void logSendEvent(PMessage message) {
PExplicitGlobal.getScheduler().updateLogNumber();
if (typedLogEnabled()) {
String payloadMsg = "";
if (message.getPayload() != null) {
payloadMsg = String.format(" with payload %s", message.getPayload());
}
typedLog(LogType.SendLog, String.format("%s in state %s sent event %s%s to %s.",
sender, sender.getCurrentState(), message.getEvent(), payloadMsg, message.getTarget()));
message.getSender(), message.getSender().getCurrentState(), message.getEvent(), payloadMsg, message.getTarget()));
}
}

Expand Down Expand Up @@ -401,7 +403,11 @@ public static void logDequeueEvent(PMachine machine, PMessage message) {
public static void logStartReplay() {
if (verbosity > 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");
}

}
}
}
15 changes: 13 additions & 2 deletions Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/logger/ScheduleWriter.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -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() {
Expand All @@ -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()));
}
}
134 changes: 0 additions & 134 deletions Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/logger/TraceLogger.java
View file

This file was deleted.

Loading

0 comments on commit 9055164

Please sign in to comment.