diff --git a/AGENTS.md b/AGENTS.md index 7df19df..b8b3ec4 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -224,7 +224,7 @@ catch (Exception ex) - **Strong consistency**: `GetDataAndWaitForIdleAsync` — always waits for idle regardless of `CacheInteraction` **Serialized Access Requirement for Hybrid/Strong Modes:** -`GetDataAndWaitOnMissAsync` and `GetDataAndWaitForIdleAsync` provide their warm-cache guarantee only under **serialized (one-at-a-time) access**. Under parallel access, `WaitForIdleAsync`'s "was idle at some point" semantics (Invariant H.49) may return the old completed TCS, missing the rebalance triggered by the concurrent request. These methods remain safe (no crashes/hangs) but the guarantee degrades under parallelism. +`GetDataAndWaitOnMissAsync` and `GetDataAndWaitForIdleAsync` provide their warm-cache guarantee only under **serialized (one-at-a-time) access**. Under parallel access, `WaitForIdleAsync`'s "was idle at some point" semantics (Invariant H.3) may return the old completed TCS, missing the rebalance triggered by the concurrent request. These methods remain safe (no crashes/hangs) but the guarantee degrades under parallelism. **Lock-Free Operations:** ```csharp diff --git a/README.md b/README.md index ff360ed..feed8ea 100644 --- a/README.md +++ b/README.md @@ -402,7 +402,7 @@ Canonical guide: `docs/diagnostics.md`. By default, `GetDataAsync` is **eventually consistent**: data is returned immediately while the cache window converges asynchronously in the background. Two opt-in extension methods provide stronger consistency guarantees. Both require a `using SlidingWindowCache.Public;` import. -> **Serialized access requirement:** The hybrid and strong consistency modes provide their warm-cache guarantee only when requests are made one at a time (serialized). Under concurrent/parallel callers they remain safe (no crashes or hangs) but the guarantee degrades — due to `AsyncActivityCounter`'s "was idle at some point" semantics (Invariant H.49) and a brief gap between the counter increment and TCS publication in `IncrementActivity`, a concurrent waiter may observe a previously completed idle TCS and return without waiting for the new rebalance. +> **Serialized access requirement:** The hybrid and strong consistency modes provide their warm-cache guarantee only when requests are made one at a time (serialized). Under concurrent/parallel callers they remain safe (no crashes or hangs) but the guarantee degrades — due to `AsyncActivityCounter`'s "was idle at some point" semantics (Invariant H.3) and a brief gap between the counter increment and TCS publication in `IncrementActivity`, a concurrent waiter may observe a previously completed idle TCS and return without waiting for the new rebalance. ### Eventual Consistency (Default) diff --git a/docs/actors.md b/docs/actors.md index ef7385d..cad9515 100644 --- a/docs/actors.md +++ b/docs/actors.md @@ -35,19 +35,18 @@ Non-responsibilities - Does not compute `DesiredCacheRange` (belongs to Cache Geometry Policy). Invariant ownership -- -1. User Path and Rebalance Execution never write to cache concurrently -- 0. User Path has higher priority than rebalance execution -- 0a. User Request MAY cancel any ongoing or pending Rebalance Execution ONLY when a new rebalance is validated as necessary -- 1. User Path always serves user requests -- 2. User Path never waits for rebalance execution -- 3. User Path is the sole source of rebalance intent -- 5. Performs only work necessary to return data -- 6. May synchronously request from IDataSource -- 7. May read cache and source, but does not mutate cache state -- 8. MUST NOT mutate cache under any circumstance (read-only) -- 10. Always returns exactly RequestedRange -- 24e. Intent MUST contain delivered data (RangeData) -- 24f. Delivered data represents what user actually received +- A.1. User Path and Rebalance Execution never write to cache concurrently +- A.2. User Path has higher priority than rebalance execution +- A.2a. User Request MAY cancel any ongoing or pending Rebalance Execution ONLY when a new rebalance is validated as necessary +- A.3. User Path always serves user requests +- A.4. User Path never waits for rebalance execution +- A.5. User Path is the sole source of rebalance intent +- A.7. Performs only work necessary to return data +- A.8. May synchronously request from IDataSource +- A.11. May read cache and source, but does not mutate cache state +- A.12. MUST NOT mutate cache under any circumstance (read-only) +- C.8e. Intent MUST contain delivered data (RangeData) +- C.8f. Delivered data represents what user actually received Components - `WindowCache` (facade / composition root; also owns `RuntimeCacheOptionsHolder` and exposes `UpdateRuntimeOptions`) @@ -69,12 +68,12 @@ Non-responsibilities - Does not perform I/O. Invariant ownership -- 29. DesiredCacheRange computed from RequestedRange + config -- 30. Independent of current cache contents -- 31. Canonical target cache state -- 32. Sliding window geometry defined by configuration -- 33. NoRebalanceRange derived from current cache range + config -- 35. Threshold sum constraint (leftThreshold + rightThreshold ≤ 1.0) +- E.1. DesiredCacheRange computed from RequestedRange + config +- E.2. Independent of current cache contents +- E.3. Canonical target cache state +- E.4. Sliding window geometry defined by configuration +- E.5. NoRebalanceRange derived from current cache range + config +- E.6. Threshold sum constraint (leftThreshold + rightThreshold ≤ 1.0) Components - `ProportionalRangePlanner` — computes `DesiredCacheRange`; reads configuration from `RuntimeCacheOptionsHolder` at invocation time @@ -95,11 +94,11 @@ Non-responsibilities - Does not call `IDataSource`. Invariant ownership -- 24. Decision Path is purely analytical (CPU-only, no I/O) -- 25. Never mutates cache state -- 26. No rebalance if inside NoRebalanceRange (Stage 1 validation) -- 27. No rebalance if DesiredCacheRange == CurrentCacheRange (Stage 4 validation) -- 28. Rebalance triggered only if ALL validation stages confirm necessity +- D.1. Decision Path is purely analytical (CPU-only, no I/O) +- D.2. Never mutates cache state +- D.3. No rebalance if inside NoRebalanceRange (Stage 1 validation) +- D.4. No rebalance if DesiredCacheRange == CurrentCacheRange (Stage 4 validation) +- D.5. Rebalance triggered only if ALL validation stages confirm necessity Components - `RebalanceDecisionEngine` @@ -121,14 +120,14 @@ Non-responsibilities - Does not determine rebalance necessity (delegates to Decision Engine). Invariant ownership -- 17. At most one active rebalance intent -- 18. Older intents may become logically superseded -- 19. Executions can be cancelled based on validation results -- 20. Obsolete intent must not start execution -- 21. At most one rebalance execution active -- 22. Execution reflects latest access pattern and validated necessity -- 23. System eventually stabilizes under load through work avoidance -- 24. Intent does not guarantee execution — execution is opportunistic and validation-driven +- C.1. At most one active rebalance intent +- C.2. Older intents may become logically superseded +- C.3. Executions can be cancelled based on validation results +- C.4. Obsolete intent must not start execution +- C.5. At most one rebalance execution active +- C.6. Execution reflects latest access pattern and validated necessity +- C.7. System eventually stabilizes under load through work avoidance +- C.8. Intent does not guarantee execution — execution is opportunistic and validation-driven Components - `IntentController` @@ -164,18 +163,18 @@ Non-responsibilities - Does not check if `DesiredCacheRange == CurrentCacheRange` (Stage 4 already passed). Invariant ownership -- A.4. Rebalance is asynchronous relative to User Path -- F.35. MUST support cancellation at all stages -- F.35a. MUST yield to User Path requests immediately upon cancellation -- F.35b. Partially executed or cancelled execution MUST NOT leave cache inconsistent -- F.36. Only path responsible for cache normalization (single-writer architecture) -- F.36a. Mutates cache ONLY for normalization using delivered data from intent -- F.37. May replace / expand / shrink cache to achieve normalization -- F.38. Requests data only for missing subranges (not covered by delivered data) -- F.39. Does not overwrite intersecting data -- F.40. Upon completion: CacheData corresponds to DesiredCacheRange -- F.41. Upon completion: CurrentCacheRange == DesiredCacheRange -- F.42. Upon completion: NoRebalanceRange recomputed +- A.6. Rebalance is asynchronous relative to User Path +- F.1. MUST support cancellation at all stages +- F.1a. MUST yield to User Path requests immediately upon cancellation +- F.1b. Partially executed or cancelled execution MUST NOT leave cache inconsistent +- F.2. Only path responsible for cache normalization (single-writer architecture) +- F.2a. Mutates cache ONLY for normalization using delivered data from intent +- F.3. May replace / expand / shrink cache to achieve normalization +- F.4. Requests data only for missing subranges (not covered by delivered data) +- F.5. Does not overwrite intersecting data +- F.6. Upon completion: CacheData corresponds to DesiredCacheRange +- F.7. Upon completion: CurrentCacheRange == DesiredCacheRange +- F.8. Upon completion: NoRebalanceRange recomputed Components - `RebalanceExecutor` @@ -190,12 +189,12 @@ Responsibilities - Coordinate single-writer access between User Path (reads) and Rebalance Execution (writes). Invariant ownership -- 11. CacheData and CurrentCacheRange are consistent -- 12. Changes applied atomically -- 13. No permanent inconsistent state -- 14. Temporary inefficiencies are acceptable -- 15. Partial / cancelled execution cannot break consistency -- 16. Only latest intent results may be applied +- B.1. CacheData and CurrentCacheRange are consistent +- B.2. Changes applied atomically +- B.3. No permanent inconsistent state +- B.4. Temporary inefficiencies are acceptable +- B.5. Partial / cancelled execution cannot break consistency +- B.6. Only latest intent results may be applied Components - `CacheState` diff --git a/docs/components/decision.md b/docs/components/decision.md index b432a09..73083ae 100644 --- a/docs/components/decision.md +++ b/docs/components/decision.md @@ -75,6 +75,6 @@ The system prioritizes **decision correctness and work avoidance** over aggressi ## See Also -- `docs/invariants.md` — formal Decision Path invariant specifications (D.24–D.29) +- `docs/invariants.md` — formal Decision Path invariant specifications (D.1–D.5) - `docs/architecture.md` — Decision-Driven Execution section - `docs/components/overview.md` — Invariant Implementation Mapping (Decision subsection) diff --git a/docs/components/execution.md b/docs/components/execution.md index 7dd5cea..6ea3290 100644 --- a/docs/components/execution.md +++ b/docs/components/execution.md @@ -53,7 +53,7 @@ The execution subsystem performs debounced, cancellable background work and is t 6. Update `CacheState.NoRebalanceRange` — new stability zone 7. Set `CacheState.IsInitialized = true` (if first execution) -**Cancellation checkpoints** (Invariant F.35): +**Cancellation checkpoints** (Invariant F.1): - Before I/O: avoids unnecessary fetches - After I/O: discards fetched data if superseded - Before mutation: guarantees only latest validated execution applies changes @@ -67,7 +67,7 @@ The execution subsystem performs debounced, cancellable background work and is t - Merges new data with preserved existing data (union operation) - Propagates `CancellationToken` to `IDataSource.FetchAsync` -**Invariants**: F.38 (incremental fetching), F.39 (data preservation during expansion). +**Invariants**: F.4 (incremental fetching), F.5 (data preservation during expansion). ## Responsibilities @@ -100,21 +100,21 @@ In both cases, `OperationCanceledException` is reported via `ICacheDiagnostics.R | Invariant | Description | |-----------|--------------------------------------------------------------------------------------------------------| -| A.7 | Only `RebalanceExecutor` writes to `CacheState` (single-writer) | -| A.8 | User path never blocks waiting for rebalance | -| B.12 | Cache updates are atomic (all-or-nothing via `Rematerialize`) | -| B.13 | Consistency under cancellation: mutations discarded if cancelled | -| B.15 | Cache contiguity maintained after every `Rematerialize` | -| B.16 | Obsolete results never applied (cancellation token identity check) | -| C.21 | Serial execution: at most one active rebalance at a time | -| F.35 | Multiple cancellation checkpoints: before I/O, after I/O, before mutation | -| F.35a | Cancellation-before-mutation guarantee | -| F.37 | `Rematerialize` accepts arbitrary range and data (full replacement) | -| F.38 | Incremental fetching: only missing subranges fetched | -| F.39 | Data preservation: existing cached data merged during expansion | -| G.45 | I/O isolation: `IDataSource` called by execution path only (not by user path during normal cache hits) | -| H.47 | Activity counter incremented before channel write / task chain step | -| H.48 | Activity counter decremented in `finally` blocks | +| A.12a/F.2 | Only `RebalanceExecutor` writes to `CacheState` (single-writer) | +| A.4 | User path never blocks waiting for rebalance | +| B.2 | Cache updates are atomic (all-or-nothing via `Rematerialize`) | +| B.3 | Consistency under cancellation: mutations discarded if cancelled | +| B.5 | Cancelled rebalance cannot violate `CacheData ↔ CurrentCacheRange` consistency | +| B.6 | Obsolete results never applied (cancellation token identity check) | +| C.5 | Serial execution: at most one active rebalance at a time | +| F.1 | Multiple cancellation checkpoints: before I/O, after I/O, before mutation | +| F.1a | Cancellation-before-mutation guarantee | +| F.3 | `Rematerialize` accepts arbitrary range and data (full replacement) | +| F.4 | Incremental fetching: only missing subranges fetched | +| F.5 | Data preservation: existing cached data merged during expansion | +| G.3 | I/O isolation: User Path MAY call `IDataSource` for U1/U5 (cold start / full miss); Rebalance Execution calls it for background normalization only | +| H.1 | Activity counter incremented before channel write / task chain step | +| H.2 | Activity counter decremented in `finally` blocks | See `docs/invariants.md` (Sections A, B, C, F, G, H) for full specification. diff --git a/docs/components/intent-management.md b/docs/components/intent-management.md index ef8411a..61cf45f 100644 --- a/docs/components/intent-management.md +++ b/docs/components/intent-management.md @@ -24,7 +24,7 @@ Intent management bridges the user path and background work. It receives access Called by `UserRequestHandler` after serving a request: 1. Atomically replaces pending intent via `Interlocked.Exchange` (latest wins; previous intent superseded) -2. Increments `AsyncActivityCounter` (before signalling — ordering required by Invariant H.47) +2. Increments `AsyncActivityCounter` (before signalling — ordering required by Invariant H.1) 3. Releases semaphore (wakes up `ProcessIntentsAsync` if sleeping) 4. Records `RebalanceIntentPublished` diagnostic event 5. Returns immediately (fire-and-forget) @@ -80,15 +80,15 @@ User burst: intent₁ → intent₂ → intent₃ | Invariant | Description | |-----------|--------------------------------------------------------------------------| -| C.17 | At most one pending intent at any time (atomic replacement) | -| C.18 | Previous intents become obsolete when superseded | -| C.19 | Cancellation is cooperative via `CancellationToken` | -| C.20 | Cancellation checked after debounce before execution starts | -| C.21 | At most one active rebalance scheduled at a time | -| C.24 | Intent does not guarantee execution | -| C.24e | Intent carries `deliveredData` (the data the user actually received) | -| H.47 | Activity counter incremented before semaphore signal (ordering) | -| H.48 | Activity counter decremented in `finally` blocks (unconditional cleanup) | +| C.1 | At most one pending intent at any time (atomic replacement) | +| C.2 | Previous intents become obsolete when superseded | +| C.3 | Cancellation is cooperative via `CancellationToken` | +| C.4 | Cancellation checked after debounce before execution starts | +| C.5 | At most one active rebalance scheduled at a time | +| C.8 | Intent does not guarantee execution | +| C.8e | Intent carries `deliveredData` (the data the user actually received) | +| H.1 | Activity counter incremented before semaphore signal (ordering) | +| H.2 | Activity counter decremented in `finally` blocks (unconditional cleanup) | See `docs/invariants.md` (Section C: Intent invariants, Section H: Activity counter invariants) for full specification. diff --git a/docs/components/overview.md b/docs/components/overview.md index f7bf5c3..838a0f8 100644 --- a/docs/components/overview.md +++ b/docs/components/overview.md @@ -258,7 +258,7 @@ The system is easier to reason about when components are grouped by: This section bridges architectural invariants (in `docs/invariants.md`) to their concrete implementations. Each invariant is enforced through specific component interactions, code patterns, or architectural constraints. ### Single-Writer Architecture -**Invariants**: A.-1, A.7, A.8, A.9, F.36 +**Invariants**: A.1, A.11, A.12, A.12a, F.2 Only `RebalanceExecutor` has write access to `CacheState` internal setters. User Path components have read-only references. Internal visibility modifiers prevent external mutations. @@ -267,7 +267,7 @@ Only `RebalanceExecutor` has write access to `CacheState` internal setters. User - `src/SlidingWindowCache/Core/UserPath/UserRequestHandler.cs` — read-only access pattern ### Priority and Cancellation -**Invariants**: A.0, A.0a, C.19, F.35a +**Invariants**: A.2, A.2a, C.3, F.1a `CancellationTokenSource` coordination between intent publishing and execution. `RebalanceDecisionEngine` validates necessity before triggering cancellation. Multiple checkpoints in execution pipeline check for cancellation. @@ -276,14 +276,14 @@ Only `RebalanceExecutor` has write access to `CacheState` internal setters. User - `src/SlidingWindowCache/Core/Rebalance/Execution/RebalanceExecutor.cs` — `ThrowIfCancellationRequested` checkpoints ### Intent Management and Cancellation -**Invariants**: A.0a, C.17, C.20, C.21 +**Invariants**: A.2a, C.1, C.4, C.5 `Interlocked.Exchange` replaces previous intent atomically (latest-wins). Single-writer architecture for intent state. Cancellation checked after debounce delay before execution starts. - `src/SlidingWindowCache/Core/Rebalance/Intent/IntentController.cs` — atomic intent replacement ### UserRequestHandler Responsibilities -**Invariants**: A.3, A.5 +**Invariants**: A.5, A.7 Only `UserRequestHandler` has access to `IntentController.PublishIntent`. Its scope is limited to data assembly; no normalization logic. @@ -291,7 +291,7 @@ Only `UserRequestHandler` has access to `IntentController.PublishIntent`. Its sc - `src/SlidingWindowCache/Core/Rebalance/Intent/IntentController.cs` — internal visibility on publication interface ### Async Execution Model -**Invariants**: A.4, G.44 +**Invariants**: A.6, G.2 `UserRequestHandler` publishes intent and returns immediately (fire-and-forget). `IRebalanceExecutionController` schedules execution via `Task.Run` or channels. User thread and ThreadPool thread contexts are separated. @@ -300,7 +300,7 @@ Only `UserRequestHandler` has access to `IntentController.PublishIntent`. Its sc - `src/SlidingWindowCache/Infrastructure/Execution/ChannelBasedRebalanceExecutionController.cs` — channel-based background execution ### Atomic Cache Updates -**Invariants**: B.12, B.13 +**Invariants**: B.2, B.3 Storage strategies build new state before atomic swap. `Volatile.Write` atomically publishes new cache state reference (Snapshot). `CopyOnReadStorage` uses a lock-protected buffer swap instead. `Rematerialize` succeeds completely or not at all. @@ -309,14 +309,14 @@ Storage strategies build new state before atomic swap. `Volatile.Write` atomical - `src/SlidingWindowCache/Core/State/CacheState.cs` — `Rematerialize` ensures atomicity ### Consistency Under Cancellation -**Invariants**: B.13, B.15, F.35b +**Invariants**: B.3, B.5, F.1b Final cancellation check before applying cache updates. Results applied atomically or discarded entirely. `try-finally` blocks ensure cleanup on cancellation. - `src/SlidingWindowCache/Core/Rebalance/Execution/RebalanceExecutor.cs` — `ThrowIfCancellationRequested` before `Rematerialize` ### Obsolete Result Prevention -**Invariants**: B.16, C.20 +**Invariants**: B.6, C.4 Each intent has a unique `CancellationToken`. Execution checks if cancellation is requested before applying results. Only results from the latest non-cancelled intent are applied. @@ -324,14 +324,14 @@ Each intent has a unique `CancellationToken`. Execution checks if cancellation i - `src/SlidingWindowCache/Core/Rebalance/Intent/IntentController.cs` — token lifecycle management ### Intent Singularity -**Invariant**: C.17 +**Invariant**: C.1 `Interlocked.Exchange` ensures exactly one active intent. New intent atomically replaces previous one. At most one pending intent at any time (no queue buildup). - `src/SlidingWindowCache/Core/Rebalance/Intent/IntentController.cs` — `Interlocked.Exchange` for atomic intent replacement ### Cancellation Protocol -**Invariant**: C.19 +**Invariant**: C.3 `CancellationToken` passed through the entire pipeline. Multiple checkpoints: before I/O, after I/O, before mutations. Results from cancelled operations are never applied. @@ -339,7 +339,7 @@ Each intent has a unique `CancellationToken`. Execution checks if cancellation i - `src/SlidingWindowCache/Infrastructure/Services/CacheDataExtensionService.cs` — cancellation token propagated to `IDataSource` ### Early Exit Validation -**Invariants**: C.20, D.29 +**Invariants**: C.4, D.5 Post-debounce cancellation check before execution. Each validation stage can exit early. All stages must pass for execution to proceed. @@ -347,14 +347,14 @@ Post-debounce cancellation check before execution. Each validation stage can exi - `src/SlidingWindowCache/Core/Rebalance/Decision/RebalanceDecisionEngine.cs` — multi-stage early exit ### Serial Execution Guarantee -**Invariant**: C.21 +**Invariant**: C.5 Previous execution cancelled before starting new one. Single `IRebalanceExecutionController` instance per cache. Intent processing loop ensures serial execution. - `src/SlidingWindowCache/Core/Rebalance/Intent/IntentController.cs` — sequential intent loop + cancellation of prior execution ### Intent Data Contract -**Invariant**: C.24e +**Invariant**: C.8e `PublishIntent` signature requires `deliveredData` parameter. `UserRequestHandler` materializes data once, passes it to both user and intent. Compiler enforces data presence. @@ -362,7 +362,7 @@ Previous execution cancelled before starting new one. Single `IRebalanceExecutio - `src/SlidingWindowCache/Core/UserPath/UserRequestHandler.cs` — single data materialization shared between paths ### Pure Decision Logic -**Invariants**: D.25, D.26 +**Invariants**: D.1, D.2 `RebalanceDecisionEngine` has no mutable fields. Decision policies are classes with no side effects. No I/O in decision path. Pure function: `(state, intent, config) → decision`. @@ -371,7 +371,7 @@ Previous execution cancelled before starting new one. Single `IRebalanceExecutio - `src/SlidingWindowCache/Core/Planning/ProportionalRangePlanner.cs` — stateless struct ### Decision-Execution Separation -**Invariant**: D.26 +**Invariant**: D.2 Decision components have no references to mutable state setters. Decision Engine reads `CacheState` but cannot modify it. Decision and Execution interfaces are distinct. @@ -379,21 +379,21 @@ Decision components have no references to mutable state setters. Decision Engine - `src/SlidingWindowCache/Core/Rebalance/Execution/RebalanceExecutor.cs` — exclusive write access ### Multi-Stage Decision Pipeline -**Invariant**: D.29 +**Invariant**: D.5 Five-stage pipeline with early exits. Stage 1: current `NoRebalanceRange` containment (fast path). Stage 2: pending `NoRebalanceRange` validation (thrashing prevention). Stage 3: `DesiredCacheRange` computation. Stage 4: equality check (`DesiredCacheRange == CurrentCacheRange`). Stage 5: execution scheduling (only if all stages pass). - `src/SlidingWindowCache/Core/Rebalance/Decision/RebalanceDecisionEngine.cs` — complete pipeline implementation ### Desired Range Computation -**Invariants**: E.30, E.31 +**Invariants**: E.1, E.2 `ProportionalRangePlanner.Plan(requestedRange, config)` is a pure function — same inputs always produce same output. Never reads `CurrentCacheRange`. Reads configuration from a shared `RuntimeCacheOptionsHolder` at invocation time to support runtime option updates. - `src/SlidingWindowCache/Core/Planning/ProportionalRangePlanner.cs` — pure range calculation ### NoRebalanceRange Computation -**Invariants**: E.34, E.35 +**Invariants**: E.5, E.6 `NoRebalanceRangePlanner.Plan(currentCacheRange)` — pure function of current range + config. Applies threshold percentages as negative expansion. Returns `null` when individual thresholds ≥ 1.0 (no stability zone possible). `WindowCacheOptions` constructor ensures threshold sum ≤ 1.0 at construction time. Reads configuration from a shared `RuntimeCacheOptionsHolder` at invocation time to support runtime option updates. @@ -401,14 +401,14 @@ Five-stage pipeline with early exits. Stage 1: current `NoRebalanceRange` contai - `src/SlidingWindowCache/Public/Configuration/WindowCacheOptions.cs` — threshold sum validation ### Cancellation Checkpoints -**Invariants**: F.35, F.35a +**Invariants**: F.1, F.1a Three checkpoints: before `IDataSource.FetchAsync`, after data fetching, before `Rematerialize`. `OperationCanceledException` propagates to cleanup handlers. - `src/SlidingWindowCache/Core/Rebalance/Execution/RebalanceExecutor.cs` — multiple checkpoint locations ### Cache Normalization Operations -**Invariant**: F.37 +**Invariant**: F.3 `CacheState.Rematerialize` accepts arbitrary range and data (full replacement). `ICacheStorage` abstraction enables different normalization strategies. @@ -416,21 +416,21 @@ Three checkpoints: before `IDataSource.FetchAsync`, after data fetching, before - `src/SlidingWindowCache/Infrastructure/Storage/` — storage strategy implementations ### Incremental Data Fetching -**Invariant**: F.38 +**Invariant**: F.4 `CacheDataExtensionService.ExtendCacheDataAsync` computes missing ranges via range subtraction (`DesiredRange \ CachedRange`). Fetches only missing subranges via `IDataSource`. - `src/SlidingWindowCache/Infrastructure/Services/CacheDataExtensionService.cs` — range gap logic in `ExtendCacheDataAsync` ### Data Preservation During Expansion -**Invariant**: F.39 +**Invariant**: F.5 New data merged with existing via range union. Existing data enumerated and preserved during rematerialization. New data only fills gaps; does not replace existing. - `src/SlidingWindowCache/Infrastructure/Services/CacheDataExtensionService.cs` — union logic in `ExtendCacheDataAsync` ### I/O Isolation -**Invariant**: G.45 +**Invariant**: G.3 `UserRequestHandler` completes before any `IDataSource.FetchAsync` calls in rebalance path. All `IDataSource` interactions happen in `RebalanceExecutor` on a background thread. @@ -438,7 +438,7 @@ New data merged with existing via range union. Existing data enumerated and pres - `src/SlidingWindowCache/Core/Rebalance/Execution/RebalanceExecutor.cs` — `IDataSource` calls only in background execution ### Activity Counter Ordering -**Invariant**: H.47 +**Invariant**: H.1 Activity counter incremented **before** semaphore signal, channel write, or volatile write (strict ordering discipline at all publication sites). @@ -446,7 +446,7 @@ Activity counter incremented **before** semaphore signal, channel write, or vola - `src/SlidingWindowCache/Infrastructure/Execution/` — increment before channel write or `Task.Run` ### Activity Counter Cleanup -**Invariant**: H.48 +**Invariant**: H.2 Decrement in `finally` blocks — unconditional execution regardless of success, failure, or cancellation. diff --git a/docs/components/public-api.md b/docs/components/public-api.md index 940b39c..1f040f6 100644 --- a/docs/components/public-api.md +++ b/docs/components/public-api.md @@ -39,7 +39,7 @@ Configuration parameters: - `LeftNoRebalanceThreshold + RightNoRebalanceThreshold ≤ 1.0` (prevents overlapping shrinkage zones) - `RebalanceQueueCapacity > 0` (when specified) -**Invariants**: E.34, E.35 (NoRebalanceRange computation and threshold sum constraint). +**Invariants**: E.5, E.6 (NoRebalanceRange computation and threshold sum constraint). ### UserCacheReadMode @@ -162,10 +162,10 @@ Composes `GetDataAsync` + conditional `WaitForIdleAsync` into a single call. Wai - Lower overhead than `GetDataAndWaitForIdleAsync` for workloads with frequent `FullHit` results **When NOT to use:** -- Parallel callers — the "warm cache after await" guarantee requires serialized (one-at-a-time) access (Invariant H.49) +- Parallel callers — the "warm cache after await" guarantee requires serialized (one-at-a-time) access (Invariant H.3) - Hot paths — even though `FullHit` skips the wait, missed requests still incur the full rebalance cycle delay -**Idle semantics**: Inherits "was idle at some point" semantics from `WaitForIdleAsync` (Invariant H.49). +**Idle semantics**: Inherits "was idle at some point" semantics from `WaitForIdleAsync` (Invariant H.3). **Exception propagation**: If `GetDataAsync` throws, `WaitForIdleAsync` is never called. If `WaitForIdleAsync` throws `OperationCanceledException`, the already-obtained result is returned (graceful degradation to eventual consistency). Other exceptions from `WaitForIdleAsync` propagate normally. @@ -190,7 +190,7 @@ Composes `GetDataAsync` + `WaitForIdleAsync` into a single call. Always waits fo - Rapid sequential requests — eliminates debounce and work-avoidance benefits - Parallel callers — same serialized access requirement as `GetDataAndWaitOnMissAsync` -**Idle semantics**: Inherits "was idle at some point" semantics from `WaitForIdleAsync` (Invariant H.49). Unlike `GetDataAndWaitOnMissAsync`, always waits even on `FullHit`. +**Idle semantics**: Inherits "was idle at some point" semantics from `WaitForIdleAsync` (Invariant H.3). Unlike `GetDataAndWaitOnMissAsync`, always waits even on `FullHit`. **Exception propagation**: If `GetDataAsync` throws, `WaitForIdleAsync` is never called. If `WaitForIdleAsync` throws `OperationCanceledException`, the already-obtained result is returned (graceful degradation to eventual consistency). Other exceptions from `WaitForIdleAsync` propagate normally. diff --git a/docs/components/rebalance-path.md b/docs/components/rebalance-path.md index 78edb63..cf379b4 100644 --- a/docs/components/rebalance-path.md +++ b/docs/components/rebalance-path.md @@ -36,7 +36,7 @@ These are distinct concerns with separate components: | **Nature** | CPU-only, pure, deterministic | Debounced, cancellable, may do I/O | | **State access** | Read-only | Write (sole) | | **I/O** | Never | Yes (`IDataSource.FetchAsync`) | -| **Invariants** | D.25, D.26, D.27, D.28, D.29 | A.7, B.12, B.13, F.35, F.37–F.39 | +| **Invariants** | D.1, D.2, D.3, D.4, D.5 | A.12a, F.2, B.2, B.3, F.1, F.3–F.5 | The formal 5-stage validation pipeline is specified in `docs/invariants.md` (Section D). @@ -77,21 +77,22 @@ The decision about *whether* to cancel is made by `RebalanceDecisionEngine` (via | Invariant | Description | |-----------|----------------------------------------------------------------| -| A.7 | Only `RebalanceExecutor` writes `CacheState` | -| B.12 | Atomic cache updates via `Rematerialize` | -| B.13 | Consistency under cancellation (discard, never partial-apply) | -| B.15 | Cache contiguity maintained after every rematerialization | -| C.19 | Cooperative cancellation via `CancellationToken` | -| C.20 | Cancellation checked after debounce, before execution | -| C.21 | At most one active rebalance scheduled at a time | -| D.25 | Decision path is purely analytical (no I/O, no state mutation) | -| D.26 | Decision never mutates cache state | -| D.27 | No rebalance if inside current NoRebalanceRange (Stage 1) | -| D.28 | No rebalance if DesiredRange == CurrentRange (Stage 4) | -| D.29 | Execution proceeds only if ALL 5 stages pass | -| F.35 | Multiple cancellation checkpoints in execution | -| F.35a | Cancellation-before-mutation guarantee | -| F.37–F.39 | Correct atomic rematerialization with data preservation | +| A.12a | Only `RebalanceExecutor` writes `CacheState` (exclusive authority) | +| F.2 | Rebalance Execution is the sole component permitted to mutate cache state | +| B.2 | Atomic cache updates via `Rematerialize` | +| B.3 | Consistency under cancellation (discard, never partial-apply) | +| B.5 | Cancelled rebalance execution cannot violate cache consistency | +| C.3 | Cooperative cancellation via `CancellationToken` | +| C.4 | Cancellation checked after debounce, before execution | +| C.5 | At most one active rebalance scheduled at a time | +| D.1 | Decision path is purely analytical (no I/O, no state mutation) | +| D.2 | Decision never mutates cache state | +| D.3 | No rebalance if inside current NoRebalanceRange (Stage 1) | +| D.4 | No rebalance if DesiredRange == CurrentRange (Stage 4) | +| D.5 | Execution proceeds only if ALL 5 stages pass | +| F.1 | Multiple cancellation checkpoints in execution | +| F.1a | Cancellation-before-mutation guarantee | +| F.3–F.5 | Correct atomic rematerialization with data preservation | See `docs/invariants.md` (Sections B, C, D, F) for full specification. diff --git a/docs/components/state-and-storage.md b/docs/components/state-and-storage.md index 5627811..af6cc88 100644 --- a/docs/components/state-and-storage.md +++ b/docs/components/state-and-storage.md @@ -25,7 +25,7 @@ State and storage define how cached data is held, read, and published. `CacheSta | `IsInitialized` | `bool` | `RebalanceExecutor` only | `UserRequestHandler` | | `NoRebalanceRange` | `Range?` | `RebalanceExecutor` only | `DecisionEngine` | -**Single-Writer Rule (Invariant A.7):** Only `RebalanceExecutor` writes any field of `CacheState`. User path components are read-only. This is enforced by internal visibility modifiers (setters are `internal`), not by locks. +**Single-Writer Rule (Invariants A.12a, F.2):** Only `RebalanceExecutor` writes any field of `CacheState`. User path components are read-only. This is enforced by internal visibility modifiers (setters are `internal`), not by locks. **Visibility model:** `CacheState` itself has no locks. Cross-thread visibility for `IsInitialized` and `NoRebalanceRange` is provided by the single-writer architecture — only one background thread ever writes these fields, and readers accept eventual consistency. Storage-level thread safety is handled inside each `ICacheStorage` implementation: `SnapshotReadStorage` uses a `volatile` array field with release/acquire fence ordering; `CopyOnReadStorage` uses a `lock` for its active-buffer swap and all reads. @@ -106,15 +106,16 @@ RebalanceExecutor ──writes──▶ CacheState.Storage.Rematerialize() | Invariant | Description | |-----------|----------------------------------------------------------------------| -| A.7 | Only `RebalanceExecutor` writes `CacheState` | -| A.9 | `IsInitialized` only transitions false → true (monotonic) | -| B.11 | Cache is always contiguous (no gaps in cached range) | -| B.12 | Cache updates are atomic via `Rematerialize` | -| B.13 | Consistency under cancellation: partial results discarded | -| B.15 | Cache contiguity invariant maintained after every rematerialization | -| E.34 | `NoRebalanceRange` is computed correctly from thresholds | -| E.35 | `NoRebalanceRange` is always contained within `CacheRange` | -| F.37 | `Rematerialize` accepts arbitrary range and replaces entire contents | +| A.11 | User Path does not mutate `CacheState` (read-only) | +| A.12a | Only `RebalanceExecutor` writes `CacheState` (exclusive authority) | +| A.12b | Cache is always contiguous (no gaps in cached range) | +| B.1 | `CacheData` and `CurrentCacheRange` are always consistent | +| B.2 | Cache updates are atomic via `Rematerialize` | +| B.3 | Consistency under cancellation: partial results discarded | +| B.5 | Cancelled rebalance execution cannot violate cache consistency | +| E.5 | `NoRebalanceRange` is derived from `CurrentCacheRange` and config | +| F.2 | Rebalance Execution is the sole authority for all cache mutations | +| F.3 | `Rematerialize` accepts arbitrary range and replaces entire contents | See `docs/invariants.md` (Sections A, B, E, F) for full specification. diff --git a/docs/components/user-path.md b/docs/components/user-path.md index dc44db7..95888b3 100644 --- a/docs/components/user-path.md +++ b/docs/components/user-path.md @@ -48,14 +48,14 @@ All user-path code executes on the **⚡ User Thread** (the caller's thread). No | Invariant | Description | |-----------|----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------| -| A.0 | User requests always served immediately (never blocked by rebalance) | -| A.3 | `UserRequestHandler` is the sole publisher of rebalance intents | -| A.4 | Intent publication is fire-and-forget (background only) | -| A.5 | User path is strictly read-only w.r.t. `CacheState` | +| A.3 | User requests always served immediately (never blocked by rebalance) | +| A.5 | `UserRequestHandler` is the sole publisher of rebalance intents | +| A.6 | Intent publication is fire-and-forget (background only) | +| A.11/A.12 | User path is strictly read-only w.r.t. `CacheState` | | A.10 | Returns exactly `RequestedRange` data | | A.10a | `RangeResult` contains `Range`, `Data`, and `CacheInteraction` — all set by `UserRequestHandler` | | A.10b | `CacheInteraction` accurately reflects the cache scenario: `FullMiss` (cold start / jump), `FullHit` (fully cached), `PartialHit` (partial overlap) | -| G.45 | I/O isolation: `IDataSource` called on user's behalf from User Thread (partial hits) or Background Thread (rebalance execution); shared `CacheDataExtensionService` used by both paths | +| G.3 | I/O isolation: `IDataSource` called on user's behalf from User Thread (partial hits) or Background Thread (rebalance execution); shared `CacheDataExtensionService` used by both paths | See `docs/invariants.md` (Section A: User Path invariants) for full specification. diff --git a/docs/diagnostics.md b/docs/diagnostics.md index 774c3b4..952e5fc 100644 --- a/docs/diagnostics.md +++ b/docs/diagnostics.md @@ -210,7 +210,7 @@ Assert.Equal(1, diagnostics.UserRequestServed); **Tracks:** Cache expansion during partial cache hit **Location:** `CacheDataExtensionService.CalculateMissingRanges` (intersection path) **Scenarios:** User Scenario U4 (partial cache hit) -**Invariant:** Invariant 9a (Cache Contiguity Rule - preserves contiguity) +**Invariant:** Invariant A.12b (Cache Contiguity Rule - preserves contiguity) **Interpretation:** Number of times cache grew while maintaining contiguity **Example Usage:** @@ -230,7 +230,7 @@ Assert.Equal(1, diagnostics.CacheExpanded); **Tracks:** Cache replacement during non-intersecting jump **Location:** `CacheDataExtensionService.CalculateMissingRanges` (no intersection path) **Scenarios:** User Scenario U5 (full cache miss - jump) -**Invariant:** Invariant 9a (Cache Contiguity Rule - prevents gaps) +**Invariant:** Invariant A.12b (Cache Contiguity Rule - prevents gaps) **Interpretation:** Number of times cache was fully replaced to maintain contiguity **Example Usage:** @@ -349,7 +349,7 @@ Assert.Equal(1, diagnostics.DataSourceFetchMissingSegments); **Tracks:** A fetched chunk returned a `null` Range — the requested segment does not exist in the data source **Location:** `CacheDataExtensionService.UnionAll` (when a `RangeChunk.Range` is null) **Context:** User Thread (Partial Cache Hit — Scenario 3) **and** Background Thread (Rebalance Execution) -**Invariants:** G.48 (IDataSource Boundary Semantics), A.9a (Cache Contiguity) +**Invariants:** G.5 (IDataSource Boundary Semantics), A.12b (Cache Contiguity) **Interpretation:** Physical boundary encountered; the unavailable segment is silently skipped to preserve cache contiguity **Typical Scenarios:** @@ -380,7 +380,7 @@ Assert.Equal(Range.Closed(1000, 1500), result.Range); #### `RebalanceIntentPublished()` **Tracks:** Rebalance intent publication by User Path **Location:** `IntentController.PublishIntent` (after scheduler receives intent) -**Invariants:** A.3 (User Path is sole source of intent), 24e (Intent contains delivered data) +**Invariants:** A.5 (User Path is sole source of intent), C.8e (Intent contains delivered data) **Note:** Intent publication does NOT guarantee execution (opportunistic) **Example Usage:** @@ -396,7 +396,7 @@ Assert.Equal(1, diagnostics.RebalanceIntentPublished); #### `RebalanceIntentCancelled()` **Tracks:** Intent cancellation before or during execution **Location:** `IntentController.ProcessIntentsAsync` (background loop — when new intent supersedes pending intent) -**Invariants:** A.0 (User Path priority), A.0a (User cancels rebalance), C.20 (Obsolete intent doesn't start) +**Invariants:** A.2 (User Path priority), A.2a (User cancels rebalance), C.4 (Obsolete intent doesn't start) **Interpretation:** Single-flight execution - new request cancels previous intent **Example Usage:** @@ -424,7 +424,7 @@ Assert.True(diagnostics.RebalanceIntentCancelled >= 1); **Tracks:** Rebalance execution start after decision approval **Location:** `IntentController.ProcessIntentsAsync` (after `RebalanceDecisionEngine` approves execution) **Scenarios:** Decision Scenario D3 (rebalance required) -**Invariant:** 28 (Rebalance triggered only if confirmed necessary) +**Invariant:** D.5 (Rebalance triggered only if confirmed necessary) **Example Usage:** ```csharp @@ -440,7 +440,7 @@ Assert.Equal(1, diagnostics.RebalanceExecutionStarted); **Tracks:** Successful rebalance completion **Location:** `RebalanceExecutor.ExecuteAsync` (after UpdateCacheState) **Scenarios:** Rebalance Scenarios R1, R2 (build from scratch, expand cache) -**Invariants:** 34 (Only Rebalance writes to cache), 35 (Atomic state update) +**Invariants:** F.2 (Only Rebalance writes to cache), B.2 (Cache updates are atomic) **Example Usage:** ```csharp @@ -455,7 +455,7 @@ Assert.Equal(1, diagnostics.RebalanceExecutionCompleted); #### `RebalanceExecutionCancelled()` **Tracks:** Rebalance cancellation mid-flight **Location:** `RebalanceExecutor.ExecuteAsync` (catch `OperationCanceledException`) -**Invariant:** 34a (Rebalance yields to User Path immediately) +**Invariant:** F.1a (Rebalance yields to User Path immediately) **Interpretation:** User Path priority enforcement - rebalance interrupted **Example Usage:** @@ -575,7 +575,7 @@ Assert.Equal(1, diagnostics.RebalanceExecutionFailed); **Tracks:** Rebalance skipped — last requested position is within the current `NoRebalanceRange` **Location:** `RebalanceDecisionEngine.Evaluate` (Stage 1 early exit) **Scenarios:** Decision Scenario D1 (inside current no-rebalance threshold) -**Invariants:** D.26 (No rebalance if inside NoRebalanceRange), D.27 (Policy-based skip) +**Invariants:** D.3 (No rebalance if inside NoRebalanceRange), C.8b (RebalanceSkippedNoRebalanceRange counter semantics) **Example Usage:** ```csharp @@ -601,7 +601,7 @@ Assert.True(diagnostics.RebalanceSkippedCurrentNoRebalanceRange >= 1); **Tracks:** Rebalance skipped — last requested position is within the *pending* (desired) `NoRebalanceRange` of an already-scheduled execution **Location:** `RebalanceDecisionEngine.Evaluate` (Stage 2 early exit) **Scenarios:** Decision Scenario D2 (pending rebalance covers the request — anti-thrashing) -**Invariants:** D.26a (No rebalance if pending rebalance covers request) +**Invariants:** D.2a (No rebalance if pending rebalance covers request) **Example Usage:** ```csharp @@ -621,7 +621,7 @@ Assert.True(diagnostics.RebalanceSkippedPendingNoRebalanceRange >= 1); **Tracks:** Rebalance skipped because desired cache range equals current cache range **Location:** `RebalanceDecisionEngine.Evaluate` (Stage 4 early exit) **Scenarios:** Decision Scenario D3 (DesiredCacheRange == CurrentCacheRange) -**Invariants:** D.27 (No rebalance if same range), D.28 (Same-range optimization) +**Invariants:** D.4 (No rebalance if same range), C.8c (RebalanceSkippedSameRange counter semantics) **Example Usage:** ```csharp @@ -639,7 +639,7 @@ Assert.True(diagnostics.RebalanceSkippedSameRange >= 0); // May or may not occur **Tracks:** Rebalance execution successfully scheduled after all decision stages approved **Location:** `IntentController.ProcessIntentsAsync` (Stage 5 — after `RebalanceDecisionEngine` returns `ShouldSchedule=true`) **Scenarios:** Decision Scenario D4 (rebalance required) -**Invariant:** D.28 (Rebalance triggered only if confirmed necessary) +**Invariant:** D.5 (Rebalance triggered only if confirmed necessary) **Example Usage:** ```csharp diff --git a/docs/glossary.md b/docs/glossary.md index f01dd7a..856dd63 100644 --- a/docs/glossary.md +++ b/docs/glossary.md @@ -107,7 +107,7 @@ AsyncActivityCounter WaitForIdleAsync (“Was Idle” Semantics) - Completes when the system was idle at some point, which is appropriate for tests and convergence checks. - It does not guarantee the system is still idle after the task completes. -- Under serialized (one-at-a-time) access this is sufficient for hybrid and strong consistency guarantees. Under parallel access the guarantee degrades: a caller may observe an already-completed (stale) idle TCS if another thread incremented the activity counter between the 0→1 transition and the new TCS publication. See Invariant H.49 and `docs/architecture.md`. +- Under serialized (one-at-a-time) access this is sufficient for hybrid and strong consistency guarantees. Under parallel access the guarantee degrades: a caller may observe an already-completed (stale) idle TCS if another thread incremented the activity counter between the 0→1 transition and the new TCS publication. See Invariant H.3 and `docs/architecture.md`. CacheInteraction - A per-request classification set on every `RangeResult` by `UserRequestHandler`, indicating how the cache contributed to serving the request. @@ -126,7 +126,7 @@ Hybrid Consistency Mode Serialized Access - An access pattern in which calls to a cache are issued one at a time (each call completes before the next begins). - Required for the `GetDataAndWaitOnMissAsync` and `GetDataAndWaitForIdleAsync` extension methods to provide their “cache has converged” guarantee. -- Under parallel access the extension methods remain safe (no deadlocks or data corruption) but the idle-wait may return early due to `AsyncActivityCounter`’s “was idle at some point” semantics (see Invariant H.49). +- Under parallel access the extension methods remain safe (no deadlocks or data corruption) but the idle-wait may return early due to `AsyncActivityCounter`’s “was idle at some point” semantics (see Invariant H.3). GetDataAndWaitOnMissAsync - Extension method on `IWindowCache` providing hybrid consistency mode. diff --git a/docs/invariants.md b/docs/invariants.md index 80f7028..97ccb13 100644 --- a/docs/invariants.md +++ b/docs/invariants.md @@ -4,7 +4,7 @@ ## Understanding This Document -This document lists **54 system invariants** that define the behavior, architecture, and design intent of the Sliding Window Cache. +This document lists **56 system invariants** that define the behavior, architecture, and design intent of the Sliding Window Cache. ### Invariant Categories @@ -148,7 +148,7 @@ without polling or timing dependencies. ### A.1 Concurrency & Priority -**A.-1** 🔵 **[Architectural]** The User Path and Rebalance Execution **never write to cache concurrently**. +**A.1** 🔵 **[Architectural]** The User Path and Rebalance Execution **never write to cache concurrently**. **Formal Specification:** - At any point in time, at most one component has write permission to CacheState @@ -159,7 +159,7 @@ without polling or timing dependencies. **Implementation:** See `docs/components/overview.md` and `docs/architecture.md` for enforcement mechanism details. -**A.0** 🔵 **[Architectural]** The User Path **always has higher priority** than Rebalance Execution. +**A.2** 🔵 **[Architectural]** The User Path **always has higher priority** than Rebalance Execution. **Formal Specification:** - User requests take precedence over background rebalance operations @@ -170,7 +170,7 @@ without polling or timing dependencies. **Implementation:** See `docs/architecture.md` and `docs/components/execution.md` for enforcement mechanism details. -**A.0a** 🟢 **[Behavioral — Test: `Invariant_A_0a_UserRequestCancelsRebalance`]** A User Request **MAY cancel** an ongoing or pending Rebalance Execution **ONLY when a new rebalance is validated as necessary** by the multi-stage decision pipeline. +**A.2a** 🟢 **[Behavioral — Test: `Invariant_A_2a_UserRequestCancelsRebalance`]** A User Request **MAY cancel** an ongoing or pending Rebalance Execution **ONLY when a new rebalance is validated as necessary** by the multi-stage decision pipeline. **Formal Specification:** - Cancellation is a coordination mechanism, not a decision mechanism @@ -185,20 +185,20 @@ without polling or timing dependencies. ### A.2 User-Facing Guarantees -**A.1** 🟢 **[Behavioral — Test: `Invariant_A2_1_UserPathAlwaysServesRequests`]** The User Path **always serves user requests** regardless of the state of rebalance execution. +**A.3** 🟢 **[Behavioral — Test: `Invariant_A_3_UserPathAlwaysServesRequests`]** The User Path **always serves user requests** regardless of the state of rebalance execution. - *Observable via*: Public API always returns data successfully - *Test verifies*: Multiple requests all complete and return correct data -**A.2** 🟢 **[Behavioral — Test: `Invariant_A2_2_UserPathNeverWaitsForRebalance`]** The User Path **never waits for rebalance execution** to complete. +**A.4** 🟢 **[Behavioral — Test: `Invariant_A_4_UserPathNeverWaitsForRebalance`]** The User Path **never waits for rebalance execution** to complete. - *Observable via*: Request completion time vs. debounce delay - *Test verifies*: Request completes in <500ms with 1-second debounce - *Conditional compliance*: `CopyOnReadStorage` acquires a short-lived `_lock` in `Read()` and `ToRangeData()`, shared with `Rematerialize()`. The lock is held only for the buffer swap and `Range` update (in `Rematerialize()`), or for the duration of the array copy (in `Read()` and `ToRangeData()`). All contention is sub-millisecond and bounded. `SnapshotReadStorage` remains - fully lock-free. See [Storage Strategies Guide](storage-strategies.md#invariant-a2---user-path-never-waits-for-rebalance-conditional-compliance) for details. + fully lock-free. See [Storage Strategies Guide](storage-strategies.md#invariant-a4---user-path-never-waits-for-rebalance-conditional-compliance) for details. -**A.3** 🔵 **[Architectural]** The User Path is the **sole source of rebalance intent**. +**A.5** 🔵 **[Architectural]** The User Path is the **sole source of rebalance intent**. **Formal Specification:** - Only User Path publishes rebalance intents @@ -209,7 +209,7 @@ without polling or timing dependencies. **Implementation:** See `docs/components/user-path.md` for enforcement mechanism details. -**A.4** 🔵 **[Architectural]** Rebalance execution is **always performed asynchronously** relative to the User Path. +**A.6** 🔵 **[Architectural]** Rebalance execution is **always performed asynchronously** relative to the User Path. **Formal Specification:** - User requests return immediately without waiting for rebalance completion @@ -220,7 +220,7 @@ without polling or timing dependencies. **Implementation:** See `docs/architecture.md` and `docs/components/execution.md` for enforcement mechanism details. -**A.5** 🔵 **[Architectural]** The User Path performs **only the work necessary to return data to the user**. +**A.7** 🔵 **[Architectural]** The User Path performs **only the work necessary to return data to the user**. **Formal Specification:** - User Path does minimal work: assemble data, return to user @@ -231,11 +231,11 @@ without polling or timing dependencies. **Implementation:** See `docs/components/user-path.md` for enforcement mechanism details. -**A.6** 🟡 **[Conceptual]** The User Path may synchronously request data from `IDataSource` in the user execution context if needed to serve `RequestedRange`. +**A.8** 🟡 **[Conceptual]** The User Path may synchronously request data from `IDataSource` in the user execution context if needed to serve `RequestedRange`. - *Design decision*: Prioritizes user-facing latency over background work - *Rationale*: User must get data immediately; background prefetch is opportunistic -**A.10** 🟢 **[Behavioral — Test: `Invariant_A2_10_UserAlwaysReceivesExactRequestedRange`]** The User always receives data **exactly corresponding to `RequestedRange`**. +**A.10** 🟢 **[Behavioral — Test: `Invariant_A_10_UserAlwaysReceivesExactRequestedRange`]** The User always receives data **exactly corresponding to `RequestedRange`**. - *Observable via*: Returned data length and content - *Test verifies*: Data matches requested range exactly (no more, no less) @@ -270,7 +270,7 @@ without polling or timing dependencies. ### A.3 Cache Mutation Rules (User Path) -**A.7** 🔵 **[Architectural]** The User Path may read from cache and `IDataSource` but **does not mutate cache state**. +**A.11** 🔵 **[Architectural]** The User Path may read from cache and `IDataSource` but **does not mutate cache state**. **Formal Specification:** - User Path has read-only access to cache state @@ -281,7 +281,7 @@ without polling or timing dependencies. **Implementation:** See `docs/architecture.md` and `docs/components/overview.md` for enforcement mechanism details. -**A.8** 🔵 **[Architectural — Tests: `Invariant_A3_8_ColdStart`, `_CacheExpansion`, `_FullCacheReplacement`]** The User Path **MUST NOT mutate cache under any circumstance**. +**A.12** 🔵 **[Architectural — Tests: `Invariant_A_12_ColdStart`, `_CacheExpansion`, `_FullCacheReplacement`]** The User Path **MUST NOT mutate cache under any circumstance**. **Formal Specification:** - User Path is strictly read-only with respect to cache state @@ -293,7 +293,7 @@ without polling or timing dependencies. **Implementation:** See `docs/architecture.md` and `docs/components/overview.md` for enforcement mechanism details. -**A.9** 🔵 **[Architectural]** Cache mutations are performed **exclusively by Rebalance Execution** (single-writer architecture). +**A.12a** 🔵 **[Architectural]** Cache mutations are performed **exclusively by Rebalance Execution** (single-writer architecture). **Formal Specification:** - Only one component has permission to write to cache state @@ -304,7 +304,7 @@ without polling or timing dependencies. **Implementation:** See `docs/architecture.md` and `docs/components/overview.md` for enforcement mechanism details. -**A.9a** 🟢 **[Behavioral — Test: `Invariant_A3_9a_CacheContiguityMaintained`]** **Cache Contiguity Rule:** `CacheData` **MUST always remain contiguous** — gapped or partially materialized cache states are invalid. +**A.12b** 🟢 **[Behavioral — Test: `Invariant_A_12b_CacheContiguityMaintained`]** **Cache Contiguity Rule:** `CacheData` **MUST always remain contiguous** — gapped or partially materialized cache states are invalid. - *Observable via*: All requests return valid contiguous data - *Test verifies*: Sequential overlapping requests all succeed @@ -312,11 +312,11 @@ without polling or timing dependencies. ## B. Cache State & Consistency Invariants -**B.11** 🟢 **[Behavioral — Test: `Invariant_B11_CacheDataAndRangeAlwaysConsistent`]** `CacheData` and `CurrentCacheRange` are **always consistent** with each other. +**B.1** 🟢 **[Behavioral — Test: `Invariant_B_1_CacheDataAndRangeAlwaysConsistent`]** `CacheData` and `CurrentCacheRange` are **always consistent** with each other. - *Observable via*: Data length always matches range size - *Test verifies*: For any request, returned data length matches expected range size -**B.12** 🔵 **[Architectural]** Changes to `CacheData` and the corresponding `CurrentCacheRange` are performed **atomically**. +**B.2** 🔵 **[Architectural]** Changes to `CacheData` and the corresponding `CurrentCacheRange` are performed **atomically**. **Formal Specification:** - Cache data and range updates are indivisible operations @@ -327,7 +327,7 @@ without polling or timing dependencies. **Implementation:** See `docs/invariants.md` (atomicity invariants) and source XML docs; architecture context in `docs/architecture.md`. -**B.13** 🔵 **[Architectural]** The system **never enters a permanently inconsistent state** with respect to `CacheData ↔ CurrentCacheRange`. +**B.3** 🔵 **[Architectural]** The system **never enters a permanently inconsistent state** with respect to `CacheData ↔ CurrentCacheRange`. **Formal Specification:** - Cache data always matches its declared range @@ -338,15 +338,15 @@ without polling or timing dependencies. **Implementation:** See `docs/architecture.md` and execution invariants in `docs/invariants.md`. -**B.14** 🟡 **[Conceptual]** Temporary geometric or coverage inefficiencies in the cache are acceptable **if they can be resolved by rebalance execution**. +**B.4** 🟡 **[Conceptual]** Temporary geometric or coverage inefficiencies in the cache are acceptable **if they can be resolved by rebalance execution**. - *Design decision*: User Path prioritizes speed over optimal cache shape - *Rationale*: Background rebalance will normalize; temporary inefficiency is acceptable -**B.15** 🟢 **[Behavioral — Test: `Invariant_B15_CancelledRebalanceDoesNotViolateConsistency`]** Partially executed or cancelled rebalance execution **cannot violate `CacheData ↔ CurrentCacheRange` consistency**. +**B.5** 🟢 **[Behavioral — Test: `Invariant_B_5_CancelledRebalanceDoesNotViolateConsistency`]** Partially executed or cancelled rebalance execution **cannot violate `CacheData ↔ CurrentCacheRange` consistency**. - *Observable via*: Cache continues serving valid data after cancellation - *Test verifies*: Rapid request changes don't corrupt cache -**B.16** 🔵 **[Architectural]** Results from rebalance execution are applied **only if they correspond to the latest active rebalance intent**. +**B.6** 🔵 **[Architectural]** Results from rebalance execution are applied **only if they correspond to the latest active rebalance intent**. **Formal Specification:** - Obsolete rebalance results are discarded @@ -361,7 +361,7 @@ without polling or timing dependencies. ## C. Rebalance Intent & Temporal Invariants -**C.17** 🔵 **[Architectural]** At most one rebalance intent may be active at any time. +**C.1** 🔵 **[Architectural]** At most one rebalance intent may be active at any time. **Formal Specification:** - System maintains at most one pending rebalance intent @@ -372,11 +372,11 @@ without polling or timing dependencies. **Implementation:** See `docs/components/intent-management.md`. -**C.18** 🟡 **[Conceptual]** Previously created intents may become **logically superseded** when a new intent is published, but rebalance execution relevance is determined by the **multi-stage rebalance validation logic**. +**C.2** 🟡 **[Conceptual]** Previously created intents may become **logically superseded** when a new intent is published, but rebalance execution relevance is determined by the **multi-stage rebalance validation logic**. - *Design intent*: Obsolescence ≠ cancellation; obsolescence ≠ guaranteed execution prevention - *Clarification*: Intents are access signals, not commands. An intent represents "user accessed this range," not "must execute rebalance." Execution decisions are governed by the Rebalance Decision Engine's analytical validation (Stage 1: Current Cache NoRebalanceRange check, Stage 2: Pending Desired Cache NoRebalanceRange check if applicable, Stage 3: DesiredCacheRange vs CurrentCacheRange equality check). Previously created intents may be superseded or cancelled, but the decision to execute is always based on current validation state, not intent age. Cancellation occurs ONLY when Decision Engine validation confirms a new rebalance is necessary. -**C.19** 🔵 **[Architectural]** Any rebalance execution can be **cancelled or have its results ignored**. +**C.3** 🔵 **[Architectural]** Any rebalance execution can be **cancelled or have its results ignored**. **Formal Specification:** - Rebalance operations are interruptible @@ -387,7 +387,7 @@ without polling or timing dependencies. **Implementation:** See `docs/architecture.md` and `docs/components/intent-management.md`. -**C.20** 🔵 **[Architectural]** If a rebalance intent becomes obsolete before execution begins, the execution **must not start**. +**C.4** 🔵 **[Architectural]** If a rebalance intent becomes obsolete before execution begins, the execution **must not start**. **Formal Specification:** - Obsolete rebalance operations must not execute @@ -398,7 +398,7 @@ without polling or timing dependencies. **Implementation:** See `docs/components/decision.md` and decision invariants in `docs/invariants.md`. -**C.21** 🔵 **[Architectural]** At any point in time, **at most one rebalance execution is active**. +**C.5** 🔵 **[Architectural]** At any point in time, **at most one rebalance execution is active**. **Formal Specification:** - Only one rebalance operation executes at a time @@ -409,15 +409,15 @@ without polling or timing dependencies. **Implementation:** See `docs/architecture.md` (execution strategies) and `docs/components/execution.md`. -**C.22** 🟡 **[Conceptual]** The results of rebalance execution **always reflect the latest user access pattern**. +**C.6** 🟡 **[Conceptual]** The results of rebalance execution **always reflect the latest user access pattern**. - *Design guarantee*: Obsolete results are discarded - *Rationale*: System converges to user's actual navigation pattern -**C.23** 🟢 **[Behavioral — Test: `Invariant_C23_SystemStabilizesUnderLoad`]** During spikes of user requests, the system **eventually stabilizes** to a consistent cache state. +**C.7** 🟢 **[Behavioral — Test: `Invariant_C_7_SystemStabilizesUnderLoad`]** During spikes of user requests, the system **eventually stabilizes** to a consistent cache state. - *Observable via*: After burst of requests, system serves data correctly - *Test verifies*: Rapid burst + wait → final request succeeds -**C.24** 🟡 **[Conceptual — Test: `Invariant_C24_IntentDoesNotGuaranteeExecution`]** **Intent does not guarantee execution. Execution is opportunistic and may be skipped entirely.** +**C.8** 🟡 **[Conceptual — Test: `Invariant_C_8_IntentDoesNotGuaranteeExecution`]** **Intent does not guarantee execution. Execution is opportunistic and may be skipped entirely.** - Publishing an intent does NOT guarantee that rebalance will execute - Execution may be cancelled before starting (due to new intent) - Execution may be cancelled during execution (User Path priority) @@ -426,7 +426,15 @@ without polling or timing dependencies. - *Design decision*: Rebalance is opportunistic, not mandatory - *Test note*: Test verifies skip behavior exists, but non-execution is acceptable -**C.24e** 🔵 **[Architectural]** Intent **MUST contain delivered data** representing what was actually returned to the user for the requested range. +**C.8a** 🟢 **[Behavioral]** Intent delivery and cache interaction classification are coupled: intent MUST be published with the actual `CacheInteraction` value for the served request. + +**C.8b** 🟢 **[Behavioral]** `RebalanceSkippedNoRebalanceRange` counter increments when execution is skipped because `RequestedRange ⊆ NoRebalanceRange`. + +**C.8c** 🟢 **[Behavioral]** `RebalanceSkippedSameRange` counter increments when execution is skipped because `DesiredCacheRange == CurrentCacheRange`. + +**C.8d** 🟢 **[Behavioral]** Execution is skipped when cancelled before it starts (not counted in skip counters; counted in cancellation counters). + +**C.8e** 🔵 **[Architectural]** Intent **MUST contain delivered data** representing what was actually returned to the user for the requested range. **Formal Specification:** - Intent includes actual data delivered to user @@ -437,7 +445,7 @@ without polling or timing dependencies. **Implementation:** See `docs/components/user-path.md` and intent invariants in `docs/invariants.md`. -**C.24f** 🟡 **[Conceptual]** Delivered data in intent serves as the **authoritative source** for Rebalance Execution, avoiding duplicate fetches and ensuring consistency with user view. +**C.8f** 🟡 **[Conceptual]** Delivered data in intent serves as the **authoritative source** for Rebalance Execution, avoiding duplicate fetches and ensuring consistency with user view. - *Design guarantee*: Rebalance Execution uses delivered data as base, not current cache - *Rationale*: Eliminates redundant IDataSource calls, ensures cache converges to what user received @@ -513,7 +521,7 @@ The system prioritizes **decision correctness and work avoidance** over aggressi **Trade-off:** Slight delay in cache optimization vs. system stability and resource efficiency -**D.25** 🔵 **[Architectural]** The Rebalance Decision Path is **purely analytical** and has **no side effects**. +**D.1** 🔵 **[Architectural]** The Rebalance Decision Path is **purely analytical** and has **no side effects**. **Formal Specification:** - Decision logic is pure: inputs → decision @@ -525,7 +533,7 @@ The system prioritizes **decision correctness and work avoidance** over aggressi **Implementation:** See `docs/components/execution.md`. -**D.26** 🔵 **[Architectural]** The Decision Path **never mutates cache state**. +**D.2** 🔵 **[Architectural]** The Decision Path **never mutates cache state**. **Formal Specification:** - Decision logic has no write access to cache @@ -536,16 +544,28 @@ The system prioritizes **decision correctness and work avoidance** over aggressi **Implementation:** See `docs/architecture.md` and `docs/components/execution.md`. -**D.27** 🟢 **[Behavioral — Test: `Invariant_D27_NoRebalanceIfRequestInNoRebalanceRange`]** If `RequestedRange` is fully contained within `NoRebalanceRange`, **rebalance execution is prohibited**. -- *Observable via*: DEBUG counters showing execution skipped (policy-based, see C.24b) +**D.2a** 🔵 **[Architectural]** Stage 2 (Pending Desired Cache NoRebalanceRange Validation) **MUST evaluate against the pending execution's `DesiredNoRebalanceRange`**, not the current cache's NoRebalanceRange. + +**Formal Specification:** +- Stage 2 reads `lastExecutionRequest?.DesiredNoRebalanceRange` (the NoRebalanceRange that will hold once the pending execution completes) +- If `RequestedRange ⊆ PendingDesiredNoRebalanceRange`, skip rebalance (anti-thrashing) +- This check is skipped if there is no pending execution (`lastExecutionRequest == null`) +- Must NOT fall back to CurrentCacheRange's NoRebalanceRange for this check (that is Stage 1) + +**Rationale:** Prevents oscillation when a rebalance is in-flight: a new intent for a nearby range should not interrupt an already-optimal pending execution. + +**Implementation:** See `RebalanceDecisionEngine` source and `docs/components/decision.md`. + +**D.3** 🟢 **[Behavioral — Test: `Invariant_D_3_NoRebalanceIfRequestInNoRebalanceRange`]** If `RequestedRange` is fully contained within `NoRebalanceRange`, **rebalance execution is prohibited**. +- *Observable via*: DEBUG counters showing execution skipped (policy-based, see C.8b) - *Test verifies*: Request within NoRebalanceRange doesn't trigger execution -**D.28** 🟢 **[Behavioral — Test: `Invariant_D28_SkipWhenDesiredEqualsCurrentRange`]** If `DesiredCacheRange == CurrentCacheRange`, **rebalance execution is not required**. -- *Observable via*: DEBUG counter `RebalanceSkippedSameRange` (optimization-based, see C.24c) +**D.4** 🟢 **[Behavioral — Test: `Invariant_D_4_SkipWhenDesiredEqualsCurrentRange`]** If `DesiredCacheRange == CurrentCacheRange`, **rebalance execution is not required**. +- *Observable via*: DEBUG counter `RebalanceSkippedSameRange` (optimization-based, see C.8c) - *Test verifies*: Repeated request with same range increments skip counter - *Implementation*: Early exit in `RebalanceDecisionEngine.Evaluate` (Stage 4) before execution is scheduled -**D.29** 🔵 **[Architectural]** Rebalance execution is triggered **only if ALL stages of the multi-stage decision pipeline confirm necessity**. +**D.5** 🔵 **[Architectural]** Rebalance execution is triggered **only if ALL stages of the multi-stage decision pipeline confirm necessity**. **Formal Specification:** - Five-stage validation pipeline gates execution @@ -568,11 +588,11 @@ The system prioritizes **decision correctness and work avoidance** over aggressi ## E. Cache Geometry & Policy Invariants -**E.30** 🟢 **[Behavioral — Test: `Invariant_E30_DesiredRangeComputedFromConfigAndRequest`]** `DesiredCacheRange` is computed **solely from `RequestedRange` and cache configuration**. +**E.1** 🟢 **[Behavioral — Test: `Invariant_E_1_DesiredRangeComputedFromConfigAndRequest`]** `DesiredCacheRange` is computed **solely from `RequestedRange` and cache configuration**. - *Observable via*: After rebalance, cache covers expected expanded range - *Test verifies*: With config (leftSize=1.0, rightSize=1.0), cache expands as expected -**E.31** 🔵 **[Architectural]** `DesiredCacheRange` is **independent of the current cache contents**, but may use configuration and `RequestedRange`. +**E.2** 🔵 **[Architectural]** `DesiredCacheRange` is **independent of the current cache contents**, but may use configuration and `RequestedRange`. **Formal Specification:** - Desired range computed only from configuration and requested range @@ -583,15 +603,15 @@ The system prioritizes **decision correctness and work avoidance** over aggressi **Implementation:** See range planner source XML docs; architecture context in `docs/components/decision.md`. -**E.32** 🟡 **[Conceptual]** `DesiredCacheRange` represents the **canonical target state** towards which the system converges. +**E.3** 🟡 **[Conceptual]** `DesiredCacheRange` represents the **canonical target state** towards which the system converges. - *Design concept*: Single source of truth for "what cache should be" - *Rationale*: Ensures deterministic convergence behavior -**E.33** 🟡 **[Conceptual]** The geometry of the sliding window is **determined by configuration**, not by scenario-specific logic. +**E.4** 🟡 **[Conceptual]** The geometry of the sliding window is **determined by configuration**, not by scenario-specific logic. - *Design principle*: Configuration drives behavior, not hard-coded heuristics - *Rationale*: Predictable, user-controllable cache shape -**E.34** 🔵 **[Architectural]** `NoRebalanceRange` is derived **from `CurrentCacheRange` and configuration**. +**E.5** 🔵 **[Architectural]** `NoRebalanceRange` is derived **from `CurrentCacheRange` and configuration**. **Formal Specification:** - No-rebalance range computed from current cache range and threshold configuration @@ -602,7 +622,7 @@ The system prioritizes **decision correctness and work avoidance** over aggressi **Implementation:** See `docs/components/decision.md`. -**E.35** 🟢 **[Behavioral]** When both `LeftThreshold` and `RightThreshold` are specified (non-null), their sum must not exceed 1.0. +**E.6** 🟢 **[Behavioral]** When both `LeftThreshold` and `RightThreshold` are specified (non-null), their sum must not exceed 1.0. **Formal Specification:** ``` @@ -627,7 +647,7 @@ leftThreshold.HasValue && rightThreshold.HasValue ### F.1 Execution Control & Cancellation -**F.35** 🟢 **[Behavioral — Test: `Invariant_F35_G46_RebalanceCancellationBehavior`]** Rebalance Execution **MUST be cancellation-safe** at all stages (before I/O, during I/O, before mutations). +**F.1** 🟢 **[Behavioral — Test: `Invariant_F_1_G_4_RebalanceCancellationBehavior`]** Rebalance Execution **MUST be cancellation-safe** at all stages (before I/O, during I/O, before mutations). - *Observable via*: Lifecycle tracking integrity (Started == Completed + Cancelled), system stability under concurrent requests - *Test verifies*: - Deterministic termination: Every started execution reaches terminal state @@ -635,9 +655,9 @@ leftThreshold.HasValue && rightThreshold.HasValue - Lifecycle integrity: Accounting remains correct under cancellation - *Implementation details*: `ThrowIfCancellationRequested()` at multiple checkpoints in execution pipeline - *Note*: Cancellation is triggered by scheduling decisions (Decision Engine validation), not automatically by user requests -- *Related*: C.24d (execution skipped due to cancellation), A.0a (User Path priority via validation-driven cancellation), G.46 (high-level guarantee) +- *Related*: C.8d (execution skipped due to cancellation), A.2a (User Path priority via validation-driven cancellation), G.4 (high-level guarantee) -**F.35a** 🔵 **[Architectural]** Rebalance Execution **MUST yield** to User Path requests immediately upon cancellation. +**F.1a** 🔵 **[Architectural]** Rebalance Execution **MUST yield** to User Path requests immediately upon cancellation. **Formal Specification:** - Background operations must check for cancellation signals @@ -648,13 +668,13 @@ leftThreshold.HasValue && rightThreshold.HasValue **Implementation:** See `docs/components/execution.md`. -**F.35b** 🟢 **[Behavioral — Covered by `Invariant_B15`]** Partially executed or cancelled Rebalance Execution **MUST NOT leave cache in inconsistent state**. +**F.1b** 🟢 **[Behavioral — Covered by `Invariant_B_5`]** Partially executed or cancelled Rebalance Execution **MUST NOT leave cache in inconsistent state**. - *Observable via*: Cache continues serving valid data after cancellation -- *Same test as B.15* +- *Same test as B.5* ### F.2 Cache Mutation Rules (Rebalance Execution) -**F.36** 🔵 **[Architectural]** The Rebalance Execution Path is the **ONLY component that mutates cache state** (single-writer architecture). +**F.2** 🔵 **[Architectural]** The Rebalance Execution Path is the **ONLY component that mutates cache state** (single-writer architecture). **Formal Specification:** - Only one component has write permission to cache state @@ -665,7 +685,7 @@ leftThreshold.HasValue && rightThreshold.HasValue **Implementation:** See `docs/architecture.md`. -**F.36a** 🟢 **[Behavioral — Test: `Invariant_F36a_RebalanceNormalizesCache`]** Rebalance Execution mutates cache for normalization using **delivered data from intent as authoritative base**: +**F.2a** 🟢 **[Behavioral — Test: `Invariant_F_2a_RebalanceNormalizesCache`]** Rebalance Execution mutates cache for normalization using **delivered data from intent as authoritative base**: - **Uses delivered data** from intent (not current cache) as starting point - **Expanding to DesiredCacheRange** by fetching only truly missing ranges - **Trimming excess data** outside `DesiredCacheRange` @@ -676,7 +696,7 @@ leftThreshold.HasValue && rightThreshold.HasValue - *Test verifies*: Cache covers larger area after rebalance completes - *Single-writer guarantee*: These are the ONLY mutations in the system -**F.37** 🔵 **[Architectural]** Rebalance Execution may **replace, expand, or shrink cache data** to achieve normalization. +**F.3** 🔵 **[Architectural]** Rebalance Execution may **replace, expand, or shrink cache data** to achieve normalization. **Formal Specification:** - Full mutation capability: expand, trim, or replace cache entirely @@ -687,7 +707,7 @@ leftThreshold.HasValue && rightThreshold.HasValue **Implementation:** See `docs/components/execution.md`. -**F.38** 🔵 **[Architectural]** Rebalance Execution requests data from `IDataSource` **only for missing subranges**. +**F.4** 🔵 **[Architectural]** Rebalance Execution requests data from `IDataSource` **only for missing subranges**. **Formal Specification:** - Fetch only gaps between existing cache and desired range @@ -698,7 +718,7 @@ leftThreshold.HasValue && rightThreshold.HasValue **Implementation:** See `docs/components/user-path.md`. -**F.39** 🔵 **[Architectural]** Rebalance Execution **does not overwrite existing data** that intersects with `DesiredCacheRange`. +**F.5** 🔵 **[Architectural]** Rebalance Execution **does not overwrite existing data** that intersects with `DesiredCacheRange`. **Formal Specification:** - Existing cached data is preserved during rebalance @@ -711,15 +731,15 @@ leftThreshold.HasValue && rightThreshold.HasValue ### F.3 Post-Execution Guarantees -**F.40** 🟢 **[Behavioral — Test: `Invariant_F40_F41_F42_PostExecutionGuarantees`]** Upon successful completion, `CacheData` **strictly corresponds to `DesiredCacheRange`**. +**F.6** 🟢 **[Behavioral — Test: `Invariant_F_6_F_7_F_8_PostExecutionGuarantees`]** Upon successful completion, `CacheData` **strictly corresponds to `DesiredCacheRange`**. - *Observable via*: After rebalance, cache serves data from expected normalized range - *Test verifies*: Can read from expected expanded range -**F.41** 🟢 **[Behavioral — Covered by same test as F.40]** Upon successful completion, `CurrentCacheRange == DesiredCacheRange`. +**F.7** 🟢 **[Behavioral — Covered by same test as F.6]** Upon successful completion, `CurrentCacheRange == DesiredCacheRange`. - *Observable indirectly*: Cache behavior matches expected range -- *Same test as F.40* +- *Same test as F.6* -**F.42** 🟡 **[Conceptual — Covered by same test as F.40]** Upon successful completion, `NoRebalanceRange` is **recomputed**. +**F.8** 🟡 **[Conceptual — Covered by same test as F.6]** Upon successful completion, `NoRebalanceRange` is **recomputed**. - *Internal state*: Not directly observable via public API - *Design guarantee*: Threshold zone updated after normalization @@ -727,11 +747,11 @@ leftThreshold.HasValue && rightThreshold.HasValue ## G. Execution Context & Scheduling Invariants -**G.43** 🟢 **[Behavioral — Test: `Invariant_G43_G44_G45_ExecutionContextSeparation`]** The User Path operates in the **user execution context**. +**G.1** 🟢 **[Behavioral — Test: `Invariant_G_1_G_2_G_3_ExecutionContextSeparation`]** The User Path operates in the **user execution context**. - *Observable via*: Request completes quickly without waiting for background work - *Test verifies*: Request time < debounce delay -### G.44: Rebalance Decision Path and Rebalance Execution Path execute outside the user execution context +### G.2: Rebalance Decision Path and Rebalance Execution Path execute outside the user execution context **Formal Specification:** The Rebalance Decision Path and Rebalance Execution Path MUST execute asynchronously outside the user execution context. User requests MUST return immediately without waiting for background analysis or I/O operations. @@ -744,9 +764,9 @@ The Rebalance Decision Path and Rebalance Execution Path MUST execute asynchrono **Rationale:** Ensures user requests remain responsive by offloading all optimization work to background threads. **Implementation:** See `docs/architecture.md`. -- 🔵 **[Architectural — Covered by same test as G.43]** +- 🔵 **[Architectural — Covered by same test as G.1]** -### G.45: I/O responsibilities are separated between User Path and Rebalance Execution Path +### G.3: I/O responsibilities are separated between User Path and Rebalance Execution Path **Formal Specification:** I/O operations (data fetching via IDataSource) are divided by responsibility: @@ -762,19 +782,25 @@ I/O operations (data fetching via IDataSource) are divided by responsibility: **Rationale:** Separates the latency-critical user-serving fetch (minimal, unavoidable) from the background optimization fetch (potentially large, deferrable). User Path I/O is bounded by the requested range; background I/O is bounded by cache geometry policy. **Implementation:** See `docs/architecture.md` and execution invariants. -- 🔵 **[Architectural — Covered by same test as G.43]** - -**G.46** 🟢 **[Behavioral — Tests: `Invariant_G46_UserCancellationDuringFetch`, `Invariant_F35_G46_RebalanceCancellationBehavior`]** Cancellation **must be supported** for all scenarios: -1. **User-facing cancellation**: User-provided CancellationToken propagates through User Path to IDataSource.FetchAsync() -2. **Background rebalance cancellation**: System supports cancellation of pending/ongoing rebalance execution -- *Observable via*: - - User cancellation: OperationCanceledException thrown during IDataSource fetch - - Rebalance cancellation: System stability and lifecycle integrity under concurrent requests -- *Test verifies*: - - `Invariant_G46_UserCancellationDuringFetch`: Cancelling during IDataSource fetch throws OperationCanceledException - - `Invariant_F35_G46_RebalanceCancellationBehavior`: Background rebalance supports cancellation mechanism (high-level guarantee) +- 🔵 **[Architectural — Covered by same test as G.1]** + +**G.4** 🟢 **[Behavioral — Tests: `Invariant_G_4_UserCancellationDuringFetch`, `Invariant_F_1_G_4_RebalanceCancellationBehavior`]** Cancellation **must be supported** for all scenarios: + - `Invariant_G_4_UserCancellationDuringFetch`: Cancelling during IDataSource fetch throws OperationCanceledException + - `Invariant_F_1_G_4_RebalanceCancellationBehavior`: Background rebalance supports cancellation mechanism (high-level guarantee) - *Important*: System does NOT guarantee cancellation on new requests. Cancellation MAY occur depending on Decision Engine scheduling validation. Focus is on system stability and cache consistency, not deterministic cancellation behavior. -- *Related*: F.35 (detailed rebalance execution cancellation mechanics), A.0a (User Path priority via validation-driven cancellation) +- *Related*: F.1 (detailed rebalance execution cancellation mechanics), A.2a (User Path priority via validation-driven cancellation) + +**G.5** 🔵 **[Architectural]** `IDataSource.FetchAsync` **MUST respect boundary semantics**: it may return a range smaller than requested (or null) for bounded data sources, and the cache must propagate this truncated result correctly. + +**Formal Specification:** +- `IDataSource.FetchAsync` returns `RangeData?` — nullable to signal unavailability +- A non-null result MAY have a smaller range than the requested range (partial fulfillment for bounded sources) +- The cache MUST use the actual returned range, not the requested range, when assembling `RangeResult` +- Callers MUST NOT assume the returned range equals the requested range + +**Rationale:** Bounded data sources (e.g., finite files, fixed-size datasets) cannot always fulfill the full requested range. The contract allows graceful truncation without exceptions. + +**Implementation:** See `IDataSource` contract, `UserRequestHandler`, `CacheDataExtensionService`, and [Boundary Handling Guide](boundary-handling.md). --- @@ -791,7 +817,7 @@ The `AsyncActivityCounter` component implements this using lock-free synchroniza ### The Two Critical Invariants -### H.47: Increment-Before-Publish Invariant +### H.1: Increment-Before-Publish Invariant **Formal Specification:** Any operation that schedules, publishes, or enqueues background work MUST increment the activity counter BEFORE making that work visible to consumers (via semaphore signal, channel write, volatile write, or task chain). @@ -810,7 +836,7 @@ When activity counter reaches zero (idle state), NO work exists in any of these **Implementation:** See `src/SlidingWindowCache/Infrastructure/Concurrency/AsyncActivityCounter.cs`. - 🔵 **[Architectural — Enforced by call site ordering]** -### H.48: Decrement-After-Completion Invariant +### H.2: Decrement-After-Completion Invariant **Formal Specification:** Any operation representing completion of background work MUST decrement the activity counter AFTER work is fully completed, cancelled, or failed. Decrement MUST execute unconditionally regardless of success/failure/cancellation path. @@ -829,7 +855,7 @@ Activity counter accurately reflects active work count at all times: **Implementation:** See `src/SlidingWindowCache/Infrastructure/Concurrency/AsyncActivityCounter.cs`. - 🔵 **[Architectural — Enforced by finally blocks]** -**H.49** 🟡 **[Conceptual — Eventual consistency design]** **"Was Idle" Semantics:** +**H.3** 🟡 **[Conceptual — Eventual consistency design]** **"Was Idle" Semantics:** `WaitForIdleAsync()` completes when the system **was idle at some point in time**, NOT when "system is idle now". - *Design rationale*: State-based completion semantics provide eventual consistency @@ -847,7 +873,7 @@ Under parallel access, the methods remain safe (no deadlocks, no crashes, no dat ### Activity-Based Stabilization Barrier -The combination of H.47 and H.48 creates a **stabilization barrier** with strong guarantees: +The combination of H.1 and H.2 creates a **stabilization barrier** with strong guarantees: **Idle state (counter=0) means:** - ✅ No intents being processed @@ -924,19 +950,19 @@ Complete trace demonstrating both invariants in current architecture: ### Relation to Other Invariants -- **A.-1** (Single-Writer Architecture): Activity tracking supports single-writer by tracking execution lifecycle -- **F.35** (Cancellation Support): DecrementActivity in finally blocks ensures counter correctness even on cancellation -- **G.46** (User/Background Cancellation): Activity counter remains balanced regardless of cancellation timing +- **A.1** (Single-Writer Architecture): Activity tracking supports single-writer by tracking execution lifecycle +- **F.1** (Cancellation Support): DecrementActivity in finally blocks ensures counter correctness even on cancellation +- **G.4** (User/Background Cancellation): Activity counter remains balanced regardless of cancellation timing --- ## I. Runtime Options Update Invariants -**I.50** 🟢 **[Behavioral — Tests: `RuntimeOptionsUpdateTests`]** `UpdateRuntimeOptions` **validates the merged options** before publishing. Invalid updates (negative sizes, threshold sum > 1.0, out-of-range threshold) throw and leave the current options unchanged. +**I.1** 🟢 **[Behavioral — Tests: `RuntimeOptionsUpdateTests`]** `UpdateRuntimeOptions` **validates the merged options** before publishing. Invalid updates (negative sizes, threshold sum > 1.0, out-of-range threshold) throw and leave the current options unchanged. - *Observable via*: Exception type and cache still accepts subsequent valid updates - *Test verifies*: `ArgumentOutOfRangeException` / `ArgumentException` thrown; cache not partially updated -**I.51** 🔵 **[Architectural]** `UpdateRuntimeOptions` uses **next-cycle semantics**: the new options snapshot takes effect on the next rebalance decision/execution cycle. Ongoing cycles use the snapshot already read at cycle start. +**I.2** 🔵 **[Architectural]** `UpdateRuntimeOptions` uses **next-cycle semantics**: the new options snapshot takes effect on the next rebalance decision/execution cycle. Ongoing cycles use the snapshot already read at cycle start. **Formal Specification:** - `RuntimeCacheOptionsHolder.Update` performs a `Volatile.Write` (release fence) @@ -947,7 +973,7 @@ Complete trace demonstrating both invariants in current architecture: **Implementation:** `RuntimeCacheOptionsHolder.Update` in `src/SlidingWindowCache/Core/State/RuntimeCacheOptionsHolder.cs`. -**I.52** 🔵 **[Architectural]** `UpdateRuntimeOptions` on a disposed cache **always throws `ObjectDisposedException`**. +**I.3** 🔵 **[Architectural]** `UpdateRuntimeOptions` on a disposed cache **always throws `ObjectDisposedException`**. **Formal Specification:** - Disposal state checked via `Volatile.Read` before any options update work @@ -955,7 +981,7 @@ Complete trace demonstrating both invariants in current architecture: **Implementation:** Disposal guard in `WindowCache.UpdateRuntimeOptions`. -**I.53** 🟡 **[Conceptual]** **`ReadMode` and `RebalanceQueueCapacity` are creation-time only** — they determine the storage strategy and execution controller strategy, which are wired at construction and cannot be replaced at runtime without reconstruction. +**I.4** 🟡 **[Conceptual]** **`ReadMode` and `RebalanceQueueCapacity` are creation-time only** — they determine the storage strategy and execution controller strategy, which are wired at construction and cannot be replaced at runtime without reconstruction. - *Design decision*: These choices affect fundamental system structure (object graph), not just configuration parameters - *Rationale*: Storage strategies and execution controllers have different object identities and lifecycles; hot-swapping them would require disposal and re-creation of component graphs @@ -963,20 +989,20 @@ Complete trace demonstrating both invariants in current architecture: ## Summary Statistics -### Total Invariants: 54 +### Total Invariants: 56 #### By Category: -- 🟢 **Behavioral** (test-covered): 20 invariants -- 🔵 **Architectural** (structure-enforced): 25 invariants +- 🟢 **Behavioral** (test-covered): 21 invariants +- 🔵 **Architectural** (structure-enforced): 26 invariants - 🟡 **Conceptual** (design-level): 9 invariants #### Test Coverage Analysis: - **29 automated tests** in `WindowCacheInvariantTests` -- **20 behavioral invariants** directly covered -- **25 architectural invariants** enforced by code structure (not tested) +- **21 behavioral invariants** directly covered +- **26 architectural invariants** enforced by code structure (not tested) - **9 conceptual invariants** documented as design guidance (not tested) -**This is by design.** The gap between 54 invariants and 29 tests is intentional: +**This is by design.** The gap between 56 invariants and 29 tests is intentional: - Architecture enforces structural constraints automatically - Conceptual invariants guide development, not runtime behavior - Tests focus on externally observable behavior diff --git a/docs/scenarios.md b/docs/scenarios.md index e2ee881..73aea41 100644 --- a/docs/scenarios.md +++ b/docs/scenarios.md @@ -129,7 +129,7 @@ Scenarios are grouped by path: 6. Rebalance intent is published; rebalance executes asynchronously 7. Data is returned to the user — `RangeResult.CacheInteraction == FullMiss` -**Critical**: Partial cache expansion is FORBIDDEN in this case — it would create logical gaps and violate the Cache Contiguity Rule (Invariant A.9a). The cache MUST remain contiguous at all times. +**Critical**: Partial cache expansion is FORBIDDEN in this case — it would create logical gaps and violate the Cache Contiguity Rule (Invariant A.12b). The cache MUST remain contiguous at all times. **Consistency note**: `GetDataAndWaitOnMissAsync` will call `WaitForIdleAsync` after this scenario (because `CacheInteraction != FullHit`), waiting for the background rebalance to complete. diff --git a/docs/state-machine.md b/docs/state-machine.md index 4020f29..23da57c 100644 --- a/docs/state-machine.md +++ b/docs/state-machine.md @@ -24,8 +24,8 @@ The cache is in one of three states: **2. Initialized** - `CacheState.IsInitialized == true` -- `CacheState.Storage` holds a contiguous, non-empty range of data consistent with `CacheState.Storage.Range` (Invariant B.11) -- Cache is contiguous — no gaps (Invariant A.9a) +- `CacheState.Storage` holds a contiguous, non-empty range of data consistent with `CacheState.Storage.Range` (Invariant B.1) +- Cache is contiguous — no gaps (Invariant A.12b) - Ready to serve user requests **3. Rebalancing** @@ -71,7 +71,7 @@ Mutation authority is constant across all states: - **User Path**: read-only with respect to shared cache state in every state - **Rebalance Execution**: sole writer in every state -See `docs/invariants.md` for the formal single-writer rule (Invariants A.-1, A.7, A.8, A.9). +See `docs/invariants.md` for the formal single-writer rule (Invariants A.1, A.11, A.12, A.12a). ### Transition Details @@ -87,7 +87,7 @@ See `docs/invariants.md` for the formal single-writer rule (Invariants A.-1, A.7 - **Mutations** (Rebalance Execution only): - Call `Storage.Rematerialize()` with delivered data and range - Set `IsInitialized = true` -- **Atomicity**: Changes applied atomically (Invariant B.12) +- **Atomicity**: Changes applied atomically (Invariant B.2) - **Postcondition**: Cache enters `Initialized` after execution completes - **Note**: User Path is read-only; initial cache population is performed exclusively by Rebalance Execution @@ -118,7 +118,7 @@ See `docs/invariants.md` for the formal single-writer rule (Invariants A.-1, A.7 - Call `Storage.Rematerialize()` with merged, trimmed data (sets storage contents and `Storage.Range`) - Set `IsInitialized = true` - Recompute `NoRebalanceRange` -- **Atomicity**: Changes applied atomically (Invariant B.12) +- **Atomicity**: Changes applied atomically (Invariant B.2) - **Postcondition**: Cache returns to stable `Initialized` state #### T4: Rebalancing → Rebalancing (New Request MAY Cancel Active Rebalance) @@ -143,12 +143,12 @@ See `docs/invariants.md` for the formal single-writer rule (Invariants A.-1, A.7 | Initialized | None | Not active | | Rebalancing | None | All cache mutations (expand, trim, Rematerialize, IsInitialized, NoRebalanceRange) — must yield on cancellation | -**User Path mutations (Invariants A.7, A.8)**: +**User Path mutations (Invariants A.11, A.12)**: - User Path NEVER calls `Storage.Rematerialize()` - User Path NEVER writes to `IsInitialized` - User Path NEVER writes to `NoRebalanceRange` -**Rebalance Execution mutations (Invariants F.36, F.36a)**: +**Rebalance Execution mutations (Invariants F.2, F.2a)**: 1. Uses delivered data from intent as authoritative base 2. Expands to `DesiredCacheRange` (fetches only truly missing ranges) 3. Trims excess data outside `DesiredCacheRange` @@ -167,15 +167,15 @@ See `docs/invariants.md` for the formal single-writer rule (Invariants A.-1, A.7 5. New rebalance proceeds with new intent's delivered data (if validated) 6. Cancelled rebalance yields without leaving cache inconsistent -**Cancellation Guarantees (Invariants F.34, F.34a, F.34b)**: +**Cancellation Guarantees (Invariants F.1, F.1a, F.1b)**: - Rebalance Execution MUST support cancellation at all stages - Rebalance Execution MUST yield immediately when cancelled - Cancelled execution MUST NOT leave cache inconsistent **State Safety**: -- **Atomicity**: All cache mutations are atomic (Invariant B.12) -- **Consistency**: `Storage` data and `Storage.Range` always consistent (Invariant B.11) -- **Contiguity**: Cache data never contains gaps (Invariant A.9a) +- **Atomicity**: All cache mutations are atomic (Invariant B.2) +- **Consistency**: `Storage` data and `Storage.Range` always consistent (Invariant B.1) +- **Contiguity**: Cache data never contains gaps (Invariant A.12b) - **Idempotence**: Multiple cancellations are safe ### State Invariants by State @@ -186,17 +186,17 @@ See `docs/invariants.md` for the formal single-writer rule (Invariants A.-1, A.7 - Rebalance Execution is not active (activates after first intent) **In Initialized**: -- `Storage` data and `Storage.Range` consistent (Invariant B.11) -- Cache is contiguous (Invariant A.9a) -- User Path is read-only (Invariant A.8) +- `Storage` data and `Storage.Range` consistent (Invariant B.1) +- Cache is contiguous (Invariant A.12b) +- User Path is read-only (Invariant A.12) - Rebalance Execution is not active **In Rebalancing**: -- `Storage` data and `Storage.Range` remain consistent (Invariant B.11) -- Cache is contiguous (Invariant A.9a) -- User Path may cause cancellation but NOT mutate (Invariants A.0, A.0a) -- Rebalance Execution is active and sole writer (Invariant F.36) -- Rebalance Execution is cancellable (Invariant F.34) +- `Storage` data and `Storage.Range` remain consistent (Invariant B.1) +- Cache is contiguous (Invariant A.12b) +- User Path may cause cancellation but NOT mutate (Invariants A.2, A.2a) +- Rebalance Execution is active and sole writer (Invariant F.2) +- Rebalance Execution is cancellable (Invariant F.1) - Single-writer architecture: no race conditions possible ## Worked Examples @@ -253,7 +253,7 @@ State: Rebalancing (R2 executing, will replace cache at DesiredCacheRange=[450,6 - Cache state consistency: `docs/invariants.md` (Cache state invariants, Section B) - Single-writer and atomic rematerialization: `docs/invariants.md` (Execution invariants, Section F) -- Cancellation protocol: `docs/invariants.md` (Execution invariants F.34, F.34a, F.34b) +- Cancellation protocol: `docs/invariants.md` (Execution invariants F.1, F.1a, F.1b) - Decision authority and validation pipeline: `docs/invariants.md` (Decision Path invariants, Section D) ## Usage diff --git a/docs/storage-strategies.md b/docs/storage-strategies.md index 75db19c..7694c3c 100644 --- a/docs/storage-strategies.md +++ b/docs/storage-strategies.md @@ -394,23 +394,23 @@ Steady state reached: Both buffers have sufficient capacity, no more allocations The staging buffer pattern directly supports key system invariants: -### Invariant A.3.8 - Cache Mutation Rules +### Invariant A.12 - Cache Mutation Rules - **Cold Start**: Staging buffer safely materializes initial cache - **Expansion**: Active storage stays immutable while LINQ chains enumerate it - **Replacement**: Atomic swap ensures clean transition -### Invariant A.3.9a - Cache Contiguity +### Invariant A.12b - Cache Contiguity - Single-pass enumeration into staging buffer maintains contiguity - No partial or gapped states -### Invariant B.11-12 - Atomic Consistency +### Invariant B.1-2 - Atomic Consistency - Swap and Range update both happen inside `lock (_lock)`, so `Read()` always observes a consistent `(_activeStorage, Range)` pair - No intermediate inconsistent state is observable -### Invariant A.2 - User Path Never Waits for Rebalance (Conditional Compliance) +### Invariant A.4 - User Path Never Waits for Rebalance (Conditional Compliance) - `CopyOnReadStorage` is **conditionally compliant**: `Read()` and `ToRangeData()` acquire `_lock`, which is also held by `Rematerialize()` for the duration of the buffer swap and Range update (a fast, @@ -418,9 +418,9 @@ The staging buffer pattern directly supports key system invariants: - Contention is limited to the swap itself — not the full rebalance cycle (fetch + decision + execution). The enumeration into the staging buffer happens **before** the lock is acquired, so the lock hold time is just the cost of two field writes and a property assignment. -- `SnapshotReadStorage` remains fully lock-free if strict A.2 compliance is required. +- `SnapshotReadStorage` remains fully lock-free if strict A.4 compliance is required. -### Invariant B.15 - Cancellation Safety +### Invariant B.5 - Cancellation Safety - If rematerialization is cancelled mid-AddRange, staging buffer is abandoned - Active storage remains unchanged, cache stays consistent diff --git a/src/SlidingWindowCache/Core/Planning/ProportionalRangePlanner.cs b/src/SlidingWindowCache/Core/Planning/ProportionalRangePlanner.cs index af9ff20..e0763ec 100644 --- a/src/SlidingWindowCache/Core/Planning/ProportionalRangePlanner.cs +++ b/src/SlidingWindowCache/Core/Planning/ProportionalRangePlanner.cs @@ -45,11 +45,11 @@ namespace SlidingWindowCache.Core.Planning; /// /// Invariant References: /// -/// E.30: DesiredCacheRange is computed solely from RequestedRange + config -/// E.31: DesiredCacheRange is independent of current cache contents -/// E.32: DesiredCacheRange defines canonical state for convergence semantics -/// E.33: Sliding window geometry is determined solely by configuration -/// D.25, D.26: Analytical/pure (CPU-only), never mutates cache state +/// E.1: DesiredCacheRange is computed solely from RequestedRange + config +/// E.2: DesiredCacheRange is independent of current cache contents +/// E.3: DesiredCacheRange defines canonical state for convergence semantics +/// E.4: Sliding window geometry is determined solely by configuration +/// D.1, D.2: Analytical/pure (CPU-only), never mutates cache state /// /// Related: (threshold calculation, when to rebalance logic) /// See: for architectural overview. @@ -77,7 +77,7 @@ internal sealed class ProportionalRangePlanner /// This constructor wires the planner to a shared options holder and domain only; it does not perform any computation or validation. The planner is invoked by RebalanceDecisionEngine during Stage 3 (Desired Range Computation) of the decision evaluation pipeline, which executes in the background intent processing loop. /// /// - /// References: Invariants E.30-E.33, D.25-D.26 (see docs/invariants.md). + /// References: Invariants E.1-E.4, D.1-D.2 (see docs/invariants.md). /// /// public ProportionalRangePlanner(RuntimeCacheOptionsHolder optionsHolder, TDomain domain) @@ -101,7 +101,7 @@ public ProportionalRangePlanner(RuntimeCacheOptionsHolder optionsHolder, TDomain /// Is pure/side-effect free: No cache state or I/O interaction /// Applies only the current options snapshot and domain arithmetic (see LeftCacheSize, RightCacheSize on ) /// Does not trigger or decide rebalance — strictly analytical - /// Enforces Invariants: E.30 (function of RequestedRange + config), E.31 (independent of cache state), E.32 (defines canonical convergent target), D.25-D.26 (analytical/CPU-only) + /// Enforces Invariants: E.1 (function of RequestedRange + config), E.2 (independent of cache state), E.3 (defines canonical convergent target), D.1-D.2 (analytical/CPU-only) /// /// /// diff --git a/src/SlidingWindowCache/Core/Rebalance/Execution/CacheDataExtensionService.cs b/src/SlidingWindowCache/Core/Rebalance/Execution/CacheDataExtensionService.cs index f9e7b6b..9d086d8 100644 --- a/src/SlidingWindowCache/Core/Rebalance/Execution/CacheDataExtensionService.cs +++ b/src/SlidingWindowCache/Core/Rebalance/Execution/CacheDataExtensionService.cs @@ -152,7 +152,7 @@ out bool isCacheExpanded /// /// Segments with null Range (unavailable data from DataSource) are filtered out /// before union. This ensures cache only contains contiguous available data, - /// preserving Invariant A.9a (Cache Contiguity). + /// preserving Invariant A.12b (Cache Contiguity). /// /// /// When DataSource returns RangeChunk with Range = null (e.g., request beyond database boundaries), diff --git a/src/SlidingWindowCache/Core/UserPath/UserRequestHandler.cs b/src/SlidingWindowCache/Core/UserPath/UserRequestHandler.cs index e099366..fbcee10 100644 --- a/src/SlidingWindowCache/Core/UserPath/UserRequestHandler.cs +++ b/src/SlidingWindowCache/Core/UserPath/UserRequestHandler.cs @@ -25,7 +25,7 @@ namespace SlidingWindowCache.Core.UserPath; /// /// Every user access that results in assembled data publishes a rebalance intent. /// Requests where IDataSource returns null for the requested range (physical boundary misses) -/// do not publish an intent, as there is no delivered data to embed (see Invariant C.24e). +/// do not publish an intent, as there is no delivered data to embed (see Invariant C.8e). /// The UserRequestHandler NEVER invokes decision logic. /// /// Responsibilities: @@ -202,7 +202,7 @@ public async ValueTask> HandleRequestAsync( // Publish intent only when there was a physical data hit (assembledData is not null). // Full vacuum (out-of-physical-bounds) requests produce no intent — there is no - // meaningful cache shift to signal to the rebalance pipeline (see Invariant C.24e). + // meaningful cache shift to signal to the rebalance pipeline (see Invariant C.8e). if (assembledData is not null) { _intentController.PublishIntent(new Intent(requestedRange, assembledData)); diff --git a/src/SlidingWindowCache/Infrastructure/Concurrency/AsyncActivityCounter.cs b/src/SlidingWindowCache/Infrastructure/Concurrency/AsyncActivityCounter.cs index ee0ece2..a1905e6 100644 --- a/src/SlidingWindowCache/Infrastructure/Concurrency/AsyncActivityCounter.cs +++ b/src/SlidingWindowCache/Infrastructure/Concurrency/AsyncActivityCounter.cs @@ -25,9 +25,9 @@ /// /// This class implements two architectural invariants that create an orchestration barrier: /// -/// H.47 - Increment-Before-Publish: Work MUST call IncrementActivity() BEFORE becoming visible -/// H.48 - Decrement-After-Completion: Work MUST call DecrementActivity() in finally block AFTER completion -/// H.49 - "Was Idle" Semantics: WaitForIdleAsync() uses eventual consistency model + /// H.1 - Increment-Before-Publish: Work MUST call IncrementActivity() BEFORE becoming visible +/// H.2 - Decrement-After-Completion: Work MUST call DecrementActivity() in finally block AFTER completion +/// H.3 - "Was Idle" Semantics: WaitForIdleAsync() uses eventual consistency model /// /// These invariants ensure idle detection never misses scheduled-but-not-yet-started work. /// See docs/invariants.md Section H for detailed explanation and call site verification. @@ -93,11 +93,11 @@ public AsyncActivityCounter() /// If this is a transition from idle (0) to busy (1), creates a new TaskCompletionSource. /// /// - /// CRITICAL INVARIANT - H.47 Increment-Before-Publish: + /// CRITICAL INVARIANT - H.1 Increment-Before-Publish: /// /// Callers MUST call this method BEFORE making work visible to consumers (e.g., semaphore signal, channel write). /// This ensures idle detection never misses scheduled-but-not-yet-started work. - /// See docs/invariants.md Section H.47 for detailed explanation and call site verification. + /// See docs/invariants.md Section H.1 for detailed explanation and call site verification. /// /// Thread-Safety: /// @@ -115,7 +115,7 @@ public AsyncActivityCounter() /// If multiple threads call IncrementActivity concurrently from idle state, Interlocked.Increment /// guarantees only ONE thread observes newCount == 1. That thread creates the TCS for this busy period. /// - /// Call Sites (verified in docs/invariants.md Section H.47): + /// Call Sites (verified in docs/invariants.md Section H.1): /// /// IntentController.PublishIntent() - line 173 before semaphore signal at line 177 /// TaskBasedRebalanceExecutionController.PublishExecutionRequest() - line 196 before Volatile.Write(_lastExecutionRequest) at line 214 and task chain publication at line 220 @@ -143,11 +143,11 @@ public void IncrementActivity() /// If this is a transition from busy to idle (counter reaches 0), signals the TaskCompletionSource. /// /// - /// CRITICAL INVARIANT - H.48 Decrement-After-Completion: + /// CRITICAL INVARIANT - H.2 Decrement-After-Completion: /// /// Callers MUST call this method in a finally block AFTER work completes (success/cancellation/exception). /// This ensures activity counter remains balanced and WaitForIdleAsync never hangs due to counter leaks. - /// See docs/invariants.md Section H.48 for detailed explanation and call site verification. + /// See docs/invariants.md Section H.2 for detailed explanation and call site verification. /// /// Thread-Safety: /// @@ -170,7 +170,7 @@ public void IncrementActivity() /// /// This race is benign: old busy period ends, new busy period begins. No corruption. /// - /// Call Sites (verified in docs/invariants.md Section H.48): + /// Call Sites (verified in docs/invariants.md Section H.2): /// /// IntentController.ProcessIntentsAsync() - finally block at line 271 /// TaskBasedRebalanceExecutionController.ExecuteRequestAsync() - finally block at line 349 diff --git a/src/SlidingWindowCache/Infrastructure/Storage/CopyOnReadStorage.cs b/src/SlidingWindowCache/Infrastructure/Storage/CopyOnReadStorage.cs index 4a9f77d..2184b76 100644 --- a/src/SlidingWindowCache/Infrastructure/Storage/CopyOnReadStorage.cs +++ b/src/SlidingWindowCache/Infrastructure/Storage/CopyOnReadStorage.cs @@ -41,7 +41,7 @@ namespace SlidingWindowCache.Infrastructure.Storage; /// /// This ensures that active storage is never observed mid-swap by a concurrent Read() or /// ToRangeData() call, preventing data races when range data is derived from the same storage -/// (e.g., during cache expansion per Invariant A.3.8). +/// (e.g., during cache expansion per Invariant A.12). /// /// Synchronization: /// @@ -67,7 +67,7 @@ namespace SlidingWindowCache.Infrastructure.Storage; /// /// /// -/// See Invariant A.2 for the conditional compliance note regarding this lock. + /// See Invariant A.4 for the conditional compliance note regarding this lock. /// /// Memory Behavior: /// @@ -129,7 +129,7 @@ public CopyOnReadStorage(TDomain domain) /// /// Staging Buffer Rematerialization: /// - /// This method implements a dual-buffer pattern to satisfy Invariants A.3.8, B.11-12: + /// This method implements a dual-buffer pattern to satisfy Invariants A.12, B.1-2: /// /// /// Acquire _lock (shared with Read() and ToRangeData()) @@ -142,7 +142,7 @@ public CopyOnReadStorage(TDomain domain) /// Why this pattern? When contains data derived from /// the same storage (e.g., during cache expansion via LINQ operations like Concat/Union), direct /// mutation of active storage would corrupt the enumeration. The staging buffer ensures active - /// storage remains unchanged during enumeration, satisfying Invariant A.3.9a (cache contiguity). + /// storage remains unchanged during enumeration, satisfying Invariant A.12b (cache contiguity). /// /// /// Why the lock? The buffer swap consists of two separate field writes, which are diff --git a/src/SlidingWindowCache/Public/Extensions/WindowCacheConsistencyExtensions.cs b/src/SlidingWindowCache/Public/Extensions/WindowCacheConsistencyExtensions.cs index 8512190..7ba6d6b 100644 --- a/src/SlidingWindowCache/Public/Extensions/WindowCacheConsistencyExtensions.cs +++ b/src/SlidingWindowCache/Public/Extensions/WindowCacheConsistencyExtensions.cs @@ -52,7 +52,7 @@ namespace SlidingWindowCache.Public.Extensions; /// However, the consistency guarantee may degrade: /// /// -/// Due to the AsyncActivityCounter's "was idle at some point" semantics (Invariant H.49), +/// Due to the AsyncActivityCounter's "was idle at some point" semantics (Invariant H.3), /// a thread that calls WaitForIdleAsync during the window between /// Interlocked.Increment (counter 0→1) and the subsequent Volatile.Write of the /// new TaskCompletionSource will observe the previous (already-completed) TCS and return @@ -139,7 +139,7 @@ public static class WindowCacheConsistencyExtensions /// the wait ensures the background rebalance builds the cache window around the new position. /// /// - /// Idle Semantics (Invariant H.49): + /// Idle Semantics (Invariant H.3): /// /// The idle wait uses "was idle at some point" semantics inherited from /// . This is sufficient for @@ -346,7 +346,7 @@ public static async ValueTask> GetDataAndWaitOnMissAs /// (hybrid consistency). /// /// - /// Idle Semantics (Invariant H.49): + /// Idle Semantics (Invariant H.3): /// /// The idle wait uses "was idle at some point" semantics inherited from /// . This is sufficient diff --git a/src/SlidingWindowCache/Public/Instrumentation/ICacheDiagnostics.cs b/src/SlidingWindowCache/Public/Instrumentation/ICacheDiagnostics.cs index 438be2a..4a0738d 100644 --- a/src/SlidingWindowCache/Public/Instrumentation/ICacheDiagnostics.cs +++ b/src/SlidingWindowCache/Public/Instrumentation/ICacheDiagnostics.cs @@ -28,7 +28,7 @@ public interface ICacheDiagnostics /// Note: This is called by the shared CacheDataExtensionService used by both User Path and Rebalance Path. /// The actual cache mutation (Rematerialize) only happens in Rebalance Execution. /// Location: CacheDataExtensionService.CalculateMissingRanges (when intersection exists) - /// Related: Invariant 9a (Cache Contiguity Rule) + /// Related: Invariant A.12b (Cache Contiguity Rule) /// void CacheExpanded(); @@ -39,7 +39,7 @@ public interface ICacheDiagnostics /// not that mutation occurred. The actual cache mutation (Rematerialize) only happens in Rebalance Execution. /// Note: This is called by the shared CacheDataExtensionService used by both User Path and Rebalance Path. /// Location: CacheDataExtensionService.CalculateMissingRanges (when no intersection exists) - /// Related: Invariant 9a (Cache Contiguity Rule - forbids gaps) + /// Related: Invariant A.12b (Cache Contiguity Rule - forbids gaps) /// void CacheReplaced(); @@ -98,7 +98,7 @@ public interface ICacheDiagnostics /// Context: User Thread (Partial Cache Hit — Scenario 3) and Background Thread (Rebalance Execution) /// /// This is informational only - the system handles boundaries gracefully by skipping - /// unavailable segments during cache union (UnionAll), preserving cache contiguity (Invariant A.9a). + /// unavailable segments during cache union (UnionAll), preserving cache contiguity (Invariant A.12b). /// /// Typical Scenarios: /// @@ -110,7 +110,7 @@ public interface ICacheDiagnostics /// Location: CacheDataExtensionService.UnionAll (when a fetched chunk has a null Range) /// /// - /// Related: Invariant G.48 (IDataSource Boundary Semantics), Invariant A.9a (Cache Contiguity) + /// Related: Invariant G.5 (IDataSource Boundary Semantics), Invariant A.12b (Cache Contiguity) /// /// void DataSegmentUnavailable(); @@ -124,9 +124,9 @@ public interface ICacheDiagnostics /// Called after UserRequestHandler publishes an intent containing delivered data to IntentController. /// Intent is published only when the user request results in assembled data (assembledData != null). /// Physical boundary misses — where IDataSource returns null for the requested range — do not produce an intent - /// because there is no delivered data to embed in the intent (see Invariant C.24e). + /// because there is no delivered data to embed in the intent (see Invariant C.8e). /// Location: IntentController.PublishIntent (after scheduler receives intent) - /// Related: Invariant A.3 (User Path is sole source of rebalance intent), Invariant 24e (Intent must contain delivered data) + /// Related: Invariant A.5 (User Path is sole source of rebalance intent), Invariant C.8e (Intent must contain delivered data) /// Note: Intent publication does NOT guarantee execution (opportunistic behavior) /// void RebalanceIntentPublished(); @@ -140,7 +140,7 @@ public interface ICacheDiagnostics /// Called when DecisionEngine determines rebalance is necessary (RequestedRange outside NoRebalanceRange and DesiredCacheRange != CurrentCacheRange). /// Indicates transition from Decision Path to Execution Path (Decision Scenario D3). /// Location: TaskBasedRebalanceExecutionController.ExecuteRequestAsync / ChannelBasedRebalanceExecutionController.ProcessExecutionRequestsAsync (before executor invocation) - /// Related: Invariant 28 (Rebalance triggered only if confirmed necessary) + /// Related: Invariant D.5 (Rebalance triggered only if confirmed necessary) /// void RebalanceExecutionStarted(); @@ -149,7 +149,7 @@ public interface ICacheDiagnostics /// Called after RebalanceExecutor successfully extends cache to DesiredCacheRange, trims excess data, and updates cache state. /// Indicates cache normalization completed and state mutations applied (Rebalance Scenarios R1, R2). /// Location: RebalanceExecutor.ExecuteAsync (final step after UpdateCacheState) - /// Related: Invariant 34 (Only Rebalance Execution writes to cache), Invariant 35 (Cache state update is atomic) + /// Related: Invariant F.2 (Only Rebalance Execution writes to cache), Invariant B.2 (Changes to CacheData and CurrentCacheRange are performed atomically) /// void RebalanceExecutionCompleted(); @@ -158,7 +158,7 @@ public interface ICacheDiagnostics /// Called when intentToken is cancelled during rebalance execution (after execution started but before completion). /// Indicates User Path priority enforcement and single-flight execution (yielding to new requests). /// Location: TaskBasedRebalanceExecutionController.ExecuteRequestAsync / ChannelBasedRebalanceExecutionController.ProcessExecutionRequestsAsync (catch OperationCanceledException during execution) - /// Related: Invariant 34a (Rebalance Execution must yield to User Path immediately) + /// Related: Invariant F.1a (Rebalance Execution must yield to User Path immediately) /// void RebalanceExecutionCancelled(); @@ -177,7 +177,7 @@ public interface ICacheDiagnostics /// Location: IntentController.RecordReason (RebalanceReason.WithinCurrentNoRebalanceRange) /// Related Invariants: /// - /// D.26: No rebalance if RequestedRange ⊆ CurrentNoRebalanceRange + /// D.3: No rebalance if RequestedRange ⊆ CurrentNoRebalanceRange /// Stage 1 is the primary fast-path optimization /// /// @@ -206,7 +206,7 @@ public interface ICacheDiagnostics /// Called when RebalanceExecutor detects that delivered data range already matches desired range, avoiding redundant I/O. /// Indicates same-range optimization preventing unnecessary fetch operations (Decision Scenario D2). /// Location: RebalanceExecutor.ExecuteAsync (before expensive I/O operations) - /// Related: Invariant D.27 (No rebalance if DesiredCacheRange == CurrentCacheRange), Invariant D.28 (Same-range optimization tracking) + /// Related: Invariant D.4 (No rebalance if DesiredCacheRange == CurrentCacheRange), Invariant C.8c (RebalanceSkippedSameRange counter semantics) /// void RebalanceSkippedSameRange(); diff --git a/tests/SlidingWindowCache.Invariants.Tests/README.md b/tests/SlidingWindowCache.Invariants.Tests/README.md index 3d07256..65273c5 100644 --- a/tests/SlidingWindowCache.Invariants.Tests/README.md +++ b/tests/SlidingWindowCache.Invariants.Tests/README.md @@ -22,8 +22,8 @@ Comprehensive unit test suite for the WindowCache library verifying system invar ## Recent Test Suite Enhancements ### Phase 1: High-Priority Gap Tests (2 tests added) -- **B.15 Enhanced**: Cancellation during I/O operations - validates consistency when rebalance is cancelled during active `FetchAsync` operations -- **B.16**: Stale result prevention - ensures only the most recent rebalance results are applied to cache, preventing race conditions from slow/obsolete executions +- **B.5 Enhanced**: Cancellation during I/O operations - validates consistency when rebalance is cancelled during active `FetchAsync` operations +- **B.6**: Stale result prevention - ensures only the most recent rebalance results are applied to cache, preventing race conditions from slow/obsolete executions ### Phase 2: Execution Strategy Coverage (4 tests converted to Theory) Tests now validate behavior across **both execution strategies**: @@ -31,19 +31,19 @@ Tests now validate behavior across **both execution strategies**: - **Channel-based** (bounded, `rebalanceQueueCapacity: 10`) - Backpressure control Converted tests: -- `Invariant_A_0a_UserRequestCancelsRebalance` -- `Invariant_C17_AtMostOneActiveIntent` -- `Invariant_F35_G46_RebalanceCancellationBehavior` +- `Invariant_A_2a_UserRequestCancelsRebalance` +- `Invariant_C_1_AtMostOneActiveIntent` +- `Invariant_F_1_G_4_RebalanceCancellationBehavior` - `ConcurrencyScenario_RapidRequestsBurstWithCancellation` ### Phase 3: Medium-Priority Gap Tests (3 tests added) -- **A.-1**: Concurrent write safety - stress test with 50 concurrent requests verifying single-writer robustness -- **C.20**: Early exit for obsolete intents - validates Decision Engine discards superseded intents efficiently -- **E.31**: Desired range independence - confirms desired range computation is deterministic regardless of cache history +- **A.1**: Concurrent write safety stress test (50 concurrent requests) **[NEW]** +- **C.4**: Early exit for obsolete intents - validates Decision Engine discards superseded intents efficiently +- **E.2**: Desired range independence - confirms desired range computation is deterministic regardless of cache history ### Phase 4: Performance Guarantee Tests (2 tests added) -- **F.38**: Incremental fetch optimization - verifies only missing data segments are fetched during cache expansion -- **F.39**: Data preservation during expansion - ensures existing cached data is never refetched, preventing wasteful I/O +- **F.4**: Incremental fetch optimization - verifies only missing data segments are fetched during cache expansion +- **F.5**: Data preservation during expansion - ensures existing cached data is never refetched, preventing wasteful I/O ### Phase 5: Storage Strategy Coverage (3 tests converted to Theory) Tests now validate behavior across **both storage strategies**: @@ -51,13 +51,13 @@ Tests now validate behavior across **both storage strategies**: - **CopyOnRead** (`UserCacheReadMode.CopyOnRead`) - Defensive copies, cheaper rematerialization Converted tests: -- `Invariant_A3_8_UserPathNeverMutatesCache` (3 scenarios × 2 storage = 6 test cases) -- `Invariant_F36a_RebalanceNormalizesCache` -- `Invariant_F40_F41_F42_PostExecutionGuarantees` +- `Invariant_A_12_UserPathNeverMutatesCache` (3 scenarios × 2 storage = 6 test cases) +- `Invariant_F_2a_RebalanceNormalizesCache` +- `Invariant_F_6_F_7_F_8_PostExecutionGuarantees` ### Test Infrastructure Enhancements - **Added**: `CreateTrackingMockDataSource` helper for validating fetch patterns -- **Added**: `A3_8_TestData` MemberData provider combining scenarios and storage strategies +- **Added**: `A_12_TestData` MemberData provider combining scenarios and storage strategies - **Updated**: `CreateDefaultOptions` to support `rebalanceQueueCapacity` parameter ### Coverage Summary @@ -93,7 +93,7 @@ Converted tests: - `RebalanceExecutionCancelled` - Rebalance execution cancelled - `RebalanceSkippedCurrentNoRebalanceRange` - **Policy-based skip (Stage 1)** - Request within current NoRebalanceRange threshold - `RebalanceSkippedPendingNoRebalanceRange` - **Policy-based skip (Stage 2)** - Request within pending NoRebalanceRange threshold - - `RebalanceSkippedSameRange` - **Optimization-based skip** (Invariant D.28) - DesiredRange == CurrentRange + - `RebalanceSkippedSameRange` - **Optimization-based skip** (Invariant D.4) - DesiredRange == CurrentRange **Note**: `CacheExpanded` and `CacheReplaced` are incremented during range analysis by the shared `CacheDataExtensionService` (used by both User Path and Rebalance Path) when determining what data needs to be fetched. They track analysis/planning, @@ -148,48 +148,48 @@ not actual cache mutations. Actual mutations only occur in Rebalance Execution v #### Test Categories: **A. User Path & Fast User Access (10 tests)** -- A.0a: User request cancels rebalance [Theory: 2 execution strategies] -- A.-1: Concurrent write safety stress test (50 concurrent requests) **[NEW]** -- A.2.1: User path always serves requests -- A.2.2: User path never waits for rebalance -- A.2.10: User always receives exact requested range -- A.3.8: User Path never mutates cache [Theory: 3 scenarios × 2 storage strategies = 6 tests] -- A.3.9a: Cache contiguity maintained +- A.2a: User request cancels rebalance [Theory: 2 execution strategies] +- A.1: Concurrent write safety stress test (50 concurrent requests) **[NEW]** +- A.3: User path always serves requests +- A.4: User path never waits for rebalance +- A.10: User always receives exact requested range +- A.12: User Path never mutates cache [Theory: 3 scenarios × 2 storage strategies = 6 tests] +- A.12b: Cache contiguity maintained **B. Cache State & Consistency (4 tests)** -- B.11: CacheData and CurrentCacheRange always consistent -- B.15: Cancelled rebalance doesn't violate consistency -- B.15 Enhanced: Cancellation during I/O operations **[NEW]** -- B.16: Only most recent rebalance results are applied (stale result prevention) **[NEW]** +- B.1: CacheData and CurrentCacheRange always consistent +- B.5: Cancelled rebalance doesn't violate consistency +- B.5 Enhanced: Cancellation during I/O operations **[NEW]** +- B.6: Only most recent rebalance results are applied (stale result prevention) **[NEW]** **C. Rebalance Intent & Temporal (5 tests)** -- C.17: At most one active intent [Theory: 2 execution strategies] -- C.18: Previous intent becomes logically superseded -- C.20: Decision Engine exits early for obsolete intents **[NEW]** -- C.24: Intent doesn't guarantee execution -- C.23: System stabilizes under load +- C.1: At most one active intent [Theory: 2 execution strategies] +- C.2: Previous intent becomes logically superseded +- C.4: Decision Engine exits early for obsolete intents **[NEW]** +- C.8: Intent doesn't guarantee execution +- C.7: System stabilizes under load **D. Rebalance Decision Path (4 tests)** -- D.27: No rebalance if request in NoRebalanceRange -- D.27 Stage 1: Skips when within current NoRebalanceRange -- D.29 Stage 2: Skips when within pending NoRebalanceRange -- D.28: Rebalance skipped when DesiredRange == CurrentRange +- D.3: No rebalance if request in NoRebalanceRange +- D.3 Stage 1: Skips when within current NoRebalanceRange +- D.5 Stage 2: Skips when within pending NoRebalanceRange +- D.4: Rebalance skipped when DesiredRange == CurrentRange **E. Cache Geometry & Policy (3 tests)** -- E.30: DesiredRange computed from config and request -- E.31: DesiredRange independent of cache state (determinism test) **[NEW]** +- E.1: DesiredRange computed from config and request +- E.2: DesiredRange independent of cache state (determinism test) **[NEW]** - ReadMode behavior verification (Snapshot and CopyOnRead) **F. Rebalance Execution (7 tests)** -- F.35, F.35a, G.46: Rebalance cancellation behavior [Theory: 2 execution strategies] -- F.36a: Rebalance normalizes cache [Theory: 2 storage strategies] -- F.38: Incremental fetch optimization (only missing subranges fetched) **[NEW]** -- F.39: Data preservation during expansion (no refetching) **[NEW]** -- F.40-42: Post-execution guarantees [Theory: 2 storage strategies] +- F.1, F.1a, G.4: Rebalance cancellation behavior [Theory: 2 execution strategies] +- F.2a: Rebalance normalizes cache [Theory: 2 storage strategies] +- F.4: Incremental fetch optimization (only missing subranges fetched) **[NEW]** +- F.5: Data preservation during expansion (no refetching) **[NEW]** +- F.6-F.8: Post-execution guarantees [Theory: 2 storage strategies] **G. Execution Context & Scheduling (2 tests)** -- G.43-45: Execution context separation -- G.46: User cancellation during fetch +- G.1-G.3: Execution context separation +- G.4: User cancellation during fetch **Additional Comprehensive Tests (2 tests)** - Complete scenario with multiple requests and rebalancing @@ -263,10 +263,10 @@ not actual cache mutations. Actual mutations only occur in Rebalance Execution v - Cache state converges asynchronously (eventual consistency) **Architectural Invariants (enforced by code structure)**: -- A.-1: User Path and Rebalance Execution never write concurrently (User Path doesn't write) -- A.8: User Path MUST NOT mutate cache (enforced by removing Rematerialize calls) -- F.36: Rebalance Execution is ONLY writer (enforced by internal setters) -- C.24e/f: Intent contains delivered data (enforced by PublishIntent signature) +- A.1: User Path and Rebalance Execution never write concurrently (User Path doesn't write) +- A.12: User Path MUST NOT mutate cache (enforced by removing Rematerialize calls) +- F.2: Rebalance Execution is ONLY writer (enforced by internal setters) +- C.8e/f: Intent contains delivered data (enforced by PublishIntent signature) ## Usage @@ -275,7 +275,7 @@ not actual cache mutations. Actual mutations only occur in Rebalance Execution v dotnet test tests/SlidingWindowCache.Invariants.Tests/SlidingWindowCache.Invariants.Tests.csproj --configuration Debug # Run specific test -dotnet test --filter "FullyQualifiedName~Invariant_D28_SkipWhenDesiredEqualsCurrentRange" +dotnet test --filter "FullyQualifiedName~Invariant_D_4_SkipWhenDesiredEqualsCurrentRange" # Run tests by category (example: all Decision Path tests) dotnet test --filter "FullyQualifiedName~Invariant_D" @@ -286,13 +286,13 @@ dotnet test --filter "FullyQualifiedName~Invariant_D" ### Skip Condition Distinction The system has **two distinct skip scenarios**, tracked by separate counters: -1. **Policy-Based Skip** (Invariants D.27 / D.29) +1. **Policy-Based Skip** (Invariants D.3 / D.5) - Counters: `RebalanceSkippedCurrentNoRebalanceRange` (Stage 1) and `RebalanceSkippedPendingNoRebalanceRange` (Stage 2) - Location: `IntentController.ProcessIntentsAsync` (after `DecisionEngine` returns `ShouldSchedule=false`) - Reason: Request within NoRebalanceRange threshold zone (current or pending) - Characteristic: Execution **never starts** (decision-level optimization) -2. **Optimization-Based Skip** (Invariant D.28) +2. **Optimization-Based Skip** (Invariant D.4) - Counter: `RebalanceSkippedSameRange` - Location: `RebalanceExecutor.ExecuteAsync` (before I/O operations) - Reason: `CurrentCacheRange == DesiredCacheRange` (already at target) diff --git a/tests/SlidingWindowCache.Invariants.Tests/WindowCacheInvariantTests.cs b/tests/SlidingWindowCache.Invariants.Tests/WindowCacheInvariantTests.cs index 9170157..a82728f 100644 --- a/tests/SlidingWindowCache.Invariants.Tests/WindowCacheInvariantTests.cs +++ b/tests/SlidingWindowCache.Invariants.Tests/WindowCacheInvariantTests.cs @@ -11,7 +11,7 @@ namespace SlidingWindowCache.Invariants.Tests; /// -/// Comprehensive test suite verifying all 47 system invariants for WindowCache. +/// Comprehensive test suite verifying all 56 system invariants for WindowCache. /// Each test references its corresponding invariant number and description. /// Tests use DEBUG instrumentation counters to verify behavioral properties. /// Uses Intervals.NET for proper range handling and inclusivity considerations. @@ -79,9 +79,9 @@ public async ValueTask DisposeAsync() }; /// - /// Provides test data combining scenarios and storage strategies for A3_8 test. + /// Provides test data combining scenarios and storage strategies for A_12 test. /// - public static IEnumerable A3_8_TestData + public static IEnumerable A_12_TestData { get { @@ -116,20 +116,19 @@ public static IEnumerable A3_8_TestData #region A. User Path & Fast User Access Invariants - #region A.1 Concurrency & Priority - + #region A.2 Concurrency & Priority /// - /// Tests Invariant A.0a (🟢 Behavioral): User Request MAY cancel ongoing or pending Rebalance Execution + /// Tests Invariant A.2a (🟢 Behavioral): User Request MAY cancel ongoing or pending Rebalance Execution /// ONLY when a new rebalance is validated as necessary by the multi-stage decision pipeline. /// Verifies cancellation is validation-driven coordination, not automatic request-driven behavior. - /// Related: A.0 (Architectural - User Path has higher priority than Rebalance Execution) + /// Related: A.2 (Architectural - User Path has higher priority than Rebalance Execution) /// Parameterized by execution strategy to verify behavior across both task-based and channel-based controllers. /// /// Human-readable name of execution strategy for test output /// Queue capacity: null = task-based (unbounded), >= 1 = channel-based (bounded) [Theory] [MemberData(nameof(ExecutionStrategyTestData))] - public async Task Invariant_A_0a_UserRequestCancelsRebalance(string executionStrategy, int? queueCapacity) + public async Task Invariant_A_2a_UserRequestCancelsRebalance(string executionStrategy, int? queueCapacity) { // ARRANGE var options = TestHelpers.CreateDefaultOptions( @@ -164,14 +163,14 @@ public async Task Invariant_A_0a_UserRequestCancelsRebalance(string executionStr } /// - /// Tests Invariant A.-1 (🔵 Architectural): Concurrent write safety under extreme load. + /// Tests Invariant A.1 (🔵 Architectural): Concurrent write safety under extreme load. /// Single-writer architecture ensures only Rebalance Execution mutates cache state, but this /// stress test verifies robustness under high concurrency with many threads making rapid requests. /// Validates that all requests are served correctly without data corruption or race conditions. /// Gap identified: No existing stress test validates concurrent safety at scale. /// [Fact] - public async Task Invariant_A_Minus1_ConcurrentWriteSafety() + public async Task Invariant_A_1_ConcurrentWriteSafety() { // ARRANGE: Create cache with moderate debounce to allow overlapping operations var options = TestHelpers.CreateDefaultOptions( @@ -220,14 +219,14 @@ public async Task Invariant_A_Minus1_ConcurrentWriteSafety() #endregion - #region A.2 User-Facing Guarantees + #region A.3 User-Facing Guarantees /// - /// Tests Invariant A.1 (🟢 Behavioral): User Path always serves user requests regardless + /// Tests Invariant A.3 (🟢 Behavioral): User Path always serves user requests regardless /// of rebalance execution state. Validates core guarantee that users are never blocked by cache maintenance. /// [Fact] - public async Task Invariant_A2_1_UserPathAlwaysServesRequests() + public async Task Invariant_A_3_UserPathAlwaysServesRequests() { // ARRANGE var (cache, _) = TrackCache(TestHelpers.CreateCacheWithDefaults(_domain, _cacheDiagnostics)); @@ -245,11 +244,11 @@ public async Task Invariant_A2_1_UserPathAlwaysServesRequests() } /// - /// Tests Invariant A.2 (🟢 Behavioral): User Path never waits for rebalance execution to complete. + /// Tests Invariant A.4 (🟢 Behavioral): User Path never waits for rebalance execution to complete. /// Verifies requests complete quickly without waiting for debounce delay or background rebalance. /// [Fact] - public async Task Invariant_A2_2_UserPathNeverWaitsForRebalance() + public async Task Invariant_A_4_UserPathNeverWaitsForRebalance() { // ARRANGE: Cache with slow rebalance (1s debounce) var options = TestHelpers.CreateDefaultOptions(debounceDelay: TimeSpan.FromSeconds(1)); @@ -275,7 +274,7 @@ public async Task Invariant_A2_2_UserPathNeverWaitsForRebalance() /// This is a fundamental correctness guarantee. /// [Fact] - public async Task Invariant_A2_10_UserAlwaysReceivesExactRequestedRange() + public async Task Invariant_A_10_UserAlwaysReceivesExactRequestedRange() { // ARRANGE var (cache, _) = TrackCache(TestHelpers.CreateCacheWithDefaults(_domain, _cacheDiagnostics)); @@ -301,7 +300,7 @@ public async Task Invariant_A2_10_UserAlwaysReceivesExactRequestedRange() #region A.3 Cache Mutation Rules (User Path) /// - /// Tests Invariant A.8 (🟢 Behavioral): User Path MUST NOT mutate cache under any circumstance. + /// Tests Invariant A.12 (🟢 Behavioral): User Path MUST NOT mutate cache under any circumstance. /// Cache mutations (population, expansion, replacement) are performed exclusively by Rebalance Execution (single-writer). /// Parameterized by storage strategy to verify behavior across both Snapshot and CopyOnRead modes. /// @@ -314,8 +313,8 @@ public async Task Invariant_A2_10_UserAlwaysReceivesExactRequestedRange() /// Cache mutations occur asynchronously via Rebalance Execution. /// [Theory] - [MemberData(nameof(A3_8_TestData))] - public async Task Invariant_A3_8_UserPathNeverMutatesCache( + [MemberData(nameof(A_12_TestData))] + public async Task Invariant_A_12_UserPathNeverMutatesCache( string scenario, int reqStart, int reqEnd, int priorStart, int priorEnd, bool hasPriorRequest, string storageName, UserCacheReadMode readMode) { @@ -352,12 +351,12 @@ public async Task Invariant_A3_8_UserPathNeverMutatesCache( } /// - /// Tests Invariant A.9a (🟢 Behavioral): Cache always represents a single contiguous range, never fragmented. + /// Tests Invariant A.12b (🟢 Behavioral): Cache always represents a single contiguous range, never fragmented. /// When non-intersecting requests arrive, cache replaces its contents entirely rather than maintaining /// multiple disjoint ranges, ensuring efficient memory usage and predictable behavior. /// [Fact] - public async Task Invariant_A3_9a_CacheContiguityMaintained() + public async Task Invariant_A_12b_CacheContiguityMaintained() { // ARRANGE var (cache, _) = TrackCache(TestHelpers.CreateCacheWithDefaults(_domain, _cacheDiagnostics)); @@ -380,11 +379,11 @@ public async Task Invariant_A3_9a_CacheContiguityMaintained() #region B. Cache State & Consistency Invariants /// - /// Tests Invariant B.11 (🟢 Behavioral): CacheData and CurrentCacheRange are always consistent. + /// Tests Invariant B.1 (🟢 Behavioral): CacheData and CurrentCacheRange are always consistent. /// At all observable points, cache's data content matches its declared range. Fundamental correctness invariant. /// [Fact] - public async Task Invariant_B11_CacheDataAndRangeAlwaysConsistent() + public async Task Invariant_B_1_CacheDataAndRangeAlwaysConsistent() { // ARRANGE var (cache, _) = TrackCache(TestHelpers.CreateCacheWithDefaults(_domain, _cacheDiagnostics)); @@ -407,12 +406,12 @@ public async Task Invariant_B11_CacheDataAndRangeAlwaysConsistent() } /// - /// Tests Invariant B.15 (🟢 Behavioral): Partially executed or cancelled Rebalance Execution + /// Tests Invariant B.5 (🟢 Behavioral): Partially executed or cancelled Rebalance Execution /// MUST NOT leave cache in inconsistent state. Verifies aggressive cancellation for user responsiveness - /// doesn't compromise correctness. Also validates F.35b (same guarantee from execution perspective). + /// doesn't compromise correctness. Also validates F.1b (same guarantee from execution perspective). /// [Fact] - public async Task Invariant_B15_CancelledRebalanceDoesNotViolateConsistency() + public async Task Invariant_B_5_CancelledRebalanceDoesNotViolateConsistency() { // ARRANGE var options = TestHelpers.CreateDefaultOptions(debounceDelay: TimeSpan.FromMilliseconds(100)); @@ -431,14 +430,14 @@ public async Task Invariant_B15_CancelledRebalanceDoesNotViolateConsistency() } /// - /// Tests Invariant B.15 Enhanced (🟢 Behavioral): Cancellation during I/O operations (during FetchAsync) + /// Tests Invariant B.5 Enhanced (🟢 Behavioral): Cancellation during I/O operations (during FetchAsync) /// MUST NOT leave cache in inconsistent state. This test verifies that when rebalance execution is cancelled /// while actively fetching data from the data source (not just during debounce), the cache remains consistent. - /// Gap identified: Original B.15 test only covers cancellation between requests (during debounce delay). + /// Gap identified: Original B.5 test only covers cancellation between requests (during debounce delay). /// This test covers cancellation during actual I/O operations when FetchAsync is in progress. /// [Fact] - public async Task Invariant_B15_Enhanced_CancellationDuringIO() + public async Task Invariant_B_5_Enhanced_CancellationDuringIO() { // ARRANGE: Cache with slow data source to allow cancellation during fetch var options = TestHelpers.CreateDefaultOptions( @@ -476,14 +475,14 @@ public async Task Invariant_B15_Enhanced_CancellationDuringIO() } /// - /// Tests Invariant B.16 (🔵 Architectural): Only most recent RebalanceResult is applied to cache. + /// Tests Invariant B.6 (🔵 Architectural): Only most recent RebalanceResult is applied to cache. /// Verifies stale result prevention - if execution completes for an obsolete intent, results are discarded. /// This architectural guarantee prevents race conditions where slow rebalances from old intents /// could overwrite cache with stale data. Gap identified: No existing test validates result application /// guards against applying stale rebalance results. /// [Fact] - public async Task Invariant_B16_OnlyLatestResultsApplied() + public async Task Invariant_B_6_OnlyLatestResultsApplied() { // ARRANGE: Cache with longer debounce to control timing var options = TestHelpers.CreateDefaultOptions( @@ -527,7 +526,7 @@ public async Task Invariant_B16_OnlyLatestResultsApplied() #region C. Rebalance Intent & Temporal Invariants /// - /// Tests Invariant C.17 (🔵 Architectural): At most one rebalance intent may be active at any time. + /// Tests Invariant C.1 (🔵 Architectural): At most one rebalance intent may be active at any time. /// This is an architectural constraint enforced by single-writer design. Test verifies system stability /// and lifecycle integrity under rapid concurrent requests, not deterministic cancellation counts. /// Parameterized by execution strategy to verify behavior across both task-based and channel-based controllers. @@ -536,7 +535,7 @@ public async Task Invariant_B16_OnlyLatestResultsApplied() /// Queue capacity: null = task-based (unbounded), >= 1 = channel-based (bounded) [Theory] [MemberData(nameof(ExecutionStrategyTestData))] - public async Task Invariant_C17_AtMostOneActiveIntent(string executionStrategy, int? queueCapacity) + public async Task Invariant_C_1_AtMostOneActiveIntent(string executionStrategy, int? queueCapacity) { // ARRANGE var options = TestHelpers.CreateDefaultOptions( @@ -564,12 +563,12 @@ public async Task Invariant_C17_AtMostOneActiveIntent(string executionStrategy, } /// - /// Tests Invariant C.18 (🟡 Conceptual): Previously created intents may become logically superseded. + /// Tests Invariant C.2 (🟡 Conceptual): Previously created intents may become logically superseded. /// This is a conceptual design intent. Test verifies system stability and cache consistency when /// multiple intents are published, not deterministic cancellation behavior (obsolescence ≠ cancellation). /// [Fact] - public async Task Invariant_C18_PreviousIntentBecomesObsolete() + public async Task Invariant_C_2_PreviousIntentBecomesObsolete() { // ARRANGE var options = TestHelpers.CreateDefaultOptions(debounceDelay: TimeSpan.FromMilliseconds(150)); @@ -600,14 +599,14 @@ public async Task Invariant_C18_PreviousIntentBecomesObsolete() } /// - /// Tests Invariant C.20 (🔵 Architectural): Decision Engine MUST exit early if intent becomes obsolete. + /// Tests Invariant C.4 (🔵 Architectural): Decision Engine MUST exit early if intent becomes obsolete. /// When processing an intent, if the intent reference changes (new intent published), Decision Engine /// should detect obsolescence and exit without scheduling execution. This prevents wasted work and /// ensures the system processes only the most recent intent. Gap identified: No test validates /// early exit behavior when intents become obsolete during decision processing. /// [Fact] - public async Task Invariant_C20_DecisionEngineExitsEarlyForObsoleteIntent() + public async Task Invariant_C_4_DecisionEngineExitsEarlyForObsoleteIntent() { // ARRANGE: Longer debounce to allow time for multiple intents to be published var options = TestHelpers.CreateDefaultOptions( @@ -648,13 +647,13 @@ public async Task Invariant_C20_DecisionEngineExitsEarlyForObsoleteIntent() } /// - /// Tests Invariant C.24 (🟡 Conceptual): Intent does not guarantee execution. Execution is opportunistic - /// and may be skipped due to: C.24a (request within NoRebalanceRange), C.24b (debounce), - /// C.24c (DesiredCacheRange equals CurrentCacheRange), C.24d (cancellation). + /// Tests Invariant C.8 (🟡 Conceptual): Intent does not guarantee execution. Execution is opportunistic + /// and may be skipped due to: C.8b (request within NoRebalanceRange), C.8c (DesiredCacheRange equals CurrentCacheRange), + /// C.8d (cancellation/debounce). /// Demonstrates cache's opportunistic, efficiency-focused design. /// [Fact] - public async Task Invariant_C24_IntentDoesNotGuaranteeExecution() + public async Task Invariant_C_8_IntentDoesNotGuaranteeExecution() { // ARRANGE: Large threshold creates large NoRebalanceRange to block rebalance var options = TestHelpers.CreateDefaultOptions(leftCacheSize: 2.0, rightCacheSize: 2.0, @@ -680,13 +679,13 @@ public async Task Invariant_C24_IntentDoesNotGuaranteeExecution() } /// - /// Tests Invariant C.23 (🟢 Behavioral): System stabilizes when user access patterns stabilize. + /// Tests Invariant C.7 (🟢 Behavioral): System stabilizes when user access patterns stabilize. /// After initial burst, when access patterns stabilize (requests in same region), system converges /// to stable state where subsequent requests are served from cache without triggering rebalance. - /// Demonstrates cache's convergence behavior. Related: C.22 (best-effort convergence guarantee). + /// Demonstrates cache's convergence behavior. Related: C.6 (best-effort convergence guarantee). /// [Fact] - public async Task Invariant_C23_SystemStabilizesUnderLoad() + public async Task Invariant_C_7_SystemStabilizesUnderLoad() { // ARRANGE var options = TestHelpers.CreateDefaultOptions(debounceDelay: TimeSpan.FromMilliseconds(50)); @@ -714,13 +713,13 @@ public async Task Invariant_C23_SystemStabilizesUnderLoad() #region D. Rebalance Decision Path Invariants /// - /// Tests Invariant D.27 (🟢 Behavioral): If RequestedRange is fully contained within NoRebalanceRange, + /// Tests Invariant D.3 (🟢 Behavioral): If RequestedRange is fully contained within NoRebalanceRange, /// rebalance execution is prohibited. Verifies ThresholdRebalancePolicy prevents unnecessary rebalance /// when requests fall within "dead zone" around current cache, reducing I/O and CPU usage. - /// Corresponds to sub-invariant C.24a (execution skipped due to policy). + /// Corresponds to sub-invariant C.8b (execution skipped due to NoRebalanceRange policy). /// [Fact] - public async Task Invariant_D27_NoRebalanceIfRequestInNoRebalanceRange() + public async Task Invariant_D_3_NoRebalanceIfRequestInNoRebalanceRange() { // ARRANGE: Large thresholds to create wide NoRebalanceRange var options = TestHelpers.CreateDefaultOptions(leftCacheSize: 2.0, rightCacheSize: 2.0, @@ -740,14 +739,14 @@ public async Task Invariant_D27_NoRebalanceIfRequestInNoRebalanceRange() } /// - /// Tests Invariant D.27 Stage 1: Rebalance skipped when request is within current cache's NoRebalanceRange. + /// Tests Invariant D.3 Stage 1: Rebalance skipped when request is within current cache's NoRebalanceRange. /// Stage 1 (current cache stability check) is the fast-path optimization that prevents unnecessary /// rebalance when the requested range is fully covered by the existing cache's no-rebalance threshold zone. /// This validates the first stage of the multi-stage decision pipeline. - /// Related: D.27 (NoRebalanceRange policy), C.24a (execution skipped due to policy). + /// Related: D.3 (NoRebalanceRange policy), C.8b (execution skipped due to NoRebalanceRange policy). /// [Fact] - public async Task Invariant_D27_Stage1_SkipsWhenWithinCurrentNoRebalanceRange() + public async Task Invariant_D_3_Stage1_SkipsWhenWithinCurrentNoRebalanceRange() { // ARRANGE: Set up cache with threshold configuration var options = TestHelpers.CreateDefaultOptions( @@ -776,14 +775,14 @@ public async Task Invariant_D27_Stage1_SkipsWhenWithinCurrentNoRebalanceRange() } /// - /// Tests Invariant D.29 Stage 2: Rebalance skipped when request is within pending rebalance's NoRebalanceRange. + /// Tests Invariant D.5 Stage 2: Rebalance skipped when request is within pending rebalance's NoRebalanceRange. /// Stage 2 (pending rebalance stability check) is the anti-thrashing optimization that prevents /// cancellation storms when a scheduled rebalance will already satisfy the incoming request. /// This validates the second stage of the multi-stage decision pipeline. - /// Related: D.29 (multi-stage validation), C.18 (intent supersession with validation). + /// Related: D.5 (multi-stage validation), C.2 (intent supersession with validation). /// [Fact] - public async Task Invariant_D29_Stage2_SkipsWhenWithinPendingNoRebalanceRange() + public async Task Invariant_D_5_Stage2_SkipsWhenWithinPendingNoRebalanceRange() { // ARRANGE: Set up cache with threshold and debounce to allow multiple intents var options = TestHelpers.CreateDefaultOptions( @@ -829,20 +828,20 @@ public async Task Invariant_D29_Stage2_SkipsWhenWithinPendingNoRebalanceRange() } /// - /// Tests Invariant D.28 (🟢 Behavioral): If DesiredCacheRange == CurrentCacheRange, rebalance execution - /// is not required (Stage 3 validation / same-range optimization). This is the final decision stage that + /// Tests Invariant D.4 (🟢 Behavioral): If DesiredCacheRange == CurrentCacheRange, rebalance execution + /// is not required (Stage 4 validation / same-range optimization). This is the final decision stage that /// prevents no-op rebalance operations when the cache is already in optimal configuration for the request. /// Verifies the RebalanceSkippedSameRange counter tracks this optimization. - /// Related: C.24c (execution skipped due to same range), D.29 (multi-stage decision pipeline). + /// Related: C.8c (execution skipped due to same range), D.5 (multi-stage decision pipeline). /// [Fact] - public async Task Invariant_D28_SkipWhenDesiredEqualsCurrentRange() + public async Task Invariant_D_4_SkipWhenDesiredEqualsCurrentRange() { // ARRANGE var options = TestHelpers.CreateDefaultOptions( leftCacheSize: 1.0, rightCacheSize: 1.0, - leftThreshold: 1, // Very small NoRebalanceRange - forces decision to Stage 3 + leftThreshold: 1, // Very small NoRebalanceRange - forces decision to Stage 4 rightThreshold: 0.0, debounceDelay: TimeSpan.FromMilliseconds(50)); var (cache, _) = TrackCache(TestHelpers.CreateCacheWithDefaults(_domain, _cacheDiagnostics, options)); @@ -858,7 +857,7 @@ public async Task Invariant_D28_SkipWhenDesiredEqualsCurrentRange() var result = await cache.GetDataAsync(initialRange, CancellationToken.None); await cache.WaitForIdleAsync(); - // ASSERT: Verify same-range skip occurred (Stage 3 validation) + // ASSERT: Verify same-range skip occurred (Stage 4 validation) TestHelpers.AssertUserDataCorrect(result.Data, initialRange); TestHelpers.AssertIntentPublished(_cacheDiagnostics, 1); TestHelpers.AssertRebalanceSkippedSameRange(_cacheDiagnostics, 1); @@ -874,14 +873,14 @@ public async Task Invariant_D28_SkipWhenDesiredEqualsCurrentRange() #region E. Cache Geometry & Policy Invariants /// - /// Tests Invariant E.30 (🟢 Behavioral): DesiredCacheRange is computed solely from RequestedRange + /// Tests Invariant E.1 (🟢 Behavioral): DesiredCacheRange is computed solely from RequestedRange /// and cache configuration. Verifies ProportionalRangePlanner computes desired cache range deterministically /// based only on user's requested range and config parameters (leftCacheSize, rightCacheSize), independent /// of current cache contents. With config (leftSize=1.0, rightSize=1.0), cache expands by RequestedRange.Span - /// on each side. Related: E.31 (Architectural - DesiredCacheRange independent of current cache contents). + /// on each side. Related: E.2 (Architectural - DesiredCacheRange independent of current cache contents). /// [Fact] - public async Task Invariant_E30_DesiredRangeComputedFromConfigAndRequest() + public async Task Invariant_E_1_DesiredRangeComputedFromConfigAndRequest() { // ARRANGE: Expansion coefficients: leftSize=1.0 (expand left by 100%), rightSize=1.0 (expand right by 100%) var options = TestHelpers.CreateDefaultOptions(leftCacheSize: 1.0, rightCacheSize: 1.0, @@ -914,14 +913,14 @@ public async Task Invariant_E30_DesiredRangeComputedFromConfigAndRequest() } /// - /// Tests Invariant E.31 (🔵 Architectural): DesiredCacheRange is independent of current cache contents. + /// Tests Invariant E.2 (🔵 Architectural): DesiredCacheRange is independent of current cache contents. /// Verifies that DesiredCacheRange is computed deterministically based only on RequestedRange and config, /// not influenced by CurrentCacheRange or intermediate cache states. Two identical requests should produce /// identical desired ranges regardless of what cache state existed before. Gap identified: No test validates /// that desired range computation is truly independent of cache history. /// [Fact] - public async Task Invariant_E31_DesiredRangeIndependentOfCacheState() + public async Task Invariant_E_2_DesiredRangeIndependentOfCacheState() { // ARRANGE: Create two separate cache instances with identical configuration var options = TestHelpers.CreateDefaultOptions( @@ -968,7 +967,7 @@ public async Task Invariant_E31_DesiredRangeIndependentOfCacheState() await cache2.DisposeAsync(); } - // NOTE: Invariant E.32, E.33, E.34: DesiredCacheRange represents canonical target state, + // NOTE: Invariant E.3, E.4, E.5: DesiredCacheRange represents canonical target state, // represents canonical target state, geometry determined by configuration, // NoRebalanceRange derived from CurrentCacheRange and config // Cannot be directly observed via public API - requires internal state inspection @@ -1048,20 +1047,20 @@ public async Task CacheHitMiss_AllScenarios() #region F. Rebalance Execution Invariants /// - /// Tests Invariants F.35 (🟢 Behavioral), F.35a (🔵 Architectural), and G.46 (🟢 Behavioral): + /// Tests Invariants F.1 (🟢 Behavioral), F.1a (🔵 Architectural), and G.4 (🟢 Behavioral): /// Rebalance Execution MUST be cancellation-safe at all stages (before I/O, during I/O, before mutations). /// Validates deterministic termination, no partial mutations, lifecycle integrity, and that cancellation /// support works as a high-level guarantee (not deterministic per-request behavior). /// Uses slow data source to allow cancellation during execution. Verifies DEBUG instrumentation counters - /// ensure proper lifecycle tracking. Related: A.0a (User Path priority via validation-driven cancellation), - /// C.24d (execution skipped due to cancellation). + /// ensure proper lifecycle tracking. Related: A.2a (User Path priority via validation-driven cancellation), + /// C.8d (execution skipped due to cancellation). /// Parameterized by execution strategy to verify behavior across both task-based and channel-based controllers. /// /// Human-readable name of execution strategy for test output /// Queue capacity: null = task-based (unbounded), >= 1 = channel-based (bounded) [Theory] [MemberData(nameof(ExecutionStrategyTestData))] - public async Task Invariant_F35_G46_RebalanceCancellationBehavior(string executionStrategy, int? queueCapacity) + public async Task Invariant_F_1_G_4_RebalanceCancellationBehavior(string executionStrategy, int? queueCapacity) { // ARRANGE: Slow data source to allow cancellation during execution var options = TestHelpers.CreateDefaultOptions( @@ -1078,11 +1077,11 @@ public async Task Invariant_F35_G46_RebalanceCancellationBehavior(string executi await cache.GetDataAsync(TestHelpers.CreateRange(110, 120), CancellationToken.None); await cache.WaitForIdleAsync(); - // ASSERT: Verify cancellation-safety (F.35, G.46) + // ASSERT: Verify cancellation-safety (F.1, G.4) // Focus on lifecycle integrity and system stability, not deterministic cancellation counts // Cancellation is triggered by Decision Engine scheduling, not automatically by requests - // Verify Rebalance lifecycle integrity: every started execution reaches terminal state (F.35) + // Verify Rebalance lifecycle integrity: every started execution reaches terminal state (F.1) TestHelpers.AssertRebalanceLifecycleIntegrity(_cacheDiagnostics); // Verify system stability: at least one rebalance completed successfully @@ -1091,7 +1090,7 @@ public async Task Invariant_F35_G46_RebalanceCancellationBehavior(string executi } /// - /// Tests Invariant F.36 (🔵 Architectural) and F.36a (🟢 Behavioral): Rebalance Execution Path is the + /// Tests Invariant F.2 (🔵 Architectural) and F.2a (🟢 Behavioral): Rebalance Execution Path is the /// only path responsible for cache normalization (expanding, trimming, recomputing NoRebalanceRange). /// After rebalance completes, cache is normalized to serve data from expanded range beyond original request. /// User Path performs minimal mutations while Rebalance Execution handles optimization. @@ -1101,7 +1100,7 @@ public async Task Invariant_F35_G46_RebalanceCancellationBehavior(string executi /// Storage read mode: Snapshot or CopyOnRead [Theory] [MemberData(nameof(StorageStrategyTestData))] - public async Task Invariant_F36a_RebalanceNormalizesCache(string storageName, UserCacheReadMode readMode) + public async Task Invariant_F_2a_RebalanceNormalizesCache(string storageName, UserCacheReadMode readMode) { // ARRANGE _ = storageName; @@ -1126,9 +1125,9 @@ public async Task Invariant_F36a_RebalanceNormalizesCache(string storageName, Us } /// - /// Tests Invariants F.40, F.41, F.42 (🟢 Behavioral/🟡 Conceptual): Post-execution guarantees. - /// F.40: CacheData corresponds to DesiredCacheRange. F.41: CurrentCacheRange == DesiredCacheRange. - /// F.42: NoRebalanceRange is recomputed. After successful rebalance, cache reaches normalized state + /// Tests Invariants F.6, F.7, F.8 (🟢 Behavioral/🟡 Conceptual): Post-execution guarantees. + /// F.6: CacheData corresponds to DesiredCacheRange. F.7: CurrentCacheRange == DesiredCacheRange. + /// F.8: NoRebalanceRange is recomputed. After successful rebalance, cache reaches normalized state /// serving data from expanded/optimized range (based on config with leftSize=1.0, rightSize=1.0). /// Parameterized by storage strategy to verify behavior across both Snapshot and CopyOnRead modes. /// @@ -1136,7 +1135,7 @@ public async Task Invariant_F36a_RebalanceNormalizesCache(string storageName, Us /// Storage read mode: Snapshot or CopyOnRead [Theory] [MemberData(nameof(StorageStrategyTestData))] - public async Task Invariant_F40_F41_F42_PostExecutionGuarantees(string storageName, UserCacheReadMode readMode) + public async Task Invariant_F_6_F_7_F_8_PostExecutionGuarantees(string storageName, UserCacheReadMode readMode) { // ARRANGE _ = storageName; @@ -1152,7 +1151,7 @@ public async Task Invariant_F40_F41_F42_PostExecutionGuarantees(string storageNa // ASSERT: At least one rebalance must complete for the post-execution guarantees to be meaningful Assert.True(_cacheDiagnostics.RebalanceExecutionCompleted > 0, - "At least one rebalance must complete so that F.40/F.41/F.42 post-execution guarantees can be verified."); + "At least one rebalance must complete so that F.6/F.7/F.8 post-execution guarantees can be verified."); // Verify rebalance was scheduled TestHelpers.AssertRebalanceScheduled(_cacheDiagnostics, 1); // After rebalance, cache should serve data from normalized range [100-10, 110+10] = [90, 120] @@ -1161,13 +1160,13 @@ public async Task Invariant_F40_F41_F42_PostExecutionGuarantees(string storageNa } /// - /// Tests Invariant F.38 (🟢 Behavioral): Incremental fetch optimization - only missing subranges are fetched. + /// Tests Invariant F.4 (🟢 Behavioral): Incremental fetch optimization - only missing subranges are fetched. /// When cache needs to expand, the system should fetch only the missing data segments from IDataSource, /// not the entire desired range. This optimization reduces I/O overhead and data source load. /// Gap identified: No test validates that only missing segments are fetched during cache expansion. /// [Fact] - public async Task Invariant_F38_IncrementalFetchOptimization() + public async Task Invariant_F_4_IncrementalFetchOptimization() { // ARRANGE: Create tracking mock to observe which ranges are fetched var options = TestHelpers.CreateDefaultOptions( @@ -1225,13 +1224,13 @@ public async Task Invariant_F38_IncrementalFetchOptimization() } /// - /// Tests Invariant F.39 (🟢 Behavioral): Data preservation during expansion - existing data is not refetched. + /// Tests Invariant F.5 (🟢 Behavioral): Data preservation during expansion - existing data is not refetched. /// When cache expands to include additional data, the system MUST NOT refetch ranges that are already /// present in the cache. This is a critical efficiency guarantee that prevents wasteful I/O operations. /// Gap identified: No test validates that existing cached data is preserved without refetching. /// [Fact] - public async Task Invariant_F39_DataPreservationDuringExpansion() + public async Task Invariant_F_5_DataPreservationDuringExpansion() { // ARRANGE: Create tracking mock to observe fetch patterns var options = TestHelpers.CreateDefaultOptions( @@ -1287,15 +1286,15 @@ public async Task Invariant_F39_DataPreservationDuringExpansion() #region G. Execution Context & Scheduling Invariants /// - /// Tests Invariants G.43, G.44, G.45: Execution context separation between User Path and Rebalance operations. - /// G.43: User Path operates in user execution context (request completes quickly). - /// G.44: Rebalance Decision/Execution Path execute outside user context (Task.Run). - /// G.45: Rebalance Execution performs I/O only in background context (not blocking user). + /// Tests Invariants G.1, G.2, G.3: Execution context separation between User Path and Rebalance operations. + /// G.1: User Path operates in user execution context (request completes quickly). + /// G.2: Rebalance Decision/Execution Path execute outside user context (Task.Run). + /// G.3: Rebalance Execution performs I/O only in background context (not blocking user). /// Verifies user requests complete quickly without blocking on background operations, proving rebalance /// work is properly scheduled on background threads. Critical for maintaining responsive user-facing latency. /// [Fact] - public async Task Invariant_G43_G44_G45_ExecutionContextSeparation() + public async Task Invariant_G_1_G_2_G_3_ExecutionContextSeparation() { // ARRANGE var options = TestHelpers.CreateDefaultOptions(debounceDelay: TimeSpan.FromMilliseconds(100)); @@ -1316,14 +1315,14 @@ public async Task Invariant_G43_G44_G45_ExecutionContextSeparation() } /// - /// Tests Invariant G.46 (🟢 Behavioral): User-facing cancellation during IDataSource fetch operations. + /// Tests Invariant G.4 (🟢 Behavioral): User-facing cancellation during IDataSource fetch operations. /// Verifies User Path properly propagates cancellation token through to IDataSource.FetchAsync(). /// Users can cancel their own requests during potentially long-running data source operations. - /// Related: G.46 covers "all scenarios" - this test focuses on user-facing cancellation. - /// See also: Invariant_F35_G46 for background rebalance cancellation. + /// Related: G.4 covers "all scenarios" - this test focuses on user-facing cancellation. + /// See also: Invariant_F_1_G_4 for background rebalance cancellation. /// [Fact] - public async Task Invariant_G46_UserCancellationDuringFetch() + public async Task Invariant_G_4_UserCancellationDuringFetch() { // ARRANGE: Slow mock data source to allow cancellation during fetch var (cache, _) = TrackCache(TestHelpers.CreateCacheWithDefaults(_domain, _cacheDiagnostics, @@ -1350,9 +1349,9 @@ public async Task Invariant_G46_UserCancellationDuringFetch() /// /// Comprehensive integration test covering multiple invariants in realistic usage scenario. - /// Tests: Cold start (A.8), Cache expansion (A.8), Background rebalance normalization (F.36a), - /// Non-intersecting replacement (A.8, A.9a), Cache consistency (B.11). - /// Validates all components work correctly together. Verifies: user requests always served (A.1), + /// Tests: Cold start (A.12), Cache expansion (A.12), Background rebalance normalization (F.2a), + /// Non-intersecting replacement (A.12, A.12b), Cache consistency (B.1). + /// Validates all components work correctly together. Verifies: user requests always served (A.3), /// data is correct (A.10), cache properly maintains state through multiple transitions. /// [Fact] @@ -1399,9 +1398,9 @@ public async Task CompleteScenario_MultipleRequestsWithRebalancing() /// /// Comprehensive concurrency test with rapid burst of 20 concurrent requests verifying intent cancellation - /// and system stability under high load. Validates: All requests served correctly (A.1, A.10), - /// Intent cancellation works (C.17, C.18), At most one active intent (C.17), - /// Cache remains consistent (B.11, B.15). Ensures single-consumer model with cancellation-based + /// and system stability under high load. Validates: All requests served correctly (A.3, A.10), + /// Intent cancellation works (C.1, C.2), At most one active intent (C.1), + /// Cache remains consistent (B.1, B.5). Ensures single-consumer model with cancellation-based /// coordination handles realistic high-load scenarios without data corruption or request failures. /// Parameterized by execution strategy to verify behavior across both task-based and channel-based controllers. /// diff --git a/tests/SlidingWindowCache.Tests.Infrastructure/Helpers/TestHelpers.cs b/tests/SlidingWindowCache.Tests.Infrastructure/Helpers/TestHelpers.cs index 6d77a6f..cecb6d2 100644 --- a/tests/SlidingWindowCache.Tests.Infrastructure/Helpers/TestHelpers.cs +++ b/tests/SlidingWindowCache.Tests.Infrastructure/Helpers/TestHelpers.cs @@ -437,7 +437,7 @@ public static void AssertRebalanceScheduled(EventCounterCacheDiagnostics cacheDi } /// - /// Asserts that rebalance was skipped because DesiredCacheRange equals CurrentCacheRange (Stage 3 / D.28). + /// Asserts that rebalance was skipped because DesiredCacheRange equals CurrentCacheRange (Stage 4 / D.4). /// /// The diagnostics instance to check. /// Minimum number of same-range skips expected (default: 1). @@ -459,7 +459,7 @@ public static void AssertRebalanceSkippedSameRange(EventCounterCacheDiagnostics /// Decision Pipeline Stages: /// - Stage 1: Current NoRebalanceRange check → SkippedCurrentNoRebalanceRange /// - Stage 2: Pending NoRebalanceRange check → SkippedPendingNoRebalanceRange - /// - Stage 3: DesiredCacheRange == CurrentCacheRange → SkippedSameRange + /// - Stage 4: DesiredCacheRange == CurrentCacheRange → SkippedSameRange /// - All stages pass → RebalanceScheduled /// - Intent superseded before decision → IntentCancelled /// @@ -473,14 +473,14 @@ public static void AssertRebalancePipelineIntegrity(EventCounterCacheDiagnostics var scheduled = cacheDiagnostics.RebalanceScheduled; var skippedStage1 = cacheDiagnostics.RebalanceSkippedCurrentNoRebalanceRange; var skippedStage2 = cacheDiagnostics.RebalanceSkippedPendingNoRebalanceRange; - var skippedStage3 = cacheDiagnostics.RebalanceSkippedSameRange; + var skippedStage4 = cacheDiagnostics.RebalanceSkippedSameRange; // Decision phase: All intents must be accounted for - var totalDecisionOutcomes = scheduled + skippedStage1 + skippedStage2 + skippedStage3; + var totalDecisionOutcomes = scheduled + skippedStage1 + skippedStage2 + skippedStage4; Assert.True(totalDecisionOutcomes <= intentPublished, $"Decision outcomes ({totalDecisionOutcomes}) cannot exceed intents published ({intentPublished}). " + $"Breakdown: Scheduled={scheduled}, SkippedStage1={skippedStage1}, SkippedStage2={skippedStage2}, " + - $"SkippedStage3={skippedStage3}"); + $"SkippedStage4={skippedStage4}"); // Execution phase: Verify lifecycle integrity AssertRebalanceLifecycleIntegrity(cacheDiagnostics); diff --git a/tests/SlidingWindowCache.Unit.Tests/Infrastructure/Storage/CopyOnReadStorageTests.cs b/tests/SlidingWindowCache.Unit.Tests/Infrastructure/Storage/CopyOnReadStorageTests.cs index c2c223f..7f1b712 100644 --- a/tests/SlidingWindowCache.Unit.Tests/Infrastructure/Storage/CopyOnReadStorageTests.cs +++ b/tests/SlidingWindowCache.Unit.Tests/Infrastructure/Storage/CopyOnReadStorageTests.cs @@ -9,7 +9,7 @@ namespace SlidingWindowCache.Unit.Tests.Infrastructure.Storage; /// /// Unit tests for CopyOnReadStorage that verify the ICacheStorage interface contract, -/// data correctness (Invariant B.11), dual-buffer staging pattern, and error handling. +/// data correctness (Invariant B.1), dual-buffer staging pattern, and error handling. /// Shared tests are inherited from . /// public class CopyOnReadStorageTests : CacheStorageTestsBase diff --git a/tests/SlidingWindowCache.Unit.Tests/Infrastructure/Storage/SnapshotReadStorageTests.cs b/tests/SlidingWindowCache.Unit.Tests/Infrastructure/Storage/SnapshotReadStorageTests.cs index 2b16262..bca702d 100644 --- a/tests/SlidingWindowCache.Unit.Tests/Infrastructure/Storage/SnapshotReadStorageTests.cs +++ b/tests/SlidingWindowCache.Unit.Tests/Infrastructure/Storage/SnapshotReadStorageTests.cs @@ -7,7 +7,7 @@ namespace SlidingWindowCache.Unit.Tests.Infrastructure.Storage; /// /// Unit tests for SnapshotReadStorage that verify the ICacheStorage interface contract, -/// data correctness (Invariant B.11), and error handling. +/// data correctness (Invariant B.1), and error handling. /// Shared tests are inherited from . /// public class SnapshotReadStorageTests : CacheStorageTestsBase diff --git a/tests/SlidingWindowCache.Unit.Tests/Infrastructure/Storage/TestInfrastructure/CacheStorageTestsBase.cs b/tests/SlidingWindowCache.Unit.Tests/Infrastructure/Storage/TestInfrastructure/CacheStorageTestsBase.cs index a96c12a..197a2c1 100644 --- a/tests/SlidingWindowCache.Unit.Tests/Infrastructure/Storage/TestInfrastructure/CacheStorageTestsBase.cs +++ b/tests/SlidingWindowCache.Unit.Tests/Infrastructure/Storage/TestInfrastructure/CacheStorageTestsBase.cs @@ -8,7 +8,7 @@ namespace SlidingWindowCache.Unit.Tests.Infrastructure.Storage.TestInfrastructur /// /// Abstract base class providing shared test coverage for all -/// implementations, enforcing the ICacheStorage interface contract, data correctness (Invariant B.11), +/// implementations, enforcing the ICacheStorage interface contract, data correctness (Invariant B.1), /// and error handling. /// /// @@ -399,10 +399,10 @@ public void ToRangeData_AfterMultipleRematerializations_ReflectsCurrentState() #endregion - #region Invariant B.11 Tests (Data/Range Consistency) + #region Invariant B.1 Tests (Data/Range Consistency) [Fact] - public void InvariantB11_DataLengthMatchesRangeSize_AfterRematerialize() + public void InvariantB1_DataLengthMatchesRangeSize_AfterRematerialize() { // ARRANGE var domain = CreateFixedStepDomain(); @@ -413,13 +413,13 @@ public void InvariantB11_DataLengthMatchesRangeSize_AfterRematerialize() storage.Rematerialize(rangeData); var data = storage.Read(storage.Range); - // ASSERT - Data length must equal range size (Invariant B.11) + // ASSERT - Data length must equal range size (Invariant B.1) var expectedLength = 51; // [0, 50] inclusive = 51 elements Assert.Equal(expectedLength, data.Length); } [Fact] - public void InvariantB11_DataLengthMatchesRangeSize_AfterMultipleRematerializations() + public void InvariantB1_DataLengthMatchesRangeSize_AfterMultipleRematerializations() { // ARRANGE var domain = CreateFixedStepDomain(); @@ -437,7 +437,7 @@ public void InvariantB11_DataLengthMatchesRangeSize_AfterMultipleRematerializati } [Fact] - public void InvariantB11_PartialReads_ConsistentWithStoredRange() + public void InvariantB1_PartialReads_ConsistentWithStoredRange() { // ARRANGE var domain = CreateFixedStepDomain();