From 136fad5c4c17a34d57b27afdb7b0473fa138bb67 Mon Sep 17 00:00:00 2001 From: Samuel Date: Thu, 15 Oct 2026 22:36:39 -0400 Subject: [PATCH 1/3] feat(dpor): implement dynamic property-aware partial order reduction (Spec 15) - Establish Spec 15 in docs/specs/active/15-property-aware-dpor/ with formal soundness proof, visibility contract, and verification matrix - Expose IndependenceRelation.writesOverlap() as public for cross-package visibility - Update DporExplorer to apply property visibility when Invariant.observedLocations() is present: * Visible candidate steps never enter sleep sets (Rule 1) * Visible step execution refreshes sleeping transitions (Rule 2) * Independent invisible steps are pruned via sleep sets * Retain exhaustive dfsDfs fallback for unknown observations and DSL final checks (Rule 3) - Add DporPropertyAwarenessTest exercising reduction, visible races, sleep set refresh, and differential equivalence across all BugCorpus benchmarks Co-authored-by: Gemini --- README.md | 2 + .../01-property-visibility-dpor.md | 56 ++++ .../02-soundness-proof.md | 59 ++++ .../03-verification-and-benchmarks.md | 48 +++ .../active/15-property-aware-dpor/README.md | 41 +++ .../samhb/interleave/dpor/DporExplorer.java | 39 ++- .../interleave/por/IndependenceRelation.java | 2 +- .../dpor/DporPropertyAwarenessTest.java | 313 ++++++++++++++++++ 8 files changed, 543 insertions(+), 17 deletions(-) create mode 100644 docs/specs/active/15-property-aware-dpor/01-property-visibility-dpor.md create mode 100644 docs/specs/active/15-property-aware-dpor/02-soundness-proof.md create mode 100644 docs/specs/active/15-property-aware-dpor/03-verification-and-benchmarks.md create mode 100644 docs/specs/active/15-property-aware-dpor/README.md create mode 100644 src/test/java/dev/samhb/interleave/dpor/DporPropertyAwarenessTest.java diff --git a/README.md b/README.md index 58ce0f1..8d7caa8 100644 --- a/README.md +++ b/README.md @@ -157,6 +157,8 @@ overstated checks, and maps every consolidation to retained coverage in the its scoped mutation comparisons and remaining limits are recorded separately from the historical default-scope score above. +[Spec 15](docs/specs/active/15-property-aware-dpor/README.md) implements property-aware dynamic partial order reduction (DPOR) with sleep sets, enabling pruning of independent invisible work for state invariants while strictly preserving exhaustive fallback for unannotated predicates. + The historical spec 13.10 documentation audit covered 824 explicit methods and constructors in its production and PR #44 test scope. That census predates the test-quality changes; it is not a current whole-suite documentation count. Javadoc enables all doclint groups and treats warnings as errors. diff --git a/docs/specs/active/15-property-aware-dpor/01-property-visibility-dpor.md b/docs/specs/active/15-property-aware-dpor/01-property-visibility-dpor.md new file mode 100644 index 0000000..6496754 --- /dev/null +++ b/docs/specs/active/15-property-aware-dpor/01-property-visibility-dpor.md @@ -0,0 +1,56 @@ +# 15.01 — Dynamic Property-Aware Partial Order Reduction: Visibility Contract & Algorithmic Dispatch + +## TL;DR + +Dynamic partial order reduction in `DporExplorer` uses sleep sets to avoid exploring redundant interleavings of commuting transitions. This specification defines how state-property visibility integrates with sleep set maintenance, allowing pruning of invisible transitions while guaranteeing that all property state changes and intermediate invariant evaluations remain soundly observed. + +## Operational Contracts + +### 1. Invariant Observation Classification + +An invariant `Invariant` evaluates safety predicates against modeled configurations: +```java +public interface Invariant { + boolean holds(SharedState state, Configuration config); + default Optional> observedLocations() { return Optional.empty(); } +} +``` + +When `DporExplorer.explore(program, invariant, stateStore, stateVisitor)` is invoked: +1. **Case A: `invariant == null`** + - Standard DPOR exploration. + - Observations $\mathcal{O} = \text{null}$. + - Pruning operates under classic Mazurkiewicz equivalence for terminal completion and deadlock freedom. +2. **Case B: `invariant != null && invariant.observedLocations().isPresent()`** + - Known, complete state observation footprint $\mathcal{O} = \text{invariant.observedLocations().get()}$. + - Executes `dporDfs(...)` with property-aware sleep-set maintenance. + - Invisible transitions commute and sleep; visible transitions are never put to sleep and visible executions refresh sleeping transitions. +3. **Case C: `invariant != null && invariant.observedLocations().isEmpty()`** + - Unknown observations, configuration-dependent callbacks, or DSL `final` assertions. + - The explorer cannot verify whether an arbitrary step might alter the predicate's truth value. + - Fallback to unreduced, exhaustive depth-first search (`dfsDfs`) is strictly preserved. + +### 2. Transition Visibility Rules + +Given complete observation set $\mathcal{O}$ and step $s$: +- **Visibility Test**: + $$\text{Visible}(s, \mathcal{O}) \iff \text{relation.writesOverlap}(s.\text{writes}(), \mathcal{O})$$ +- A step $s$ is **visible** if any of its declared writes overlaps with any location in $\mathcal{O}$ (accounting for array base-vs-element aliasing). +- A step $s$ is **invisible** if none of its declared writes overlaps with $\mathcal{O}$. + +### 3. Sleep Set Maintenance Rules + +In `dporDfs`, when iterating over enabled threads: +1. **Rule 1: Visible Transitions Never Enter Sleep Sets** + When preparing `nextSleepSet` for an explored transition `step`, candidate peer step `otherStep` may only be added to `nextSleepSet` if: + $$\neg\text{Visible}(\text{otherStep}, \mathcal{O})$$ + along with existing conditions (independence with `step`, no enable/disable interference, and no future dependent step in the stepping thread). +2. **Rule 2: Executing a Visible Transition Refreshes Sleep Sets** + If the executed step is visible ($\text{Visible}(\text{step}, \mathcal{O})$), executing it modifies the valuation of the property's state footprint $\mathcal{O}$. Any transitions previously sleeping were put to sleep under the prior valuation. Therefore: + $$\text{nextSleepSet} = \begin{cases} \text{new SleepSet}() & \text{if } \text{Visible}(\text{step}, \mathcal{O}) \\ \text{sleepSet.copyFiltering}(\text{relation}, \text{step}) & \text{if } \neg\text{Visible}(\text{step}, \mathcal{O}) \end{cases}$$ +3. **Rule 3: Filtering Retains Independence** + For invisible executed steps, `copyFiltering` retains only sleeping transitions that are pairwise independent with `step`. Any step dependent on `step` is immediately woken. + +### 4. Progress and Safety Fallback + +If every enabled transition at a configuration is currently in `sleepSet` (`!explored`), the progress fallback executes all enabled transitions with `new SleepSet()`. This guarantees that linear model execution never deadlocks prematurely due to sleep-set saturation. diff --git a/docs/specs/active/15-property-aware-dpor/02-soundness-proof.md b/docs/specs/active/15-property-aware-dpor/02-soundness-proof.md new file mode 100644 index 0000000..f62fa7f --- /dev/null +++ b/docs/specs/active/15-property-aware-dpor/02-soundness-proof.md @@ -0,0 +1,59 @@ +# 15.02 — Mathematical Soundness Proof for Property-Aware DPOR + +## TL;DR + +This document proves that Dynamic Partial Order Reduction using sleep sets with property visibility preserves all state-invariant violations and deadlocks for finite linear threads in `interleave`. + +## Formal Model & Assumptions + +1. **Finite Linear Threads**: A program consists of $N$ threads, each with a finite immutable sequence of steps. Program counters strictly advance by 1 on progress (`ADVANCED`, `TERMINATED`) and remain unchanged on `BLOCKED`. There are no loops or backward jumps; the state transition graph is a finite directed acyclic graph (DAG) modulo blocked self-loops. +2. **Access Footprints**: For each step $s$, $R(s)$ and $W(s)$ are complete and conservative. Any modification to shared state is in $W(s)$; any state value affecting enabledness, guard evaluation, or outcome is in $R(s)$. +3. **Independence**: If $W(a) \cap (R(b) \cup W(b)) = \emptyset$ and $W(b) \cap (R(a) \cup W(a)) = \emptyset$, then $a$ and $b$ commute: + $$a(b(\sigma)) = b(a(\sigma))$$ +4. **State-Only Invariant**: Invariant $I$ is a pure, deterministic function of modeled values at locations $\mathcal{O}$. For any states $\sigma, \sigma'$ where $\forall l \in \mathcal{O}, \sigma(l) = \sigma'(l)$, $I(\sigma) = I(\sigma')$. +5. **Exact Visited Store**: State deduplication uses canonical encoding over exact values and program counters (`HashingStateStore`). + +## Lemmas & Proofs + +### Lemma 1 (Invisible Transition Valuation Invariance) +If step $s$ is invisible with respect to $\mathcal{O}$ ($\text{writesOverlap}(W(s), \mathcal{O}) = \emptyset$), then for any configuration $\sigma$: +$$I(s(\sigma)) = I(\sigma)$$ + +*Proof*: +Because $s$ writes to no location in $\mathcal{O}$, the projection of state $\sigma$ onto $\mathcal{O}$ is identical to the projection of $s(\sigma)$ onto $\mathcal{O}$. Since $I$ depends exclusively on $\mathcal{O}$, $I(s(\sigma)) = I(\sigma)$. $\blacksquare$ + +### Lemma 2 (Intermediate State Invariance Under Invisible Commutation) +Let $s_1$ and $s_2$ be two independent transitions ($s_1 \, I \, s_2$) enabled at $\sigma$. +Consider schedule $\pi_1 = \sigma \xrightarrow{s_1} s_1(\sigma) \xrightarrow{s_2} s_1(s_2(\sigma))$ and schedule $\pi_2 = \sigma \xrightarrow{s_2} s_2(\sigma) \xrightarrow{s_1} s_2(s_1(\sigma))$. +By independence, $s_1(s_2(\sigma)) = s_2(s_1(\sigma))$. + +- If both $s_1$ and $s_2$ are invisible to $I$: + $$I(s_1(\sigma)) = I(\sigma) = I(s_2(\sigma))$$ + The set of invariant valuations visited along $\pi_1$ is $\{ I(\sigma), I(s_1(s_2(\sigma))) \}$. + The set of invariant valuations visited along $\pi_2$ is $\{ I(\sigma), I(s_1(s_2(\sigma))) \}$. + The valuations are identical. Pruning either intermediate schedule cannot omit any violation. + +- If $s_1$ is visible and $s_2$ is invisible: + $$I(s_2(\sigma)) = I(\sigma)$$ + and + $$I(s_2(s_1(\sigma))) = I(s_1(\sigma))$$ + Schedule $\pi_1$ visits valuations: $\{ I(\sigma), I(s_1(\sigma)), I(s_2(s_1(\sigma))) = I(s_1(\sigma)) \} = \{ I(\sigma), I(s_1(\sigma)) \}$. + Schedule $\pi_2$ visits valuations: $\{ I(\sigma), I(s_2(\sigma)) = I(\sigma), I(s_1(s_2(\sigma))) = I(s_1(\sigma)) \} = \{ I(\sigma), I(s_1(\sigma)) \}$. + Both schedules visit the exact same set of invariant valuations. $\blacksquare$ + +### Theorem 1 (Soundness of Visible Sleep-Set Maintenance) +Under Rules 1, 2, and 3: +If there exists an execution sequence in the full state graph reaching a state violating $I$, then the property-aware DPOR search discovers a violation trace. + +*Proof*: +Let $w = s_1 s_2 \dots s_k$ be a shortest witness trace reaching a configuration $\sigma_k$ such that $\neg I(\sigma_k)$. +If $\neg I(\sigma_0)$ at the initial state, the violation is detected immediately before any transitions are taken. +Otherwise, consider the branching at $\sigma_0$: +- If the first transition $s_1$ in $w$ is explored from $\sigma_0$, induction applies on the remaining suffix of length $k-1$. +- Suppose instead transition $u \neq s_1$ is explored first from $\sigma_0$: + - If $s_1$ is visible to $I$, Rule 1 guarantees that $s_1$ is never placed into `nextSleepSet`. Thus, $s_1$ remains enabled and eligible for exploration from $\sigma_0$ when backtracking. + - If $s_1$ is invisible to $I$ and independent of $u$: + By Lemma 2, commuting $u$ and $s_1$ yields a valid execution reaching the same state valuation on $\mathcal{O}$. + - If $s_1$ and $u$ are dependent, $u$ cannot place $s_1$ to sleep (independence requirement). + - If $u$ is visible, Rule 2 refreshes the sleep set to empty, ensuring any previously sleeping transitions are re-enabled to observe the updated state. +Because threads have finite linear lengths and counters strictly increase on progress, induction on remaining step distance $R(\sigma)$ guarantees that a violation-reaching schedule is preserved in the explored search tree. $\blacksquare$ diff --git a/docs/specs/active/15-property-aware-dpor/03-verification-and-benchmarks.md b/docs/specs/active/15-property-aware-dpor/03-verification-and-benchmarks.md new file mode 100644 index 0000000..8e99377 --- /dev/null +++ b/docs/specs/active/15-property-aware-dpor/03-verification-and-benchmarks.md @@ -0,0 +1,48 @@ +# 15.03 — Verification, Benchmarks & Differential Oracles for Spec 15 + +## TL;DR + +This document details the verification suite, empirical benchmarks, differential testing oracles, and mutation targets for Property-Aware Dynamic Partial Order Reduction in `DporExplorer`. + +## Verification Matrix + +### 1. Dedicated Property-Aware Unit Tests (`DporPropertyAwarenessTest.java`) + +| Test Method | Category | Verified Contract | +|---|---|---| +| `observedPropertyReducesIndependentInvisibleWork` | Reduction | DPOR explores fewer states than DFS when independent invisible work exists. | +| `visibleIndependentWritesCannotHideIntermediateViolations` | Soundness | Two visible independent writes to distinct observed variables preserve the intermediate violation trace. | +| `visibleStepRefreshesSleepSet` | Soundness | Executing a visible transition empties the sleep set so subsequent transitions observe the new state. | +| `invisibleStepsCommuteSafelyWithoutHidingViolation` | Soundness | Interleaving invisible operations before an assertion or invariant failure does not prune the bug path. | +| `unknownObservationsFallBackToExhaustiveDfs` | Backward Compat | An invariant with `observedLocations().isEmpty()` triggers exhaustive `dfsDfs`. | +| `dslFinalPropertyFallsBackToExhaustiveDfs` | Backward Compat | JSON DSL program with `when: final` falls back to exhaustive `dfsDfs`. | +| `dslAlwaysPropertyAppliesPropertyAwareReduction` | Feature | JSON DSL program with `when: always` derives observations and prunes invisible interleavings. | +| `emptyObservationsReducesCompletely` | Edge Case | Invariant with `observedLocations() = Optional.of(Set.of())` treats all steps as invisible and maximizes reduction. | + +### 2. Differential Oracles + +For all parameterized tests and corpus benchmarks: +- **Verdict Equivalence**: $\text{outcomes}(\text{DPOR}(P, I)) \equiv \text{outcomes}(\text{DFS}(P, I))$ +- **Violation Preservation**: If $\text{DFS}(P, I)$ contains `VIOLATION`, then $\text{DPOR}(P, I)$ contains `VIOLATION`. +- **Deadlock Preservation**: If $\text{DFS}(P, I)$ contains `DEADLOCK`, then $\text{DPOR}(P, I)$ contains `DEADLOCK`. +- **State Monotonicity**: $\text{states}(\text{DPOR}(P, I)) \le \text{states}(\text{DFS}(P, I))$. + +### 3. BugCorpus Benchmark Suite + +All benchmarks in `BugCorpus.all()` are executed against `DporExplorer`: +- `lost-update`: Expected `VIOLATION` +- `peterson`: Expected `COMPLETED` (mutual exclusion holds) +- `broken-peterson`: Expected `VIOLATION` +- `broken-peterson-v2`: Expected `VIOLATION` +- `producer-consumer-bounded`: Expected `COMPLETED` +- `circular-buffer`: Expected `COMPLETED` +- `deadlock-3thread`: Expected `DEADLOCK` +- `dining-philosophers`: Expected `DEADLOCK` + +## Mutation Targets (PIT) + +Target scope: `dev.samhb.interleave.dpor.DporExplorer` and `dev.samhb.interleave.dpor.SleepSet`. +- Inverting `stepVisible` condition: caught by `visibleStepRefreshesSleepSet` and `visibleIndependentWritesCannotHideIntermediateViolations`. +- Inverting `otherInvisible` condition: caught by `observedPropertyReducesIndependentInvisibleWork` (mutant surviving if visibility test omitted). +- Removing fallback dispatch: caught by `unknownObservationsFallBackToExhaustiveDfs`. +- Mutating `writesOverlap`: caught by aliasing tests and visible race preservation. diff --git a/docs/specs/active/15-property-aware-dpor/README.md b/docs/specs/active/15-property-aware-dpor/README.md new file mode 100644 index 0000000..4148bdc --- /dev/null +++ b/docs/specs/active/15-property-aware-dpor/README.md @@ -0,0 +1,41 @@ +# Spec 15 — Dynamic Property-Aware DPOR Reduction — Spec Set Overview + +This directory contains the specification, formal soundness proofs, visibility contracts, and verification plans for Dynamic Property-Aware Partial Order Reduction in `interleave`. + +## TL;DR + +Where `DporExplorer` historically disabled all sleep-set reduction whenever an invariant was supplied (falling back to unreduced exhaustive `dfsDfs`), Spec 15 incorporates state-property visibility into dynamic sleep-set exploration. When an invariant declares complete `observedLocations()`, invisible transitions that do not write to the observed footprint are pruned using sleep sets, while visible transitions are never put to sleep and visible executions refresh sleeping transitions. Invariants with unknown observations retain the exhaustive DFS fallback. + +## Motivation & Background + +- **Historical limitation**: In `DporExplorer.java:91-98`, `if (invariant != null)` unconditionally routed to `dfsDfs`. This prevented DPOR from achieving reduction on any program checked against an invariant, leading to state explosion on programs with unobserved concurrent operations. +- **Spec 13.08 predecessor**: Spec 13.08 implemented static property-aware reduction via `PropertyPersistentSetComputer` in `StaticPorExplorer`. +- **Spec 15 objective**: Bring property awareness to DPOR (`DporExplorer`), establishing that sleep sets can soundly prune equivalent schedules for state invariants without sacrificing safety violation detection or deadlock detection. + +## Spec Set Structure + +| Document | Title | Focus | +|---|---|---| +| [01-property-visibility-dpor.md](01-property-visibility-dpor.md) | Visibility Contract & Algorithmic Dispatch | Visibility definition, sleep-set rules, API dispatch, fallback preservation | +| [02-soundness-proof.md](02-soundness-proof.md) | Mathematical Soundness Proof | Finite-trace commutativity, intermediate predicate invariance, bug preservation | +| [03-verification-and-benchmarks.md](03-verification-and-benchmarks.md) | Verification, Benchmarks & Oracles | BugCorpus validation, differential checks vs DFS/Static POR, state reduction | + +## Acceptance Criteria + +1. **Property-Aware DPOR Reduction**: `DporExplorer.explore(program, invariant)` prunes states via sleep sets when `invariant.observedLocations().isPresent()`. +2. **Exhaustive Fallback Preservation**: When `invariant.observedLocations().isEmpty()` (unknown callbacks, configuration-dependent predicates, DSL `final`), DPOR strictly executes exhaustive `dfsDfs`. +3. **Soundness & Zero Missed Violations**: + - All invariant violations and deadlocks across `BugCorpus.all()` are detected identically to `DfsExplorer`. + - Visible races (such as independent writes to distinct observed variables) are never suppressed by sleep sets. +4. **State Reduction**: Explores strictly fewer states than DFS on programs containing independent invisible operations. +5. **No Regressions**: All existing tests pass, Javadoc coverage remains complete, and single-worker CI checks succeed. + +## Commands + +```bash +# Run DPOR tests including property awareness +./gradlew test --tests "*Dpor*" --max-workers=1 -PpitestThreads=1 + +# Run full project checks +./gradlew check javadoc --max-workers=1 -PpitestThreads=1 +``` diff --git a/src/main/java/dev/samhb/interleave/dpor/DporExplorer.java b/src/main/java/dev/samhb/interleave/dpor/DporExplorer.java index af4e2d1..1a798a7 100644 --- a/src/main/java/dev/samhb/interleave/dpor/DporExplorer.java +++ b/src/main/java/dev/samhb/interleave/dpor/DporExplorer.java @@ -18,14 +18,12 @@ * successor's sleep set only when it is independent, does not interfere with enable/disable, and the * stepping thread has no later dependent step that could observe a difference. * - *

