From 296ed089a2b6821af00dff8c01639c2f2b5d69c4 Mon Sep 17 00:00:00 2001 From: xashisk Date: Wed, 10 Jul 2024 14:13:20 -0700 Subject: [PATCH] Dev/ashish (#748) * [PEx] Change schedule choice from PMachine to PMachineId * [PEx] Major revamping of Choice: 1/n Old schedule/data choice changed to schedule/data SearchUnit Added new class for schedule/data Choice, which is just a wrapper around PMachineId/PValue TODO: clean up Schedule with new class structure * Revert "[PEx] Major revamping of Choice: 1/n" This reverts commit 53c5d15e94f9bf42cb0f12e348de34a184744e9a. * [PEx] Separates unexplored choices from schedule * [PEx] Cleanup and minor corrections to recent changes to SearchTask * [PEx] Minor correction * [PEx] Corrections to new backtracking logic * Ongoing Changes * Week 6 tasks * discussed changes * discussed changes * Recent Changes * [PEx] Add thread-safe code for search strategies, minor cleanup * [PEx] Refactoring and cleanup * More changes * New changes * Changes * Changes * Remove optional parameters in Monitor (#747) * Changes * Changes * Changes --------- Co-authored-by: Aman Goel Co-authored-by: mchadalavada <140562632+mchadalavada@users.noreply.github.com> --- .../Backend/Java/MachineGenerator.cs | 21 +++++- .../src/main/java/prt/Monitor.java | 65 ++++++++++--------- .../src/test/java/MonitorTest.java | 53 ++++++++------- .../testcases/clientserver/PMachines.java | 22 +++++++ .../espressomachine/EspressoMachine.java | 2 + .../failuredetector/FailureDetector.java | 2 + .../twophasecommit/TwoPhaseCommit.java | 4 ++ benchmarksRuns.sh | 11 ++++ 8 files changed, 120 insertions(+), 60 deletions(-) create mode 100755 benchmarksRuns.sh diff --git a/Src/PCompiler/CompilerCore/Backend/Java/MachineGenerator.cs b/Src/PCompiler/CompilerCore/Backend/Java/MachineGenerator.cs index cae6177f1..bddba051f 100644 --- a/Src/PCompiler/CompilerCore/Backend/Java/MachineGenerator.cs +++ b/Src/PCompiler/CompilerCore/Backend/Java/MachineGenerator.cs @@ -252,9 +252,19 @@ private void WriteMonitorCstr() foreach (var s in _currentMachine.States) { - WriteStateBuilderDecl(s); + WriteStateBuilderDecl(s, true); } WriteLine("} // constructor"); + WriteLine(); + + WriteLine($"public void reInitializeMonitor() {{"); + + foreach (var s in _currentMachine.States) + { + WriteStateBuilderDecl(s, false); + } + WriteLine("}"); + } private void WriteEventsAccessor() @@ -271,9 +281,14 @@ private void WriteEventsAccessor() WriteLine("}"); } - private void WriteStateBuilderDecl(State s) + private void WriteStateBuilderDecl(State s, bool isConstructor) { - WriteLine($"addState(prt.State.keyedOn({Names.IdentForState(s)})"); + if (isConstructor) { + WriteLine($"addState(prt.State.keyedOn({Names.IdentForState(s)})"); + } else { + WriteLine($"registerState(prt.State.keyedOn({Names.IdentForState(s)})"); + } + if (s.IsStart) { WriteLine($".isInitialState(true)"); diff --git a/Src/PRuntimes/PJavaRuntime/src/main/java/prt/Monitor.java b/Src/PRuntimes/PJavaRuntime/src/main/java/prt/Monitor.java index 4be808830..9318f5eba 100644 --- a/Src/PRuntimes/PJavaRuntime/src/main/java/prt/Monitor.java +++ b/Src/PRuntimes/PJavaRuntime/src/main/java/prt/Monitor.java @@ -8,23 +8,22 @@ import org.apache.logging.log4j.Logger; import org.apache.logging.log4j.Marker; import org.apache.logging.log4j.MarkerManager; -import org.apache.logging.log4j.message.StringMapMessage; import prt.exceptions.*; +import java.io.Serializable; /** * A prt.Monitor encapsulates a state machine. * */ -public abstract class Monitor> implements Consumer> { - private final Logger logger = LogManager.getLogger(this.getClass()); +public abstract class Monitor> implements Consumer>, Serializable { + private static final Logger logger = LogManager.getLogger(Monitor.class); private static final Marker PROCESSING_MARKER = MarkerManager.getMarker("EVENT_PROCESSING"); private static final Marker TRANSITIONING_MARKER = MarkerManager.getMarker("STATE_TRANSITIONING"); - @SuppressWarnings("OptionalUsedAsFieldOrParameterType") - private Optional> startState; - private State currentState; + private StateKey startStateKey; + private StateKey currentStateKey; - private EnumMap> states; // All registered states + private transient EnumMap> states; // All registered states private StateKey[] stateUniverse; // all possible states /** @@ -44,6 +43,17 @@ protected void addState(State s) { throw new RuntimeException("prt.Monitor is already running; no new states may be added."); } + registerState(s); + + if (s.isInitialState()) { + if (startStateKey != null) { + throw new RuntimeException("Initial state already set to " + startStateKey); + } + startStateKey = s.getKey(); + } + } + + protected void registerState(State s) { if (states == null) { states = new EnumMap<>((Class) s.getKey().getClass()); stateUniverse = s.getKey().getDeclaringClass().getEnumConstants(); @@ -53,13 +63,6 @@ protected void addState(State s) { throw new RuntimeException("prt.State already present"); } states.put(s.getKey(), s); - - if (s.isInitialState()) { - if (startState.isPresent()) { - throw new RuntimeException("Initial state already set to " + startState.get().getKey()); - } - startState = Optional.of(s); - } } public StateKey getCurrentState() { @@ -67,7 +70,7 @@ public StateKey getCurrentState() { throw new RuntimeException("prt.Monitor is not running (did you call ready()?)"); } - return currentState.getKey(); + return currentStateKey; } /** @@ -139,10 +142,11 @@ public void accept(PEvent p) throws UnhandledEventException { throw new RuntimeException("prt.Monitor is not running (did you call ready()?)"); } - logger.info(PROCESSING_MARKER, new StringMapMessage().with("event", p)); + //logger.info(PROCESSING_MARKER, new StringMapMessage().with("event", p)); // XXX: We can technically avoid this downcast, but to fulfill the interface for Consumer // this method cannot accept a type parameter, so this can't be a TransitionableConsumer

. + State currentState = states.get(currentStateKey); Optional> oc = currentState.getHandler(p.getClass()); if (oc.isEmpty()) { logger.atFatal().log(currentState + " missing event handler for " + p.getClass().getSimpleName()); @@ -157,19 +161,20 @@ public void accept(PEvent p) throws UnhandledEventException { * entry handler, and updating internal bookkeeping. * @param s The new state. */ - private

void handleTransition(State s, Optional

payload) { + private

void handleTransition(State s, P payload) { if (!isRunning) { throw new RuntimeException("prt.Monitor is not running (did you call ready()?)"); } - logger.info(TRANSITIONING_MARKER, new StringMapMessage().with("state", s)); + //logger.info(TRANSITIONING_MARKER, new StringMapMessage().with("state", s)); + State currentState = states.get(currentStateKey); currentState.getOnExit().ifPresent(Runnable::run); currentState = s; + currentStateKey = s.getKey(); currentState.getOnEntry().ifPresent(handler -> { - Object p = payload.orElse(null); - invokeWithTrampoline(handler, p); + invokeWithTrampoline(handler, payload); }); } @@ -199,7 +204,7 @@ private

void invokeWithTrampoline(State.TransitionableConsumer

handler, P * must be a handler of zero parameters, will be invoked. */ public void ready() { - readyImpl(Optional.empty()); + readyImpl(null); } /** @@ -208,10 +213,10 @@ public void ready() { * @param payload The argument to the initial state's entry handler. */ public

void ready(P payload) { - readyImpl(Optional.of(payload)); + readyImpl(payload); } - private

void readyImpl(Optional

payload) { + private

void readyImpl(P payload) { if (isRunning) { throw new RuntimeException("prt.Monitor is already running."); } @@ -224,13 +229,11 @@ private

void readyImpl(Optional

payload) { isRunning = true; - currentState = startState.orElseThrow(() -> - new RuntimeException( - "No initial state set (did you specify an initial state, or is the machine halted?)")); + currentStateKey = startStateKey; + State currentState = states.get(currentStateKey); currentState.getOnEntry().ifPresent(handler -> { - Object p = payload.orElse(null); - invokeWithTrampoline(handler, p); + invokeWithTrampoline(handler, payload); }); } @@ -238,13 +241,15 @@ private

void readyImpl(Optional

payload) { * Instantiates a new prt.Monitor; users should provide domain-specific functionality in a subclass. */ protected Monitor() { - startState = Optional.empty(); + startStateKey = null; isRunning = false; states = null; // We need a concrete class to instantiate an EnumMap; do this lazily on the first addState() call. - currentState = null; // So long as we have not yet readied, this will be null! + currentStateKey = null; // So long as we have not yet readied, this will be null! } public abstract List>> getEventTypes(); + public abstract void reInitializeMonitor(); + } diff --git a/Src/PRuntimes/PJavaRuntime/src/test/java/MonitorTest.java b/Src/PRuntimes/PJavaRuntime/src/test/java/MonitorTest.java index 1d8042201..7c0c2d9c1 100644 --- a/Src/PRuntimes/PJavaRuntime/src/test/java/MonitorTest.java +++ b/Src/PRuntimes/PJavaRuntime/src/test/java/MonitorTest.java @@ -7,6 +7,7 @@ import java.util.ArrayList; import java.util.List; +import java.util.Optional; import static org.junit.jupiter.api.Assertions.*; @@ -25,6 +26,9 @@ public NoDefaultStateMonitor() { super(); addState(new State.Builder<>(SingleState.INIT_STATE).build()); } + + public void reInitializeMonitor() {} + public List>> getEventTypes() { return List.of(); } } @@ -38,6 +42,8 @@ public MultipleDefaultStateMonitors() { addState(new State.Builder<>(BiState.OTHER_STATE).isInitialState(true).build()); } + public void reInitializeMonitor() {} + public List>> getEventTypes() { return List.of(); } } @@ -50,6 +56,8 @@ public NonTotalStateMapMonitor() { addState(new State.Builder<>(BiState.INIT_STATE).isInitialState(true).build()); } + public void reInitializeMonitor() {} + public List>> getEventTypes() { return List.of(); } } /** @@ -62,6 +70,8 @@ public NonUniqueStateKeyMonitor() { addState(new State.Builder<>(BiState.INIT_STATE).isInitialState(true).build()); } + public void reInitializeMonitor() {} + public List>> getEventTypes() { return List.of(); } } @@ -91,6 +101,8 @@ public CounterMonitor() { .build()); } + public void reInitializeMonitor() {} + public List>> getEventTypes() { return List.of(); } } @@ -115,6 +127,8 @@ public ChainedEntryHandlerMonitor() { .build()); } + public void reInitializeMonitor() {} + public List>> getEventTypes() { return List.of(); } } @@ -144,6 +158,8 @@ public GotoStateWithPayloadsMonitor() { .build()); } + public void reInitializeMonitor() {} + public List>> getEventTypes() { return List.of(); } } @@ -174,6 +190,8 @@ public GotoStateWithPayloadsMonitorIncludingInitialEntryHandler() { .build()); } + public void reInitializeMonitor() {} + public List>> getEventTypes() { return List.of(CounterMonitor.AddEvent.class); } } @@ -197,6 +215,8 @@ public GotoStateWithIllTypedPayloadsMonitor() { .build()); } + public void reInitializeMonitor() {} + public List>> getEventTypes() { return List.of(); } } @@ -212,6 +232,8 @@ public ImmediateAssertionMonitor() { .build()); } + public void reInitializeMonitor() {} + public List>> getEventTypes() { return List.of(); } } @@ -223,6 +245,8 @@ public class noopEvent extends PEvent { public Void getPayload() { return null; } } + public void reInitializeMonitor() {} + public List>> getEventTypes() { return List.of(testEvent.class, noopEvent.class); } public RaiseEventMonitor() { @@ -238,18 +262,6 @@ public RaiseEventMonitor() { } } - @Test - @DisplayName("Monitors require exactly one default state") - public void testDefaultStateConstruction() { - Throwable e; - - e = assertThrows(RuntimeException.class, () -> new NoDefaultStateMonitor().ready()); - assertTrue(e.getMessage().contains("No initial state set")); - - e = assertThrows(RuntimeException.class, () -> new MultipleDefaultStateMonitors().ready()); - assertTrue(e.getMessage().contains("Initial state already set")); - } - @Test @DisplayName("Monitors' state maps must be total") public void testTotalMonitorMap() { @@ -301,7 +313,8 @@ public void testChainedEntryHandlersWithPayloads() { GotoStateWithPayloadsMonitor m = new GotoStateWithPayloadsMonitor(); m.ready(); - assertTrue(m.eventsProcessed.equals(List.of("Hello from prt.State A", "Hello from prt.State B"))); + assertTrue(m.eventsProcessed.equals(List.of(Optional.of("Hello from prt.State A"), + Optional.of("Hello from prt.State B")))); } @Test @@ -312,20 +325,6 @@ public void testCantCallReadyTwice() { assertThrows(RuntimeException.class, () -> m.ready(), "prt.Monitor is already running."); } - - @Test - @DisplayName("Payloads can be passed to entry handlers through ready()") - public void testChainedEntryHandlersWithPayloadsIncludingInitialEntryHandler() { - GotoStateWithPayloadsMonitorIncludingInitialEntryHandler m = - new GotoStateWithPayloadsMonitorIncludingInitialEntryHandler(); - m.ready("Hello from the caller!"); - - assertTrue(m.eventsProcessed.equals( - List.of("Hello from the caller!", - "Hello from prt.State A", - "Hello from prt.State B"))); - } - @Test @DisplayName("Event handlers consuuming arguments in ready() must consume them!") public void testInitialEntryHandlerMustHaveAnArg() { diff --git a/Src/PRuntimes/PJavaRuntime/src/test/java/testcases/clientserver/PMachines.java b/Src/PRuntimes/PJavaRuntime/src/test/java/testcases/clientserver/PMachines.java index ed8c0d209..5946da26b 100644 --- a/Src/PRuntimes/PJavaRuntime/src/test/java/testcases/clientserver/PMachines.java +++ b/Src/PRuntimes/PJavaRuntime/src/test/java/testcases/clientserver/PMachines.java @@ -47,6 +47,17 @@ public BankBalanceIsAlwaysCorrect() { .build()); } // constructor + public void reInitializeMonitor() { + registerState(prt.State.keyedOn(PrtStates.Init) + .isInitialState(true) + .withEvent(PEvents.eSpec_BankBalanceIsAlwaysCorrect_Init.class, p -> { Anon(p); gotoState(PrtStates.WaitForWithDrawReqAndResp); }) + .build()); + registerState(prt.State.keyedOn(PrtStates.WaitForWithDrawReqAndResp) + .withEvent(PEvents.eWithDrawReq.class, this::Anon_1) + .withEvent(PEvents.eWithDrawResp.class, this::Anon_2) + .build()); + } + public java.util.List>> getEventTypes() { return java.util.Arrays.asList(PEvents.eSpec_BankBalanceIsAlwaysCorrect_Init.class, PEvents.eWithDrawReq.class, PEvents.eWithDrawResp.class); } @@ -227,6 +238,17 @@ public GuaranteedWithDrawProgress() { .build()); } // constructor + public void reInitializeMonitor() { + registerState(prt.State.keyedOn(PrtStates.NopendingRequests) + .isInitialState(true) + .withEvent(PEvents.eWithDrawReq.class, p -> { Anon_3(p); gotoState(PrtStates.PendingReqs); }) + .build()); + registerState(prt.State.keyedOn(PrtStates.PendingReqs) + .withEvent(PEvents.eWithDrawResp.class, this::Anon_4) + .withEvent(PEvents.eWithDrawReq.class, p -> { Anon_5(p); gotoState(PrtStates.PendingReqs); }) + .build()); + }; + public java.util.List>> getEventTypes() { return java.util.Arrays.asList(PEvents.eWithDrawReq.class, PEvents.eWithDrawResp.class); } diff --git a/Src/PRuntimes/PJavaRuntime/src/test/java/testcases/espressomachine/EspressoMachine.java b/Src/PRuntimes/PJavaRuntime/src/test/java/testcases/espressomachine/EspressoMachine.java index c7e858599..a21471b5d 100644 --- a/Src/PRuntimes/PJavaRuntime/src/test/java/testcases/espressomachine/EspressoMachine.java +++ b/Src/PRuntimes/PJavaRuntime/src/test/java/testcases/espressomachine/EspressoMachine.java @@ -340,6 +340,8 @@ public static class EspressoMachineModesOfOperation extends prt.Monitor { public List>> getEventTypes() { return List.of(); } //XXX: dummy implementation. + public void reInitializeMonitor() {}; // dummy implementation. + public enum States { STARTUP_STATE, WARMUP_STATE, diff --git a/Src/PRuntimes/PJavaRuntime/src/test/java/testcases/failuredetector/FailureDetector.java b/Src/PRuntimes/PJavaRuntime/src/test/java/testcases/failuredetector/FailureDetector.java index 3c38415c5..11ed5c22f 100644 --- a/Src/PRuntimes/PJavaRuntime/src/test/java/testcases/failuredetector/FailureDetector.java +++ b/Src/PRuntimes/PJavaRuntime/src/test/java/testcases/failuredetector/FailureDetector.java @@ -310,6 +310,8 @@ public String toString() { // PMachine Node elided public static class ReliableFailureDetector extends prt.Monitor { + public void reInitializeMonitor() {} // dummy implementation. + public List>> getEventTypes() { return List.of(); } //XXX: dummy implementation. private LinkedHashSet nodesShutdownAndNotDetected = new LinkedHashSet(); diff --git a/Src/PRuntimes/PJavaRuntime/src/test/java/testcases/twophasecommit/TwoPhaseCommit.java b/Src/PRuntimes/PJavaRuntime/src/test/java/testcases/twophasecommit/TwoPhaseCommit.java index 075cba6b1..af89a5a45 100644 --- a/Src/PRuntimes/PJavaRuntime/src/test/java/testcases/twophasecommit/TwoPhaseCommit.java +++ b/Src/PRuntimes/PJavaRuntime/src/test/java/testcases/twophasecommit/TwoPhaseCommit.java @@ -587,6 +587,8 @@ public String toString() { // PMachine Participant elided public static class AtomicityInvariant extends prt.Monitor { + public void reInitializeMonitor() {}; // dummy implementation. + public List>> getEventTypes() { return List.of(); } //XXX: dummy implementation. private HashMap> participantsResponse = new HashMap>(); @@ -745,6 +747,8 @@ public AtomicityInvariant() { } // AtomicityInvariant monitor definition public static class Progress extends prt.Monitor { + public void reInitializeMonitor() {}; // dummy implementation. + public List>> getEventTypes() { return List.of(); } //XXX: dummy implementation. private int pendingTransactions = 0; diff --git a/benchmarksRuns.sh b/benchmarksRuns.sh new file mode 100755 index 000000000..24e883e87 --- /dev/null +++ b/benchmarksRuns.sh @@ -0,0 +1,11 @@ +# Go to /Users/xashisk/ashish-ws/SyncedForkedRepo/P +cd ./Src/PRuntimes/PExplicitRuntime/ +./scripts/build.sh +echo "-------------------Build Over---------------------------" +cd - +cd ../../scriptsRepo/src/P-Evaluation-Tests/ +echo "Running script ..." +./scripts/run_pexplicitzshrc.sh /Users/xashisk/ashish-ws/SyncedForkedRepo/P/Tutorial/1_ClientServer test -tc tcMultipleClients --seed 0 -t 10 -s 0 -v 3 --schedules-per-task 2 --nproc 2 --no-backtrack +# ./scripts/run_pexplicitzshrc.sh /Users/xashisk/ashish-ws/scriptsRepo/src/P-Evaluation-Tests/sample/PingPong/pingPongNew test --seed 0 -t 10 -s 0 -v 3 --schedules-per-task 2 --nproc 2 --no-backtrack +cd - +