feat(dpor): implement dynamic property-aware partial order reduction (Spec 15)

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
@@ -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.

docs/specs/active/15-property-aware-dpor/01-property-visibility-dpor.md

@@ -0,0 +1,57 @@
+# 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<Set<MemoryLocation>> 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.

docs/specs/active/15-property-aware-dpor/02-soundness-proof.md

@@ -0,0 +1,73 @@
+# 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$:
+  - 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}$.
+  - 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
+
+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$

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 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 8 benchmarks in `BugCorpus.all()` are executed against `DporExplorer`:
+- `peterson`: Expected `COMPLETED` (mutual exclusion holds)
+- `broken-peterson`: Expected `VIOLATION`
+- `broken-peterson-v2`: Expected `VIOLATION`
+- `deadlock`: Expected `DEADLOCK`
+- `double-checked-locking`: Expected `VIOLATION`
+- `lost-update`: Expected `VIOLATION`
+- `lost-update-3t`: Expected `VIOLATION`
+- `torn-counter`: Expected `VIOLATION`
+
+## 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.

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
+```