Replays the trace from the initial state using {@link ExecutionDriver} and - * verifies the final configuration matches the expected outcome. For VIOLATION - * outcomes, the invariant is re-checked to ensure the trace genuinely reproduces - * the bug. + * verifies the final configuration matches the expected outcome. Only thread choices are + * replayed; recorded step outcomes and the trace's terminal verdict are ignored. Replay + * stops when the schedule is consumed or all threads terminate. * - *
The VIOLATION guard is not {@code isDeadlockCandidate()}, and must not be "simplified" into - * it. The guard below expands to {@code !allTerminated() && !enabled.isEmpty()} — live threads - * and something still enabled — which is a different predicate from "not a deadlock". Using - * the canonical predicate here would accept deadlocked configurations that violate the invariant, - * and would let the minimiser shrink a trace into one that ends in a state the search would have - * classified differently. The cost of the current form is that a violation occurring in a deadlocked - * state is not recognised as still failing, so such a trace cannot be minimised. That is a real - * limitation, but fixing it changes which traces the minimiser accepts and needs its own - * specification and tests rather than a quiet edit here. Recorded in - * {@code docs/specs/active/13-deferred-debt/03-canonical-configuration-key.md}. + *
For {@code VIOLATION} outcomes with an invariant, the invariant predicate is evaluated + * directly regardless of thread termination or deadlock status, ensuring invariant violations + * occurring in deadlocked terminal configurations are recognized and minimizable. When no invariant + * is supplied, fallback checks require live threads and non-deadlocked configurations. + * + *
An {@link IllegalScheduleException} from replay or invariant evaluation produces + * {@code false}; other runtime exceptions propagate to the caller. * * @param program the program to replay * @param trace the trace to replay * @param expectedOutcome the expected outcome to verify * @param invariant the invariant to check for VIOLATION outcomes; may be null - * @return true if the replayed trace reproduces the expected outcome + * @return true if the final configuration satisfies the selected outcome check; + * false for an illegal schedule or {@code INCOMPLETE} */ private boolean isStillFailing(Program program, Trace trace, TraceOutcome expectedOutcome, Invariant invariant) { try { @@ -108,7 +106,7 @@ private boolean isStillFailing(Program program, Trace trace, TraceOutcome expect case COMPLETED -> config.allTerminated(); case DEADLOCK -> config.isDeadlockCandidate(); case VIOLATION -> invariant != null - ? !config.allTerminated() && !config.isDeadlockCandidate() && !invariant.holds(config.state(), config) + ? !invariant.holds(config.state(), config) : !config.allTerminated() && !config.isDeadlockCandidate(); // INCOMPLETE describes the search, not a schedule: it means the preemption bound // was reached. No replay of a prefix can reproduce that, so reporting true here diff --git a/src/main/java/dev/samhb/interleave/search/CorruptedTraceException.java b/src/main/java/dev/samhb/interleave/search/CorruptedTraceException.java new file mode 100644 index 0000000..b9aac0e --- /dev/null +++ b/src/main/java/dev/samhb/interleave/search/CorruptedTraceException.java @@ -0,0 +1,16 @@ +/** Signals a recorded trace outcome that diverges from actual step execution. */ +package dev.samhb.interleave.search; + +/** + * Signals that replaying a recorded step produced an execution outcome that disagrees + * with the outcome recorded in the trace. + */ +public class CorruptedTraceException extends RuntimeException { + /** + * Creates corrupted trace exception with diagnostic message. + * @param message diagnostic explaining the outcome mismatch + */ + public CorruptedTraceException(String message) { + super(message); + } +} diff --git a/src/main/java/dev/samhb/interleave/search/TraceReplayer.java b/src/main/java/dev/samhb/interleave/search/TraceReplayer.java index d7e6679..8947910 100644 --- a/src/main/java/dev/samhb/interleave/search/TraceReplayer.java +++ b/src/main/java/dev/samhb/interleave/search/TraceReplayer.java @@ -9,12 +9,13 @@ public final class TraceReplayer { public TraceReplayer() {} /** - * Replays thread choices while trusting the step outcomes recorded in the trace. + * Replays thread choices while validating each step outcome against the trace. * *
The program supplies a fresh initial configuration. Each chosen step mutates that - * configuration’s state; the recorded outcome, rather than the returned execution outcome, - * controls counter advancement. This method does not validate trace consistency or verdicts. - * Callers must supply aligned thread/outcome lists and valid thread IDs and counters. + * configuration’s state and must produce the outcome recorded in the trace. + * An empty trace returns the initial configuration. Replay does not reject a chosen step + * solely because it is disabled, or validate the trace's terminal verdict. Exceptions from + * model callbacks propagate to the caller. * *
{@code
* Configuration end = new TraceReplayer().replay(program, trace);
@@ -22,6 +23,7 @@ public TraceReplayer() {}
* @param program program whose initial state and steps are replayed
* @param trace recorded thread choices and outcomes
* @return configuration after the recorded prefix has been executed
+ * @throws CorruptedTraceException if an executed step outcome differs from the trace outcome
* @throws IndexOutOfBoundsException if a recorded thread, counter, or outcome index is invalid
*/
public Configuration replay(Program program, Trace trace) {
@@ -35,10 +37,17 @@ public Configuration replay(Program program, Trace trace) {
int pc = config.programCounters().get(threadId);
Step step = thread.steps().get(pc);
- step.execute(config.state());
+ StepOutcome actualOutcome = step.execute(config.state());
+ if (actualOutcome != outcome) {
+ throw new CorruptedTraceException(
+ "Trace outcome mismatch at step " + i + " (thread " + threadId + "): "
+ + "recorded " + outcome + " but execution produced " + actualOutcome
+ );
+ }
config = config.successor(threadId, outcome, program.threads(), config.state());
}
return config;
}
}
+
diff --git a/src/test/java/dev/samhb/interleave/minimize/DeltaDebuggerTest.java b/src/test/java/dev/samhb/interleave/minimize/DeltaDebuggerTest.java
index 6571ecb..1dae302 100644
--- a/src/test/java/dev/samhb/interleave/minimize/DeltaDebuggerTest.java
+++ b/src/test/java/dev/samhb/interleave/minimize/DeltaDebuggerTest.java
@@ -92,4 +92,58 @@ void minimize_returnsSubsequence() {
assertTrue(minimizedIndex == minimizedThreadIds.size(),
"Minimized trace should be a subsequence of original");
}
+
+ @Test
+ void minimize_invariantViolationInDeadlockedConfiguration_succeeds() {
+ // T0 writes counter=1 then blocks on a condition that never becomes true.
+ // T1 performs an irrelevant read then terminates.
+ // Invariant asserts counter != 1.
+ // The terminal configuration is deadlocked (T0 live and blocked; T1 terminated),
+ // yet violates the invariant. DeltaDebugger should accept and minimize this trace.
+ Program program = new Program(CounterState.of(0), List.of(
+ new ModelThread(0, List.of(
+ new WriteCounterStep(0),
+ new Step() {
+ @Override
+ public boolean enabled(SharedState state) {
+ return false; // permanently blocked -> deadlock candidate
+ }
+
+ @Override
+ public StepOutcome execute(SharedState state) {
+ return StepOutcome.BLOCKED;
+ }
+
+ @Override
+ public Set reads() {
+ return Set.of();
+ }
+
+ @Override
+ public Set writes() {
+ return Set.of();
+ }
+ }
+ )),
+ new ModelThread(1, List.of(new ReadCounterStep(1)))
+ ));
+
+ Invariant invariant = (state, config) -> ((CounterState) state).counter() != 1;
+ Trace failing = Trace.of(
+ List.of(1, 0),
+ List.of(StepOutcome.ADVANCED, StepOutcome.ADVANCED),
+ TraceOutcome.VIOLATION
+ );
+
+ Configuration end = new TraceReplayer().replay(program, failing);
+ assertTrue(end.isDeadlockCandidate(), "Replayed configuration must be a deadlock candidate");
+ assertFalse(invariant.holds(end.state(), end), "Invariant must fail");
+
+ DeltaDebugger debugger = new DeltaDebugger();
+ Trace minimized = debugger.minimize(program, failing, TraceOutcome.VIOLATION, invariant);
+
+ assertEquals(List.of(0), minimized.threadIds(), "Should shrink away T1's irrelevant read");
+ assertEquals(List.of(StepOutcome.ADVANCED), minimized.outcomes());
+ }
}
+
diff --git a/src/test/java/dev/samhb/interleave/search/TraceReplayerTest.java b/src/test/java/dev/samhb/interleave/search/TraceReplayerTest.java
new file mode 100644
index 0000000..f0ef946
--- /dev/null
+++ b/src/test/java/dev/samhb/interleave/search/TraceReplayerTest.java
@@ -0,0 +1,55 @@
+/** Verifies trace replay against actual step execution and detects corrupted outcomes. */
+package dev.samhb.interleave.search;
+
+import dev.samhb.interleave.bugs.ReadCounterStep;
+import dev.samhb.interleave.bugs.WriteCounterStep;
+import dev.samhb.interleave.core.*;
+import org.junit.jupiter.api.Test;
+
+import java.util.List;
+
+import static org.junit.jupiter.api.Assertions.*;
+
+class TraceReplayerTest {
+
+ @Test
+ void replay_matchingTrace_succeeds() {
+ Program program = new Program(CounterState.of(0), List.of(
+ new ModelThread(0, List.of(new WriteCounterStep(0), new ReadCounterStep(0)))
+ ));
+
+ Trace trace = Trace.of(
+ List.of(0, 0),
+ List.of(StepOutcome.ADVANCED, StepOutcome.ADVANCED),
+ TraceOutcome.COMPLETED
+ );
+
+ TraceReplayer replayer = new TraceReplayer();
+ Configuration end = replayer.replay(program, trace);
+
+ assertEquals(1, ((CounterState) end.state()).counter());
+ assertTrue(end.allTerminated());
+ }
+
+ @Test
+ void replay_divergentOutcome_throwsCorruptedTraceException() {
+ Program program = new Program(CounterState.of(0), List.of(
+ new ModelThread(0, List.of(new WriteCounterStep(0)))
+ ));
+
+ // The step produces StepOutcome.ADVANCED, but the trace erroneously claims BLOCKED
+ Trace corruptedTrace = Trace.of(
+ List.of(0),
+ List.of(StepOutcome.BLOCKED),
+ TraceOutcome.VIOLATION
+ );
+
+ TraceReplayer replayer = new TraceReplayer();
+ CorruptedTraceException ex = assertThrows(
+ CorruptedTraceException.class,
+ () -> replayer.replay(program, corruptedTrace)
+ );
+
+ assertTrue(ex.getMessage().contains("recorded BLOCKED but execution produced ADVANCED"));
+ }
+}