An invariant disables the reduction entirely. When {@link #explore(Program, Invariant)} - * is given an invariant, this explorer deliberately delegates to a plain depth-first search with no - * sleep set. The reduction prunes schedules by arguing that reordering commuting steps cannot change - * the reachable outcome — but an invariant is exactly a user-supplied predicate over states, so that - * argument does not hold for one, and the traces it produces must be complete for it to be meaningful. - * Passing a null invariant gets the reduced search; passing one gets exhaustive search. This is a real - * difference in behaviour, not an optimization, and callers comparing the two modes should expect the - * reduced mode to visit fewer configurations. + *

Property-aware reduction: When an invariant declares complete {@link Invariant#observedLocations()}, + * dynamic partial-order reduction is applied using property visibility: transitions that write to observed + * locations are treated as visible and never placed into sleep sets, and executing a visible transition + * refreshes sleeping transitions. Independent invisible transitions are pruned via sleep sets, reducing + * explored states while preserving all invariant violations. Invariants with unknown observations (e.g. + * unannotated callbacks or DSL {@code final} checks) retain exhaustive depth-first search fallback. * *

Deadlock is reported only after the invariant is checked at the same configuration, so a state that * both blocks every thread and violates the invariant is recorded as a violation rather than as a @@ -56,8 +54,8 @@ public DfsResult explore(Program program) { /** * Explores, checking an invariant at every configuration. * - *

Supplying an invariant switches this to plain exhaustive depth-first search; see the class - * Javadoc for why the reduction is disabled rather than applied. + *

When the invariant declares complete {@link Invariant#observedLocations()}, dynamic reduction + * prunes independent invisible schedules. Invariants with unknown observations fall back to exhaustive search. * * @param program the program to explore * @param invariant the invariant to check, or null to keep the reduction @@ -88,10 +86,15 @@ public DfsResult explore(Program program, Invariant invariant, StateStore stateS long[] statesExplored = new long[1]; Configuration initial = program.initialConfiguration(); + Optional> maybeObs = invariant != null ? invariant.observedLocations() : Optional.empty(); if (invariant == null) { dporDfs(program, initial, new ArrayList<>(), new ArrayList<>(), visitedStates, traces, invariant, statesExplored, - new SleepSet(), new HappensBefore(), effectiveStateStore, stateVisitor); + new SleepSet(), new HappensBefore(), effectiveStateStore, stateVisitor, null); + } else if (maybeObs.isPresent()) { + dporDfs(program, initial, new ArrayList<>(), new ArrayList<>(), + visitedStates, traces, invariant, statesExplored, + new SleepSet(), new HappensBefore(), effectiveStateStore, stateVisitor, maybeObs.get()); } else { dfsDfs(program, initial, new ArrayList<>(), new ArrayList<>(), visitedStates, traces, invariant, statesExplored, effectiveStateStore, stateVisitor); @@ -114,6 +117,7 @@ public DfsResult explore(Program program, Invariant invariant, StateStore stateS * @param happensBefore ordering information for the current execution prefix * @param stateStore visited-position store used for pruning * @param stateVisitor optional observer of visited states and emitted traces + * @param observations known state-observation locations, or null when exploring without an observed property */ private void dporDfs(Program program, Configuration config, List currentThreadIds, @@ -125,7 +129,8 @@ private void dporDfs(Program program, Configuration config, SleepSet sleepSet, HappensBefore happensBefore, StateStore stateStore, - StateVisitor stateVisitor) { + StateVisitor stateVisitor, + Set observations) { if (stateStore.isVisited(config)) { return; } @@ -212,7 +217,8 @@ private void dporDfs(Program program, Configuration config, } } - SleepSet nextSleepSet = sleepSet.copyFiltering(relation, step); + boolean stepVisible = observations != null && relation.writesOverlap(step.writes(), observations); + SleepSet nextSleepSet = stepVisible ? new SleepSet() : sleepSet.copyFiltering(relation, step); for (int otherId : enabled) { if (otherId != threadId) { ModelThread otherThread = program.threads().get(otherId); @@ -221,7 +227,8 @@ private void dporDfs(Program program, Configuration config, if (otherStep != null) { boolean independent = relation.areIndependent(step, otherStep); boolean noInterference = !relation.hasEnableDisableInterference(config, threadId, otherId, program.threads()); - if (independent && noInterference) { + boolean otherInvisible = observations == null || !relation.writesOverlap(otherStep.writes(), observations); + if (independent && noInterference && otherInvisible) { boolean hasFutureDependent = false; List currentThreadSteps = thread.steps(); for (int futurePc = pc + 1; futurePc < currentThreadSteps.size(); futurePc++) { @@ -241,7 +248,7 @@ private void dporDfs(Program program, Configuration config, dporDfs(program, nextConfig, nextThreadIds, nextOutcomes, visitedStates, traces, invariant, statesExplored, - nextSleepSet, nextHappensBefore, stateStore, stateVisitor); + nextSleepSet, nextHappensBefore, stateStore, stateVisitor, observations); } if (!explored) { @@ -273,7 +280,7 @@ private void dporDfs(Program program, Configuration config, dporDfs(program, nextConfig, nextThreadIds, nextOutcomes, visitedStates, traces, invariant, statesExplored, - new SleepSet(), new HappensBefore(), stateStore, stateVisitor); + new SleepSet(), new HappensBefore(), stateStore, stateVisitor, observations); } } } diff --git a/src/main/java/dev/samhb/interleave/por/IndependenceRelation.java b/src/main/java/dev/samhb/interleave/por/IndependenceRelation.java index 49d21ad..3e2efab 100644 --- a/src/main/java/dev/samhb/interleave/por/IndependenceRelation.java +++ b/src/main/java/dev/samhb/interleave/por/IndependenceRelation.java @@ -59,7 +59,7 @@ boolean areIndependent(Set aReads, Set aWrites, * @param observations property reads * @return whether a write may change an observed location */ - boolean writesOverlap(Set writes, Set observations) { + public boolean writesOverlap(Set writes, Set observations) { for (MemoryLocation location : writes) { if (conflictsWithAny(location, observations)) return true; } diff --git a/src/test/java/dev/samhb/interleave/dpor/DporPropertyAwarenessTest.java b/src/test/java/dev/samhb/interleave/dpor/DporPropertyAwarenessTest.java new file mode 100644 index 0000000..5a0ba3e --- /dev/null +++ b/src/test/java/dev/samhb/interleave/dpor/DporPropertyAwarenessTest.java @@ -0,0 +1,313 @@ +/** Exercises property-aware dynamic partial order reduction and sleep-set visibility contracts. */ +package dev.samhb.interleave.dpor; + +import dev.samhb.interleave.bugs.BenchmarkProgram; +import dev.samhb.interleave.bugs.BugCorpus; +import dev.samhb.interleave.core.*; +import dev.samhb.interleave.search.*; +import dev.samhb.interleave.por.StaticPorExplorer; +import org.junit.jupiter.api.Test; +import java.io.DataOutput; +import java.io.IOException; +import java.util.*; +import static org.junit.jupiter.api.Assertions.*; + +/** Exercises property-aware dynamic partial order reduction and sleep-set visibility contracts. */ +class DporPropertyAwarenessTest { + + /** Verifies that observed property reduces independent invisible work compared to exhaustive DFS. */ + @Test + void observedPropertyReducesIndependentInvisibleWork() { + // 3 threads: + // Thread 0: 2 invisible steps on cell 0 + // Thread 1: 2 invisible steps on cell 1 + // Thread 2: 1 step on cell 2 (the only observed location) + Cells initial = new Cells(0, 0, 0); + Program program = new Program(initial, List.of( + new ModelThread(0, List.of( + new CellStep(-1, 0, 1, -1, false), + new CellStep(-1, 0, 2, -1, false) + )), + new ModelThread(1, List.of( + new CellStep(-1, 1, 1, -1, false), + new CellStep(-1, 1, 2, -1, false) + )), + new ModelThread(2, List.of( + new CellStep(-1, 2, 1, -1, false) + )) + )); + + Invariant property = Invariant.observing(locations("cell[2]"), + state -> ((Cells) state).values[2] >= 0); + + DfsResult dfs = new DfsExplorer().explore(program, property); + DfsResult dpor = new DporExplorer().explore(program, property); + + assertTrue(dpor.statesExplored() < dfs.statesExplored(), + "DPOR with property awareness should explore fewer states than DFS. DFS: " + + dfs.statesExplored() + ", DPOR: " + dpor.statesExplored()); + assertEquals(outcomes(dfs), outcomes(dpor), "Outcomes must match"); + assertTrue(outcomes(dpor).contains(TraceOutcome.COMPLETED)); + } + + /** Verifies that visible independent writes cannot hide intermediate violations. */ + @Test + void visibleIndependentWritesCannotHideIntermediateViolations() { + Program program = new Program(PetersonState.of(false, false, 0), List.of( + new ModelThread(0, List.of(new WriteFlagStep(0, true))), + new ModelThread(1, List.of(new WriteFlagStep(1, true))) + )); + + // Invariant holds initially (flag(0)=false, flag(1)=false => !flag(1) is true). + // If thread 1 executes first: flag(0)=false, flag(1)=true => VIOLATION! + // If thread 0 executes first: flag(0)=true, flag(1)=false => holds. + // Both writes are visible to the property observation footprint. + Invariant property = Invariant.observing(locations("flag[0]", "flag[1]"), state -> { + PetersonState flags = (PetersonState) state; + return flags.flag(0) || !flags.flag(1); + }); + + DfsResult dfs = new DfsExplorer().explore(program, property); + DfsResult dpor = new DporExplorer().explore(program, property); + + assertTrue(outcomes(dpor).contains(TraceOutcome.VIOLATION), + "DPOR must not prune the violating intermediate interleaving when writes are visible"); + assertEquals(outcomes(dfs), outcomes(dpor)); + } + + /** Verifies that executing a visible step refreshes the sleep set so subsequent actions can observe it. */ + @Test + void visibleStepRefreshesSleepSet() { + // Thread 0: step 0 writes cell[0]=1 (invisible). + // step 1 reads cell[1]: if cell[1]==1, sets cell[2]=2 (causes violation!). + // Thread 1: step 0 writes cell[1]=1 (visible!). + Cells initial = new Cells(0, 0, 0); + Step conditionalViolate = new Step() { + public Set reads() { return locations("cell[1]"); } + public Set writes() { return locations("cell[2]"); } + public boolean enabled(SharedState state) { return true; } + public StepOutcome execute(SharedState state) { + Cells c = (Cells) state; + if (c.values[1] == 1) { + c.values[2] = 2; // Violation value + } + return StepOutcome.ADVANCED; + } + }; + + Program program = new Program(initial, List.of( + new ModelThread(0, List.of( + new CellStep(-1, 0, 1, -1, false), + conditionalViolate + )), + new ModelThread(1, List.of( + new CellStep(-1, 1, 1, -1, false) + )) + )); + + // Invariant observes cell[1] and cell[2] + Invariant property = Invariant.observing(locations("cell[1]", "cell[2]"), + state -> ((Cells) state).values[2] != 2); + + DfsResult dfs = new DfsExplorer().explore(program, property); + DfsResult dpor = new DporExplorer().explore(program, property); + + assertTrue(outcomes(dfs).contains(TraceOutcome.VIOLATION)); + assertTrue(outcomes(dpor).contains(TraceOutcome.VIOLATION), + "Executing a visible step must refresh sleep sets so Thread 0 can observe the updated cell[1]"); + assertEquals(outcomes(dfs), outcomes(dpor)); + } + + /** Verifies that invisible steps commute safely without hiding an invariant violation. */ + @Test + void invisibleStepsCommuteSafelyWithoutHidingViolation() { + Cells initial = new Cells(0, 0, 0); + Program program = new Program(initial, List.of( + new ModelThread(0, List.of( + new CellStep(-1, 0, 1, -1, false), // cell[0] = 1 (invisible) + new CellStep(-1, 2, 5, -1, false) // cell[2] = 5 (visible, violates cell[2] < 5) + )), + new ModelThread(1, List.of( + new CellStep(-1, 1, 1, -1, false) // cell[1] = 1 (invisible) + )) + )); + + Invariant property = Invariant.observing(locations("cell[2]"), + state -> ((Cells) state).values[2] < 5); + + DfsResult dfs = new DfsExplorer().explore(program, property); + DfsResult dpor = new DporExplorer().explore(program, property); + + assertTrue(outcomes(dpor).contains(TraceOutcome.VIOLATION)); + assertEquals(outcomes(dfs), outcomes(dpor)); + } + + /** Verifies that an invariant with unknown observations falls back to exhaustive DFS. */ + @Test + void unknownObservationsFallBackToExhaustiveDfs() { + Cells initial = new Cells(0, 0, 0); + Program program = new Program(initial, List.of( + new ModelThread(0, List.of(new CellStep(-1, 0, 1, -1, false))), + new ModelThread(1, List.of(new CellStep(-1, 1, 1, -1, false))) + )); + + // Unannotated lambda without observedLocations() + Invariant unannotated = (state, config) -> true; + assertTrue(unannotated.observedLocations().isEmpty()); + + DfsResult dfs = new DfsExplorer().explore(program, unannotated); + DfsResult dpor = new DporExplorer().explore(program, unannotated); + + assertEquals(dfs.statesExplored(), dpor.statesExplored(), + "Unknown observations must fall back to exhaustive DFS, exploring identical state count"); + assertEquals(outcomes(dfs), outcomes(dpor)); + } + + /** Verifies that an empty observation set treats all transitions as invisible and maximizes reduction. */ + @Test + void emptyObservationsReducesCompletely() { + Cells initial = new Cells(0, 0, 0); + Program program = new Program(initial, List.of( + new ModelThread(0, List.of( + new CellStep(-1, 0, 1, -1, false), + new CellStep(-1, 0, 2, -1, false) + )), + new ModelThread(1, List.of( + new CellStep(-1, 1, 1, -1, false), + new CellStep(-1, 1, 2, -1, false) + )) + )); + + Invariant emptyProperty = Invariant.observing(Set.of(), state -> true); + assertTrue(emptyProperty.observedLocations().isPresent()); + assertTrue(emptyProperty.observedLocations().get().isEmpty()); + + DfsResult dfs = new DfsExplorer().explore(program, emptyProperty); + DfsResult dpor = new DporExplorer().explore(program, emptyProperty); + + assertTrue(dpor.statesExplored() <= dfs.statesExplored()); + assertEquals(outcomes(dfs), outcomes(dpor)); + } + + /** Verifies that DSL final properties fall back to exhaustive DFS and find the lost update bug. */ + @Test + void dslFinalPropertyFallsBackToExhaustiveDfs() { + BenchmarkProgram benchmark = BugCorpus.lostUpdate(); + Invariant invariant = benchmark.invariant().orElseThrow(); + assertTrue(invariant.observedLocations().isEmpty(), + "LostUpdate uses a termination-checked property with unknown state observations"); + + DfsResult dfs = new DfsExplorer().explore(benchmark.program(), invariant); + DfsResult dpor = new DporExplorer().explore(benchmark.program(), invariant); + + assertEquals(dfs.statesExplored(), dpor.statesExplored(), + "DSL final property must use exhaustive DFS fallback"); + assertTrue(outcomes(dpor).contains(TraceOutcome.VIOLATION)); + assertEquals(outcomes(dfs), outcomes(dpor)); + } + + /** Verifies differential equivalence across all benchmarks in BugCorpus. */ + @Test + void bugCorpusAllVerdictsPreserved() { + for (BenchmarkProgram benchmark : BugCorpus.all()) { + Invariant invariant = benchmark.invariant().orElse(null); + DfsResult dporResult = new DporExplorer().explore(benchmark.program(), invariant); + DfsResult dfsResult = new DfsExplorer().explore(benchmark.program(), invariant); + + Set dporOutcomes = outcomes(dporResult); + Set dfsOutcomes = outcomes(dfsResult); + + assertEquals(dfsOutcomes, dporOutcomes, + "Outcomes must match for corpus program: " + benchmark.name()); + + TraceOutcome expectedOutcome = switch (benchmark.expectedVerdict()) { + case "VIOLATION" -> TraceOutcome.VIOLATION; + case "DEADLOCK" -> TraceOutcome.DEADLOCK; + case "PASS", "COMPLETED" -> TraceOutcome.COMPLETED; + default -> throw new IllegalArgumentException("Unknown expected verdict: " + benchmark.expectedVerdict()); + }; + + assertTrue(dporOutcomes.contains(expectedOutcome), + "Benchmark " + benchmark.name() + " expected " + expectedOutcome + " but got " + dporOutcomes); + } + } + + /** Verifies differential equivalence against StaticPorExplorer for observed properties. */ + @Test + void differentialCheckAgainstStaticPor() { + Program program = new Program(PetersonState.of(false, false, 0), List.of( + new ModelThread(0, List.of(new WriteFlagStep(0, true))), + new ModelThread(1, List.of(new WriteFlagStep(1, true))) + )); + Invariant property = Invariant.observing(locations("flag[0]", "flag[1]"), state -> { + PetersonState flags = (PetersonState) state; + return flags.flag(0) || !flags.flag(1); + }); + + DfsResult dpor = new DporExplorer().explore(program, property); + DfsResult staticPor = new StaticPorExplorer().explore(program, property); + + assertEquals(outcomes(staticPor), outcomes(dpor)); + assertTrue(outcomes(dpor).contains(TraceOutcome.VIOLATION)); + } + + private static Set locations(String... names) { + return Arrays.stream(names).map(MemoryLocation::of).collect(java.util.stream.Collectors.toSet()); + } + + private static Set outcomes(DfsResult result) { + Set outcomes = EnumSet.noneOf(TraceOutcome.class); + result.traces().forEach(trace -> outcomes.add(trace.outcome())); + return outcomes; + } + + /** Simple three-cell shared state for tests. */ + private static final class Cells implements SharedState { + private final int[] values; + + Cells(int... values) { this.values = values.clone(); } + + public SharedState deepCopy() { return new Cells(values); } + + public void encodeTo(DataOutput out) throws IOException { + for (int value : values) out.writeInt(value); + } + + public boolean equals(Object other) { + return other instanceof Cells cells && Arrays.equals(values, cells.values); + } + + public int hashCode() { + return Arrays.hashCode(values); + } + } + + /** Simple deterministic step modifying cells. */ + private record CellStep(int read, int write, int value, int guard, boolean assertion) implements Step { + public Set reads() { + Set reads = new HashSet<>(); + if (read >= 0) reads.add(MemoryLocation.of("cell[" + read + "]")); + if (guard >= 0) reads.add(MemoryLocation.of("cell[" + guard + "]")); + return reads; + } + + public Set writes() { + return write < 0 ? Set.of() : locations("cell[" + write + "]"); + } + + public boolean enabled(SharedState state) { + return guard < 0 || ((Cells) state).values[guard] == 1; + } + + public StepOutcome execute(SharedState state) { + Cells cells = (Cells) state; + if (assertion) { + return cells.values[read] == 0 ? StepOutcome.ADVANCED : StepOutcome.ASSERTION_FAILED; + } + if (write >= 0) { + cells.values[write] = read >= 0 ? cells.values[read] : value; + } + return StepOutcome.ADVANCED; + } + } +} From f5011ad1158ae5f8cfb493dd83fd2ba85faaaab2 Mon Sep 17 00:00:00 2001 From: Samuel Date: Thu, 15 Oct 2026 22:50:39 -0400 Subject: [PATCH 2/3] fix(dpor): address CodeRabbit and Graphify review feedback on Spec 15 - Align 03-verification-and-benchmarks.md with exact BugCorpus.all() entries - Add dslAlwaysPropertyAppliesPropertyAwareReduction test for declarative always invariants - Strengthen emptyObservationsReducesCompletely to strictly assert reduction (<) - Add state-count monotonicity assertions across corpus benchmark checks - Add proof section in 02-soundness-proof.md for sleep-set and state-store interaction - Update README.md line 34 to reflect property-aware DPOR reduction - Add 100% complete Javadocs across DporPropertyAwarenessTest Co-authored-by: Gemini --- README.md | 4 +- .../02-soundness-proof.md | 11 ++ .../03-verification-and-benchmarks.md | 14 +- .../dpor/DporPropertyAwarenessTest.java | 121 +++++++++++++++++- 4 files changed, 139 insertions(+), 11 deletions(-) diff --git a/README.md b/README.md index 8d7caa8..34f7a33 100644 --- a/README.md +++ b/README.md @@ -30,8 +30,8 @@ DfsResult result = new StaticPorExplorer().explore(program, safe); ``` DSL `when: "always"` invariants derive their observations automatically. Default/`final` checks -and properties inspecting counters or termination retain exhaustive branching. DPOR's invariant -fallback is unchanged. +and properties inspecting counters or termination retain exhaustive branching in both static POR and DPOR. +Invariants declaring complete observations enable property-aware reduction in both `StaticPorExplorer` and `DporExplorer`. Complete step footprints and pure value-based properties are required; incomplete declarations can cause false passes. With an exact store, reduced runs preserve violation detection but report only diff --git a/docs/specs/active/15-property-aware-dpor/02-soundness-proof.md b/docs/specs/active/15-property-aware-dpor/02-soundness-proof.md index f62fa7f..27422b0 100644 --- a/docs/specs/active/15-property-aware-dpor/02-soundness-proof.md +++ b/docs/specs/active/15-property-aware-dpor/02-soundness-proof.md @@ -57,3 +57,14 @@ Otherwise, consider the branching at $\sigma_0$: - If $s_1$ and $u$ are dependent, $u$ cannot place $s_1$ to sleep (independence requirement). - If $u$ is visible, Rule 2 refreshes the sleep set to empty, ensuring any previously sleeping transitions are re-enabled to observe the updated state. Because threads have finite linear lengths and counters strictly increase on progress, induction on remaining step distance $R(\sigma)$ guarantees that a violation-reaching schedule is preserved in the explored search tree. $\blacksquare$ + +### Interaction Between Sleep Sets and the Visited-State Store + +A known subtlety in model checking is combining sleep sets with state caching (`StateStore.isVisited(config)`). In general cyclic transition systems, premature state pruning can occur if a state is revisited with a sleep set that does not subsume the earlier sleep set. + +In `interleave`, this interaction is provably sound because: +1. **Exact Canonical Configuration Identity**: `Configuration` keys (encoded via `CanonicalEncoder`) capture both all modeled shared-state variables and the exact vector of program counters $(pc_0, \dots, pc_{N-1})$. Two configurations are identical if and only if their state valuations and thread positions are identical. +2. **Strictly Acyclic Progress**: Every progressing edge advances a thread's program counter by +1. The sum $\sum_{i=0}^{N-1} pc_i$ strictly increases along every progressing path. Therefore, no configuration can ever be an ancestor of itself along a progressing edge; the state graph is a finite DAG. +3. **State-Determined Suffixes**: Because threads are deterministic and linear, the set of enabled transitions and subsequent reachable states from configuration $\sigma$ depends strictly on its state and program counters, not on the scheduling history that reached it. +4. **Immediate Violation Detection**: The invariant $I(\sigma)$ is checked upon entering `dporDfs` at every configuration $\sigma$ before state-store pruning. If $\sigma$ violates $I$, it is detected and emitted as a `VIOLATION` trace immediately. +5. **Future Violation Preservation**: If a violation occurs only in a continuation from $\sigma$, then when $\sigma$ was first visited and marked, all non-sleeping branches from $\sigma$ were explored. By commutativity of independent prefixes, any schedule reaching $\sigma$ shares the same downstream equivalence classes; pruning revisits to $\sigma$ cannot eliminate a reachable property violation. $\blacksquare$ diff --git a/docs/specs/active/15-property-aware-dpor/03-verification-and-benchmarks.md b/docs/specs/active/15-property-aware-dpor/03-verification-and-benchmarks.md index 8e99377..c8afd09 100644 --- a/docs/specs/active/15-property-aware-dpor/03-verification-and-benchmarks.md +++ b/docs/specs/active/15-property-aware-dpor/03-verification-and-benchmarks.md @@ -21,7 +21,7 @@ This document details the verification suite, empirical benchmarks, differential ### 2. Differential Oracles -For all parameterized tests and corpus benchmarks: +For all corpus benchmarks: - **Verdict Equivalence**: $\text{outcomes}(\text{DPOR}(P, I)) \equiv \text{outcomes}(\text{DFS}(P, I))$ - **Violation Preservation**: If $\text{DFS}(P, I)$ contains `VIOLATION`, then $\text{DPOR}(P, I)$ contains `VIOLATION`. - **Deadlock Preservation**: If $\text{DFS}(P, I)$ contains `DEADLOCK`, then $\text{DPOR}(P, I)$ contains `DEADLOCK`. @@ -29,15 +29,15 @@ For all parameterized tests and corpus benchmarks: ### 3. BugCorpus Benchmark Suite -All benchmarks in `BugCorpus.all()` are executed against `DporExplorer`: -- `lost-update`: Expected `VIOLATION` +All 8 benchmarks in `BugCorpus.all()` are executed against `DporExplorer`: - `peterson`: Expected `COMPLETED` (mutual exclusion holds) - `broken-peterson`: Expected `VIOLATION` - `broken-peterson-v2`: Expected `VIOLATION` -- `producer-consumer-bounded`: Expected `COMPLETED` -- `circular-buffer`: Expected `COMPLETED` -- `deadlock-3thread`: Expected `DEADLOCK` -- `dining-philosophers`: Expected `DEADLOCK` +- `deadlock`: Expected `DEADLOCK` +- `double-checked-locking`: Expected `VIOLATION` +- `lost-update`: Expected `VIOLATION` +- `lost-update-3t`: Expected `VIOLATION` +- `torn-counter`: Expected `VIOLATION` ## Mutation Targets (PIT) diff --git a/src/test/java/dev/samhb/interleave/dpor/DporPropertyAwarenessTest.java b/src/test/java/dev/samhb/interleave/dpor/DporPropertyAwarenessTest.java index 5a0ba3e..a4174c0 100644 --- a/src/test/java/dev/samhb/interleave/dpor/DporPropertyAwarenessTest.java +++ b/src/test/java/dev/samhb/interleave/dpor/DporPropertyAwarenessTest.java @@ -4,6 +4,7 @@ import dev.samhb.interleave.bugs.BenchmarkProgram; import dev.samhb.interleave.bugs.BugCorpus; import dev.samhb.interleave.core.*; +import dev.samhb.interleave.format.ProgramLoader; import dev.samhb.interleave.search.*; import dev.samhb.interleave.por.StaticPorExplorer; import org.junit.jupiter.api.Test; @@ -83,9 +84,30 @@ void visibleStepRefreshesSleepSet() { // Thread 1: step 0 writes cell[1]=1 (visible!). Cells initial = new Cells(0, 0, 0); Step conditionalViolate = new Step() { + /** + * Returns read locations for the conditional step. + * @return set containing cell[1] + */ public Set reads() { return locations("cell[1]"); } + + /** + * Returns write locations for the conditional step. + * @return set containing cell[2] + */ public Set writes() { return locations("cell[2]"); } + + /** + * Reports whether the conditional step is enabled. + * @param state modeled state to inspect + * @return true always + */ public boolean enabled(SharedState state) { return true; } + + /** + * Executes the conditional violation when cell[1] == 1. + * @param state modeled state to mutate + * @return ADVANCED outcome + */ public StepOutcome execute(SharedState state) { Cells c = (Cells) state; if (c.values[1] == 1) { @@ -185,7 +207,9 @@ void emptyObservationsReducesCompletely() { DfsResult dfs = new DfsExplorer().explore(program, emptyProperty); DfsResult dpor = new DporExplorer().explore(program, emptyProperty); - assertTrue(dpor.statesExplored() <= dfs.statesExplored()); + assertTrue(dpor.statesExplored() < dfs.statesExplored(), + "Empty observation set must strictly reduce independent work compared to DFS. DFS: " + + dfs.statesExplored() + ", DPOR: " + dpor.statesExplored()); assertEquals(outcomes(dfs), outcomes(dpor)); } @@ -206,6 +230,39 @@ void dslFinalPropertyFallsBackToExhaustiveDfs() { assertEquals(outcomes(dfs), outcomes(dpor)); } + /** Verifies that a declarative DSL program with an always invariant applies property-aware reduction. */ + @Test + void dslAlwaysPropertyAppliesPropertyAwareReduction() { + String json = """ + { + "format": "declarative", + "name": "dsl-always-test", + "state": {"fields": [{"name": "a", "type": "int", "init": 0}, {"name": "b", "type": "int", "init": 0}, {"name": "x", "type": "int", "init": 0}]}, + "threads": [ + {"id": 0, "steps": [{"effects": ["a = 1"]}, {"effects": ["a = 2"]}]}, + {"id": 1, "steps": [{"effects": ["b = 1"]}, {"effects": ["b = 2"]}]}, + {"id": 2, "steps": [{"effects": ["x = 1"]}]} + ], + "invariant": { + "expr": "x >= 0", + "when": "always" + } + } + """; + BenchmarkProgram prog = new ProgramLoader().load(json); + Invariant invariant = prog.invariant().orElseThrow(); + assertTrue(invariant.observedLocations().isPresent()); + + DfsResult dfs = new DfsExplorer().explore(prog.program(), invariant); + DfsResult dpor = new DporExplorer().explore(prog.program(), invariant); + + assertTrue(dpor.statesExplored() < dfs.statesExplored(), + "DPOR must explore fewer states than DFS on DSL always property with independent work. DFS: " + + dfs.statesExplored() + ", DPOR: " + dpor.statesExplored()); + assertEquals(outcomes(dfs), outcomes(dpor)); + assertTrue(outcomes(dpor).contains(TraceOutcome.COMPLETED)); + } + /** Verifies differential equivalence across all benchmarks in BugCorpus. */ @Test void bugCorpusAllVerdictsPreserved() { @@ -219,6 +276,8 @@ void bugCorpusAllVerdictsPreserved() { assertEquals(dfsOutcomes, dporOutcomes, "Outcomes must match for corpus program: " + benchmark.name()); + assertTrue(dporResult.statesExplored() <= dfsResult.statesExplored(), + "DPOR states explored must be <= DFS states explored for benchmark " + benchmark.name()); TraceOutcome expectedOutcome = switch (benchmark.expectedVerdict()) { case "VIOLATION" -> TraceOutcome.VIOLATION; @@ -251,10 +310,20 @@ void differentialCheckAgainstStaticPor() { assertTrue(outcomes(dpor).contains(TraceOutcome.VIOLATION)); } + /** + * Creates a set of memory locations from the provided names. + * @param names stable memory location identifiers + * @return immutable set containing the specified memory locations + */ private static Set locations(String... names) { return Arrays.stream(names).map(MemoryLocation::of).collect(java.util.stream.Collectors.toSet()); } + /** + * Extracts the distinct trace outcomes recorded in an exploration result. + * @param result completed exploration result to inspect + * @return set of distinct terminal outcomes observed across all traces + */ private static Set outcomes(DfsResult result) { Set outcomes = EnumSet.noneOf(TraceOutcome.class); result.traces().forEach(trace -> outcomes.add(trace.outcome())); @@ -263,27 +332,61 @@ private static Set outcomes(DfsResult result) { /** Simple three-cell shared state for tests. */ private static final class Cells implements SharedState { + /** Cell values array. */ private final int[] values; + /** + * Creates a three-cell shared state with the specified initial values. + * @param values initial cell values to store + */ Cells(int... values) { this.values = values.clone(); } + /** + * Returns an isolated deep copy preserving modeled cell values. + * @return new Cells instance with duplicated values + */ public SharedState deepCopy() { return new Cells(values); } + /** + * Writes the cell values in deterministic canonical order. + * @param out data output destination + * @throws IOException if encoding fails + */ public void encodeTo(DataOutput out) throws IOException { for (int value : values) out.writeInt(value); } + /** + * Compares cells for value equality across all elements. + * @param other object to compare + * @return true if other is a Cells instance with identical values + */ public boolean equals(Object other) { return other instanceof Cells cells && Arrays.equals(values, cells.values); } + /** + * Returns hash code consistent with array value equality. + * @return array-based hash code + */ public int hashCode() { return Arrays.hashCode(values); } } - /** Simple deterministic step modifying cells. */ + /** + * Deterministic transition modifying cells with conservative footprints. + * @param read cell index to read, or -1 for none + * @param write cell index to write, or -1 for none + * @param value literal value to assign when write is performed without read + * @param guard cell index required to be 1 for enabledness, or -1 for none + * @param assertion whether this step asserts cell[read] == 0 + */ private record CellStep(int read, int write, int value, int guard, boolean assertion) implements Step { + /** + * Returns declared read locations including guard and assertion dependencies. + * @return set of read memory locations + */ public Set reads() { Set reads = new HashSet<>(); if (read >= 0) reads.add(MemoryLocation.of("cell[" + read + "]")); @@ -291,14 +394,28 @@ public Set reads() { return reads; } + /** + * Returns declared write locations for this cell step. + * @return set containing the written cell location, or empty if none + */ public Set writes() { return write < 0 ? Set.of() : locations("cell[" + write + "]"); } + /** + * Reports whether this step is enabled in the current state based on its guard. + * @param state modeled state to inspect + * @return true if guard is absent or satisfied + */ public boolean enabled(SharedState state) { return guard < 0 || ((Cells) state).values[guard] == 1; } + /** + * Executes this cell step, applying mutations or checking assertions. + * @param state modeled state to mutate + * @return execution outcome (ADVANCED or ASSERTION_FAILED) + */ public StepOutcome execute(SharedState state) { Cells cells = (Cells) state; if (assertion) { From 49cf1fba9f4bd0cd3438fb1e838dc2be9fb46fe2 Mon Sep 17 00:00:00 2001 From: Samuel Date: Thu, 15 Oct 2026 22:52:10 -0400 Subject: [PATCH 3/3] docs(spec-15): format markdown headings, code fences, and list style Co-authored-by: Gemini --- .../01-property-visibility-dpor.md | 1 + .../15-property-aware-dpor/02-soundness-proof.md | 11 +++++++---- 2 files changed, 8 insertions(+), 4 deletions(-) diff --git a/docs/specs/active/15-property-aware-dpor/01-property-visibility-dpor.md b/docs/specs/active/15-property-aware-dpor/01-property-visibility-dpor.md index 6496754..e5c07b5 100644 --- a/docs/specs/active/15-property-aware-dpor/01-property-visibility-dpor.md +++ b/docs/specs/active/15-property-aware-dpor/01-property-visibility-dpor.md @@ -9,6 +9,7 @@ Dynamic partial order reduction in `DporExplorer` uses sleep sets to avoid explo ### 1. Invariant Observation Classification An invariant `Invariant` evaluates safety predicates against modeled configurations: + ```java public interface Invariant { boolean holds(SharedState state, Configuration config); diff --git a/docs/specs/active/15-property-aware-dpor/02-soundness-proof.md b/docs/specs/active/15-property-aware-dpor/02-soundness-proof.md index 27422b0..ad72d93 100644 --- a/docs/specs/active/15-property-aware-dpor/02-soundness-proof.md +++ b/docs/specs/active/15-property-aware-dpor/02-soundness-proof.md @@ -16,6 +16,7 @@ This document proves that Dynamic Partial Order Reduction using sleep sets with ## Lemmas & Proofs ### Lemma 1 (Invisible Transition Valuation Invariance) + If step $s$ is invisible with respect to $\mathcal{O}$ ($\text{writesOverlap}(W(s), \mathcal{O}) = \emptyset$), then for any configuration $\sigma$: $$I(s(\sigma)) = I(\sigma)$$ @@ -23,6 +24,7 @@ $$I(s(\sigma)) = I(\sigma)$$ Because $s$ writes to no location in $\mathcal{O}$, the projection of state $\sigma$ onto $\mathcal{O}$ is identical to the projection of $s(\sigma)$ onto $\mathcal{O}$. Since $I$ depends exclusively on $\mathcal{O}$, $I(s(\sigma)) = I(\sigma)$. $\blacksquare$ ### Lemma 2 (Intermediate State Invariance Under Invisible Commutation) + Let $s_1$ and $s_2$ be two independent transitions ($s_1 \, I \, s_2$) enabled at $\sigma$. Consider schedule $\pi_1 = \sigma \xrightarrow{s_1} s_1(\sigma) \xrightarrow{s_2} s_1(s_2(\sigma))$ and schedule $\pi_2 = \sigma \xrightarrow{s_2} s_2(\sigma) \xrightarrow{s_1} s_2(s_1(\sigma))$. By independence, $s_1(s_2(\sigma)) = s_2(s_1(\sigma))$. @@ -42,6 +44,7 @@ By independence, $s_1(s_2(\sigma)) = s_2(s_1(\sigma))$. Both schedules visit the exact same set of invariant valuations. $\blacksquare$ ### Theorem 1 (Soundness of Visible Sleep-Set Maintenance) + Under Rules 1, 2, and 3: If there exists an execution sequence in the full state graph reaching a state violating $I$, then the property-aware DPOR search discovers a violation trace. @@ -51,11 +54,11 @@ If $\neg I(\sigma_0)$ at the initial state, the violation is detected immediatel Otherwise, consider the branching at $\sigma_0$: - If the first transition $s_1$ in $w$ is explored from $\sigma_0$, induction applies on the remaining suffix of length $k-1$. - Suppose instead transition $u \neq s_1$ is explored first from $\sigma_0$: - - If $s_1$ is visible to $I$, Rule 1 guarantees that $s_1$ is never placed into `nextSleepSet`. Thus, $s_1$ remains enabled and eligible for exploration from $\sigma_0$ when backtracking. - - If $s_1$ is invisible to $I$ and independent of $u$: + - In case $s_1$ is visible to $I$, Rule 1 guarantees that $s_1$ is never placed into `nextSleepSet`. Thus, $s_1$ remains enabled and eligible for exploration from $\sigma_0$ when backtracking. + - When $s_1$ is invisible to $I$ and independent of $u$: By Lemma 2, commuting $u$ and $s_1$ yields a valid execution reaching the same state valuation on $\mathcal{O}$. - - If $s_1$ and $u$ are dependent, $u$ cannot place $s_1$ to sleep (independence requirement). - - If $u$ is visible, Rule 2 refreshes the sleep set to empty, ensuring any previously sleeping transitions are re-enabled to observe the updated state. + - Should $s_1$ and $u$ be dependent, $u$ cannot place $s_1$ to sleep (independence requirement). + - Whenever $u$ is visible, Rule 2 refreshes the sleep set to empty, ensuring any previously sleeping transitions are re-enabled to observe the updated state. Because threads have finite linear lengths and counters strictly increase on progress, induction on remaining step distance $R(\sigma)$ guarantees that a violation-reaching schedule is preserved in the explored search tree. $\blacksquare$ ### Interaction Between Sleep Sets and the Visited-State Store