diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index ee45df1..ab50396 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -81,6 +81,7 @@ jobs: run: | cargo miri test --package cachekit --lib ds:: -- --skip concurrent --skip stress --skip large --skip performance --skip memory cargo miri test --package cachekit --lib policy:: -- --skip concurrent --skip stress --skip large --skip performance --skip memory + cargo miri test --test policy_semantics --all-features smoke_ -- --test-threads=1 env: MIRIFLAGS: -Zmiri-isolation-error=warn @@ -93,7 +94,9 @@ jobs: - uses: actions/checkout@v6 - uses: actions-rust-lang/setup-rust-toolchain@v1 - name: Run property tests with increased cases - run: PROPTEST_CASES=1000 cargo test --lib property_tests + run: | + PROPTEST_CASES=1000 cargo test --lib property_tests + PROPTEST_CASES=1000 cargo test --test policy_semantics --all-features env: RUST_BACKTRACE: 1 diff --git a/.gitignore b/.gitignore index 00196c8..07a4902 100644 --- a/.gitignore +++ b/.gitignore @@ -66,3 +66,10 @@ docs/benchmarks/*/* !docs/benchmarks/*/charts.js !docs/benchmarks/*/index.md !docs/benchmarks/*/results.json + +# TLA+ TLC run artifacts (manual model checking — see docs/testing/specs/formal/). +# Spec sources (*.tla, *.cfg) stay tracked; TLC writes these on each run. +docs/testing/specs/formal/**/states/ +docs/testing/specs/formal/**/*_TTrace_*.bin +docs/testing/specs/formal/**/*_TTrace_*.tla +docs/testing/specs/formal/**/*.tlc diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index a09f852..c87b872 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -216,6 +216,13 @@ Use conventional commit format for PR titles: Consider using `proptest` for testing complex invariants. +### Policy Semantic Oracles + +New eviction policies with deterministic semantics should include a +reference model in `tests/abstract_models/` and proptest/smoke coverage +in `tests/policy_semantics/`. See +[Policy semantic testing](docs/testing/static-analysis.md). + ### Test Organization ```rust diff --git a/docs/design/trait-hierarchy.md b/docs/design/trait-hierarchy.md index 27b773c..36f20ff 100644 --- a/docs/design/trait-hierarchy.md +++ b/docs/design/trait-hierarchy.md @@ -401,6 +401,12 @@ it. The `RecencyTracking` / `FrequencyTracking` / `HistoryTracking` naming established the convention; adding `WeightTracking` only when GDS lands keeps the surface honest. +## Testing + +Policy semantic tests assert behavior through these capability traits +(`VictimInspectable`, `RecencyTracking`, `EvictingCache`, etc.). See +[Policy semantic testing](../testing/static-analysis.md). + ## See also - [Design overview](design.md) — §7 frames the layering at the diff --git a/docs/index.md b/docs/index.md index 07faa26..a99a821 100644 --- a/docs/index.md +++ b/docs/index.md @@ -59,4 +59,5 @@ Key features: ## Testing and Fuzzing - [Testing strategy](testing/testing.md) +- [Policy semantic testing](testing/static-analysis.md) - [Adding fuzz targets](testing/adding-fuzz-targets.md) diff --git a/docs/policies/README.md b/docs/policies/README.md index 3fb33d5..7b2e818 100644 --- a/docs/policies/README.md +++ b/docs/policies/README.md @@ -34,25 +34,25 @@ If you can only implement one “general purpose” policy for mixed workloads, ### Implemented Policies (CacheKit) -| Policy | Summary | Doc | -|--------|---------|-----| -| LRU | Strong default for temporal locality | [LRU doc](lru.md) | -| MRU | Evicts most recent (niche: cyclic patterns) | [MRU doc](mru.md) | -| SLRU | Segmented LRU with probation/protected | [SLRU doc](slru.md) | -| LFU | Frequency-driven, stable hot sets | [LFU doc](lfu.md) | -| Heap-LFU | LFU with heap eviction | [Heap-LFU doc](heap-lfu.md) | -| MFU | Evicts highest frequency (niche/baseline) | [MFU doc](mfu.md) | -| LRU-K | Scan-resistant recency | [LRU-K doc](lru-k.md) | -| 2Q | Probation + protected queues | [2Q doc](2q.md) | -| ARC | Adaptive recency/frequency balance | [ARC doc](arc.md) | -| CAR | ARC-like with Clock (lower hit overhead) | [CAR doc](car.md) | -| FIFO | Simple insertion-order (oldest first) | [FIFO doc](fifo.md) | -| LIFO | Stack-based (newest first) | [LIFO doc](lifo.md) | -| Clock | Approximate LRU | [Clock doc](clock.md) | -| Clock-PRO | Scan-resistant Clock variant | [Clock-PRO doc](clock-pro.md) | -| NRU | Coarse recency tracking | [NRU doc](nru.md) | -| S3-FIFO | Scan-resistant FIFO | [S3-FIFO doc](s3-fifo.md) | -| Random | Baseline: uniform random eviction | [Random doc](random.md) | +| Policy | Summary | Semantic oracle | Doc | +|--------|---------|-----------------|-----| +| LRU | Strong default for temporal locality | exact | [LRU doc](lru.md) | +| MRU | Evicts most recent (niche: cyclic patterns) | exact | [MRU doc](mru.md) | +| SLRU | Segmented LRU with probation/protected | mirror | [SLRU doc](slru.md) | +| LFU | Frequency-driven, stable hot sets | exact | [LFU doc](lfu.md) | +| Heap-LFU | LFU with heap eviction | exact | [Heap-LFU doc](heap-lfu.md) | +| MFU | Evicts highest frequency (niche/baseline) | exact | [MFU doc](mfu.md) | +| LRU-K | Scan-resistant recency | exact | [LRU-K doc](lru-k.md) | +| 2Q | Probation + protected queues | mirror | [2Q doc](2q.md) | +| ARC | Adaptive recency/frequency balance | bounded | [ARC doc](arc.md) | +| CAR | ARC-like with Clock (lower hit overhead) | bounded | [CAR doc](car.md) | +| FIFO | Simple insertion-order (oldest first) | exact | [FIFO doc](fifo.md) | +| LIFO | Stack-based (newest first) | exact | [LIFO doc](lifo.md) | +| Clock | Approximate LRU | mirror | [Clock doc](clock.md) | +| Clock-PRO | Scan-resistant Clock variant | bounded | [Clock-PRO doc](clock-pro.md) | +| NRU | Coarse recency tracking | mirror | [NRU doc](nru.md) | +| S3-FIFO | Scan-resistant FIFO | bounded | [S3-FIFO doc](s3-fifo.md) | +| Random | Baseline: uniform random eviction | none | [Random doc](random.md) | ### Roadmap Policies (Planned) diff --git a/docs/testing/specs/README.md b/docs/testing/specs/README.md new file mode 100644 index 0000000..5be8bcd --- /dev/null +++ b/docs/testing/specs/README.md @@ -0,0 +1,87 @@ +# Operational policy specs + +Human-readable specifications for eviction policies used as the **source of truth** for test-side oracles. + +## Directory layout + +```text +docs/testing/specs/ +├── README.md, matrix.md, template.md, tla-guide.md # hub docs +├── _includes/ # shared fragments (Op mapping, maturity levels) +├── policies/ # human operational specs by tier +│ ├── exact/ # FIFO, LRU, LFU, … +│ ├── mirror/ # Clock, 2Q, … +│ ├── bounded/ # ARC, S3-FIFO, … +│ └── composed/ # TTL +└── formal/ # TLA+ modules + TLC runbooks + ├── fifo/ + └── lru/ +``` + +**Canonical index:** [matrix.md](matrix.md) (maturity, harness mode, model paths per policy). + +## Pipeline (all tiers) + +```text +policies//.md + → reference/ PolicyModel (optional — independent formulation) + → exact/ PolicyModel (deque / DS-shaped oracle) + → policy_semantics dual-run vs implementation +``` + +| Tier | Harness mode | Oracle | +|------|--------------|--------| +| Exact / mirror | DualRun | `exact/` `PolicyModel` vs impl | +| Exact (policies with `reference/` rows) | CrossModel | `reference/` vs `exact/` | +| Bounded | InvariantOnly | structural invariants on impl | +| Composed (TTL) | DualRun + deadlines | `LruOccupancyModel` + TTL layer | + +Cross-model tests prove `reference/` agrees with `exact/` on the same traces. Impl dual-run proves `exact/` agrees with real caches. + +## Required sections (every policy spec) + +Use [template.md](template.md) as the skeleton: + +1. **Maturity banner** — `stub`, `reference`, and/or `tla` +2. **State variables** — abstract state at rest between operations +3. **Init** — empty cache at capacity `C` +4. **Per-`Op` transitions** — match the harness [`Op`](../../../tests/abstract_models/mod.rs) alphabet +5. **Tie-breaks** — deterministic victim and rank when multiple keys qualify +6. **Observables** — `resident`, `peek_victim`, `recency_rank` (if applicable), `hit` classification +7. **API mapping** — how each `Op` maps to cache traits (`peek` must not promote on LRU, etc.) + +Shared harness `Op` table: [_includes/harness-op-mapping.md](_includes/harness-op-mapping.md). Trait semantics: [trait hierarchy](../../design/trait-hierarchy.md). + +## Spec-change checklist + +When a spec changes, update in order: + +1. Spec doc under `policies//` +2. `tests/abstract_models/reference/.rs` (if reference model exists) +3. Cross-model test expectations (if behavior changed) +4. `tests/abstract_models/exact/.rs` if the exact model was wrong +5. `formal//` TLA+ module and `tlc.md` alignment notes (if applicable) +6. Row in [matrix.md](matrix.md) + +## TLA+ (optional manual check) + +FIFO and LRU include TLA+ pilots under [formal/](formal/README.md). **Read first:** [tla-guide.md](tla-guide.md). TLC is **not** run in CI. + +```bash +./scripts/run-tlc.sh fifo # or ./scripts/run-fifo-tlc.sh +./scripts/run-tlc.sh lru # or ./scripts/run-lru-tlc.sh +``` + +Success: no `SemanticOK` violation on the bundled config. Runbooks: [formal/fifo/tlc.md](formal/fifo/tlc.md), [formal/lru/tlc.md](formal/lru/tlc.md). + +**TLC vs Rust:** TLC proves `SemanticOK` on reachable states for a finite instance; proptest runs long sequential traces on `u8` keys. They are complementary. + +## Related documentation + +- [Policy matrix](matrix.md) — canonical index +- [Policy specs by tier](policies/README.md) +- [Spec template](template.md) — new policy skeleton +- [TLA+ guide](tla-guide.md) — contributor guide +- [Abstract models README](../../../tests/abstract_models/README.md) +- [Policy semantic testing](../static-analysis.md) +- [Testing strategy](../testing.md) diff --git a/docs/testing/specs/_includes/harness-op-mapping.md b/docs/testing/specs/_includes/harness-op-mapping.md new file mode 100644 index 0000000..6c67cd2 --- /dev/null +++ b/docs/testing/specs/_includes/harness-op-mapping.md @@ -0,0 +1,15 @@ +# Harness `Op` mapping (shared) + +Standard mapping from harness [`Op`](../../../../tests/abstract_models/mod.rs) to cache traits. Copy into policy specs; adjust side effects per policy. + +| `Op` | Cache API | Typical side effects | +|------|-----------|----------------------| +| `Insert(k)` | `insert(k, v)` | Evict if full; may promote on re-insert (policy-specific) | +| `Get(k)` | `get(k)` | Promote on hit (recency / frequency policies) | +| `Peek(k)` | `peek(k)` | **No promotion** on LRU-family policies | +| `GetMut(k)` | `get_mut(k)` | Promote on hit where adapter models it | +| `Touch(k)` | `touch(k)` | Promote on hit | +| `Remove(k)` | `remove(k)` | Remove key; ordering side effects policy-specific | +| `EvictOne` | `evict_one()` | Evict victim per policy rule | + +Align with [trait hierarchy](../../../design/trait-hierarchy.md): `Peek` must not change `recency_rank` on LRU-family policies. diff --git a/docs/testing/specs/_includes/spec-maturity.md b/docs/testing/specs/_includes/spec-maturity.md new file mode 100644 index 0000000..35c4843 --- /dev/null +++ b/docs/testing/specs/_includes/spec-maturity.md @@ -0,0 +1,9 @@ +# Spec maturity levels (shared) + +| Level | Meaning | +|-------|---------| +| `stub` | Transcribed from executable oracle; independent reference pending | +| `reference` | Independent naive `reference/` model exists | +| `tla` | Machine-readable TLA+ module under [`formal/`](../formal/README.md) + TLC runbook | + +Canonical per-policy status: [matrix.md](../matrix.md). diff --git a/docs/testing/specs/formal/README.md b/docs/testing/specs/formal/README.md new file mode 100644 index 0000000..04fafcd --- /dev/null +++ b/docs/testing/specs/formal/README.md @@ -0,0 +1,30 @@ +# Formal (TLA+) specs + +Optional machine-readable specs for finite-state model checking with TLC. **Manual only** — not run in CI. + +## Layout + +Each policy with TLA+ support lives in its own subdirectory: + +```text +formal/ +├── fifo/ +│ ├── Fifo.tla # MODULE name must match filename +│ ├── fifo.cfg # TLC constants and INVARIANT +│ └── tlc.md # Runbook and alignment log +└── lru/ + ├── Lru.tla + ├── lru.cfg + └── tlc.md +``` + +Human operational specs remain under [`policies/`](../policies/README.md). Contributor guide: [tla-guide.md](../tla-guide.md). + +## Run TLC + +```bash +./scripts/run-tlc.sh fifo # or: ./scripts/run-fifo-tlc.sh +./scripts/run-tlc.sh lru # or: ./scripts/run-lru-tlc.sh +``` + +Success: no `SemanticOK` violation on the bundled config. See per-policy `tlc.md` runbooks for alignment checklists. diff --git a/docs/testing/specs/formal/fifo/Fifo.tla b/docs/testing/specs/formal/fifo/Fifo.tla new file mode 100644 index 0000000..cdf545c --- /dev/null +++ b/docs/testing/specs/formal/fifo/Fifo.tla @@ -0,0 +1,143 @@ +---------------------------- MODULE Fifo ---------------------------- +(* + FIFO cache — formal structural spec. + + Human spec: docs/testing/specs/policies/exact/fifo.md + Reader doc: docs/testing/specs/tla-guide.md + Runbook: docs/testing/specs/formal/fifo/tlc.md + Rust oracle: tests/abstract_models/reference/fifo.rs (NaiveFifoModel) + + Structural Op mapping (harness Op in policy_semantics): + InsertNew(k) -> Op::Insert(k) when k is not resident + RemoveKey(k) -> Op::Remove(k) + EvictOldest -> Op::EvictOne + + Omitted (no state change on FIFO): Get, Peek, GetMut, Touch; + Insert of resident key (value update only). + + TLC-only (not fifo.md semantics): NoVictim sentinel, MaxQueueLen, + ExplorationOK, InsertNew queue guards, CHECK_DEADLOCK FALSE in fifo.cfg. +*) + +EXTENDS FiniteSets, Sequences, Integers + +(* Keys: finite key universe for TLC. Capacity: max residents. + NoVictim: sentinel when peek_victim is undefined (empty cache). + MaxQueueLen: TLC exploration bound on stale queue growth. *) +CONSTANTS Keys, Capacity, NoVictim, MaxQueueLen + +ASSUME NoVictim \notin Keys +ASSUME MaxQueueLen \in Nat + +(* cache: set of resident keys (fifo.md: store). + queue: append-only insertion log; may contain stale keys after Remove. *) +VARIABLES cache, queue + +vars == <> + +Init == + /\ cache = {} + /\ queue = <<>> + +(* Set of all keys appearing anywhere in queue (for invariants). *) +QueueContents == + {queue[i] : i \in 1..Len(queue)} + +(* peek_victim: front-to-back scan; skip stale; NoVictim if none live. *) +OldestLive == + LET scan[i \in Nat] == + IF i > Len(queue) + THEN NoVictim + ELSE IF queue[i] \in cache + THEN queue[i] + ELSE scan[i + 1] + IN scan[1] + +(* fifo.md eviction: pop front through victim (skip stale entries first). + Matches NaiveFifoModel::evict_oldest pop_front loop. *) +RECURSIVE PopThroughVictim(_, _) +PopThroughVictim(q, v) == + IF Len(q) = 0 + THEN q + ELSE IF q[1] = v + THEN SubSeq(q, 2, Len(q)) + ELSE PopThroughVictim(SubSeq(q, 2, Len(q)), v) + +(* fifo.md: |store| <= capacity *) +LenBound == + Cardinality(cache) <= Capacity + +(* Every queue slot holds a key from the finite universe. *) +QueueConsistency == + \A i \in 1..Len(queue): + queue[i] \in Keys + +(* fifo.md: store subseteq keys(insertion_order) *) +CacheKeysInQueue == + cache \subseteq QueueContents + +(* Observable: empty cache <-> no peek_victim (NaiveFifoModel::peek_victim_key). *) +PeekVictimOK == + (cache = {}) <=> (OldestLive = NoVictim) + +(* When victim is defined, it must be resident. *) +VictimInCache == + OldestLive # NoVictim => OldestLive \in cache + +(* Policy invariants — checked as INVARIANT SemanticOK in fifo.cfg. *) +SemanticOK == + /\ cache \subseteq Keys + /\ LenBound + /\ QueueConsistency + /\ CacheKeysInQueue + /\ PeekVictimOK + /\ VictimInCache + +(* TLC pruning only — NOT part of fifo.md. See fifo-tla-guide.md. *) +QueueLengthBound == + Len(queue) <= MaxQueueLen + +ExplorationOK == + QueueLengthBound + +TypeOK == + SemanticOK /\ ExplorationOK + +(* Op::EvictOne — remove oldest live key; compact queue through victim. *) +EvictOldest == + /\ cache # {} + /\ LET victim == OldestLive + IN /\ victim # NoVictim + /\ cache' = cache \ {victim} + /\ queue' = PopThroughVictim(queue, victim) + +(* Op::Insert for k not in cache. At capacity: evict then append. *) +InsertNew(k) == + /\ k \in Keys \ cache + /\ IF Cardinality(cache) >= Capacity + THEN LET victim == OldestLive + newQueue == Append(PopThroughVictim(queue, victim), k) + IN /\ victim # NoVictim + /\ Len(newQueue) <= MaxQueueLen + /\ cache' = (cache \ {victim}) \union {k} + /\ queue' = newQueue + ELSE /\ Len(queue) < MaxQueueLen + /\ cache' = cache \union {k} + /\ queue' = Append(queue, k) + +(* Op::Remove — drop from cache; leave stale entry in queue. *) +RemoveKey(k) == + /\ k \in cache + /\ cache' = cache \ {k} + /\ UNCHANGED queue + +(* Nondeterministic structural step (TLC explores all interleavings). *) +Next == + \/ \E k \in Keys : InsertNew(k) + \/ \E k \in Keys : RemoveKey(k) + \/ EvictOldest + +(* Init and every Next or stutter ([][Next]_vars). *) +Spec == Init /\ [][Next]_vars + +============================================================================= diff --git a/docs/testing/specs/formal/fifo/fifo.cfg b/docs/testing/specs/formal/fifo/fifo.cfg new file mode 100644 index 0000000..3f487b0 --- /dev/null +++ b/docs/testing/specs/formal/fifo/fifo.cfg @@ -0,0 +1,17 @@ +\* FIFO TLC config — see tla-guide.md and formal/fifo/tlc.md +SPECIFICATION Spec +CONSTANTS + \* Small finite instance for state-space exploration + Keys = {k1, k2} + Capacity = 2 + NoVictim = NoVictim + \* TLC pruning bound (stale queue growth after Remove); not fifo.md semantics + MaxQueueLen = 12 +\* Policy invariants only (excludes ExplorationOK queue cap from proof goal) +INVARIANT + SemanticOK +CONSTRAINT + QueueLengthBound +\* Exploration may stall when queue is full under MaxQueueLen +CHECK_DEADLOCK + FALSE diff --git a/docs/testing/specs/formal/fifo/tlc.md b/docs/testing/specs/formal/fifo/tlc.md new file mode 100644 index 0000000..c51232a --- /dev/null +++ b/docs/testing/specs/formal/fifo/tlc.md @@ -0,0 +1,76 @@ +# FIFO TLA+ runbook + +**Read first:** [tla-guide.md](../../tla-guide.md) (FIFO worked example; glossary, invariants). + +Manual optional check for [`Fifo.tla`](Fifo.tla) against [`fifo.md`](../../policies/exact/fifo.md) and `NaiveFifoModel`. + +## Prerequisites + +- [TLA+ Toolbox](https://github.com/tlaplus/tlaplus/releases) or `tlc` on `PATH` + +## Run TLC + +From repo root: + +```bash +./scripts/run-fifo-tlc.sh +# or: +./scripts/run-tlc.sh fifo +``` + +Or from this directory: + +```bash +tlc -config fifo.cfg Fifo.tla +``` + +**Success criteria:** TLC completes with no `SemanticOK` violation on the bundled config. `CHECK_DEADLOCK` is `FALSE` because `MaxQueueLen` is a TLC exploration bound (stale-queue growth can stall inserts). + +### macOS filename + +Module name is `Fifo` — TLC requires file `Fifo.tla`. On case-insensitive volumes Finder may show `fifo.tla`; do not duplicate or delete. + +## Re-run triggers + +Re-run TLC and update the alignment log when any of these change: + +- [`fifo.md`](../../policies/exact/fifo.md) +- [`Fifo.tla`](Fifo.tla) +- [`fifo.cfg`](fifo.cfg) +- `OldestLive`, `PopThroughVictim`, or `NaiveFifoModel` eviction logic + +## State-space vs trace testing + +| TLC | Rust `policy_semantics` | +|-----|-------------------------| +| Explores all `Next` transitions from reachable states | Runs fixed sequential `Vec>` traces | +| Finite `Keys = {k1, k2}`, `Capacity = 2` | Random keys `0..=255`, capacity `1..=16` | +| Proves `SemanticOK` on all reachable states (under `QueueLengthBound` constraint) | Proves step-wise observables via dual-run | + +TLC does **not** replace proptest. Trace-export cross-check is deferred. + +## Alignment checklist + +For each `Next` action, `NaiveFifoModel::apply` must agree on observables: + +| TLA+ action | `Op` | Resident set | `peek_victim` | Queue update | +|-------------|------|--------------|---------------|--------------| +| `InsertNew(k)` at capacity | `Insert(k)` | evict oldest live, then add `k` | oldest live in queue | `PopThroughVictim` then append `k` | +| `InsertNew(k)` below capacity | `Insert(k)` | add `k` | unchanged except new tail | append `k` | +| `RemoveKey(k)` | `Remove(k)` | remove `k`; queue retains stale entries | skip stale on scan | queue unchanged | +| `EvictOldest` | `EvictOne` | remove oldest live | next oldest live | `PopThroughVictim` | + +Semantic invariants (`PeekVictimOK`, `VictimInCache`) align with `peek_victim_key()` on every reachable state. + +**Known limitations:** + +- `Get` / `Peek` not modeled (structural no-ops on FIFO). +- Finite `Keys` in TLC vs `u8` in proptest. +- Resident re-`Insert` omitted (`InsertNew` requires `k \notin cache`). + +## Alignment log + +| Date | TLC result | Notes | +|------|------------|-------| +| 2026-06-06 | Pass | Initial pilot: `PopThroughVictim`, `CacheKeysInQueue`, `Keys={k1,k2}` | +| 2026-06-06 | Pass | Hardening: `SemanticOK`/`ExplorationOK`, `PeekVictimOK`, `run-fifo-tlc.sh` | diff --git a/docs/testing/specs/formal/lru/Lru.tla b/docs/testing/specs/formal/lru/Lru.tla new file mode 100644 index 0000000..e99309a --- /dev/null +++ b/docs/testing/specs/formal/lru/Lru.tla @@ -0,0 +1,110 @@ +---------------------------- MODULE Lru ---------------------------- +(* + LRU cache — formal structural spec (deque formulation). + + Human spec: docs/testing/specs/policies/exact/lru.md + Reader doc: docs/testing/specs/tla-guide.md + Runbook: docs/testing/specs/formal/lru/tlc.md + Rust oracle: tests/abstract_models/reference/lru.rs (NaiveLruModel) + + Structural Op mapping (harness Op in policy_semantics): + InsertNew(k) -> Op::Insert(k) when k is not resident + PromoteKey(k) -> Op::Insert(k) on resident; Op::Get/Touch on hit + RemoveKey(k) -> Op::Remove(k) + EvictLru -> Op::EvictOne + + Omitted (no state change on LRU): Peek; GetMut in LruCore adapter. +*) + +EXTENDS FiniteSets, Sequences, Integers + +CONSTANTS Keys, Capacity, NoVictim + +ASSUME NoVictim \notin Keys + +(* order: MRU-first deque (lru.md); front = MRU, back = LRU victim. *) +VARIABLES order + +vars == <> + +Init == + /\ order = <<>> + +(* Resident keys derived from deque (no stale entries). *) +Cache == + {order[i] : i \in 1..Len(order)} + +(* lru.md peek_victim: back of order, or none if empty. *) +LruKey == + IF Len(order) = 0 + THEN NoVictim + ELSE order[Len(order)] + +(* Remove all occurrences of key (deque has no duplicates in reachable states). *) +RemoveKeyFromOrder(q, k) == + SelectSeq(q, LAMBDA x: x # k) + +(* Promote k to MRU (front). *) +PromoteInOrder(q, k) == + <> \o RemoveKeyFromOrder(q, k) + +LenBound == + Len(order) <= Capacity + +OrderInKeys == + \A i \in 1..Len(order): + order[i] \in Keys + +NoDuplicates == + \A i, j \in 1..Len(order): + (i # j) => (order[i] # order[j]) + +PeekVictimOK == + (Len(order) = 0) <=> (LruKey = NoVictim) + +VictimInCache == + LruKey # NoVictim => LruKey \in Cache + +SemanticOK == + /\ LenBound + /\ OrderInKeys + /\ NoDuplicates + /\ PeekVictimOK + /\ VictimInCache + +TypeOK == + SemanticOK + +(* Op::EvictOne — remove LRU (back). *) +EvictLru == + /\ Len(order) > 0 + /\ order' = SubSeq(order, 1, Len(order) - 1) + +(* Op::Insert for k not in cache. At capacity: drop LRU then prepend k. *) +InsertNew(k) == + /\ k \in Keys \ Cache + /\ LET base == + IF Len(order) >= Capacity + THEN SubSeq(order, 1, Len(order) - 1) + ELSE order + IN order' = <> \o base + +(* Op::Insert (resident), Get, Touch — promote to MRU. *) +PromoteKey(k) == + /\ k \in Cache + /\ order' = PromoteInOrder(order, k) + +(* Op::Remove — drop key from deque. *) +RemoveKey(k) == + /\ k \in Cache + /\ order' = RemoveKeyFromOrder(order, k) + +Next == + \/ \E k \in Keys : InsertNew(k) + \/ \E k \in Keys : PromoteKey(k) + \/ \E k \in Keys : RemoveKey(k) + \/ EvictLru + +Spec == Init /\ [][Next]_vars + +============================================================================= diff --git a/docs/testing/specs/formal/lru/lru.cfg b/docs/testing/specs/formal/lru/lru.cfg new file mode 100644 index 0000000..e57412e --- /dev/null +++ b/docs/testing/specs/formal/lru/lru.cfg @@ -0,0 +1,11 @@ +\* LRU TLC config — see tla-guide.md and formal/lru/tlc.md +SPECIFICATION Spec +CONSTANTS + \* Small finite instance for state-space exploration + Keys = {k1, k2} + Capacity = 2 + NoVictim = NoVictim +INVARIANT + SemanticOK +CHECK_DEADLOCK + TRUE diff --git a/docs/testing/specs/formal/lru/tlc.md b/docs/testing/specs/formal/lru/tlc.md new file mode 100644 index 0000000..bee30c8 --- /dev/null +++ b/docs/testing/specs/formal/lru/tlc.md @@ -0,0 +1,77 @@ +# LRU TLA+ runbook + +**Read first:** [tla-guide.md](../../tla-guide.md) (LRU worked example; glossary, invariants). + +Manual optional check for [`Lru.tla`](Lru.tla) against [`lru.md`](../../policies/exact/lru.md) and `NaiveLruModel`. + +## Prerequisites + +- [TLA+ Toolbox](https://github.com/tlaplus/tlaplus/releases) or `tlc` on `PATH` + +## Run TLC + +From repo root: + +```bash +./scripts/run-lru-tlc.sh +# or: +./scripts/run-tlc.sh lru +``` + +Or from this directory: + +```bash +tlc -config lru.cfg Lru.tla +``` + +**Success criteria:** TLC completes with no `SemanticOK` violation on the bundled config. + +### macOS filename + +Module name is `Lru` — TLC requires file `Lru.tla`. On case-insensitive volumes Finder may show `lru.tla`; do not duplicate or delete. + +## Re-run triggers + +Re-run TLC and update the alignment log when any of these change: + +- [`lru.md`](../../policies/exact/lru.md) +- [`Lru.tla`](Lru.tla) +- [`lru.cfg`](lru.cfg) +- `NaiveLruModel` promotion / eviction logic + +## State-space vs trace testing + +| TLC | Rust `policy_semantics` | +|-----|-------------------------| +| Explores all `Next` transitions from reachable states | Runs fixed sequential `Vec>` traces | +| Finite `Keys = {k1, k2}`, `Capacity = 2` | Random keys `0..=255`, capacity `1..=16` | +| Proves `SemanticOK` on all reachable states | Proves step-wise observables via dual-run + cross-model | + +TLC does **not** replace proptest. Trace-export cross-check is deferred. + +## Alignment checklist + +For each `Next` action, `NaiveLruModel::apply` must agree on observables: + +| TLA+ action | `Op` | Resident set | `peek_victim` | Order / timestamps | +|-------------|------|--------------|---------------|-------------------| +| `InsertNew(k)` at capacity | `Insert(k)` | evict LRU, add `k` at MRU | new LRU | drop back, prepend `k` | +| `InsertNew(k)` below capacity | `Insert(k)` | add `k` | unchanged except new MRU | prepend `k` | +| `PromoteKey(k)` | `Insert(k)` resident / `Get` / `Touch` hit | unchanged | may change LRU | move `k` to front | +| `RemoveKey(k)` | `Remove(k)` | remove `k` | next LRU if `k` was LRU | filter `k` from deque | +| `EvictLru` | `EvictOne` | remove LRU | next LRU | drop back | + +Semantic invariants (`PeekVictimOK`, `VictimInCache`, `NoDuplicates`) align with `peek_victim_key()` on every reachable state. + +**Known limitations:** + +- `Peek` not modeled (no promotion). +- `GetMut` omitted in `LruCore` adapter tests (modeled as promote in exact model only). +- Finite `Keys` in TLC vs `u8` in proptest. +- Deque formulation in TLA+; `NaiveLruModel` uses timestamps (cross-model proves equivalence). + +## Alignment log + +| Date | TLC result | Notes | +|------|------------|-------| +| 2026-06-06 | Pass | Initial pilot: MRU-first deque, `Keys={k1,k2}`, `Capacity=2` | diff --git a/docs/testing/specs/matrix.md b/docs/testing/specs/matrix.md new file mode 100644 index 0000000..5d25206 --- /dev/null +++ b/docs/testing/specs/matrix.md @@ -0,0 +1,47 @@ +# Policy spec matrix + +**Canonical index** for the spec-first harness. Other docs ([static-analysis.md](../static-analysis.md), [abstract_models README](../../../tests/abstract_models/README.md)) link here rather than duplicating rows. + +| Policy | Spec maturity | Tier | Harness mode(s) | Spec doc | Exact model | Reference model | Bounded module | Op strategy | Traits asserted | TLA+ | +|--------|---------------|------|-----------------|----------|-------------|-----------------|----------------|-------------|-----------------|------| +| FIFO | reference, tla | exact | DualRun, CrossModel | [fifo.md](policies/exact/fifo.md) | `exact/fifo.rs` (`FifoModel`) | `reference/fifo.rs` (`NaiveFifoModel`) | — | `standard_op_list` | VictimInspectable, EvictingCache | [Fifo.tla](formal/fifo/Fifo.tla) | +| LRU | reference, tla | exact | DualRun, CrossModel | [lru.md](policies/exact/lru.md) | `exact/lru.rs` (`LruOccupancyModel`) | `reference/lru.rs` (`NaiveLruModel`) | — | `standard_op_list` | VictimInspectable, RecencyTracking, EvictingCache | [Lru.tla](formal/lru/Lru.tla) | +| Fast-LRU | reference | exact | DualRun, CrossModel | [fast-lru.md](policies/exact/fast-lru.md) | `exact/lru.rs` (`LruOccupancyModel`) | `reference/lru.rs` (`NaiveLruModel`) | — | `op_strategy_with_get_mut` | VictimInspectable, RecencyTracking, EvictingCache | — | +| LIFO | reference | exact | DualRun, CrossModel | [lifo.md](policies/exact/lifo.md) | `exact/lifo.rs` (`LifoModel`) | `reference/lifo.rs` (`NaiveLifoModel`) | — | `standard_op_list` | VictimInspectable, EvictingCache | — | +| MRU | reference | exact | DualRun, CrossModel | [mru.md](policies/exact/mru.md) | `exact/mru.rs` (`MruModel`) | `reference/mru.rs` (`NaiveMruModel`) | — | `standard_op_list` | EvictingCache | — | +| LFU | reference | exact | DualRun, CrossModel | [lfu.md](policies/exact/lfu.md) | `exact/lfu.rs` (`LfuModel`) | `reference/lfu.rs` (`NaiveLfuModel`) | — | `standard_op_list` | VictimInspectable, FrequencyTracking, EvictingCache | — | +| Heap-LFU | reference | exact | DualRun, CrossModel | [heap-lfu.md](policies/exact/heap-lfu.md) | `exact/heap_lfu.rs` (`HeapLfuModel`) | `reference/heap_lfu.rs` (`NaiveHeapLfuModel`) | — | `standard_op_list` | residency (`Ord` tie-break) | — | +| MFU | reference | exact | DualRun, CrossModel | [mfu.md](policies/exact/mfu.md) | `exact/mfu.rs` (`MfuModel`) | `reference/mfu.rs` (`NaiveMfuModel`) | — | `standard_op_list_mfu_safe` | residency (seq tie-break) | — | +| LRU-K | reference | exact | DualRun, CrossModel | [lru-k.md](policies/exact/lru-k.md) | `exact/lru_k.rs` (`LruKModel`) | `reference/lru_k.rs` (`NaiveLruKModel`) | — | `standard_op_list` | HistoryTracking, EvictingCache | — | +| Clock | stub | mirror | DualRun | [clock.md](policies/mirror/clock.md) | `exact/clock.rs` (`ClockModel`) | — | — | `standard_op_list` | EvictingCache | — | +| 2Q | stub | mirror | DualRun | [two-q.md](policies/mirror/two-q.md) | `exact/two_q.rs` (`TwoQModel`) | — | — | `standard_op_list_no_evict` | residency | — | +| SLRU | stub | mirror | DualRun | [slru.md](policies/mirror/slru.md) | `exact/slru.rs` (`SlruModel`) | — | — | `standard_op_list_no_evict` | residency | — | +| NRU | stub | mirror | DualRun | [nru.md](policies/mirror/nru.md) | `exact/nru.rs` (`NruModel`) | — | — | `short_op_list_no_evict` | residency | — | +| ARC | stub | bounded | InvariantOnly | [arc.md](policies/bounded/arc.md) | — | — | `bounded/arc.rs` | `standard_op_list` | `debug_validate_invariants` | — | +| CAR | stub | bounded | InvariantOnly | [car.md](policies/bounded/car.md) | — | — | `bounded/car.rs` | `standard_op_list` | `debug_validate_invariants` | — | +| Clock-PRO | stub | bounded | InvariantOnly | [clock-pro.md](policies/bounded/clock-pro.md) | — | — | `bounded/clock_pro.rs` | `standard_op_list` | `debug_validate_invariants` | — | +| S3-FIFO | stub | bounded | InvariantOnly | [s3-fifo.md](policies/bounded/s3-fifo.md) | — | — | `bounded/s3_fifo.rs` | `op_strategy_with_get_mut` | `check_invariants`, residency | — | +| TTL | stub | composed | DualRun | [ttl.md](policies/composed/ttl.md) | `exact/lru.rs` (`LruOccupancyModel`) | — | — | TTL integration traces | `LruOccupancyModel` + deadlines | — | +| Random | — | — | — | — | — | — | — | — | — | — | + +**Status:** Random policy is deferred (no semantic harness). + +## Harness modes + +| Mode | Oracle | +|------|--------| +| **DualRun** | `exact/` `PolicyModel` vs implementation | +| **CrossModel** | `reference/` vs `exact/` (all exact-tier policies with reference models) | +| **InvariantOnly** | `len <= capacity` + `debug_validate_invariants` / `check_invariants` | + +## Spec maturity + +See [_includes/spec-maturity.md](_includes/spec-maturity.md). + +## Related + +- [policies/README.md](policies/README.md) — tier layout and onboarding +- [formal/README.md](formal/README.md) — TLA+ directory layout +- [template.md](template.md) — spec skeleton for new policies +- [tla-guide.md](tla-guide.md) — adding TLA+ specs +- [README.md](README.md) — pipeline and checklist diff --git a/docs/testing/specs/policies/README.md b/docs/testing/specs/policies/README.md new file mode 100644 index 0000000..3b11fc0 --- /dev/null +++ b/docs/testing/specs/policies/README.md @@ -0,0 +1,24 @@ +# Policy operational specs + +Human-readable specifications organized by harness tier. Each file is the **source of truth** for its policy's semantics. + +## Layout + +| Directory | Tier | Harness mode | Examples | +|-----------|------|--------------|----------| +| [exact/](exact/) | Exact | DualRun, CrossModel | FIFO, LRU, LFU | +| [mirror/](mirror/) | Mirror | DualRun | Clock, 2Q, SLRU | +| [bounded/](bounded/) | Bounded | InvariantOnly | ARC, S3-FIFO | +| [composed/](composed/) | Composed | DualRun + layer | TTL | + +**Canonical index:** [matrix.md](../matrix.md) (maturity, models, op strategy, traits). + +## Add a new policy + +1. Copy [template.md](../template.md) into the tier directory (`policies//.md`). +2. Implement `exact/` and optionally `reference/` models under `tests/abstract_models/`. +3. Wire `policy_semantics` tests and feature gates. +4. Append a row to [matrix.md](../matrix.md). +5. Optional TLA+: add `formal//` per [tla-guide.md](../tla-guide.md). + +Shared fragments: [_includes/](../_includes/) (harness `Op` table, maturity definitions). diff --git a/docs/testing/specs/policies/bounded/arc.md b/docs/testing/specs/policies/bounded/arc.md new file mode 100644 index 0000000..6a2614e --- /dev/null +++ b/docs/testing/specs/policies/bounded/arc.md @@ -0,0 +1,45 @@ +# ARC operational spec + +> **Spec maturity:** stub +> +> **Executable oracle:** invariant checks on [`ArcCore`](../../../../src/policy/arc.rs); no full `PolicyModel` yet. + +Adaptive Replacement Cache: dynamically balances recency (T1) and frequency (T2) lists. Victim selection is **adaptive** — not uniquely determined from residency alone. + +## State (implementation-shaped) + +ARC maintains T1, T2, B1, B2 ghost lists and adaptation parameter `p`. Exact victim depends on list lengths and `p`. + +## Harness contract (InvariantOnly) + +| Check | When | +|-------|------| +| `len <= capacity` | After every `Op` | +| `debug_validate_invariants()` | After every `Op` | + +## Per-`Op` adapter behavior + +| `Op` | Effect | +|------|--------| +| `Insert(k)` | `insert(k, v)` | +| `Get(k)` | `get(k)` | +| `Peek(k)` | `peek(k)` | +| `Remove(k)` | `remove(k)` | +| `GetMut` / `Touch` / `EvictOne` | No-op in adapter | + +## Observables + +- **Residency** may be probed in smoke tests. +- **Victim:** legal set (future: `OracleExpectation::Legal`); not asserted in v1. + +## Future work + +- Independent reference model for adaptive victim intervals. +- Full `PolicyModel` dual-run when legal-victim oracle is defined. + +## References + +- Megiddo & Modha, *ARC: A Self-Tuning, Low Overhead Replacement Cache* +- Tests: `policy_semantics/arc_tests.rs` +- Bounded module: `tests/abstract_models/bounded/arc.rs` +- Policy matrix: [matrix.md](../../matrix.md) diff --git a/docs/testing/specs/policies/bounded/car.md b/docs/testing/specs/policies/bounded/car.md new file mode 100644 index 0000000..db769d2 --- /dev/null +++ b/docs/testing/specs/policies/bounded/car.md @@ -0,0 +1,36 @@ +# CAR operational spec + +> **Spec maturity:** stub +> +> **Executable oracle:** invariant checks on [`CarCore`](../../../../src/policy/car.rs); no full `PolicyModel` yet. + +Clock with Adaptive Replacement (CAR): clock-based scan with adaptive hand and ghost entries. Victim is **not** uniquely determined from residency alone. + +## Harness contract (InvariantOnly) + +| Check | When | +|-------|------| +| `len <= capacity` | After every `Op` | +| `debug_validate_invariants()` | After every `Op` on `CarCore` | + +## Per-`Op` adapter behavior + +| `Op` | Effect | +|------|--------| +| `Insert(k)` | `insert(k, v)` | +| `Get(k)` | `get(k)` | +| `Peek(k)` | `peek(k)` | +| `Remove(k)` | `remove(k)` | +| `GetMut` / `Touch` / `EvictOne` | No-op in adapter | + +## Observables + +- Residency probed in smoke tests. +- Victim legal set deferred (`OracleExpectation::Legal`). + +## References + +- CacheKit: [`CarCore`](../../../../src/policy/car.rs) +- Tests: `policy_semantics/car_tests.rs` +- Bounded module: `tests/abstract_models/bounded/car.rs` +- Policy matrix: [matrix.md](../../matrix.md) diff --git a/docs/testing/specs/policies/bounded/clock-pro.md b/docs/testing/specs/policies/bounded/clock-pro.md new file mode 100644 index 0000000..9a13b2e --- /dev/null +++ b/docs/testing/specs/policies/bounded/clock-pro.md @@ -0,0 +1,36 @@ +# Clock-PRO operational spec + +> **Spec maturity:** stub +> +> **Executable oracle:** invariant checks on [`ClockProCache`](../../../../src/policy/clock_pro.rs); no full `PolicyModel` yet. + +Clock-PRO: hot/cold/non-resident lists with clock-style second chances. Hot/cold/non-resident structure makes exact victim prediction impractical. + +## Harness contract (InvariantOnly) + +| Check | When | +|-------|------| +| `len <= capacity` | After every `Op` | +| `debug_validate_invariants()` | After every `Op` | + +## Per-`Op` adapter behavior + +| `Op` | Effect | +|------|--------| +| `Insert(k)` | `insert(k, v)` | +| `Get(k)` | `get(k)` | +| `Peek(k)` | `peek(k)` | +| `Remove(k)` | `remove(k)` | +| `GetMut` / `Touch` / `EvictOne` | No-op in adapter | + +## Observables + +- Structural invariants only in v1. +- Victim legal set deferred. + +## References + +- CacheKit: [`ClockProCache`](../../../../src/policy/clock_pro.rs) +- Tests: `policy_semantics/clock_pro_tests.rs` +- Bounded module: `tests/abstract_models/bounded/clock_pro.rs` +- Policy matrix: [matrix.md](../../matrix.md) diff --git a/docs/testing/specs/policies/bounded/s3-fifo.md b/docs/testing/specs/policies/bounded/s3-fifo.md new file mode 100644 index 0000000..5ca1fd4 --- /dev/null +++ b/docs/testing/specs/policies/bounded/s3-fifo.md @@ -0,0 +1,37 @@ +# S3-FIFO operational spec + +> **Spec maturity:** stub +> +> **Executable oracle:** invariant checks on [`S3FifoCache`](../../../../src/policy/s3_fifo.rs); no full `PolicyModel` yet. + +S3-FIFO: three FIFO queues (small, main, ghost) for scan resistance. Victim selection depends on queue roles — not uniquely determined here. + +## Harness contract (InvariantOnly) + +| Check | When | +|-------|------| +| `len <= capacity` | After every `Op` | +| `check_invariants()` | After every `Op` (debug builds only in adapter) | + +## Per-`Op` adapter behavior + +| `Op` | Effect | +|------|--------| +| `Insert(k)` | `insert(k, v)` | +| `Get(k)` | `get(k)` | +| `Peek(k)` | `peek(k)` | +| `GetMut(k)` | `get_mut(k)` | +| `Remove(k)` | `remove(k)` | +| `Touch` / `EvictOne` | No-op in adapter | + +## Observables + +- Residency bound in smoke tests. +- Op strategy: `op_strategy_with_get_mut`. + +## References + +- Yang et al., *S3-FIFO: A Simple and Scalable FIFO-based Cache Admission and Eviction Policy* +- Tests: `policy_semantics/s3_fifo_tests.rs` +- Bounded module: `tests/abstract_models/bounded/s3_fifo.rs` +- Policy matrix: [matrix.md](../../matrix.md) diff --git a/docs/testing/specs/policies/composed/ttl.md b/docs/testing/specs/policies/composed/ttl.md new file mode 100644 index 0000000..3c3136f --- /dev/null +++ b/docs/testing/specs/policies/composed/ttl.md @@ -0,0 +1,42 @@ +# TTL operational spec + +> **Spec maturity:** stub +> +> **Executable oracle:** `tests/abstract_models/exact/lru.rs` (`LruOccupancyModel`) for LRU layer; TTL deadlines tested in `ttl_integration_test.rs`. + +TTL (composed tier): LRU eviction semantics plus **time-to-live** expiration on entries. Not a standalone eviction policy — a decorator over an inner cache. + +## Composition + +```text +Expiring + MockClock + → LRU residency from LruOccupancyModel (when inner is LRU-family) + → deadline / TtlStatus checks from integration tests +``` + +## State (conceptual) + +| Layer | State | +|-------|-------| +| Inner (e.g. Fast-LRU) | Standard LRU state — see [lru.md](lru.md) | +| TTL | Per-key expiry instant; default TTL on insert | + +## Harness contract (composed) + +| Check | Where | +|-------|-------| +| LRU residency / rank | `LruOccupancyModel` (when applicable) | +| `TtlStatus::{Live, Expired, Absent}` | `ttl_integration_test.rs` | +| `insert_with_ttl`, `expire`, clock advance | `MockClock` deterministic traces | + +## Per-`Op` notes + +- Standard `Op` alphabet applies to the inner cache through the expiring wrapper. +- TTL-specific ops (`insert_with_ttl`, time advance) are hand-written in integration tests. + +## References + +- CacheKit: [`Expiring`](../../../../src/policy/expiring.rs), [`CacheBuilder`](../../../../src/builder.rs) +- Tests: [`ttl_integration_test.rs`](../../../../../tests/ttl_integration_test.rs) +- Base LRU spec: [lru.md](lru.md) +- Policy matrix: [matrix.md](../../matrix.md) diff --git a/docs/testing/specs/policies/exact/fast-lru.md b/docs/testing/specs/policies/exact/fast-lru.md new file mode 100644 index 0000000..fa51649 --- /dev/null +++ b/docs/testing/specs/policies/exact/fast-lru.md @@ -0,0 +1,34 @@ +# Fast-LRU operational spec + +> **Spec maturity:** reference +> +> **Executable oracle:** `tests/abstract_models/exact/lru.rs` (`LruOccupancyModel`); shared reference: `reference/lru.rs` (`NaiveLruModel`) — same LRU semantics as [lru.md](lru.md). + +Fast-LRU is LRU with the same eviction semantics as [lru.md](lru.md). This document records Fast-LRU-specific harness behavior; the deque oracle is shared with LRU. + +## State + +Same as LRU: MRU-first `order: Seq` (or timestamp formulation in `NaiveLruModel`). + +## Observables + +Same as LRU: `resident`, `peek_victim` (LRU = back), `recency_rank`, `hit`. + +## Operations + +Same per-`Op` transitions as [lru.md](lru.md). + +## Harness differences + +| Aspect | Fast-LRU | LRU (`LruCore`) | +|--------|----------|-----------------| +| `GetMut(k)` | Applied via `get_mut` (promotes on hit) | No-op in adapter | +| Op strategy | `op_strategy_with_get_mut` | `standard_op_list` | +| Impl | [`FastLru`](../../../../src/policy/fast_lru.rs) | [`LruCore`](../../../../src/policy/lru.rs) | + +Dual-impl equivalence: `dual_impl_tests.rs` asserts `LruCore` vs `FastLru` agree on `contains`, `peek_victim`, `recency_rank`. + +## References + +- Base spec: [lru.md](lru.md) +- Policy matrix: [matrix.md](../../matrix.md) diff --git a/docs/testing/specs/policies/exact/fifo.md b/docs/testing/specs/policies/exact/fifo.md new file mode 100644 index 0000000..207716a --- /dev/null +++ b/docs/testing/specs/policies/exact/fifo.md @@ -0,0 +1,87 @@ +# FIFO operational spec + +> **Spec maturity:** reference, tla +> +> **Executable oracle:** `tests/abstract_models/exact/fifo.rs` (`FifoModel`); independent reference: `reference/fifo.rs` (`NaiveFifoModel`). + +First-In-First-Out cache replacement: evict the **oldest live insertion** when space is needed. This spec is independent of `FifoCache` internals; implementations must refine it. + +## State + +| Variable | Type | Meaning | +|----------|------|---------| +| `store` | `Set` | Keys currently resident | +| `insertion_order` | `Seq` | Append-only log of first-insert order (may contain stale keys) | +| `capacity` | `usize` | Maximum resident count | + +**Invariant:** `store ⊆ keys(insertion_order)` (every resident key appears in the log at least once). + +## Init + +- `store = ∅` +- `insertion_order = ⟨⟩` +- `capacity = C` (given) + +## Observables + +| Observable | Definition | +|------------|------------| +| `resident` | `store` | +| `peek_victim` | Front-to-back scan of `insertion_order`; first key still in `store`, or none if empty | +| `hit` | `Get` / `Peek` / `GetMut`: `MustHit` if key ∈ `store`, else `MustMiss` | +| `evicted_on_insert` | Key removed by eviction triggered by this `Insert`, if any | + +## Operations + +### `Insert(k)` + +1. If `k ∈ store`: **no structural change** (value update only; queue unchanged). +2. If `capacity = 0`: no-op. +3. If `|store| ≥ capacity`: evict `peek_victim` (pop stale entries from front until a live key is removed from `store`). +4. Add `k` to `store` and append `k` to `insertion_order`. + +### `Get(k)` / `Peek(k)` / `GetMut(k)` + +- Set `hit` from membership in `store`. +- **No** change to `store` or `insertion_order`. + +### `Touch(k)` + +- Harness adapter: no-op on cache. +- Model sets `hit = MayHitOrMiss`. + +### `Remove(k)` + +- Remove `k` from `store` if present. +- **Do not** remove `k` from `insertion_order` (stale entries skipped on eviction). + +### `EvictOne` + +- If `peek_victim` is `v`: remove `v` from `store` and record `victim = Exact(v)`. +- Pop stale keys from front of `insertion_order` until the evicted key is consumed. + +## Tie-breaks + +- Victim: deterministic **front-to-back** scan of `insertion_order`. +- First live key wins; no randomness. + +## Harness `Op` mapping + +| `Op` | Cache API | Side effects | +|------|-----------|--------------| +| `Insert(k)` | `insert(k, v)` | May evict | +| `Get(k)` | `get(k)` | None (FIFO) | +| `Peek(k)` | `peek(k)` | None | +| `GetMut(k)` | — | No-op in adapter | +| `Touch(k)` | — | No-op in adapter | +| `Remove(k)` | `remove(k)` | None on queue | +| `EvictOne` | `evict_one()` | Evict oldest live | + +## Formal spec (TLA+) + +Machine-readable structural spec: [`Fifo.tla`](../../formal/fifo/Fifo.tla). Reader guide: [tla-guide.md](../../tla-guide.md) (FIFO example). Run TLC: [`scripts/run-fifo-tlc.sh`](../../../../../scripts/run-fifo-tlc.sh) (checks `SemanticOK` invariants; manual, not CI). Runbook: [formal/fifo/tlc.md](../../formal/fifo/tlc.md). + +## References + +- Johnson, T. & Shasha, D. *2Q: A Low Overhead High Performance Buffer Management Replacement Algorithm.* (FIFO as baseline insertion-order policy.) +- CacheKit: [`FifoCache`](../../../../src/policy/fifo.rs) must refine this spec. diff --git a/docs/testing/specs/policies/exact/heap-lfu.md b/docs/testing/specs/policies/exact/heap-lfu.md new file mode 100644 index 0000000..4469f2f --- /dev/null +++ b/docs/testing/specs/policies/exact/heap-lfu.md @@ -0,0 +1,61 @@ +# Heap-LFU operational spec + +> **Spec maturity:** reference +> +> **Executable oracle:** `tests/abstract_models/exact/heap_lfu.rs` (`HeapLfuModel`); independent reference: `reference/heap_lfu.rs` (`NaiveHeapLfuModel`). + +Heap-backed LFU: evict the key with **minimum frequency**; tie-break by **key order** (`Ord`). + +## State + +| Variable | Type | Meaning | +|----------|------|---------| +| `freq` | `Map` | Live frequency per resident key | +| `heap` | min-heap of `(freq, k)` | May contain stale entries; rebuilt when oversized | +| `capacity` | `usize` | Maximum resident count | + +## Init + +- `freq = ∅`, `heap = ∅`, `capacity = C` + +## Observables + +| Observable | Definition | +|------------|------------| +| `resident` | Keys in `freq` | +| `peek_victim` | Min frequency; smallest `K` by `Ord` at ties | +| `hit` | `MustHit` / `MustMiss` | + +## Operations + +### `Insert(k)` + +1. If `k ∈ resident`: no-op for frequency (value update only in implementation). +2. Else if full: pop valid min from heap (skip stale), evict, record `evicted_on_insert`. +3. Set `freq[k] = 1`, push to heap. + +### `Get(k)` / `Peek(k)` + +- Set `hit`. `Get` increments frequency on hit. + +### `GetMut(k)` / `Touch(k)` + +- `Touch`: increment on hit. `GetMut`: no-op in adapter. + +### `Remove(k)` / `EvictOne` + +- Remove from `freq`; heap lazily cleaned on eviction/rebuild. + +## Tie-breaks + +- Equal frequency: evict **smallest `K` by `Ord`**. + +## Harness notes + +- Tests assert **residency only** (heap staleness makes frequency oracle fragile). +- Op strategy: `standard_op_list` (not `mfu_safe`; rebuild handles staleness). + +## References + +- CacheKit: [`HeapLfuCache`](../../../../src/policy/heap_lfu.rs) +- Policy matrix: [matrix.md](../../matrix.md) diff --git a/docs/testing/specs/policies/exact/lfu.md b/docs/testing/specs/policies/exact/lfu.md new file mode 100644 index 0000000..7f5b236 --- /dev/null +++ b/docs/testing/specs/policies/exact/lfu.md @@ -0,0 +1,81 @@ +# LFU operational spec + +> **Spec maturity:** reference +> +> **Executable oracle:** `tests/abstract_models/exact/lfu.rs` (`LfuModel`); independent reference: `reference/lfu.rs` (`NaiveLfuModel`). + +Least Frequently Used cache replacement: evict the key with **minimum access frequency** when space is needed. + +## State + +| Variable | Type | Meaning | +|----------|------|---------| +| `freq` | `Map` | Access count per resident key | +| `buckets` | frequency-ordered structure | Min-frequency bucket with FIFO tie-break | +| `capacity` | `usize` | Maximum resident count | + +## Init + +- `freq = ∅`, `capacity = C` +- New inserts start at frequency 1. + +## Observables + +| Observable | Definition | +|------------|------------| +| `resident` | Keys in `freq` | +| `peek_victim` | Minimum frequency; FIFO order within min bucket | +| `frequency(k)` | `freq[k]` if resident | +| `hit` | `MustHit` / `MustMiss` from membership | + +## Operations + +### `Insert(k)` + +1. If `k ∈ resident`: increment frequency (via `increment_frequency` on impl). +2. Else if full: evict min-frequency victim (FIFO tie within bucket), record `evicted_on_insert`. +3. Insert `k` at frequency 1. + +### `Get(k)` / `Peek(k)` + +- Set `hit`. `Get` increments frequency on hit. + +### `GetMut(k)` + +- No-op in harness adapter. + +### `Touch(k)` + +- `increment_frequency(k)` on hit (same frequency effect as `Get`). + +### `Remove(k)` + +- Remove `k` from frequency structure. + +### `EvictOne` + +- Evict min-frequency victim (FIFO tie-break). + +## Tie-breaks + +- **Victim:** lowest frequency; within equal frequency, **FIFO** (oldest in min bucket). +- Hand-written test `hand_written_lfu_fifo_tie_break` locks this behavior. + +## Harness `Op` mapping + +| `Op` | Cache API | Side effects | +|------|-----------|--------------| +| `Insert(k)` | `insert(k, v)` | Freq 1 or increment | +| `Get(k)` | `get(k)` | Increment on hit | +| `Peek(k)` | `peek(k)` | None | +| `GetMut(k)` | — | No-op | +| `Touch(k)` | `increment_frequency(k)` | Increment on hit | +| `Remove(k)` | `remove(k)` | Remove | +| `EvictOne` | `evict_one()` | Evict min freq | + +**Dual-run extra check:** after each step, `cache.frequency(k) == model.frequency(k)` for all resident `k`. + +## References + +- CacheKit: [`LfuCache`](../../../../src/policy/lfu.rs) +- Policy matrix: [matrix.md](../../matrix.md) diff --git a/docs/testing/specs/policies/exact/lifo.md b/docs/testing/specs/policies/exact/lifo.md new file mode 100644 index 0000000..25e06eb --- /dev/null +++ b/docs/testing/specs/policies/exact/lifo.md @@ -0,0 +1,73 @@ +# LIFO operational spec + +> **Spec maturity:** reference +> +> **Executable oracle:** `tests/abstract_models/exact/lifo.rs` (`LifoModel`); independent reference: `reference/lifo.rs` (`NaiveLifoModel`). + +Last-In-First-Out cache replacement: evict the **most recently inserted** key (top of stack) when space is needed. + +## State + +| Variable | Type | Meaning | +|----------|------|---------| +| `stack` | `Seq` | Back = newest (MRU of stack); all keys resident | +| `capacity` | `usize` | Maximum resident count | + +## Init + +- `stack = ⟨⟩` +- `capacity = C` + +## Observables + +| Observable | Definition | +|------------|------------| +| `resident` | Keys in `stack` | +| `peek_victim` | Back of `stack` (newest), or none if empty | +| `hit` | `MustHit` / `MustMiss` from membership | + +## Operations + +### `Insert(k)` + +1. If `k ∈ resident`: no structural change (value update only). +2. If `capacity = 0`: no-op. +3. If `|resident| ≥ capacity`: evict back of `stack` (newest), record `evicted_on_insert`. +4. Push `k` onto back of `stack`. + +### `Get(k)` / `Peek(k)` / `GetMut(k)` + +- Set `hit` from membership. **No** promotion or stack reorder. + +### `Touch(k)` + +- Harness adapter: no-op. Model sets `hit = MayHitOrMiss`. + +### `Remove(k)` + +- Remove `k` from `stack` if present. + +### `EvictOne` + +- If stack nonempty: `victim = Exact(back)`, pop back. + +## Tie-breaks + +- Victim: always newest (stack back). Deterministic. + +## Harness `Op` mapping + +| `Op` | Cache API | Side effects | +|------|-----------|--------------| +| `Insert(k)` | `insert(k, v)` | May evict newest | +| `Get(k)` | `get(k)` | None | +| `Peek(k)` | `peek(k)` | None | +| `GetMut(k)` | — | No-op in adapter | +| `Touch(k)` | — | No-op in adapter | +| `Remove(k)` | `remove(k)` | Remove from stack | +| `EvictOne` | `evict_one()` | Evict newest | + +## References + +- CacheKit: [`LifoCore`](../../../../src/policy/lifo.rs) +- Policy matrix: [matrix.md](../../matrix.md) diff --git a/docs/testing/specs/policies/exact/lru-k.md b/docs/testing/specs/policies/exact/lru-k.md new file mode 100644 index 0000000..4504e63 --- /dev/null +++ b/docs/testing/specs/policies/exact/lru-k.md @@ -0,0 +1,63 @@ +# LRU-K operational spec + +> **Spec maturity:** reference +> +> **Executable oracle:** `tests/abstract_models/exact/lru_k.rs` (`LruKModel`); independent reference: `reference/lru_k.rs` (`NaiveLruKModel`). + +LRU-K: track last **K** access times per key; evict from **cold** segment using LRU; promote to **hot** after K-th access. + +## State + +| Variable | Type | Meaning | +|----------|------|---------| +| `cold` | `Seq` | LRU-ordered cold segment (back = victim) | +| `hot` | `Seq` | LRU-ordered hot segment | +| `segment` | `Map` | Per-key segment | +| `history` | `Map>` | Last K access timestamps (step counter) | +| `tick` | `ℕ` | Monotonic step counter | +| `k` | `usize` | History depth (parameter) | +| `capacity` | `usize` | Maximum resident count | + +## Init + +- Segments empty, `tick = 0`, `capacity = C`, `k` given. + +## Observables + +| Observable | Definition | +|------------|------------| +| `resident` | Keys in `segment` | +| `peek_victim` | Back of `cold` (LRU among cold keys) | +| `history(k)` | Last K access times for `k` | +| `hit` | `MustHit` / `MustMiss` | + +## Operations + +### `Insert(k)` / `Get(k)` / `Peek(k)` / `Touch(k)` + +- Record access in `history`; increment `tick` on promoting ops. +- On K-th distinct access: promote `k` from cold to hot (MRU in hot). +- On insert when full: evict LRU from cold. + +### `Remove(k)` / `EvictOne` + +- Remove from appropriate segment and history. + +## Tie-breaks + +- Cold victim: LRU (back of `cold` deque). +- Hot segment: LRU ordering within hot (not eviction victim until demoted). + +## Harness `Op` mapping + +| `Op` | Traits asserted | +|------|-----------------| +| All | `HistoryTracking`, `EvictingCache` | + +`GetMut`: no-op in adapter. + +## References + +- O'Neil, O'Neil & Weikum, *The LRU-K Page Replacement Algorithm* +- CacheKit: [`LruKCache`](../../../../src/policy/lru_k.rs) +- Policy matrix: [matrix.md](../../matrix.md) diff --git a/docs/testing/specs/policies/exact/lru.md b/docs/testing/specs/policies/exact/lru.md new file mode 100644 index 0000000..70f7483 --- /dev/null +++ b/docs/testing/specs/policies/exact/lru.md @@ -0,0 +1,88 @@ +# LRU operational spec + +> **Spec maturity:** reference, tla +> +> **Executable oracle:** `tests/abstract_models/exact/lru.rs` (`LruOccupancyModel`); independent reference: `reference/lru.rs` (`NaiveLruModel`). Optional TLA+: [`Lru.tla`](../../formal/lru/Lru.tla) — run [`scripts/run-lru-tlc.sh`](../../../../../scripts/run-lru-tlc.sh); see [formal/lru/tlc.md](../../formal/lru/tlc.md). + +Least Recently Used cache replacement: evict the key whose **most recent access is oldest** when space is needed. This spec is independent of `LruCore` / `FastLru` internals; implementations must refine it. + +## State + +Two equivalent formulations: + +1. **Deque (MRU-first):** `order: Seq` listing resident keys; front = MRU, back = LRU. +2. **Timestamps:** `access: Map` last-access time per resident key; monotonic `clock` incremented once per op that records access. + +This document uses deque notation; the reference model uses timestamps. + +## Init + +- `order = ⟨⟩` (or `access = ∅`, `clock = 0`) +- `capacity = C` + +## Observables + +| Observable | Definition | +|------------|------------| +| `resident` | Keys in `order` | +| `peek_victim` | Back of `order` (LRU), or none if empty | +| `recency_rank(k)` | Index of `k` in `order` (0 = MRU); undefined if absent | +| `hit` | Per op: `MustHit` / `MustMiss` from membership | + +**Timestamp recency rank:** sort resident keys by `(access[k] desc, k asc)`; rank = index of `k`. + +## Operations + +### `Insert(k)` + +1. If `k ∈ resident`: **promote to MRU** (move to front / set `access[k] = ++clock`). +2. Else if `|resident| ≥ capacity`: evict LRU (pop back / min timestamp), record `evicted_on_insert`. +3. Insert `k` at MRU (push front / assign new timestamp). + +### `Get(k)` / `GetMut(k)` + +- If `k ∈ resident`: `MustHit`, promote to MRU. +- Else: `MustMiss`, no change. + +### `Peek(k)` + +- If `k ∈ resident`: `MustHit`. +- Else: `MustMiss`. +- **No promotion.** + +### `Touch(k)` + +- Same as `Get` for promotion: promote on hit, `MustMiss` if absent. + +### `Remove(k)` + +- Remove `k` from `order` / `access` if present. No promotion. + +### `EvictOne` + +- If LRU exists: remove back of `order`, `victim = Exact(lru)`. + +## Tie-breaks + +- **Victim:** LRU = back of deque = minimum `access[k]`. +- **Equal timestamps:** evict smallest `K` by `Ord` (monotonic clock per op normally keeps timestamps unique). +- **Recency rank ties:** break by `k asc` when sorting `(timestamp desc, key asc)`. + +## Harness `Op` mapping + +| `Op` | Cache API | Side effects | +|------|-----------|--------------| +| `Insert(k)` | `insert(k, v)` | Promote if resident; else insert/evict | +| `Get(k)` | `get(k)` | Promote on hit | +| `Peek(k)` | `peek(k)` | No promotion | +| `GetMut(k)` | — | No-op in adapter (LRU tests) | +| `Touch(k)` | `touch(k)` | Promote on hit | +| `Remove(k)` | `remove(k)` | Remove | +| `EvictOne` | `evict_one()` | Evict LRU | + +Align with [trait hierarchy](../../../design/trait-hierarchy.md): `Peek` must not change `recency_rank`. + +## References + +- Standard LRU semantics (Douglas & Thies, *LRU-K* and related literature). +- CacheKit: [`LruCore`](../../../../src/policy/lru.rs), [`FastLru`](../../../../src/policy/fast_lru.rs) must refine this spec. diff --git a/docs/testing/specs/policies/exact/mfu.md b/docs/testing/specs/policies/exact/mfu.md new file mode 100644 index 0000000..938140b --- /dev/null +++ b/docs/testing/specs/policies/exact/mfu.md @@ -0,0 +1,57 @@ +# MFU operational spec + +> **Spec maturity:** reference +> +> **Executable oracle:** `tests/abstract_models/exact/mfu.rs` (`MfuModel`); independent reference: `reference/mfu.rs` (`NaiveMfuModel`). + +Most Frequently Used cache replacement: evict the key with **maximum frequency** when space is needed. + +## State + +| Variable | Type | Meaning | +|----------|------|---------| +| `freq` | `Map` | Live frequency per resident key | +| `heap` | max-heap with sequence numbers | Stale entries possible | +| `capacity` | `usize` | Maximum resident count | + +## Init + +- `freq = ∅`, `capacity = C` + +## Observables + +| Observable | Definition | +|------------|------------| +| `resident` | Keys in `freq` | +| `peek_victim` | Max frequency; highest sequence number at ties (newest heap entry) | +| `hit` | `MustHit` / `MustMiss` | + +## Operations + +### `Insert(k)` + +1. If `k ∈ resident`: increment frequency. +2. Else if full: evict max-frequency victim (newest heap entry at ties), record `evicted_on_insert`. +3. Insert at frequency 1. + +### `Get(k)` / `Peek(k)` + +- Set `hit`. `Get` increments on hit. + +### `Remove(k)` / `EvictOne` + +- **Skipped in proptest** — stale heap entries break `debug_validate_invariants` when keys are removed outside insert/evict path. + +## Tie-breaks + +- Equal max frequency: **newest heap entry** (highest sequence number) is evicted first; older entries survive. + +## Harness notes + +- Op strategy: `standard_op_list_mfu_safe` (no `Remove` / `EvictOne` in traces). +- Tests assert residency only. + +## References + +- CacheKit: [`MfuCore`](../../../../src/policy/mfu.rs) +- Policy matrix: [matrix.md](../../matrix.md) diff --git a/docs/testing/specs/policies/exact/mru.md b/docs/testing/specs/policies/exact/mru.md new file mode 100644 index 0000000..1f16255 --- /dev/null +++ b/docs/testing/specs/policies/exact/mru.md @@ -0,0 +1,76 @@ +# MRU operational spec + +> **Spec maturity:** reference +> +> **Executable oracle:** `tests/abstract_models/exact/mru.rs` (`MruModel`); independent reference: `reference/mru.rs` (`NaiveMruModel`). + +Most Recently Used cache replacement: evict the **most recently used** key (head of list) when space is needed. + +## State + +| Variable | Type | Meaning | +|----------|------|---------| +| `order` | `Seq` | Front = MRU (eviction victim); back = LRU | +| `capacity` | `usize` | Maximum resident count | + +## Init + +- `order = ⟨⟩` +- `capacity = C` + +## Observables + +| Observable | Definition | +|------------|------------| +| `resident` | Keys in `order` | +| `peek_victim` | Not asserted in harness (no `VictimInspectable` on impl) | +| `hit` | `MustHit` / `MustMiss` from membership | + +## Operations + +### `Insert(k)` + +1. If `k ∈ resident`: no-op for ordering (value update only in implementation). +2. Else if `|resident| ≥ capacity`: evict front (MRU), record `evicted_on_insert`. +3. Insert `k` at front. + +### `Get(k)` / `GetMut(k)` + +- If hit: promote to MRU. Set `hit` accordingly. + +### `Peek(k)` + +- Set `hit` from membership. **No promotion.** + +### `Touch(k)` + +- Promote on hit (same as `Get`). + +### `Remove(k)` + +- Remove `k` from `order` if present. + +### `EvictOne` + +- If MRU exists: remove front, `victim = Exact(front)`. + +## Tie-breaks + +- Victim on insert: head (MRU). Deterministic. + +## Harness `Op` mapping + +| `Op` | Cache API | Side effects | +|------|-----------|--------------| +| `Insert(k)` | `insert(k, v)` | Promote or insert/evict MRU | +| `Get(k)` | `get(k)` | Promote on hit | +| `Peek(k)` | `peek(k)` | No promotion | +| `GetMut(k)` | — | No-op in adapter | +| `Touch(k)` | `touch(k)` | Promote on hit | +| `Remove(k)` | `remove(k)` | Remove | +| `EvictOne` | `evict_one()` | Evict MRU | + +## References + +- CacheKit: [`MruCache`](../../../../src/policy/mru.rs) +- Policy matrix: [matrix.md](../../matrix.md) diff --git a/docs/testing/specs/policies/mirror/clock.md b/docs/testing/specs/policies/mirror/clock.md new file mode 100644 index 0000000..3e419f3 --- /dev/null +++ b/docs/testing/specs/policies/mirror/clock.md @@ -0,0 +1,51 @@ +# Clock operational spec + +> **Spec maturity:** stub +> +> **Executable oracle:** `tests/abstract_models/exact/clock.rs` (`ClockModel`) — mirrors [`ClockRing`](../../../../src/ds/clock_ring.rs) until an independent `reference/` model exists. + +Clock (second-chance): circular buffer with reference bits; evict first **unreferenced** slot on the clock hand. + +## State + +| Variable | Type | Meaning | +|----------|------|---------| +| `ring` | `ClockRing` | Circular slots with reference bits | +| `hand` | index | Clock sweep position | + +## Init + +- Empty ring at capacity `C`. + +## Observables + +| Observable | Definition | +|------------|------------| +| `resident` | Keys present in ring slots | +| `peek_victim` | First unreferenced slot from hand (second-chance sweep) | +| `hit` | `MustHit` / `MustMiss` | + +## Operations + +### `Insert(k)` + +- If new and full: sweep hand, clear reference bits, evict first unreferenced slot. +- Set reference bit on access/insert. + +### `Get(k)` / `Peek(k)` + +- `Get`: set reference bit on hit. `Peek`: no bit change. + +### `EvictOne` + +- Sweep and evict first unreferenced entry. + +## Harness notes + +- **Tier:** mirror — model wraps real `ClockRing` DS. +- Dual-impl: `ClockCache` vs `ClockRing` residency in `dual_impl_tests.rs`. + +## References + +- CacheKit: [`ClockCache`](../../../../src/policy/clock.rs) +- Policy matrix: [matrix.md](../../matrix.md) diff --git a/docs/testing/specs/policies/mirror/nru.md b/docs/testing/specs/policies/mirror/nru.md new file mode 100644 index 0000000..4ab63b7 --- /dev/null +++ b/docs/testing/specs/policies/mirror/nru.md @@ -0,0 +1,54 @@ +# NRU operational spec + +> **Spec maturity:** stub +> +> **Executable oracle:** `tests/abstract_models/exact/nru.rs` (`NruModel`) until an independent `reference/` model exists. + +Not Recently Used: track reference bit per key in insertion order; evict first **unreferenced** key (swap-remove). + +## State + +| Variable | Type | Meaning | +|----------|------|---------| +| `keys` | `Seq` | Insertion order (swap-remove on eviction) | +| `referenced` | `Map` | Reference bit per key | +| `capacity` | `usize` | Maximum resident count | + +## Init + +- `keys = ⟨⟩`, `referenced = ∅`, `capacity = C` +- New inserts start **unreferenced** (`false`). + +## Observables + +| Observable | Definition | +|------------|------------| +| `resident` | Keys in `keys` | +| `hit` | `MustHit` / `MustMiss` | + +## Operations + +### `Insert(k)` (new key) + +- If full: scan `keys` for first unreferenced; swap-remove and evict. +- Append `k` as unreferenced. + +### `Get(k)` / `Peek(k)` + +- `Get`: set `referenced[k] = true` on hit. +- `Peek`: no reference-bit change. + +### `Remove(k)` + +- Swap-remove `k` from `keys`. + +## Harness notes + +- **Tier:** mirror. +- No `EvictingCache` — op strategy `short_op_list_no_evict` (O(n) eviction scans). +- No explicit `EvictOne` in traces. + +## References + +- CacheKit: [`NruCache`](../../../../src/policy/nru.rs) +- Policy matrix: [matrix.md](../../matrix.md) diff --git a/docs/testing/specs/policies/mirror/slru.md b/docs/testing/specs/policies/mirror/slru.md new file mode 100644 index 0000000..b2e5f12 --- /dev/null +++ b/docs/testing/specs/policies/mirror/slru.md @@ -0,0 +1,55 @@ +# SLRU operational spec + +> **Spec maturity:** stub +> +> **Executable oracle:** `tests/abstract_models/exact/slru.rs` (`SlruModel`) — mirrors `SlruCore` until an independent `reference/` model exists. + +Segmented LRU: probationary and protected segments; evict LRU from probationary; re-access promotes to protected MRU. + +## State + +| Variable | Type | Meaning | +|----------|------|---------| +| `probationary` | `Seq` | Head = MRU, tail = LRU (eviction victim) | +| `protected` | `Seq` | Head = MRU, tail = LRU | +| `segments` | `Map` | Per-key segment | +| `probationary_cap` | `usize` | Max probationary size | +| `capacity` | `usize` | Total capacity | + +## Init + +- Both segments empty; `probationary_cap = floor(capacity * probationary_frac)`. + +## Observables + +| Observable | Definition | +|------------|------------| +| `resident` | Keys in either segment | +| `hit` | `MustHit` / `MustMiss` | + +## Operations + +### `Insert(k)` (new key) + +- Insert at probationary MRU; evict probationary LRU if full. + +### `Get(k)` / `Peek(k)` + +- On hit in probationary: promote to protected MRU. +- On hit in protected: promote within protected. +- `Peek`: no promotion. + +### `Remove(k)` + +- Remove from segment deques and map. + +## Harness notes + +- **Tier:** mirror. +- No `EvictingCache` — op strategy `standard_op_list_no_evict`. +- Tests assert residency only. + +## References + +- CacheKit: [`SlruCore`](../../../../src/policy/slru.rs) +- Policy matrix: [matrix.md](../../matrix.md) diff --git a/docs/testing/specs/policies/mirror/two-q.md b/docs/testing/specs/policies/mirror/two-q.md new file mode 100644 index 0000000..9cd7cfb --- /dev/null +++ b/docs/testing/specs/policies/mirror/two-q.md @@ -0,0 +1,56 @@ +# 2Q operational spec + +> **Spec maturity:** stub +> +> **Executable oracle:** `tests/abstract_models/exact/two_q.rs` (`TwoQModel`) — mirrors `TwoQCore` until an independent `reference/` model exists. + +2Q: two queues (probation A1 and protected Am); new keys enter probation; re-access promotes to protected; evict LRU from probation. + +## State + +| Variable | Type | Meaning | +|----------|------|---------| +| `probation` | `Seq` | A1 queue — head = newest, tail = LRU (eviction victim) | +| `protected` | `Seq` | Am queue — head = MRU, tail = LRU | +| `queues` | `Map` | Per-key queue membership | +| `probation_cap` | `usize` | Max probation size | +| `protected_cap` | `usize` | Max protected size | + +## Init + +- Both queues empty; caps derived from total capacity and `a1_frac`. + +## Observables + +| Observable | Definition | +|------------|------------| +| `resident` | Keys in either queue | +| `hit` | `MustHit` / `MustMiss` | + +## Operations + +### `Insert(k)` (new key) + +- Insert at head of probation; evict probation tail if over cap; may demote protected LRU to probation. + +### `Get(k)` / `Peek(k)` + +- On hit in probation: promote to protected MRU. +- On hit in protected: promote to protected MRU. +- `Peek`: no promotion. + +### `Remove(k)` + +- Remove from whichever queue holds `k`. + +## Harness notes + +- **Tier:** mirror. +- No `EvictingCache` on impl — op strategy `standard_op_list_no_evict` (no `EvictOne`). +- Tests assert residency only. + +## References + +- Johnson & Shasha, *2Q: A Low Overhead High Performance Buffer Management Replacement Algorithm* +- CacheKit: [`TwoQCore`](../../../../src/policy/two_q.rs) +- Policy matrix: [matrix.md](../../matrix.md) diff --git a/docs/testing/specs/template.md b/docs/testing/specs/template.md new file mode 100644 index 0000000..3612a05 --- /dev/null +++ b/docs/testing/specs/template.md @@ -0,0 +1,77 @@ +# <Policy> operational spec + +> **Spec maturity:** `stub` | `reference` | `tla` (comma-separated if multiple) +> +> **Executable oracle:** `tests/abstract_models/exact/<policy>.rs` until an independent `reference/` model exists. + +<One-sentence policy definition. This spec is independent of implementation internals; implementations must refine it.> + +## State + +| Variable | Type | Meaning | +|----------|------|---------| +| | | | + +**Invariants:** (structural properties at rest) + +## Init + +- `capacity = C` (given) +- … + +## Observables + +| Observable | Definition | +|------------|------------| +| `resident` | Keys currently in cache | +| `peek_victim` | Next eviction candidate, or none if empty | +| `recency_rank(k)` | 0 = MRU (LRU-family only); undefined if absent | +| `hit` | `MustHit` / `MustMiss` / `MayHitOrMiss` per op | +| `evicted_on_insert` | Key removed by eviction triggered by this `Insert`, if any | + +## Operations + +### `Insert(k)` + +1. … + +### `Get(k)` / `GetMut(k)` + +- … + +### `Peek(k)` + +- … +- **No promotion** (LRU-family). + +### `Touch(k)` + +- … + +### `Remove(k)` + +- … + +### `EvictOne` + +- … + +## Tie-breaks + +- Victim: … +- Equal ranks: … + +## Harness `Op` mapping + +See [_includes/harness-op-mapping.md](_includes/harness-op-mapping.md) for the standard table. Adjust side effects per policy above. + +## Formal spec (optional) + +If present: `formal/<policy>/<Policy>.tla` + `tlc.md`. See [tla-guide.md](tla-guide.md) and [formal/README.md](formal/README.md). + +## References + +- Literature / algorithm source (if applicable) +- CacheKit: [`<Impl>`](../../../src/policy/<module>.rs) must refine this spec +- Policy matrix: [matrix.md](matrix.md) +- Tier index: [policies/README.md](policies/README.md) diff --git a/docs/testing/specs/tla-guide.md b/docs/testing/specs/tla-guide.md new file mode 100644 index 0000000..cb4191f --- /dev/null +++ b/docs/testing/specs/tla-guide.md @@ -0,0 +1,200 @@ +# TLA+ contributor guide + +How to add optional TLA+ specs for cache policies. TLA+ checks **structural invariants on all reachable states** for a finite instance; Rust proptest checks **step-wise observables on long random traces**. They are complementary. + +## When to add TLA+ + +| Tier | TLA+ fit | +|------|----------| +| **Exact** | Good when state is finite and victim rules are deterministic | +| **Mirror** | Possible if the mirrored DS has bounded finite state | +| **Bounded** | Defer — adaptive victims and legal sets are harder to model finitely | +| **Composed** | Defer — TTL deadlines add continuous time | + +Start with a human operational spec ([template.md](template.md)) before writing TLA+. + +## File layout + +Human operational specs live under `policies//`. TLA+ artifacts live under `formal//`: + +```text +docs/testing/specs/ +├── policies/exact/.md # human source of truth +├── formal// +│ ├── .tla # MODULE name must match filename (case-sensitive on Linux) +│ ├── .cfg # TLC constants, INVARIANT, CONSTRAINT +│ └── tlc.md # Runbook + alignment checklist +├── tla-guide.md # This file +└── formal/README.md # Formal specs index +``` + +Run TLC via the generic wrapper: + +```bash +./scripts/run-tlc.sh fifo +# or aliases: +./scripts/run-fifo-tlc.sh +./scripts/run-tlc.sh lru +./scripts/run-lru-tlc.sh +``` + +TLC is **manual only** — not run in CI. + +## Authoring checklist + +1. **Separate semantic from exploration invariants** + - `SemanticOK` — policy truth (matches operational spec) + - `ExplorationOK` — finiteness bounds (`MaxQueueLen`, etc.) not in the human spec + +2. **Use a sentinel for optional values** — e.g. `NoVictim` instead of `NULL`. + +3. **Match harness `Op` alphabet** — document omitted ops (read-only hits, value-only updates). + +4. **Set `CHECK_DEADLOCK FALSE`** when exploration constraints can stall the state graph. + +5. **Document alignment** in `formal//tlc.md` with a change log when spec or `.tla` changes. + +6. **macOS filename note** — TLC requires filename to match `MODULE` name. On case-insensitive volumes `Fifo.tla` may appear as `fifo.tla`; do not create duplicates. + +--- + +## Worked example: FIFO + +FIFO is the reference TLA+ pilot. Human spec: [fifo.md](policies/exact/fifo.md). Runbook: [formal/fifo/tlc.md](formal/fifo/tlc.md). + +### Purpose + +| Artifact | What it proves | +|----------|----------------| +| [fifo.md](policies/exact/fifo.md) | Human-readable source of truth | +| [Fifo.tla](formal/fifo/Fifo.tla) + TLC | Structural FIFO invariants on **all reachable states** for a tiny finite instance | +| `NaiveFifoModel` + proptest | Step-wise observables on **long random traces** (`u8` keys, capacity `1..=16`) | + +### State variables glossary + +| TLA+ | [fifo.md](policies/exact/fifo.md) | `NaiveFifoModel` | +|------|-------------------|------------------| +| `cache` | `store` | `store: HashSet` | +| `queue` | `insertion_order` | `insertion_order: VecDeque` | +| `Capacity` | `capacity` | `capacity: usize` | +| `OldestLive` | `peek_victim` | `oldest_key()` / `peek_victim_key()` | +| `NoVictim` | none (empty cache) | `None` | + +**Stale entries:** after `RemoveKey`, removed keys stay in `queue` but not in `cache`. `OldestLive` skips them when scanning front-to-back. + +### State layout (example) + +```text +Capacity = 2 + +cache = {k2, k3} ← residents (set) +queue = ⟨k1, k2, k3⟩ ← insertion log (sequence) + ^stale ^live ^live + +OldestLive = k2 ← first queue element still in cache +``` + +### Action catalog + +| TLA+ action | Harness `Op` | Enabled when | `cache'` | `queue'` | +|-------------|--------------|--------------|----------|----------| +| `InsertNew(k)` | `Insert(k)` (new key) | `k ∉ cache`, queue room / eviction succeeds | add `k`; evict oldest if full | `PopThroughVictim` + append `k` if full; else append | +| `RemoveKey(k)` | `Remove(k)` | `k ∈ cache` | remove `k` | unchanged (stale remains) | +| `EvictOldest` | `EvictOne` | cache nonempty, victim exists | remove oldest live | `PopThroughVictim` | + +**Intentionally omitted:** `Get`, `Peek`, `GetMut`, `Touch` (no structural change); `Insert(k)` when `k ∈ cache` (value update only). + +### Invariants + +**`SemanticOK`** (policy truth — checked by TLC): + +| Operator | Meaning | +|----------|---------| +| `LenBound` | `\|cache\| ≤ Capacity` | +| `CacheKeysInQueue` | every resident key appears in `queue` | +| `QueueConsistency` | every queue element ∈ `Keys` | +| `PeekVictimOK` | cache empty ↔ `OldestLive = NoVictim` | +| `VictimInCache` | when victim defined, it is in `cache` | + +**`ExplorationOK`** (TLC finiteness only): + +| Operator | Meaning | +|----------|---------| +| `QueueLengthBound` | `Len(queue) ≤ MaxQueueLen` | + +### How to read `Fifo.tla` + +1. CONSTANTS / VARIABLES +2. Init +3. Helpers — `OldestLive`, `PopThroughVictim` +4. Invariants — `SemanticOK`, `ExplorationOK` +5. Actions — `InsertNew`, `RemoveKey`, `EvictOldest` +6. Next / Spec + +### Related files + +| File | Role | +|------|------| +| [Fifo.tla](formal/fifo/Fifo.tla) | Machine-readable spec (module `Fifo`) | +| [fifo.cfg](formal/fifo/fifo.cfg) | TLC constants and `INVARIANT SemanticOK` | +| [formal/fifo/tlc.md](formal/fifo/tlc.md) | FIFO runbook and alignment log | +| [fifo.md](policies/exact/fifo.md) | Human operational spec | +| [scripts/run-fifo-tlc.sh](../../../scripts/run-fifo-tlc.sh) | One-command TLC runner | + +--- + +## Worked example: LRU + +Second TLA+ pilot. Human spec: [lru.md](policies/exact/lru.md). Runbook: [formal/lru/tlc.md](formal/lru/tlc.md). + +### Purpose + +| Artifact | What it proves | +|----------|----------------| +| [lru.md](policies/exact/lru.md) | Human-readable source of truth | +| [Lru.tla](formal/lru/Lru.tla) + TLC | Structural LRU invariants on **all reachable states** for a tiny finite instance | +| `NaiveLruModel` + cross-model / proptest | Step-wise observables on **long random traces** | + +### State variables glossary + +| TLA+ | [lru.md](policies/exact/lru.md) | `NaiveLruModel` | +|------|------------------|-----------------| +| `order` | `order` (MRU-first deque) | `access` timestamps (equivalent oracle) | +| `LruKey` | `peek_victim` (back of deque) | `lru_victim()` / `peek_victim_key()` | +| `Capacity` | `capacity` | `capacity: usize` | +| `NoVictim` | none (empty cache) | `None` | + +Unlike FIFO, the LRU deque has **no stale entries** — `RemoveKey` filters the key from `order`. + +### Action catalog + +| TLA+ action | Harness `Op` | Enabled when | Effect | +|-------------|--------------|--------------|--------| +| `InsertNew(k)` | `Insert(k)` (new key) | `k ∉ Cache` | prepend `k`; evict LRU (back) if full | +| `PromoteKey(k)` | `Insert(k)` resident / `Get` / `Touch` hit | `k ∈ Cache` | move `k` to MRU (front) | +| `RemoveKey(k)` | `Remove(k)` | `k ∈ Cache` | remove `k` from deque | +| `EvictLru` | `EvictOne` | deque nonempty | drop LRU (back) | + +**Intentionally omitted:** `Peek` (no promotion); `GetMut` in `LruCore` adapter (no-op). + +### Invariants (`SemanticOK`) + +| Operator | Meaning | +|----------|---------| +| `LenBound` | `Len(order) ≤ Capacity` | +| `NoDuplicates` | deque entries are unique | +| `OrderInKeys` | every element ∈ `Keys` | +| `PeekVictimOK` | empty ↔ `LruKey = NoVictim` | +| `VictimInCache` | victim defined ⇒ resident | + +No `ExplorationOK` queue cap is needed — deque length is bounded by `Capacity`. + +### Related files + +| File | Role | +|------|------| +| [Lru.tla](formal/lru/Lru.tla) | Machine-readable spec (module `Lru`) | +| [lru.cfg](formal/lru/lru.cfg) | TLC constants and `INVARIANT SemanticOK` | +| [formal/lru/tlc.md](formal/lru/tlc.md) | LRU runbook and alignment log | +| [lru.md](policies/exact/lru.md) | Human operational spec | +| [scripts/run-lru-tlc.sh](../../../scripts/run-lru-tlc.sh) | One-command TLC runner | diff --git a/docs/testing/static-analysis.md b/docs/testing/static-analysis.md new file mode 100644 index 0000000..85a7a48 --- /dev/null +++ b/docs/testing/static-analysis.md @@ -0,0 +1,188 @@ +# Policy Semantic Testing (Static Analysis Oracles) + +## Overview + +This harness is a **test-side abstract interpreter** for eviction policies. It reuses ideas from WCET static cache analysis (ages, residency, must/may hit classification) as **semantic oracles** — not as a program analyzer. + +**What it is** + +- Reference models under [`tests/abstract_models/`](../../tests/abstract_models/) that predict residency, hit/miss, and victims from access traces ([README](../../tests/abstract_models/README.md)) +- Integration tests in `tests/policy_semantics/` that **dual-run** exact/mirror models against real implementations, or run **invariant-only** checks for bounded policies (ARC, CAR, Clock-PRO, S3-FIFO) +- Complements unit tests, in-module property tests, and fuzz targets (correctness only; not bench workloads) + +**What it is not** + +- A public `cachekit::analysis` API +- WCET analysis of arbitrary Rust CFGs +- Concurrency or performance testing + +## Background: WCET concepts reused here + +| Concept | Harness use | +|---------|-------------| +| LRU ages (0 = MRU) | Exact `LruOccupancyModel` and `recency_rank` assertions | +| Interval / legal victims | `OracleExpectation::Legal` for adaptive policies (Phase 3b) | +| Must / may hit-miss | `HitMiss::{MustHit,MustMiss,MayHitOrMiss}` | +| Path-sensitive traces | Future work (not yet implemented); dual-impl equivalence ships first | + +See [trait hierarchy](../design/trait-hierarchy.md) for `peek` vs `get` vs `touch` semantics asserted by the harness. + +## Spec-first oracles + +Operational specs in [`specs/`](specs/) are the source of truth. **Canonical policy index:** [matrix.md](specs/matrix.md) (tier, harness mode, models, op strategy, traits). + +```text +spec doc → reference/ PolicyModel (optional) → exact/ PolicyModel → implementation dual-run +``` + +| Harness mode | Tier | Oracle | +|--------------|------|--------| +| DualRun | exact, mirror, composed | `exact/` vs impl | +| CrossModel | exact (all policies with `reference/` models) | `reference/` vs `exact/` | +| InvariantOnly | bounded | structural invariants on impl | + +**FIFO + LRU worked example:** + +| Layer | FIFO | LRU | +|-------|------|-----| +| Spec | [fifo.md](specs/policies/exact/fifo.md) | [lru.md](specs/policies/exact/lru.md) | +| Reference | `NaiveFifoModel` | `NaiveLruModel` | +| Exact | `FifoModel` | `LruOccupancyModel` | +| Cross-model | `prop_fifo_naive_matches_current_model` | `prop_lru_naive_matches_current_model` | +| Impl dual-run | `prop_fifo_matches_model` | `prop_lru_core_matches_model` | + +All exact-tier policies in [matrix.md](specs/matrix.md) now have reference models (LRU-K completes the set). Mirror and bounded policies remain `stub` maturity with invariant-only or dual-run harnesses. + +**Failure interpretation:** reference ≠ exact → fix spec or `exact/` model; reference = exact but impl fails → fix implementation or adapter. + +FIFO and LRU include optional [TLA+](specs/formal/fifo/Fifo.tla) specs (manual TLC, not CI). Read [tla-guide.md](specs/tla-guide.md); run [`scripts/run-fifo-tlc.sh`](../../scripts/run-fifo-tlc.sh), [`scripts/run-lru-tlc.sh`](../../scripts/run-lru-tlc.sh), or [`scripts/run-tlc.sh`](../../scripts/run-tlc.sh). Runbooks: [formal/fifo/tlc.md](specs/formal/fifo/tlc.md), [formal/lru/tlc.md](specs/formal/lru/tlc.md). + +## Architecture + +```mermaid +flowchart TB + subgraph harness [tests/abstract_models] + OpEnum["Op incl. GetMut"] + Exact[exact models] + Bounded[bounded checks] + end + subgraph entry [tests/policy_semantics] + Proptest[proptest traces] + Smoke[smoke_ Miri traces] + end + Proptest --> Exact + Proptest --> entry + Smoke --> entry + entry --> policies[Policy implementations] + Exact --> policies +``` + +### Core types (`tests/abstract_models/mod.rs`) + +| Type | Role | +|------|------| +| `Op` | `Insert`, `Get`, `Peek`, `GetMut`, `Touch`, `Remove`, `EvictOne` | +| `HitMiss` | `MustHit`, `MustMiss`, `MayHitOrMiss` (bounded / TTL only) | +| `PolicyModel` | `apply(op) -> ModelStep` | +| `ModelStep` | `resident`, `hit`, `victim`, `evicted_on_insert` | +| `OracleExpectation` | `Exact(k)`, `Legal(set)`, `None` | + +**Peek vs get:** `Peek` must not change `recency_rank`; `Get` / `GetMut` / `Touch` promote on LRU-family policies. + +## Policy coverage matrix + +| Policy | Model type | Module | Traits asserted | Status | +|--------|------------|--------|-----------------|--------| +| LRU | exact | `exact/lru.rs` | VictimInspectable, RecencyTracking, EvictingCache | done | +| Fast-LRU | exact | `exact/lru.rs` | VictimInspectable, RecencyTracking, EvictingCache | done | +| FIFO | exact | `exact/fifo.rs` | VictimInspectable, EvictingCache | done | +| LIFO | exact | `exact/lifo.rs` | VictimInspectable, EvictingCache | done | +| MRU | exact | `exact/mru.rs` | EvictingCache | done | +| LFU | exact | `exact/lfu.rs` | VictimInspectable, FrequencyTracking, EvictingCache | done | +| Heap-LFU | exact | `exact/heap_lfu.rs` | residency (heap tie-break via `Ord`) | done | +| MFU | exact | `exact/mfu.rs` | residency (`FxHashMap` peek scan) | done | +| LRU-K | exact | `exact/lru_k.rs` | HistoryTracking, EvictingCache | done | +| Clock | exact mirror | `exact/clock.rs` | EvictingCache | done | +| 2Q | exact mirror | `exact/two_q.rs` | residency (no `EvictingCache`) | done | +| SLRU | exact mirror | `exact/slru.rs` | residency | done | +| NRU | exact mirror | `exact/nru.rs` | residency (no explicit `EvictingCache`) | done | +| S3-FIFO | bounded | `bounded/s3_fifo.rs` | `check_invariants`, residency | done | +| ARC | bounded | `bounded/arc.rs` | `debug_validate_invariants` | done | +| CAR | bounded | `bounded/car.rs` | `debug_validate_invariants` (`CarCore`) | done | +| Clock-PRO | bounded | `bounded/clock_pro.rs` | structural checks | done | +| Random | none | — | — | deferred | +| Expiring/TTL | composed | `ttl_integration_test.rs` | `LruOccupancyModel` + deadlines | done | + +Bounded **Module** column entries (`bounded/*.rs`) are documentation stubs; tests live in `policy_semantics/*_tests.rs`. + +## Running the harness + +```bash +# Full matrix (all policy features) +cargo test --test policy_semantics --all-features + +# Default features only +cargo test --test policy_semantics + +# Single policy proptest +cargo test --test policy_semantics --all-features prop_lru_core_matches_model + +# High case count (CI property-tests job) +PROPTEST_CASES=1000 cargo test --test policy_semantics --all-features + +# Miri smoke traces (CI miri job) +cargo miri test --test policy_semantics --all-features smoke_ -- --test-threads=1 + +# TTL layer (uses shared LruOccupancyModel) +cargo test --test ttl_integration_test --features ttl +``` + +Proptests use `#[cfg_attr(miri, ignore)]`; Miri runs only `smoke_*` hand-written traces. + +## Adding a new policy model + +See also the [abstract_models contributor checklist](../../tests/abstract_models/README.md#adding-a-new-model). + +1. Add model code by tier: exact/mirror → `tests/abstract_models/exact/.rs` implementing `PolicyModel`; bounded → `tests/abstract_models/bounded/.rs` doc stub (no `PolicyModel` required today). +2. Cite tie-break / mirror source in the module `//!` doc. +3. Add `tests/policy_semantics/_tests.rs` with dual-run or invariant-only `run_ops`, plus `smoke_*` + `prop_*`. +4. Gate the module in `tests/policy_semantics/main.rs` with `#[cfg(feature = "policy-…")]`. +5. Append a row to [matrix.md](specs/matrix.md). + +Use `op_strategy_no_evict()` when the policy lacks [`EvictingCache`](../../src/traits.rs). + +## Model tiers + +**Exact** — residency, victim, and rank (where applicable) must match. + +**Mirror** — full queue/segment state transcribed from implementation (`TwoQCore`, `SlruCore`, `ClockRing`). + +**Bounded** — invariant-only tests assert `len <= capacity` and `debug_validate_invariants` / `check_invariants`. Sibling `bounded/*.rs` files are feature-gated doc stubs. Victim may be a legal set (future). + +## Dual-impl equivalence + +`tests/policy_semantics/dual_impl_tests.rs`: + +- `LruCore` vs `FastLru` — `contains`, `peek_victim`, `recency_rank` +- `ClockCache` vs `ClockRing` — residency agreement + +## Debugging failures + +1. Re-run the failing `smoke_*` test with `--nocapture`. +2. Shrink with `PROPTEST_CASES=1 cargo test … prop_… -- --nocapture`. +3. Compare model `apply(op)` step to cache state after each op. +4. Check adapter: `Arc` vs `V`, `increment_frequency` vs `touch`, `*k` when matching `&Op`. + +## CI integration + +- Main `test` job: `cargo test --tests --all-features` (256 proptest cases by default). +- `property-tests` job: `PROPTEST_CASES=1000 cargo test --test policy_semantics --all-features`. +- `miri` job: `cargo miri test --test policy_semantics --all-features smoke_`. + +## Related documentation + +- [Operational policy specs](specs/README.md) — spec-first source of truth +- [Abstract models README](../../tests/abstract_models/README.md) — directory layout and policy matrix +- [Testing strategy](testing.md) — four test layers including policy semantics +- [Trait hierarchy](../design/trait-hierarchy.md) — capability traits used as oracles +- [Policy catalog](../policies/README.md) — semantic oracle column diff --git a/docs/testing/testing.md b/docs/testing/testing.md index 858274b..e73b78d 100644 --- a/docs/testing/testing.md +++ b/docs/testing/testing.md @@ -84,7 +84,22 @@ cargo test prop_ PROPTEST_CASES=10000 cargo test prop_len_within_capacity ``` -### 3. Fuzz Tests +### 3. Policy Semantic Tests + +**Location**: `tests/abstract_models/`, `tests/policy_semantics/` + +**Purpose**: Catch semantic drift in eviction, residency, and rank behavior. Exact and mirror policies use dual-run reference models; bounded policies (ARC, CAR, Clock-PRO, S3-FIFO) use invariant-only structural checks. + +**Run**: + +```bash +cargo test --test policy_semantics --all-features +PROPTEST_CASES=1000 cargo test --test policy_semantics --all-features +``` + +See [Policy semantic testing (static analysis oracles)](static-analysis.md) for architecture, policy matrix, and contributor checklist. Operational specs live under [specs/policies/](specs/policies/README.md) by tier; FIFO and LRU also have [formal/](specs/formal/README.md) TLA+ pilots. Spec-derived `reference/` models are cross-checked against `exact/` oracles before impl dual-run. + +### 4. Fuzz Tests **Location**: `fuzz/fuzz_targets/` @@ -159,10 +174,11 @@ cargo test --features concurrency Our CI runs: 1. Unit tests on all supported platforms -2. Property tests with increased case count (1000) -3. Quick fuzz tests on PRs (60 seconds per target) -4. Continuous fuzzing nightly (1 hour per target) -5. Tests with all feature combinations +2. Property tests with increased case count (1000), including `policy_semantics` +3. Miri smoke tests for `policy_semantics` (`smoke_*` traces) +4. Quick fuzz tests on PRs (60 seconds per target) +5. Continuous fuzzing nightly (1 hour per target) +6. Tests with all feature combinations **See [Fuzzing in CI/CD](fuzzing-cicd.md) for detailed fuzzing setup.** diff --git a/scripts/run-fifo-tlc.sh b/scripts/run-fifo-tlc.sh new file mode 100755 index 0000000..5e76acc --- /dev/null +++ b/scripts/run-fifo-tlc.sh @@ -0,0 +1,8 @@ +#!/usr/bin/env bash +# Run TLC on the FIFO TLA+ spec (manual check, not CI). +# Thin alias for scripts/run-tlc.sh — see docs/testing/specs/tla-guide.md + +set -euo pipefail + +ROOT="$(cd "$(dirname "$0")/.." && pwd)" +exec "${ROOT}/scripts/run-tlc.sh" fifo diff --git a/scripts/run-lru-tlc.sh b/scripts/run-lru-tlc.sh new file mode 100755 index 0000000..7dfb0b6 --- /dev/null +++ b/scripts/run-lru-tlc.sh @@ -0,0 +1,8 @@ +#!/usr/bin/env bash +# Run TLC on the LRU TLA+ spec (manual check, not CI). +# Thin alias for scripts/run-tlc.sh — see docs/testing/specs/tla-guide.md + +set -euo pipefail + +ROOT="$(cd "$(dirname "$0")/.." && pwd)" +exec "${ROOT}/scripts/run-tlc.sh" lru diff --git a/scripts/run-tlc.sh b/scripts/run-tlc.sh new file mode 100755 index 0000000..842e21e --- /dev/null +++ b/scripts/run-tlc.sh @@ -0,0 +1,45 @@ +#!/usr/bin/env bash +# Run TLC on a TLA+ spec (manual check, not CI). +# Usage: ./scripts/run-tlc.sh [policy] +# policy: fifo (default) | lru +# See docs/testing/specs/tla-guide.md + +set -euo pipefail + +ROOT="$(cd "$(dirname "$0")/.." && pwd)" +SPECS="${ROOT}/docs/testing/specs" + +POLICY="${1:-fifo}" + +case "${POLICY}" in + Fifo|fifo) + SLUG="fifo" + FORMAL_DIR="${SPECS}/formal/fifo" + MODULE="Fifo" + CONFIG="fifo.cfg" + ;; + Lru|lru) + SLUG="lru" + FORMAL_DIR="${SPECS}/formal/lru" + MODULE="Lru" + CONFIG="lru.cfg" + ;; + *) + echo "error: unknown policy '${POLICY}' (expected fifo or lru)" >&2 + exit 1 + ;; +esac + +if ! command -v tlc >/dev/null 2>&1; then + echo "error: tlc not found on PATH" >&2 + echo "Install TLA+ tools: https://github.com/tlaplus/tlaplus/releases" >&2 + exit 1 +fi + +cd "${FORMAL_DIR}" +echo "Running TLC: ${CONFIG} + ${MODULE}.tla" +tlc -config "${CONFIG}" "${MODULE}.tla" +echo "" +echo "TLC: invariant check passed (${MODULE})." +echo "Guide: docs/testing/specs/tla-guide.md" +echo "Runbook: docs/testing/specs/formal/${SLUG}/tlc.md" diff --git a/src/policy/mfu.rs b/src/policy/mfu.rs index 58299e8..d470b30 100644 --- a/src/policy/mfu.rs +++ b/src/policy/mfu.rs @@ -334,6 +334,9 @@ where if current_freq == entry.freq { self.map.remove(&entry.key); self.frequencies.remove(&entry.key); + if self.map.is_empty() { + self.freq_heap.clear(); + } #[cfg(debug_assertions)] self.validate_invariants(); @@ -348,6 +351,9 @@ where if let Some(entry) = self.freq_heap.pop() { self.map.remove(&entry.key); self.frequencies.remove(&entry.key); + if self.map.is_empty() { + self.freq_heap.clear(); + } #[cfg(debug_assertions)] self.validate_invariants(); @@ -428,6 +434,9 @@ where pub fn remove(&mut self, key: &K) -> Option { self.frequencies.remove(key); let result = self.map.remove(key); + if result.is_some() && self.map.is_empty() { + self.freq_heap.clear(); + } #[cfg(debug_assertions)] if result.is_some() { @@ -463,6 +472,9 @@ where if current_freq == entry.freq { if let Some(value) = self.map.remove(&entry.key) { self.frequencies.remove(&entry.key); + if self.map.is_empty() { + self.freq_heap.clear(); + } #[cfg(feature = "metrics")] self.metrics.record_pop_mfu_found(); diff --git a/tests/README.md b/tests/README.md index 512d97d..5d46153 100644 --- a/tests/README.md +++ b/tests/README.md @@ -23,9 +23,17 @@ This directory contains all integration and regression tests for cachekit. - **`policy_invariants.rs`** - Cross-policy behavioral consistency (e.g. capacity-0 semantics) +### Policy Semantic Tests + +- **`abstract_models/`** — Reference models (exact, mirror, bounded) used as test-side oracles. + See [abstract_models/README.md](abstract_models/README.md). +- **`policy_semantics/`** — Proptest and Miri smoke traces: dual-run for exact/mirror policies, + invariant-only for bounded policies. Run: `cargo test --test policy_semantics --all-features`. + ### Integration Tests - **`lru_integration_test.rs`** - LRU policy integration tests +- **`ttl_integration_test.rs`** - TTL layer tests (reuses `LruOccupancyModel`) ## Performance Testing Philosophy diff --git a/tests/abstract_models/README.md b/tests/abstract_models/README.md new file mode 100644 index 0000000..cb9a967 --- /dev/null +++ b/tests/abstract_models/README.md @@ -0,0 +1,229 @@ +# Abstract Policy Models + +Reference semantics for eviction policies used as **test-side oracles**. Exact and mirror models predict residency, hit/miss, and victims from access traces; integration tests in [`policy_semantics/`](../policy_semantics/) **dual-run** those models against real implementations. Bounded-tier policies use **invariant-only** tests (no `PolicyModel` dual-run today). + +This is not a public API. For the full harness design (WCET concepts reused, CI, debugging), see [Policy semantic testing](../../docs/testing/static-analysis.md). + +## Purpose + +Cache policies are easy to get subtly wrong: tie-break order, peek vs get promotion, stale queue entries, and adaptive victim selection all drift without exhaustive traces. Abstract models give a **deterministic specification** that proptest and Miri smoke tests can compare against every step. + +``` +access trace ──► PolicyModel::apply(op) ──► ModelStep + │ │ + │ ▼ + real policy assert residency, + (LruCore, etc.) victim, rank, hit/miss +``` + +## Directory layout + +``` +abstract_models/ +├── mod.rs # Op, HitMiss, PolicyModel, ModelStep, proptest strategies +├── driver.rs # Shared assertion helpers (assert_peek_victim, assert_models_agree, …) +├── reference/ # Spec-derived models (transcribed from docs/testing/specs/) +│ ├── fifo.rs # NaiveFifoModel +│ ├── heap_lfu.rs # NaiveHeapLfuModel +│ ├── mfu.rs # NaiveMfuModel +│ ├── lru.rs # NaiveLruModel (timestamp formulation) +│ ├── lifo.rs # NaiveLifoModel +│ ├── lfu.rs # NaiveLfuModel +│ ├── lru_k.rs # NaiveLruKModel +│ └── mru.rs # NaiveMruModel +├── exact/ # Deterministic victims and residency +│ ├── lru.rs # LruOccupancyModel (LRU, Fast-LRU, TTL layer) +│ ├── fifo.rs # FifoModel +│ ├── lfu.rs # LfuModel +│ └── … # One module per exact/mirror policy +└── bounded/ # Invariant-only oracles (feature-gated doc stubs) + ├── mod.rs # re-exports bounded policy stubs + ├── arc.rs # doc stub — tests in policy_semantics/arc_tests.rs + ├── car.rs # doc stub + ├── clock_pro.rs + └── s3_fifo.rs +``` + +The harness is compiled into two integration test crates via `#[path]`: + +- [`policy_semantics/main.rs`](../policy_semantics/main.rs) — proptest + smoke matrix +- [`ttl_integration_test.rs`](../ttl_integration_test.rs) — `LruOccupancyModel` + TTL deadlines + +## Core types (`mod.rs`) + +| Type | Role | +|------|------| +| `Op` | Trace alphabet: `Insert`, `Get`, `Peek`, `GetMut`, `Touch`, `Remove`, `EvictOne` | +| `HitMiss` | `MustHit`, `MustMiss`, `MayHitOrMiss` (bounded / TTL only) | +| `PolicyModel` | `apply(op) -> ModelStep`, `peek_victim_key`, `resident_set` | +| `ModelStep` | `resident`, `hit`, `victim`, `evicted_on_insert` after one op | +| `OracleExpectation` | `Exact(k)`, `Legal(set)`, `None` | + +**Peek vs get:** `Peek` must not change `recency_rank`; `Get`, `GetMut`, and `Touch` promote on LRU-family policies. See [trait hierarchy](../../docs/design/trait-hierarchy.md). + +## Model tiers + +### Reference (`reference/`) + +Spec-first oracles transcribed from [operational specs](../../docs/testing/specs/). Independent formulation from `exact/` models (e.g. LRU timestamps vs deque). Cross-model tests in `policy_semantics/` assert `reference/` agrees with `exact/` on the same traces. + +| Policy | Reference model | Spec | Cross-model signal | +|--------|-----------------|------|-------------------| +| FIFO | `NaiveFifoModel` | [fifo.md](../../docs/testing/specs/policies/exact/fifo.md) | Drift guard (low day-one — `FifoModel` is already spec-shaped) | +| LRU | `NaiveLruModel` | [lru.md](../../docs/testing/specs/policies/exact/lru.md) | High — deque vs timestamp independence | +| Fast-LRU | `NaiveLruModel` (shared) | [fast-lru.md](../../docs/testing/specs/policies/exact/fast-lru.md) | Same reference; `op_strategy_with_get_mut` cross-model | +| LIFO | `NaiveLifoModel` | [lifo.md](../../docs/testing/specs/policies/exact/lifo.md) | Drift guard — `Vec` stack vs `VecDeque` exact | +| LFU | `NaiveLfuModel` | [lfu.md](../../docs/testing/specs/policies/exact/lfu.md) | High — `first_seen` log vs `FrequencyBuckets` | +| MRU | `NaiveMruModel` | [mru.md](../../docs/testing/specs/policies/exact/mru.md) | Drift guard — `Vec` index-0 vs `VecDeque` exact | +| Heap-LFU | `NaiveHeapLfuModel` | [heap-lfu.md](../../docs/testing/specs/policies/exact/heap-lfu.md) | High — `HashMap` Ord-min vs `BinaryHeap` exact | +| MFU | `NaiveMfuModel` | [mfu.md](../../docs/testing/specs/policies/exact/mfu.md) | High — `last_seq` map vs `BinaryHeap` exact | +| LRU-K | `NaiveLruKModel` | [lru-k.md](../../docs/testing/specs/policies/exact/lru-k.md) | High — `Vec` segments vs `VecDeque` exact | + +FIFO and LRU have [TLA+ pilots](../../docs/testing/specs/formal/fifo/Fifo.tla) ([`Lru.tla`](../../docs/testing/specs/formal/lru/Lru.tla)) — read [tla-guide.md](../../docs/testing/specs/tla-guide.md); run [`scripts/run-fifo-tlc.sh`](../../scripts/run-fifo-tlc.sh) or [`scripts/run-lru-tlc.sh`](../../scripts/run-lru-tlc.sh) (manual, not CI). + +### Exact (`exact/`) + +Residency, victim, and recency rank (where applicable) must match the implementation exactly. + +Examples: `LruOccupancyModel`, `FifoModel`, `LfuModel`, `MruModel`. + +### Mirror (`exact/`) + +Full internal state transcribed from the implementation rather than a simplified abstract rule. Used when the policy's behavior is defined by its data structure. + +Examples: `ClockModel` (wraps `ClockRing`), `TwoQModel` (`TwoQCore` queues), `SlruModel`, `NruModel`. + +### Bounded (`bounded/`) + +Adaptive or scan-resistant policies where the victim is not uniquely determined from residency alone. Models assert: + +- `len <= capacity` +- residency after inserts +- `debug_validate_invariants` / `check_invariants` on the real cache +- `OracleExpectation::Legal` victim sets (future: full legal-set checks) + +Examples: ARC, CAR, Clock-PRO, S3-FIFO. Sibling files (`arc.rs`, etc.) are **documentation stubs** only; real checks live in `policy_semantics/*_tests.rs`. Submodules are gated by matching `policy-*` features (same as `exact/`). + +## Harness modes + +| Mode | Tests | Helper | +|------|-------|--------| +| **DualRun** | `prop_*_matches_model` | [`assert_dual_run_step`](driver.rs) or [`assert_dual_run_step_no_victim`](driver.rs) | +| **CrossModel** | `prop_*_naive_matches_current` | [`assert_models_agree`](driver.rs) | +| **InvariantOnly** | `prop_*_invariants` | [`run_invariant_trace`](driver.rs) | + +Metadata and contributor checklist: [`spec_harness.rs`](spec_harness.rs). + +## Policy coverage + +**Canonical index:** [matrix.md](../../docs/testing/specs/matrix.md) (spec maturity, tier, harness mode, op strategy, traits). + +Onboard a new policy using [template.md](../../docs/testing/specs/template.md). + +## Proptest strategies + +| Strategy | Use when | +|----------|----------| +| `standard_op_list()` | Default dual-run policies (LRU, FIFO, LFU, Clock, …) | +| `standard_op_list_no_evict()` | 2Q, SLRU (no `EvictingCache`; includes `Remove`) | +| `standard_op_list_mfu_safe()` | MFU only (skips `Remove`/`EvictOne`; stale heap) | +| `op_strategy_with_get_mut()` | Fast-LRU, S3-FIFO proptests | +| `short_op_list_no_evict()` | NRU (O(n) eviction; shorter traces) | + +Capacities: `standard_capacity()` → `1..=16`. Trace lengths: `standard_op_list()` → `0..120` ops. Heap-LFU uses `standard_op_list()` (heap rebuild handles staleness on insert/evict). + +## Running tests + +```bash +# Full policy matrix (all features) +cargo test --test policy_semantics --all-features + +# Single policy +cargo test --test policy_semantics --all-features prop_lru_core_matches_model + +# High case count (CI) +PROPTEST_CASES=1000 cargo test --test policy_semantics --all-features + +# Miri smoke traces only +cargo miri test --test policy_semantics --all-features smoke_ -- --test-threads=1 + +# TTL layer (shared LruOccupancyModel) +cargo test --test ttl_integration_test --features ttl +``` + +Proptests use `#[cfg_attr(miri, ignore)]`; Miri runs hand-written `smoke_*` traces only. + +## Adding a new model + +**Spec-first flow (recommended for exact policies):** + +1. Write operational spec in [`docs/testing/specs/policies//`](../../docs/testing/specs/policies/README.md) (state, per-`Op` rules, tie-breaks). +2. Implement `reference/.rs` from the spec only (independent formulation). +3. Implement or align `exact/.rs`; cite the spec doc in `//!` header. +4. Add cross-model tests: `prop__naive_matches_current_model` using `assert_models_agree`. +5. Add impl dual-run: `run_ops`, `smoke_*`, `prop_*_matches_model`. +6. Gate features and append a row to [matrix.md](../../docs/testing/specs/matrix.md). + +**Tier choice:** Simple deterministic eviction → `exact/`. Behavior tied to internal DS → mirror in `exact/`. Adaptive victim → `bounded/` (doc stub + invariant-only tests). + +**Bounded policies:** add a `//!` doc stub in `bounded/.rs` (no `PolicyModel` required today); invariant-only `run_ops` in `policy_semantics/`. + +Use `op_strategy_no_evict()` when the policy does not implement [`EvictingCache`](../../src/traits.rs). + +### Dual-run pattern + +All `policy_semantics/*_tests.rs` dual-run loops use shared helpers (except [`dual_impl_tests.rs`](../policy_semantics/dual_impl_tests.rs)). + +Minimal (LIFO): [`lifo_tests.rs`](../policy_semantics/lifo_tests.rs) + +```rust +assert_dual_run_step(cache, model, &step, |k| cache.contains(k), |_, _, _| {}); +``` + +No `VictimInspectable` (MRU, mirror policies): use [`assert_dual_run_step_no_victim`](driver.rs) — see [`mru_tests.rs`](../policy_semantics/mru_tests.rs). + +### Dual-run extra closure + +Policy-specific oracles go in the `extra` closure: + +- **LFU frequency:** [`lfu_tests.rs`](../policy_semantics/lfu_tests.rs) +- **LRU recency / peek:** [`lru_tests.rs`](../policy_semantics/lru_tests.rs), [`fast_lru_tests.rs`](../policy_semantics/fast_lru_tests.rs) +- **LRU-K access count:** [`lru_k_tests.rs`](../policy_semantics/lru_k_tests.rs) + +```rust +assert_dual_run_step(cache, model, &step, |k| cache.contains(k), |cache, model, step| { + for k in &step.resident { + assert_eq!(cache.frequency(k), model.frequency(k)); + } +}); +``` + +### Invariant-only pattern + +Bounded tier — see [`arc_tests.rs`](../policy_semantics/arc_tests.rs): + +```rust +run_invariant_trace(cache, ops, apply_arc_op, |cache| { + cache.debug_validate_invariants(); +}); +``` + +For S3-FIFO, wrap `check_invariants` in `#[cfg(debug_assertions)]` inside the `check` closure. + +Shared helpers live in [`driver.rs`](driver.rs): `assert_dual_run_step`, `assert_dual_run_step_no_victim`, `run_invariant_trace`, `assert_peek_victim`, `assert_recency_rank`, `assert_models_agree`, `assert_models_agree_with_recency`, and `probe_resident`. + +## Debugging failures + +1. Re-run the failing `smoke_*` test with `--nocapture`. +2. Shrink: `PROPTEST_CASES=1 cargo test --test policy_semantics prop_ -- --nocapture`. +3. Step through `model.apply(op)` vs cache state after each op. +4. Check the adapter: `Arc` vs `V`, `increment_frequency` vs `touch`, dereference `&Op` keys when matching. + +## Related documentation + +- [Policy spec matrix](../../docs/testing/specs/matrix.md) +- [Operational policy specs](../../docs/testing/specs/README.md) +- [Policy semantic testing (full harness)](../../docs/testing/static-analysis.md) +- [Testing strategy](../../docs/testing/testing.md) +- [Trait hierarchy](../../docs/design/trait-hierarchy.md) +- [Policy catalog](../../docs/policies/README.md) diff --git a/tests/abstract_models/bounded/arc.rs b/tests/abstract_models/bounded/arc.rs new file mode 100644 index 0000000..a377a47 --- /dev/null +++ b/tests/abstract_models/bounded/arc.rs @@ -0,0 +1,9 @@ +//! ARC bounded oracle — structural invariant checks, not a full adaptive model. +//! +//! **Source:** [`docs/testing/specs/policies/bounded/arc.md`](../../../docs/testing/specs/policies/bounded/arc.md) · +//! [matrix.md](../../../docs/testing/specs/matrix.md) +//! **Tier:** bounded. Victim selection is adaptive; this module documents the test contract. +//! **Checks:** `len <= capacity`, `ArcCore::debug_validate_invariants` after every op. +//! **Tests:** `policy_semantics/arc_tests.rs`. +//! **Op strategy:** [`op_strategy`](super::super::op_strategy) (`GetMut`/`Touch`/`EvictOne` no-op +//! in adapter). diff --git a/tests/abstract_models/bounded/car.rs b/tests/abstract_models/bounded/car.rs new file mode 100644 index 0000000..532b21c --- /dev/null +++ b/tests/abstract_models/bounded/car.rs @@ -0,0 +1,9 @@ +//! CAR bounded oracle — structural invariant checks on `CarCore`. +//! +//! **Source:** [`docs/testing/specs/policies/bounded/car.md`](../../../docs/testing/specs/policies/bounded/car.md) · +//! [matrix.md](../../../docs/testing/specs/matrix.md) +//! **Tier:** bounded. Clock-with-adaptation victim is not modeled exactly. +//! **Checks:** `len <= capacity`, `CarCore::debug_validate_invariants` after every op. +//! **Tests:** `policy_semantics/car_tests.rs`. +//! **Op strategy:** [`op_strategy`](super::super::op_strategy) (`GetMut`/`Touch`/`EvictOne` no-op +//! in adapter). diff --git a/tests/abstract_models/bounded/clock_pro.rs b/tests/abstract_models/bounded/clock_pro.rs new file mode 100644 index 0000000..b0bd182 --- /dev/null +++ b/tests/abstract_models/bounded/clock_pro.rs @@ -0,0 +1,9 @@ +//! Clock-PRO bounded oracle — structural invariant checks. +//! +//! **Source:** [`docs/testing/specs/policies/bounded/clock-pro.md`](../../../docs/testing/specs/policies/bounded/clock-pro.md) · +//! [matrix.md](../../../docs/testing/specs/matrix.md) +//! **Tier:** bounded. Hot/cold/non-resident lists make exact victim prediction impractical. +//! **Checks:** `len <= capacity`, `ClockProCache::debug_validate_invariants` after every op. +//! **Tests:** `policy_semantics/clock_pro_tests.rs`. +//! **Op strategy:** [`op_strategy`](super::super::op_strategy) (`GetMut`/`Touch`/`EvictOne` no-op +//! in adapter). diff --git a/tests/abstract_models/bounded/mod.rs b/tests/abstract_models/bounded/mod.rs new file mode 100644 index 0000000..ed0e9aa --- /dev/null +++ b/tests/abstract_models/bounded/mod.rs @@ -0,0 +1,16 @@ +//! Bounded reference models for adaptive and scan-resistant policies. +//! +//! When a victim is not uniquely determined from residency alone (ARC, CAR, Clock-PRO, +//! S3-FIFO), tests use **invariant-only** checks rather than a `PolicyModel` dual-run. +//! +//! Sibling modules are **documentation stubs** only; real checks live in +//! `policy_semantics/*_tests.rs`. + +#[cfg(feature = "policy-arc")] +pub mod arc; +#[cfg(feature = "policy-car")] +pub mod car; +#[cfg(feature = "policy-clock-pro")] +pub mod clock_pro; +#[cfg(feature = "policy-s3-fifo")] +pub mod s3_fifo; diff --git a/tests/abstract_models/bounded/s3_fifo.rs b/tests/abstract_models/bounded/s3_fifo.rs new file mode 100644 index 0000000..836aee2 --- /dev/null +++ b/tests/abstract_models/bounded/s3_fifo.rs @@ -0,0 +1,8 @@ +//! S3-FIFO bounded oracle — residency and structural invariant checks. +//! +//! **Source:** [`docs/testing/specs/policies/bounded/s3-fifo.md`](../../../docs/testing/specs/policies/bounded/s3-fifo.md) · +//! [matrix.md](../../../docs/testing/specs/matrix.md) +//! **Tier:** bounded. Three-queue scan resistance; victim not uniquely determined here. +//! **Checks:** `len <= capacity`, `S3FifoCache::check_invariants` after every op. +//! **Tests:** `policy_semantics/s3_fifo_tests.rs`. +//! **Op strategy:** [`op_strategy_with_get_mut`](super::super::op_strategy_with_get_mut). diff --git a/tests/abstract_models/driver.rs b/tests/abstract_models/driver.rs new file mode 100644 index 0000000..ee21576 --- /dev/null +++ b/tests/abstract_models/driver.rs @@ -0,0 +1,198 @@ +//! Shared assertion helpers for dual-run cache vs model tests. +//! +//! These functions compare a real cache (implementing capability traits from +//! [`cachekit::traits`](../../src/traits.rs)) against a [`PolicyModel`] step produced by +//! [`PolicyModel::apply`]. +//! +//! Typical usage in `policy_semantics/*_tests.rs`: +//! +//! ```ignore +//! let step = model.apply(op.clone()); +//! // … apply op to cache … +//! assert_peek_victim(cache, model); +//! assert_recency_rank(cache, model.model_recency_rank(k), k); +//! ``` + +use std::collections::HashSet; +use std::hash::Hash; + +use cachekit::traits::{Cache, RecencyTracking, VictimInspectable}; + +use crate::abstract_models::{ModelStep, Op, PolicyModel}; + +/// Optional recency rank for cross-model agreement (LRU family). +pub trait ModelRecencyRank { + /// Recency rank (0 = MRU), or `None` if absent. + fn model_recency_rank(&self, key: &K) -> Option; +} + +/// Assert `peek_victim` matches model when cache is non-empty. +pub fn assert_peek_victim(cache: &C, model: &M) +where + K: Clone + Eq + Hash + std::fmt::Debug, + C: VictimInspectable, + M: PolicyModel, +{ + match model.peek_victim_key() { + Some(expected) => { + let (key, _) = cache.peek_victim().expect("model has victim"); + assert_eq!(*key, expected); + }, + None => assert!(cache.peek_victim().is_none()), + } +} + +/// Assert recency ranks match between cache and LRU model. +pub fn assert_recency_rank(cache: &C, model_rank: Option, key: &K) +where + K: Eq + Hash, + C: RecencyTracking, +{ + assert_eq!(cache.recency_rank(key), model_rank); +} + +/// Assert cache state matches a [`ModelStep`] after one dual-run op. +/// +/// Always checks residency (`probe`), `peek_victim`, and `len <= capacity`. +/// Use [`assert_dual_run_step_no_victim`] when the cache lacks [`VictimInspectable`]. +/// Pass an `extra` closure for policy-specific checks (e.g. LFU frequency, LRU recency). +pub fn assert_dual_run_step( + cache: &C, + model: &M, + step: &ModelStep, + probe: impl Fn(&K) -> bool, + mut extra: F, +) where + K: Clone + From + Eq + Hash + std::fmt::Debug, + C: Cache + VictimInspectable, + M: PolicyModel, + F: FnMut(&C, &M, &ModelStep), +{ + let resident = probe_resident(probe); + assert_eq!(resident, step.resident); + assert!(cache.len() <= cache.capacity()); + assert_peek_victim(cache, model); + extra(cache, model, step); +} + +/// Like [`assert_dual_run_step`], but skips `peek_victim` (policies without [`VictimInspectable`]). +pub fn assert_dual_run_step_no_victim( + cache: &C, + model: &M, + step: &ModelStep, + probe: impl Fn(&K) -> bool, + mut extra: F, +) where + K: Clone + From + Eq + Hash + std::fmt::Debug, + C: Cache, + M: PolicyModel, + F: FnMut(&C, &M, &ModelStep), +{ + let resident = probe_resident(probe); + assert_eq!(resident, step.resident); + assert!(cache.len() <= cache.capacity()); + extra(cache, model, step); +} + +/// Apply a trace and run invariant checks after every step (bounded tier). +/// +/// The `apply` closure handles policy-specific op mapping (including no-op +/// `GetMut`/`Touch`/`EvictOne`). The `check` closure is caller-supplied — e.g. ARC uses +/// `debug_validate_invariants`; S3-FIFO may wrap `check_invariants` in `#[cfg(debug_assertions)]`. +pub fn run_invariant_trace( + cache: &mut C, + ops: &[Op], + mut apply: impl FnMut(&mut C, Op), + check: impl Fn(&C), +) where + K: Clone, + C: Cache, +{ + for op in ops { + apply(cache, op.clone()); + assert!(cache.len() <= cache.capacity()); + check(cache); + } +} + +/// Residency set from probing the `u8` key space (`0..=255`). +/// +/// Canonical helper for dual-run tests; replaces inline `(0..=255u8).filter(…).collect()`. +pub fn probe_resident(contains: impl Fn(&K) -> bool) -> HashSet +where + K: Clone + From + Eq + Hash, +{ + (0..=255u8).map(K::from).filter(|k| contains(k)).collect() +} + +/// Step two [`PolicyModel`] implementations on the same trace and assert agreement. +pub fn assert_models_agree(model_a: &mut M1, model_b: &mut M2, ops: &[Op]) +where + K: Clone + Eq + Hash + std::fmt::Debug, + M1: PolicyModel, + M2: PolicyModel, +{ + for op in ops { + let s1 = model_a.apply(op.clone()); + let s2 = model_b.apply(op.clone()); + assert_eq!(s1.resident, s2.resident, "resident after {op:?}"); + assert_eq!(s1.hit, s2.hit, "hit after {op:?}"); + assert_eq!( + s1.evicted_on_insert, s2.evicted_on_insert, + "evicted_on_insert after {op:?}" + ); + assert_eq!( + model_a.peek_victim_key(), + model_b.peek_victim_key(), + "peek_victim after {op:?}" + ); + } +} + +/// Like [`assert_models_agree`], plus recency rank per resident key (LRU family). +pub fn assert_models_agree_with_recency( + model_a: &mut M1, + model_b: &mut M2, + ops: &[Op], +) where + K: Clone + Eq + Hash + std::fmt::Debug, + M1: PolicyModel + ModelRecencyRank, + M2: PolicyModel + ModelRecencyRank, +{ + for op in ops { + let s1 = model_a.apply(op.clone()); + let s2 = model_b.apply(op.clone()); + assert_eq!(s1.resident, s2.resident, "resident after {op:?}"); + assert_eq!(s1.hit, s2.hit, "hit after {op:?}"); + assert_eq!( + s1.evicted_on_insert, s2.evicted_on_insert, + "evicted_on_insert after {op:?}" + ); + assert_eq!( + model_a.peek_victim_key(), + model_b.peek_victim_key(), + "peek_victim after {op:?}" + ); + assert_models_recency_agree(model_a, model_b, &s1.resident, op); + } +} + +/// Recency rank agreement for models implementing [`ModelRecencyRank`]. +pub fn assert_models_recency_agree( + model_a: &M1, + model_b: &M2, + resident: &HashSet, + op: &Op, +) where + K: Eq + Hash + std::fmt::Debug, + M1: ModelRecencyRank, + M2: ModelRecencyRank, +{ + for k in resident { + assert_eq!( + model_a.model_recency_rank(k), + model_b.model_recency_rank(k), + "recency_rank for {k:?} after {op:?}" + ); + } +} diff --git a/tests/abstract_models/exact/clock.rs b/tests/abstract_models/exact/clock.rs new file mode 100644 index 0000000..10ec823 --- /dev/null +++ b/tests/abstract_models/exact/clock.rs @@ -0,0 +1,102 @@ +//! Clock reference model — mirrors [`ClockRing`](cachekit::ds::ClockRing) semantics. +//! +//! **Tier:** mirror (wraps the real `ClockRing` DS rather than an abstract rule). +//! **Source:** [`docs/testing/specs/policies/mirror/clock.md`](../../../docs/testing/specs/policies/mirror/clock.md) · +//! [matrix.md](../../../docs/testing/specs/matrix.md) +//! **Victim:** first unreferenced slot on the clock hand; referenced entries survive a sweep. +//! **Tests:** `policy_semantics/clock_tests.rs` — residency via [`PolicyModel`]. +//! **Op strategy:** [`op_strategy`](super::super::op_strategy) (includes `EvictOne`). + +use std::collections::HashSet; +use std::hash::Hash; + +use cachekit::ds::ClockRing; + +use crate::abstract_models::{HitMiss, ModelStep, Op, OracleExpectation, PolicyModel}; + +#[derive(Debug)] +pub struct ClockModel +where + K: Clone + Eq + Hash, +{ + ring: ClockRing, +} + +impl ClockModel +where + K: Clone + Eq + Hash, +{ + pub fn new(capacity: usize) -> Self { + Self { + ring: ClockRing::new(capacity), + } + } + + fn collect_resident(&self) -> HashSet { + self.ring.keys().cloned().collect() + } +} + +impl PolicyModel for ClockModel +where + K: Clone + Eq + Hash, + V: Clone + Default, +{ + fn capacity(&self) -> usize { + self.ring.capacity() + } + + fn resident_set(&self) -> HashSet { + self.collect_resident() + } + + fn peek_victim_key(&self) -> Option { + self.ring.peek_victim().map(|(k, _)| k.clone()) + } + + fn apply(&mut self, op: Op) -> ModelStep { + let mut step = ModelStep::new(self.collect_resident()); + + match op { + Op::Insert(key) => { + let before = self.collect_resident(); + let evicted = self.ring.insert(key.clone(), V::default()); + if let Some((k, _)) = evicted { + if !before.contains(&key) { + step.evicted_on_insert = Some(k); + } + } + }, + Op::Get(key) => { + let hit = self.ring.get(&key).is_some(); + step.hit = Some(if hit { + HitMiss::MustHit + } else { + HitMiss::MustMiss + }); + }, + Op::Peek(key) => { + let hit = self.ring.peek(&key).is_some(); + step.hit = Some(if hit { + HitMiss::MustHit + } else { + HitMiss::MustMiss + }); + }, + Op::GetMut(_) | Op::Touch(_) => { + step.hit = Some(HitMiss::MayHitOrMiss); + }, + Op::Remove(key) => { + self.ring.remove(&key); + }, + Op::EvictOne => { + if let Some((victim, _)) = self.ring.pop_victim() { + step.victim = OracleExpectation::Exact(victim); + } + }, + } + + step.resident = self.collect_resident(); + step + } +} diff --git a/tests/abstract_models/exact/fifo.rs b/tests/abstract_models/exact/fifo.rs new file mode 100644 index 0000000..cb436db --- /dev/null +++ b/tests/abstract_models/exact/fifo.rs @@ -0,0 +1,129 @@ +//! FIFO reference model (insertion-order queue with stale skips). +//! +//! **Tier:** exact. +//! **Source:** [`docs/testing/specs/policies/exact/fifo.md`](../../../docs/testing/specs/policies/exact/fifo.md) · +//! [matrix.md](../../../docs/testing/specs/matrix.md) +//! **Tie-break:** stale deque entries (removed keys) are skipped on eviction. +//! **Tests:** `policy_semantics/fifo_tests.rs` — `VictimInspectable`, `EvictingCache`. +//! **Op strategy:** [`op_strategy`](super::super::op_strategy). + +use std::collections::{HashSet, VecDeque}; +use std::hash::Hash; + +use crate::abstract_models::{HitMiss, ModelStep, Op, OracleExpectation, PolicyModel}; + +#[derive(Debug, Clone)] +pub struct FifoModel { + store: HashSet, + insertion_order: VecDeque, + capacity: usize, +} + +impl FifoModel +where + K: Clone + Eq + Hash, +{ + pub fn new(capacity: usize) -> Self { + Self { + store: HashSet::new(), + insertion_order: VecDeque::new(), + capacity, + } + } + + fn collect_resident(&self) -> HashSet { + self.store.clone() + } + + fn evict_oldest(&mut self) -> Option { + while let Some(oldest) = self.insertion_order.pop_front() { + if self.store.contains(&oldest) { + self.store.remove(&oldest); + return Some(oldest); + } + } + None + } + + fn oldest_key(&self) -> Option { + self.insertion_order + .iter() + .find(|k| self.store.contains(*k)) + .cloned() + } +} + +impl PolicyModel for FifoModel +where + K: Clone + Eq + Hash, +{ + fn capacity(&self) -> usize { + self.capacity + } + + fn resident_set(&self) -> HashSet { + self.collect_resident() + } + + fn peek_victim_key(&self) -> Option { + self.oldest_key() + } + + fn apply(&mut self, op: Op) -> ModelStep { + let mut step = ModelStep::new(self.collect_resident()); + + match op { + Op::Insert(key) => { + if self.store.contains(&key) { + return step; + } + if self.capacity == 0 { + return step; + } + if self.store.len() >= self.capacity { + step.evicted_on_insert = self.evict_oldest(); + } + self.store.insert(key.clone()); + self.insertion_order.push_back(key); + }, + Op::Get(key) => { + let hit = self.store.contains(&key); + step.hit = Some(if hit { + HitMiss::MustHit + } else { + HitMiss::MustMiss + }); + }, + Op::Peek(key) => { + let hit = self.store.contains(&key); + step.hit = Some(if hit { + HitMiss::MustHit + } else { + HitMiss::MustMiss + }); + }, + Op::GetMut(key) => { + let hit = self.store.contains(&key); + step.hit = Some(if hit { + HitMiss::MustHit + } else { + HitMiss::MustMiss + }); + }, + Op::Touch(_) => { + step.hit = Some(HitMiss::MayHitOrMiss); + }, + Op::Remove(key) => { + self.store.remove(&key); + }, + Op::EvictOne => { + if let Some(victim) = self.evict_oldest() { + step.victim = OracleExpectation::Exact(victim); + } + }, + } + + step.resident = self.collect_resident(); + step + } +} diff --git a/tests/abstract_models/exact/heap_lfu.rs b/tests/abstract_models/exact/heap_lfu.rs new file mode 100644 index 0000000..9091de4 --- /dev/null +++ b/tests/abstract_models/exact/heap_lfu.rs @@ -0,0 +1,187 @@ +//! Heap-LFU reference model — mirrors `HeapLfuCache` heap eviction semantics. +//! +//! **Tier:** exact. +//! **Source:** [`docs/testing/specs/policies/exact/heap-lfu.md`](../../../docs/testing/specs/policies/exact/heap-lfu.md) · +//! [matrix.md](../../../docs/testing/specs/matrix.md) +//! **Cross-model sibling:** [`reference/heap_lfu.rs`](../reference/heap_lfu.rs) (`NaiveHeapLfuModel`). +//! **Victim:** lowest frequency; `Ord` tie-break on key when frequencies tie. +//! **Peek:** min `(freq, key)` over `freq` map (Ord tie-break; aligns with heap `pop_lfu`). +//! **Tests:** `policy_semantics/heap_lfu_tests.rs` — residency only (heap stale entries). +//! **Op strategy:** [`standard_op_list`](super::super::standard_op_list) (not `mfu_safe`; heap +//! rebuild handles staleness on insert/evict). + +use std::cmp::Reverse; +use std::collections::{BinaryHeap, HashMap, HashSet}; +use std::hash::Hash; + +use crate::abstract_models::{HitMiss, ModelStep, Op, OracleExpectation, PolicyModel}; + +#[derive(Debug)] +pub struct HeapLfuModel +where + K: Clone + Eq + Hash + Ord, +{ + freq: HashMap, + heap: BinaryHeap>, + capacity: usize, +} + +impl HeapLfuModel +where + K: Clone + Eq + Hash + Ord, +{ + const MAX_HEAP_FACTOR: usize = 4; + + pub fn new(capacity: usize) -> Self { + Self { + freq: HashMap::new(), + heap: BinaryHeap::new(), + capacity, + } + } + + fn collect_resident(&self) -> HashSet { + self.freq.keys().cloned().collect() + } + + fn add_to_heap(&mut self, key: &K, frequency: u64) { + self.heap.push(Reverse((frequency, key.clone()))); + self.maybe_rebuild_heap(); + } + + fn maybe_rebuild_heap(&mut self) { + let live = self.freq.len().max(1); + if self.heap.len() <= live.saturating_mul(Self::MAX_HEAP_FACTOR) { + return; + } + self.heap.clear(); + for (key, &f) in &self.freq { + self.heap.push(Reverse((f, key.clone()))); + } + } + + fn pop_lfu(&mut self) -> Option { + let mut stale = 0usize; + while let Some(Reverse((heap_freq, key))) = self.heap.peek().cloned() { + if let Some(¤t) = self.freq.get(&key) { + if heap_freq == current { + let Reverse((_, key)) = self.heap.pop().unwrap(); + return Some(key); + } + } + self.heap.pop(); + stale += 1; + if stale >= self.freq.len().max(1) { + self.maybe_rebuild_heap(); + stale = 0; + } + } + None + } + + fn peek_lfu_key(&self) -> Option { + self.freq + .iter() + .min_by(|(k1, f1), (k2, f2)| f1.cmp(f2).then(k1.cmp(k2))) + .map(|(k, _)| k.clone()) + } + + fn bump_freq(&mut self, key: &K) { + let new_f = { + let f = self.freq.get_mut(key).unwrap(); + *f += 1; + *f + }; + self.add_to_heap(key, new_f); + } +} + +impl PolicyModel for HeapLfuModel +where + K: Clone + Eq + Hash + Ord, +{ + fn capacity(&self) -> usize { + self.capacity + } + + fn resident_set(&self) -> HashSet { + self.collect_resident() + } + + fn peek_victim_key(&self) -> Option { + self.peek_lfu_key() + } + + fn apply(&mut self, op: Op) -> ModelStep { + let mut step = ModelStep::new(self.collect_resident()); + + match op { + Op::Insert(key) => { + if self.freq.contains_key(&key) { + return step; + } + if self.capacity == 0 { + return step; + } + if self.freq.len() >= self.capacity { + if let Some(victim) = self.pop_lfu() { + step.evicted_on_insert = Some(victim.clone()); + self.freq.remove(&victim); + } + } + self.freq.insert(key.clone(), 1); + self.add_to_heap(&key, 1); + }, + Op::Get(key) => { + let hit = self.freq.contains_key(&key); + step.hit = Some(if hit { + HitMiss::MustHit + } else { + HitMiss::MustMiss + }); + if hit { + self.bump_freq(&key); + } + }, + Op::GetMut(key) => { + let hit = self.freq.contains_key(&key); + step.hit = Some(if hit { + HitMiss::MustHit + } else { + HitMiss::MustMiss + }); + if hit { + self.bump_freq(&key); + } + }, + Op::Peek(key) => { + let hit = self.freq.contains_key(&key); + step.hit = Some(if hit { + HitMiss::MustHit + } else { + HitMiss::MustMiss + }); + }, + Op::Touch(key) => { + if self.freq.contains_key(&key) { + self.bump_freq(&key); + step.hit = Some(HitMiss::MustHit); + } else { + step.hit = Some(HitMiss::MustMiss); + } + }, + Op::Remove(key) => { + self.freq.remove(&key); + }, + Op::EvictOne => { + if let Some(victim) = self.pop_lfu() { + step.victim = OracleExpectation::Exact(victim.clone()); + self.freq.remove(&victim); + } + }, + } + + step.resident = self.collect_resident(); + step + } +} diff --git a/tests/abstract_models/exact/lfu.rs b/tests/abstract_models/exact/lfu.rs new file mode 100644 index 0000000..168c3a1 --- /dev/null +++ b/tests/abstract_models/exact/lfu.rs @@ -0,0 +1,130 @@ +//! LFU reference model using [`FrequencyBuckets`](cachekit::ds::FrequencyBuckets). +//! +//! **Tier:** exact. +//! **Source:** [`docs/testing/specs/policies/exact/lfu.md`](../../../docs/testing/specs/policies/exact/lfu.md) · +//! [matrix.md](../../../docs/testing/specs/matrix.md) +//! **Cross-model sibling:** [`reference/lfu.rs`](../reference/lfu.rs) (`NaiveLfuModel`). +//! **Victim:** minimum frequency; FIFO tie-break within the min bucket. +//! **Tests:** `policy_semantics/lfu_tests.rs` — `VictimInspectable`, `FrequencyTracking`, +//! `EvictingCache`. +//! **Op strategy:** [`op_strategy`](super::super::op_strategy). + +use std::collections::HashSet; +use std::hash::Hash; + +use cachekit::ds::FrequencyBuckets; + +use crate::abstract_models::{HitMiss, ModelStep, Op, OracleExpectation, PolicyModel}; + +#[derive(Debug)] +pub struct LfuModel +where + K: Eq + Hash + Clone, +{ + buckets: FrequencyBuckets, + capacity: usize, +} + +impl LfuModel +where + K: Eq + Hash + Clone, +{ + pub fn new(capacity: usize) -> Self { + Self { + buckets: FrequencyBuckets::with_capacity(capacity), + capacity, + } + } + + fn collect_resident(&self) -> HashSet { + self.buckets.iter().map(|(_, m)| m.key.clone()).collect() + } + + pub fn frequency(&self, key: &K) -> Option { + self.buckets.frequency(key) + } +} + +impl PolicyModel for LfuModel +where + K: Eq + Hash + Clone, +{ + fn capacity(&self) -> usize { + self.capacity + } + + fn resident_set(&self) -> HashSet { + self.collect_resident() + } + + fn peek_victim_key(&self) -> Option { + self.buckets.peek_min_key().cloned() + } + + fn apply(&mut self, op: Op) -> ModelStep { + let mut step = ModelStep::new(self.collect_resident()); + + match op { + Op::Insert(key) => { + if self.buckets.contains(&key) { + return step; + } + if self.capacity == 0 { + return step; + } + if self.buckets.len() >= self.capacity { + step.evicted_on_insert = self.buckets.pop_min().map(|(k, _)| k); + } + self.buckets.insert(key); + }, + Op::Get(key) => { + let hit = self.buckets.contains(&key); + step.hit = Some(if hit { + HitMiss::MustHit + } else { + HitMiss::MustMiss + }); + if hit { + self.buckets.touch(&key); + } + }, + Op::Peek(key) => { + let hit = self.buckets.contains(&key); + step.hit = Some(if hit { + HitMiss::MustHit + } else { + HitMiss::MustMiss + }); + }, + Op::GetMut(key) => { + let hit = self.buckets.contains(&key); + step.hit = Some(if hit { + HitMiss::MustHit + } else { + HitMiss::MustMiss + }); + if hit { + self.buckets.touch(&key); + } + }, + Op::Touch(key) => { + if self.buckets.touch(&key).is_some() { + step.hit = Some(HitMiss::MustHit); + } else { + step.hit = Some(HitMiss::MustMiss); + } + }, + Op::Remove(key) => { + self.buckets.remove(&key); + }, + Op::EvictOne => { + if let Some((victim, _)) = self.buckets.pop_min() { + step.victim = OracleExpectation::Exact(victim); + } + }, + } + + step.resident = self.collect_resident(); + step + } +} diff --git a/tests/abstract_models/exact/lifo.rs b/tests/abstract_models/exact/lifo.rs new file mode 100644 index 0000000..48e97f9 --- /dev/null +++ b/tests/abstract_models/exact/lifo.rs @@ -0,0 +1,102 @@ +//! LIFO reference model (victim = newest / top of stack). +//! +//! **Tier:** exact. +//! **Source:** [`docs/testing/specs/policies/exact/lifo.md`](../../../docs/testing/specs/policies/exact/lifo.md) · +//! [matrix.md](../../../docs/testing/specs/matrix.md) +//! **Cross-model sibling:** [`reference/lifo.rs`](../reference/lifo.rs) (`NaiveLifoModel`). +//! **Tests:** `policy_semantics/lifo_tests.rs` — `VictimInspectable`, `EvictingCache`. +//! **Op strategy:** [`op_strategy`](super::super::op_strategy). + +use std::collections::{HashSet, VecDeque}; +use std::hash::Hash; + +use crate::abstract_models::{HitMiss, ModelStep, Op, OracleExpectation, PolicyModel}; + +#[derive(Debug, Clone)] +pub struct LifoModel { + stack: VecDeque, + capacity: usize, +} + +impl LifoModel +where + K: Clone + Eq + Hash, +{ + pub fn new(capacity: usize) -> Self { + Self { + stack: VecDeque::new(), + capacity, + } + } + + fn contains_key(&self, key: &K) -> bool { + self.stack.iter().any(|k| k == key) + } + + fn collect_resident(&self) -> HashSet { + self.stack.iter().cloned().collect() + } + + fn newest_key(&self) -> Option { + self.stack.back().cloned() + } +} + +impl PolicyModel for LifoModel +where + K: Clone + Eq + Hash, +{ + fn capacity(&self) -> usize { + self.capacity + } + + fn resident_set(&self) -> HashSet { + self.collect_resident() + } + + fn peek_victim_key(&self) -> Option { + self.newest_key() + } + + fn apply(&mut self, op: Op) -> ModelStep { + let mut step = ModelStep::new(self.collect_resident()); + + match op { + Op::Insert(key) => { + if self.contains_key(&key) { + // update — stack order unchanged + } else if self.capacity == 0 { + return step; + } else { + if self.stack.len() >= self.capacity { + step.evicted_on_insert = self.stack.pop_back(); + } + self.stack.push_back(key); + } + }, + Op::Get(key) | Op::Peek(key) | Op::GetMut(key) => { + let hit = self.contains_key(&key); + step.hit = Some(if hit { + HitMiss::MustHit + } else { + HitMiss::MustMiss + }); + }, + Op::Touch(_) => { + step.hit = Some(HitMiss::MayHitOrMiss); + }, + Op::Remove(key) => { + self.stack.retain(|k| k != &key); + }, + Op::EvictOne => { + if let Some(victim) = self.newest_key() { + step.victim = OracleExpectation::Exact(victim.clone()); + self.stack.pop_back(); + } + }, + } + + step.resident = self.collect_resident(); + step + } +} diff --git a/tests/abstract_models/exact/lru.rs b/tests/abstract_models/exact/lru.rs new file mode 100644 index 0000000..5943c41 --- /dev/null +++ b/tests/abstract_models/exact/lru.rs @@ -0,0 +1,172 @@ +//! LRU occupancy model (MRU at front, LRU at back). +//! +//! **Tier:** exact. +//! **Source:** [`docs/testing/specs/policies/exact/lru.md`](../../../docs/testing/specs/policies/exact/lru.md) · +//! [fast-lru.md](../../../docs/testing/specs/policies/exact/fast-lru.md) · +//! [matrix.md](../../../docs/testing/specs/matrix.md) +//! **Recency:** rank 0 = MRU; used by `assert_recency_rank` in LRU and Fast-LRU tests. +//! **Tests:** `policy_semantics/lru_tests.rs`, `fast_lru_tests.rs`; also composed in +//! `ttl_integration_test.rs`. +//! **Op strategy:** [`op_strategy`](super::super::op_strategy) (LRU); +//! [`op_strategy_with_get_mut`](super::super::op_strategy_with_get_mut) (Fast-LRU). + +use std::collections::{HashSet, VecDeque}; +use std::hash::Hash; + +use crate::abstract_models::driver::ModelRecencyRank; +use crate::abstract_models::{HitMiss, ModelStep, Op, OracleExpectation, PolicyModel}; + +/// MRU-first deque matching `FastLru` head/tail semantics. +#[derive(Debug, Clone)] +pub struct LruOccupancyModel { + order: VecDeque, + capacity: usize, +} + +impl LruOccupancyModel +where + K: Clone + Eq + Hash, +{ + pub fn new(capacity: usize) -> Self { + Self { + order: VecDeque::new(), + capacity, + } + } + + pub fn touch_key(&mut self, key: K) { + self.order.retain(|k| k != &key); + self.order.push_front(key); + } + + fn contains_key(&self, key: &K) -> bool { + self.order.iter().any(|k| k == key) + } + + fn collect_resident(&self) -> HashSet { + self.order.iter().cloned().collect() + } + + fn lru_key(&self) -> Option { + self.order.back().cloned() + } + + fn recency_rank(&self, key: &K) -> Option { + self.order.iter().position(|k| k == key) + } + + fn insert_new(&mut self, key: K) -> Option { + if self.capacity == 0 { + return None; + } + let mut evicted = None; + while self.order.len() >= self.capacity { + evicted = self.order.pop_back(); + } + self.order.push_front(key); + evicted + } +} + +impl PolicyModel for LruOccupancyModel +where + K: Clone + Eq + Hash, +{ + fn capacity(&self) -> usize { + self.capacity + } + + fn resident_set(&self) -> HashSet { + self.collect_resident() + } + + fn peek_victim_key(&self) -> Option { + self.lru_key() + } + + fn apply(&mut self, op: Op) -> ModelStep { + let mut step = ModelStep::new(self.collect_resident()); + + match op { + Op::Insert(key) => { + if self.contains_key(&key) { + self.touch_key(key); + } else { + step.evicted_on_insert = self.insert_new(key); + } + step.victim = OracleExpectation::None; + }, + Op::Get(key) => { + let hit = self.contains_key(&key); + step.hit = Some(if hit { + HitMiss::MustHit + } else { + HitMiss::MustMiss + }); + if hit { + self.touch_key(key); + } + }, + Op::Peek(key) => { + let hit = self.contains_key(&key); + step.hit = Some(if hit { + HitMiss::MustHit + } else { + HitMiss::MustMiss + }); + }, + Op::GetMut(key) => { + let hit = self.contains_key(&key); + step.hit = Some(if hit { + HitMiss::MustHit + } else { + HitMiss::MustMiss + }); + if hit { + self.touch_key(key); + } + }, + Op::Touch(key) => { + if self.contains_key(&key) { + self.touch_key(key); + step.hit = Some(HitMiss::MustHit); + } else { + step.hit = Some(HitMiss::MustMiss); + } + }, + Op::Remove(key) => { + if self.contains_key(&key) { + self.order.retain(|k| k != &key); + } + }, + Op::EvictOne => { + if let Some(victim) = self.lru_key() { + step.victim = OracleExpectation::Exact(victim.clone()); + self.order.pop_back(); + } + }, + } + + step.resident = self.collect_resident(); + step + } +} + +impl ModelRecencyRank for LruOccupancyModel +where + K: Clone + Eq + Hash, +{ + fn model_recency_rank(&self, key: &K) -> Option { + self.recency_rank(key) + } +} + +impl LruOccupancyModel +where + K: Clone + Eq + Hash, +{ + /// Recency rank for assertions (0 = MRU). + pub fn model_recency_rank(&self, key: &K) -> Option { + self.recency_rank(key) + } +} diff --git a/tests/abstract_models/exact/lru_k.rs b/tests/abstract_models/exact/lru_k.rs new file mode 100644 index 0000000..85114e9 --- /dev/null +++ b/tests/abstract_models/exact/lru_k.rs @@ -0,0 +1,207 @@ +//! LRU-K reference model (step-counter time, cold/hot segments). +//! +//! **Tier:** exact. +//! **Source:** [`docs/testing/specs/policies/exact/lru-k.md`](../../../docs/testing/specs/policies/exact/lru-k.md) · +//! [matrix.md](../../../docs/testing/specs/matrix.md) +//! **Cross-model sibling:** [`reference/lru_k.rs`](../reference/lru_k.rs) (`NaiveLruKModel`). +//! **Victim:** LRU in cold segment; promote to hot after K-th access (step-counter history). +//! **Tests:** `policy_semantics/lru_k_tests.rs` — `HistoryTracking`, `EvictingCache`. +//! **Op strategy:** [`op_strategy`](super::super::op_strategy). + +use std::collections::{HashMap, HashSet, VecDeque}; +use std::hash::Hash; + +use crate::abstract_models::{HitMiss, ModelStep, Op, OracleExpectation, PolicyModel}; + +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +enum Segment { + Cold, + Hot, +} + +#[derive(Debug)] +pub struct LruKModel +where + K: Clone + Eq + Hash, +{ + tick: u64, + k: usize, + cold: VecDeque, + hot: VecDeque, + segment: HashMap, + history: HashMap>, + capacity: usize, +} + +impl LruKModel +where + K: Clone + Eq + Hash, +{ + pub fn new(capacity: usize, k: usize) -> Self { + Self { + tick: 0, + k, + cold: VecDeque::new(), + hot: VecDeque::new(), + segment: HashMap::new(), + history: HashMap::new(), + capacity, + } + } + + fn collect_resident(&self) -> HashSet { + self.segment.keys().cloned().collect() + } + + fn record_access(&mut self, key: &K) { + self.tick = self.tick.saturating_add(1); + let h = self.history.entry(key.clone()).or_default(); + h.push_back(self.tick); + while h.len() > self.k { + h.pop_front(); + } + } + + fn detach(&mut self, key: &K) { + match self.segment.get(key) { + Some(Segment::Cold) => self.cold.retain(|k| k != key), + Some(Segment::Hot) => self.hot.retain(|k| k != key), + None => {}, + } + } + + fn promote_if_needed(&mut self, key: K) { + let count = self.history.get(&key).map(|h| h.len()).unwrap_or(0); + if count >= self.k { + self.detach(&key); + self.hot.push_front(key.clone()); + self.segment.insert(key, Segment::Hot); + } + } + + fn move_hot_front(&mut self, key: &K) { + if matches!(self.segment.get(key), Some(Segment::Hot)) { + self.detach(key); + self.hot.push_front(key.clone()); + } + } + + fn evict_inner(&mut self) -> Option { + if let Some(k) = self.cold.pop_back() { + self.segment.remove(&k); + self.history.remove(&k); + return Some(k); + } + if let Some(k) = self.hot.pop_back() { + self.segment.remove(&k); + self.history.remove(&k); + return Some(k); + } + None + } + + fn evict_if_needed(&mut self) -> Option { + let mut evicted = None; + while self.segment.len() >= self.capacity { + evicted = self.evict_inner(); + } + evicted + } + + pub fn access_count(&self, key: &K) -> Option { + self.history.get(key).map(|h| h.len()) + } +} + +impl PolicyModel for LruKModel +where + K: Clone + Eq + Hash, +{ + fn capacity(&self) -> usize { + self.capacity + } + + fn resident_set(&self) -> HashSet { + self.collect_resident() + } + + fn peek_victim_key(&self) -> Option { + self.cold.back().or_else(|| self.hot.back()).cloned() + } + + fn apply(&mut self, op: Op) -> ModelStep { + let mut step = ModelStep::new(self.collect_resident()); + + match op { + Op::Insert(key) => { + if self.segment.contains_key(&key) { + self.record_access(&key); + self.promote_if_needed(key.clone()); + self.move_hot_front(&key); + return step; + } + if self.capacity == 0 { + return step; + } + step.evicted_on_insert = self.evict_if_needed(); + self.tick = self.tick.saturating_add(1); + self.history + .entry(key.clone()) + .or_default() + .push_back(self.tick); + self.cold.push_front(key.clone()); + self.segment.insert(key, Segment::Cold); + }, + Op::Get(key) => { + let hit = self.segment.contains_key(&key); + step.hit = Some(if hit { + HitMiss::MustHit + } else { + HitMiss::MustMiss + }); + if hit { + self.record_access(&key); + self.promote_if_needed(key.clone()); + self.move_hot_front(&key); + } + }, + Op::Peek(key) => { + let hit = self.segment.contains_key(&key); + step.hit = Some(if hit { + HitMiss::MustHit + } else { + HitMiss::MustMiss + }); + }, + Op::GetMut(key) => { + let hit = self.segment.contains_key(&key); + step.hit = Some(if hit { + HitMiss::MustHit + } else { + HitMiss::MustMiss + }); + if hit { + self.record_access(&key); + self.promote_if_needed(key.clone()); + self.move_hot_front(&key); + } + }, + Op::Touch(_) => { + step.hit = Some(HitMiss::MayHitOrMiss); + }, + Op::Remove(key) => { + self.detach(&key); + self.segment.remove(&key); + self.history.remove(&key); + }, + Op::EvictOne => { + if let Some(victim) = self.evict_inner() { + step.victim = OracleExpectation::Exact(victim); + } + }, + } + + step.resident = self.collect_resident(); + step + } +} diff --git a/tests/abstract_models/exact/mfu.rs b/tests/abstract_models/exact/mfu.rs new file mode 100644 index 0000000..a942fdc --- /dev/null +++ b/tests/abstract_models/exact/mfu.rs @@ -0,0 +1,221 @@ +//! MFU reference model — mirrors `MfuCore` heap eviction semantics. +//! +//! **Tier:** exact. +//! **Source:** [`docs/testing/specs/policies/exact/mfu.md`](../../../docs/testing/specs/policies/exact/mfu.md) · +//! [matrix.md](../../../docs/testing/specs/matrix.md) +//! **Cross-model sibling:** [`reference/mfu.rs`](../reference/mfu.rs) (`NaiveMfuModel`). +//! **Victim:** highest frequency; sequence-number tie-break (newest heap entry evicted first). +//! **Peek:** max valid `HeapEntry` in heap (aligns with `pop_mfu` tie-break). +//! **Tests:** `policy_semantics/mfu_tests.rs` — residency only. +//! **Op strategy:** [`op_strategy_mfu_safe`](super::super::op_strategy_mfu_safe) — skips +//! `Remove`/`EvictOne` because stale heap entries break `debug_validate_invariants`. + +use std::cmp::Ordering; +use std::collections::{BinaryHeap, HashSet}; +use std::hash::Hash; + +use rustc_hash::FxHashMap; + +use crate::abstract_models::{HitMiss, ModelStep, Op, OracleExpectation, PolicyModel}; + +#[derive(Clone)] +struct HeapEntry { + freq: u64, + seq: u64, + key: K, +} + +impl PartialEq for HeapEntry { + fn eq(&self, other: &Self) -> bool { + self.freq == other.freq && self.seq == other.seq + } +} + +impl Eq for HeapEntry {} + +impl PartialOrd for HeapEntry { + fn partial_cmp(&self, other: &Self) -> Option { + Some(self.cmp(other)) + } +} + +impl Ord for HeapEntry { + fn cmp(&self, other: &Self) -> Ordering { + self.freq + .cmp(&other.freq) + .then_with(|| self.seq.cmp(&other.seq)) + } +} + +pub struct MfuModel +where + K: Eq + Hash + Clone, +{ + freq: FxHashMap, + heap: BinaryHeap>, + capacity: usize, + seq: u64, +} + +impl MfuModel +where + K: Eq + Hash + Clone, +{ + const HEAP_REBUILD_FACTOR: usize = 3; + + pub fn new(capacity: usize) -> Self { + Self { + freq: FxHashMap::default(), + heap: BinaryHeap::new(), + capacity, + seq: 0, + } + } + + fn collect_resident(&self) -> HashSet { + self.freq.keys().cloned().collect() + } + + fn push_heap(&mut self, key: K, frequency: u64) { + self.seq += 1; + self.heap.push(HeapEntry { + freq: frequency, + seq: self.seq, + key, + }); + if self.heap.len() > self.freq.len() * Self::HEAP_REBUILD_FACTOR { + self.rebuild_heap(); + } + } + + fn rebuild_heap(&mut self) { + let entries: Vec<_> = self.freq.iter().map(|(k, &f)| (k.clone(), f)).collect(); + self.heap.clear(); + for (key, f) in entries { + self.push_heap(key, f); + } + } + + fn pop_mfu(&mut self) -> Option { + while let Some(entry) = self.heap.pop() { + if let Some(¤t) = self.freq.get(&entry.key) { + if current == entry.freq { + self.freq.remove(&entry.key); + return Some(entry.key); + } + } + } + if !self.freq.is_empty() { + self.rebuild_heap(); + if let Some(entry) = self.heap.pop() { + self.freq.remove(&entry.key); + return Some(entry.key); + } + } + None + } + + fn peek_mfu_key(&self) -> Option { + self.heap + .iter() + .filter(|entry| self.freq.get(&entry.key) == Some(&entry.freq)) + .max() + .map(|entry| entry.key.clone()) + } + + fn bump_freq(&mut self, key: K) { + let new_f = { + let f = self.freq.get_mut(&key).unwrap(); + *f += 1; + *f + }; + self.push_heap(key, new_f); + } +} + +impl PolicyModel for MfuModel +where + K: Eq + Hash + Clone, +{ + fn capacity(&self) -> usize { + self.capacity + } + + fn resident_set(&self) -> HashSet { + self.collect_resident() + } + + fn peek_victim_key(&self) -> Option { + self.peek_mfu_key() + } + + fn apply(&mut self, op: Op) -> ModelStep { + let mut step = ModelStep::new(self.collect_resident()); + + match op { + Op::Insert(key) => { + if self.freq.contains_key(&key) { + self.bump_freq(key); + } else if self.capacity == 0 { + return step; + } else { + while self.freq.len() >= self.capacity { + if let Some(victim) = self.pop_mfu() { + if step.evicted_on_insert.is_none() { + step.evicted_on_insert = Some(victim); + } + } else { + break; + } + } + self.freq.insert(key.clone(), 1); + self.push_heap(key, 1); + } + }, + Op::Get(key) => { + let hit = self.freq.contains_key(&key); + step.hit = Some(if hit { + HitMiss::MustHit + } else { + HitMiss::MustMiss + }); + if hit { + self.bump_freq(key); + } + }, + Op::GetMut(key) => { + let hit = self.freq.contains_key(&key); + step.hit = Some(if hit { + HitMiss::MustHit + } else { + HitMiss::MustMiss + }); + if hit { + self.bump_freq(key); + } + }, + Op::Peek(key) => { + let hit = self.freq.contains_key(&key); + step.hit = Some(if hit { + HitMiss::MustHit + } else { + HitMiss::MustMiss + }); + }, + Op::Touch(_) => { + step.hit = Some(HitMiss::MayHitOrMiss); + }, + Op::Remove(key) => { + self.freq.remove(&key); + }, + Op::EvictOne => { + if let Some(victim) = self.pop_mfu() { + step.victim = OracleExpectation::Exact(victim); + } + }, + } + + step.resident = self.collect_resident(); + step + } +} diff --git a/tests/abstract_models/exact/mod.rs b/tests/abstract_models/exact/mod.rs new file mode 100644 index 0000000..94ec9f4 --- /dev/null +++ b/tests/abstract_models/exact/mod.rs @@ -0,0 +1,37 @@ +//! Exact and mirror reference models. +//! +//! **Exact** models encode the policy rule directly (e.g. LRU deque, FIFO insertion order). +//! Victims and residency must match the implementation on every trace step. +//! +//! **Mirror** models transcribe internal state from the real data structure (`ClockRing`, +//! `TwoQCore`, `SlruCore`) rather than a simplified abstract rule. Use when behavior is +//! defined by the DS layout. +//! +//! See the [policy matrix](../../../docs/testing/specs/matrix.md) for per-policy model types. +//! +//! Each submodule is gated by the matching `policy-*` feature (plus `ttl` for `lru`). + +#[cfg(feature = "policy-clock")] +pub mod clock; +#[cfg(feature = "policy-fifo")] +pub mod fifo; +#[cfg(feature = "policy-heap-lfu")] +pub mod heap_lfu; +#[cfg(feature = "policy-lfu")] +pub mod lfu; +#[cfg(feature = "policy-lifo")] +pub mod lifo; +#[cfg(any(feature = "policy-lru", feature = "policy-fast-lru", feature = "ttl"))] +pub mod lru; +#[cfg(feature = "policy-lru-k")] +pub mod lru_k; +#[cfg(feature = "policy-mfu")] +pub mod mfu; +#[cfg(feature = "policy-mru")] +pub mod mru; +#[cfg(feature = "policy-nru")] +pub mod nru; +#[cfg(feature = "policy-slru")] +pub mod slru; +#[cfg(feature = "policy-two-q")] +pub mod two_q; diff --git a/tests/abstract_models/exact/mru.rs b/tests/abstract_models/exact/mru.rs new file mode 100644 index 0000000..13719d6 --- /dev/null +++ b/tests/abstract_models/exact/mru.rs @@ -0,0 +1,128 @@ +//! MRU reference model (victim = most recently used / head). +//! +//! **Tier:** exact. +//! **Source:** [`docs/testing/specs/policies/exact/mru.md`](../../../docs/testing/specs/policies/exact/mru.md) · +//! [matrix.md](../../../docs/testing/specs/matrix.md) +//! **Cross-model sibling:** [`reference/mru.rs`](../reference/mru.rs) (`NaiveMruModel`). +//! **Tests:** `policy_semantics/mru_tests.rs` — `EvictingCache` (no `VictimInspectable`). +//! **Op strategy:** [`op_strategy`](super::super::op_strategy). + +use std::collections::{HashSet, VecDeque}; +use std::hash::Hash; + +use crate::abstract_models::{HitMiss, ModelStep, Op, OracleExpectation, PolicyModel}; + +/// MRU list: head = MRU (eviction victim on insert). +#[derive(Debug, Clone)] +pub struct MruModel { + order: VecDeque, + capacity: usize, +} + +impl MruModel +where + K: Clone + Eq + Hash, +{ + pub fn new(capacity: usize) -> Self { + Self { + order: VecDeque::new(), + capacity, + } + } + + fn contains_key(&self, key: &K) -> bool { + self.order.iter().any(|k| k == key) + } + + fn collect_resident(&self) -> HashSet { + self.order.iter().cloned().collect() + } + + fn mru_key(&self) -> Option { + self.order.front().cloned() + } + + fn promote(&mut self, key: K) { + self.order.retain(|k| k != &key); + self.order.push_front(key); + } +} + +impl PolicyModel for MruModel +where + K: Clone + Eq + Hash, +{ + fn capacity(&self) -> usize { + self.capacity + } + + fn resident_set(&self) -> HashSet { + self.collect_resident() + } + + fn peek_victim_key(&self) -> Option { + self.mru_key() + } + + fn apply(&mut self, op: Op) -> ModelStep { + let mut step = ModelStep::new(self.collect_resident()); + + match op { + Op::Insert(key) => { + if self.contains_key(&key) || self.capacity == 0 { + return step; + } else { + while self.order.len() >= self.capacity { + step.evicted_on_insert = self.order.pop_front(); + } + self.order.push_front(key); + } + }, + Op::Get(key) => { + let hit = self.contains_key(&key); + step.hit = Some(if hit { + HitMiss::MustHit + } else { + HitMiss::MustMiss + }); + if hit { + self.promote(key); + } + }, + Op::Peek(key) => { + let hit = self.contains_key(&key); + step.hit = Some(if hit { + HitMiss::MustHit + } else { + HitMiss::MustMiss + }); + }, + Op::GetMut(key) => { + let hit = self.contains_key(&key); + step.hit = Some(if hit { + HitMiss::MustHit + } else { + HitMiss::MustMiss + }); + if hit { + self.promote(key); + } + }, + Op::Touch(_) => { + step.hit = Some(HitMiss::MayHitOrMiss); + }, + Op::Remove(key) => { + self.order.retain(|k| k != &key); + }, + Op::EvictOne => { + if let Some(victim) = self.mru_key() { + step.victim = OracleExpectation::Exact(victim.clone()); + self.order.pop_front(); + } + }, + } + + step.resident = self.collect_resident(); + step + } +} diff --git a/tests/abstract_models/exact/nru.rs b/tests/abstract_models/exact/nru.rs new file mode 100644 index 0000000..004df4a --- /dev/null +++ b/tests/abstract_models/exact/nru.rs @@ -0,0 +1,160 @@ +//! NRU reference model (swap-remove eviction, new inserts start unreferenced). +//! +//! **Tier:** mirror. +//! **Source:** [`docs/testing/specs/policies/mirror/nru.md`](../../../docs/testing/specs/policies/mirror/nru.md) · +//! [matrix.md](../../../docs/testing/specs/matrix.md) +//! **Victim:** first unreferenced key in insertion order; swap-remove on eviction. +//! **Tests:** `policy_semantics/nru_tests.rs` — residency only (no `EvictingCache`). +//! **Op strategy:** [`short_op_list_no_evict`](super::super::short_op_list_no_evict) — O(n) +//! eviction scans; no explicit `EvictOne`. + +use std::collections::{HashMap, HashSet}; +use std::hash::Hash; + +use crate::abstract_models::{HitMiss, ModelStep, Op, OracleExpectation, PolicyModel}; + +#[derive(Debug)] +pub struct NruModel +where + K: Clone + Eq + Hash, +{ + keys: Vec, + referenced: HashMap, + capacity: usize, +} + +impl NruModel +where + K: Clone + Eq + Hash, +{ + pub fn new(capacity: usize) -> Self { + Self { + keys: Vec::new(), + referenced: HashMap::new(), + capacity, + } + } + + fn collect_resident(&self) -> HashSet { + self.keys.iter().cloned().collect() + } + + fn swap_remove_at(&mut self, idx: usize) -> K { + let victim = self.keys.swap_remove(idx); + self.referenced.remove(&victim); + victim + } + + fn evict_one_inner(&mut self) -> Option { + if self.keys.is_empty() { + return None; + } + + for idx in 0..self.keys.len() { + let key = &self.keys[idx]; + if !self.referenced.get(key).copied().unwrap_or(false) { + return Some(self.swap_remove_at(idx)); + } + } + + for key in &self.keys { + self.referenced.insert(key.clone(), false); + } + + if self.keys.is_empty() { + return None; + } + Some(self.swap_remove_at(0)) + } +} + +impl PolicyModel for NruModel +where + K: Clone + Eq + Hash, +{ + fn capacity(&self) -> usize { + self.capacity + } + + fn resident_set(&self) -> HashSet { + self.collect_resident() + } + + fn peek_victim_key(&self) -> Option { + for key in &self.keys { + if !self.referenced.get(key).copied().unwrap_or(false) { + return Some(key.clone()); + } + } + self.keys.first().cloned() + } + + fn apply(&mut self, op: Op) -> ModelStep { + let mut step = ModelStep::new(self.collect_resident()); + + match op { + Op::Insert(key) => { + if let std::collections::hash_map::Entry::Occupied(mut e) = + self.referenced.entry(key.clone()) + { + e.insert(true); + return step; + } + if self.capacity == 0 { + return step; + } + if self.keys.len() >= self.capacity { + step.evicted_on_insert = self.evict_one_inner(); + } + self.keys.push(key.clone()); + self.referenced.insert(key, false); + }, + Op::Get(key) => { + let hit = self.referenced.contains_key(&key); + step.hit = Some(if hit { + HitMiss::MustHit + } else { + HitMiss::MustMiss + }); + if hit { + self.referenced.insert(key, true); + } + }, + Op::Peek(key) => { + let hit = self.referenced.contains_key(&key); + step.hit = Some(if hit { + HitMiss::MustHit + } else { + HitMiss::MustMiss + }); + }, + Op::GetMut(key) => { + let hit = self.referenced.contains_key(&key); + step.hit = Some(if hit { + HitMiss::MustHit + } else { + HitMiss::MustMiss + }); + if hit { + self.referenced.insert(key, true); + } + }, + Op::Touch(_) => { + step.hit = Some(HitMiss::MayHitOrMiss); + }, + Op::Remove(key) => { + if let Some(pos) = self.keys.iter().position(|k| k == &key) { + self.swap_remove_at(pos); + } + }, + Op::EvictOne => { + if let Some(victim) = self.evict_one_inner() { + step.victim = OracleExpectation::Exact(victim); + } + }, + } + + step.resident = self.collect_resident(); + step + } +} diff --git a/tests/abstract_models/exact/slru.rs b/tests/abstract_models/exact/slru.rs new file mode 100644 index 0000000..747c5ed --- /dev/null +++ b/tests/abstract_models/exact/slru.rs @@ -0,0 +1,183 @@ +//! SLRU reference model — mirrors `SlruCore` segment caps and LRU ordering. +//! +//! **Tier:** mirror. +//! **Source:** [`docs/testing/specs/policies/mirror/slru.md`](../../../docs/testing/specs/policies/mirror/slru.md) · +//! [matrix.md](../../../docs/testing/specs/matrix.md) +//! **Victim:** LRU in probationary segment; promote to protected on re-access. +//! **Tests:** `policy_semantics/slru_tests.rs` — residency only (no `EvictingCache`). +//! **Op strategy:** [`standard_op_list_no_evict`](super::super::standard_op_list_no_evict). + +use std::collections::{HashMap, HashSet, VecDeque}; +use std::hash::Hash; + +use crate::abstract_models::{HitMiss, ModelStep, Op, OracleExpectation, PolicyModel}; + +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +enum Segment { + Probationary, + Protected, +} + +#[derive(Debug)] +pub struct SlruModel +where + K: Clone + Eq + Hash, +{ + /// Head = MRU, tail = LRU. + probationary: VecDeque, + protected: VecDeque, + segments: HashMap, + capacity: usize, + probationary_cap: usize, +} + +impl SlruModel +where + K: Clone + Eq + Hash, +{ + pub fn new(capacity: usize, probationary_frac: f64) -> Self { + let probationary_cap = (capacity as f64 * probationary_frac) as usize; + Self { + probationary: VecDeque::new(), + protected: VecDeque::new(), + segments: HashMap::new(), + capacity, + probationary_cap, + } + } + + fn len(&self) -> usize { + self.segments.len() + } + + fn collect_resident(&self) -> HashSet { + self.segments.keys().cloned().collect() + } + + fn detach(&mut self, key: &K) { + if let Some(seg) = self.segments.get(key).copied() { + match seg { + Segment::Probationary => self.probationary.retain(|k| k != key), + Segment::Protected => self.protected.retain(|k| k != key), + } + } + } + + fn promote(&mut self, key: K) { + self.detach(&key); + self.protected.push_front(key.clone()); + self.segments.insert(key, Segment::Protected); + } + + fn evict_inner(&mut self) -> Option { + if self.probationary.len() > self.probationary_cap { + if let Some(k) = self.probationary.pop_back() { + self.segments.remove(&k); + return Some(k); + } + } + if let Some(k) = self.protected.pop_back() { + self.segments.remove(&k); + return Some(k); + } + if let Some(k) = self.probationary.pop_back() { + self.segments.remove(&k); + return Some(k); + } + None + } + + fn evict_if_needed(&mut self) -> Option { + let mut last = None; + while self.len() >= self.capacity { + last = self.evict_inner(); + } + last + } +} + +impl PolicyModel for SlruModel +where + K: Clone + Eq + Hash, +{ + fn capacity(&self) -> usize { + self.capacity + } + + fn resident_set(&self) -> HashSet { + self.collect_resident() + } + + fn peek_victim_key(&self) -> Option { + if self.probationary.len() > self.probationary_cap { + return self.probationary.back().cloned(); + } + self.protected + .back() + .or_else(|| self.probationary.back()) + .cloned() + } + + fn apply(&mut self, op: Op) -> ModelStep { + let mut step = ModelStep::new(self.collect_resident()); + + match op { + Op::Insert(key) => { + if self.segments.contains_key(&key) { + return step; + } + if self.capacity == 0 { + return step; + } + step.evicted_on_insert = self.evict_if_needed(); + self.probationary.push_front(key.clone()); + self.segments.insert(key, Segment::Probationary); + }, + Op::Get(key) => { + let hit = self.segments.contains_key(&key); + step.hit = Some(if hit { + HitMiss::MustHit + } else { + HitMiss::MustMiss + }); + if hit { + self.promote(key); + } + }, + Op::Peek(key) => { + let hit = self.segments.contains_key(&key); + step.hit = Some(if hit { + HitMiss::MustHit + } else { + HitMiss::MustMiss + }); + }, + Op::GetMut(key) => { + let hit = self.segments.contains_key(&key); + step.hit = Some(if hit { + HitMiss::MustHit + } else { + HitMiss::MustMiss + }); + if hit { + self.promote(key); + } + }, + Op::Touch(_) => { + step.hit = Some(HitMiss::MayHitOrMiss); + }, + Op::Remove(key) => { + self.detach(&key); + self.segments.remove(&key); + }, + Op::EvictOne => { + if let Some(victim) = self.evict_inner() { + step.victim = OracleExpectation::Exact(victim); + } + }, + } + + step.resident = self.collect_resident(); + step + } +} diff --git a/tests/abstract_models/exact/two_q.rs b/tests/abstract_models/exact/two_q.rs new file mode 100644 index 0000000..bcf0aaf --- /dev/null +++ b/tests/abstract_models/exact/two_q.rs @@ -0,0 +1,184 @@ +//! 2Q reference model — mirrors `TwoQCore` queue caps and eviction order. +//! +//! **Tier:** mirror. +//! **Source:** [`docs/testing/specs/policies/mirror/two-q.md`](../../../docs/testing/specs/policies/mirror/two-q.md) · +//! [matrix.md](../../../docs/testing/specs/matrix.md) +//! **Queues:** probation (A1) and protected (Am); victim is LRU in probation. +//! **Tests:** `policy_semantics/two_q_tests.rs` — residency only (no `EvictingCache`). +//! **Op strategy:** [`standard_op_list_no_evict`](super::super::standard_op_list_no_evict). + +use std::collections::{HashMap, HashSet, VecDeque}; +use std::hash::Hash; + +use crate::abstract_models::{HitMiss, ModelStep, Op, OracleExpectation, PolicyModel}; + +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +enum Queue { + Probation, + Protected, +} + +#[derive(Debug)] +pub struct TwoQModel +where + K: Clone + Eq + Hash, +{ + /// Head = newest (insert here), tail = oldest (evict here). + probation: VecDeque, + /// Head = MRU, tail = LRU (evict here). + protected: VecDeque, + queues: HashMap, + protected_cap: usize, + probation_cap: usize, +} + +impl TwoQModel +where + K: Clone + Eq + Hash, +{ + pub fn new(protected_cap: usize, a1_frac: f64) -> Self { + let probation_cap = (protected_cap as f64 * a1_frac) as usize; + Self { + probation: VecDeque::new(), + protected: VecDeque::new(), + queues: HashMap::new(), + protected_cap, + probation_cap, + } + } + + fn len(&self) -> usize { + self.queues.len() + } + + fn collect_resident(&self) -> HashSet { + self.queues.keys().cloned().collect() + } + + fn detach(&mut self, key: &K) { + if let Some(q) = self.queues.get(key).copied() { + match q { + Queue::Probation => self.probation.retain(|k| k != key), + Queue::Protected => self.protected.retain(|k| k != key), + } + } + } + + fn promote_to_protected(&mut self, key: K) { + self.detach(&key); + self.protected.push_front(key.clone()); + self.queues.insert(key, Queue::Protected); + } + + fn evict_one_inner(&mut self) -> Option { + if self.probation.len() > self.probation_cap { + if let Some(k) = self.probation.pop_back() { + self.queues.remove(&k); + return Some(k); + } + } + if let Some(k) = self.protected.pop_back() { + self.queues.remove(&k); + return Some(k); + } + if let Some(k) = self.probation.pop_back() { + self.queues.remove(&k); + return Some(k); + } + None + } + + fn evict_if_needed(&mut self) -> Option { + let mut last = None; + while self.len() >= self.protected_cap { + last = self.evict_one_inner(); + } + last + } +} + +impl PolicyModel for TwoQModel +where + K: Clone + Eq + Hash, +{ + fn capacity(&self) -> usize { + self.protected_cap + } + + fn resident_set(&self) -> HashSet { + self.collect_resident() + } + + fn peek_victim_key(&self) -> Option { + if self.probation.len() > self.probation_cap { + return self.probation.back().cloned(); + } + self.protected + .back() + .or_else(|| self.probation.back()) + .cloned() + } + + fn apply(&mut self, op: Op) -> ModelStep { + let mut step = ModelStep::new(self.collect_resident()); + + match op { + Op::Insert(key) => { + if self.queues.contains_key(&key) { + return step; + } + if self.protected_cap == 0 { + return step; + } + step.evicted_on_insert = self.evict_if_needed(); + self.probation.push_front(key.clone()); + self.queues.insert(key, Queue::Probation); + }, + Op::Get(key) => { + let hit = self.queues.contains_key(&key); + step.hit = Some(if hit { + HitMiss::MustHit + } else { + HitMiss::MustMiss + }); + if hit { + self.promote_to_protected(key); + } + }, + Op::Peek(key) => { + let hit = self.queues.contains_key(&key); + step.hit = Some(if hit { + HitMiss::MustHit + } else { + HitMiss::MustMiss + }); + }, + Op::GetMut(key) => { + let hit = self.queues.contains_key(&key); + step.hit = Some(if hit { + HitMiss::MustHit + } else { + HitMiss::MustMiss + }); + if hit { + self.promote_to_protected(key); + } + }, + Op::Touch(_) => { + step.hit = Some(HitMiss::MayHitOrMiss); + }, + Op::Remove(key) => { + self.detach(&key); + self.queues.remove(&key); + }, + Op::EvictOne => { + if let Some(victim) = self.evict_one_inner() { + step.victim = OracleExpectation::Exact(victim); + } + }, + } + + step.resident = self.collect_resident(); + step + } +} diff --git a/tests/abstract_models/mod.rs b/tests/abstract_models/mod.rs new file mode 100644 index 0000000..5e1b198 --- /dev/null +++ b/tests/abstract_models/mod.rs @@ -0,0 +1,234 @@ +//! Policy semantic test harness (abstract interpretation oracles). +//! +//! ## Architecture +//! +//! Reference models predict cache observables from access traces. Integration tests in +//! [`policy_semantics`](../policy_semantics/) dual-run each [`PolicyModel`] against the real +//! policy implementation step by step. +//! +//! ```text +//! Op trace ──► PolicyModel::apply ──► ModelStep ──► assert vs cache +//! ``` +//! +//! Models live under [`reference`] (spec-derived), [`exact`] (deterministic victims), +//! and [`bounded`] (doc stubs). +//! Submodules and op strategies are gated by matching `policy-*` features. +//! Assertion helpers are in [`driver`]. +//! +//! ## Key components +//! +//! - [`Op`] — unified trace alphabet (`Insert`, `Get`, `Peek`, `GetMut`, `Touch`, `Remove`, `EvictOne`) +//! - [`HitMiss`] — `MustHit` / `MustMiss` / `MayHitOrMiss` (bounded and TTL only) +//! - [`ModelStep`] — residency, hit classification, victim expectation, insert eviction +//! - [`OracleExpectation`] — `Exact(key)`, `Legal(set)`, or `None` +//! - [`PolicyModel`] — `apply`, `peek_victim_key`, `resident_set`, `capacity` +//! +//! ## Proptest strategies +//! +//! Use [`op_strategy_no_evict`] for policies without [`EvictingCache`](../../src/traits.rs). +//! Use [`op_strategy_with_get_mut`] for Fast-LRU and S3-FIFO. Use [`op_strategy_mfu_safe`] when +//! `Remove`/`EvictOne` would leave a stale heap (MFU, Heap-LFU). +//! +//! ## Further reading +//! +//! - [README](README.md) — directory layout, harness modes, contributor checklist +//! - [spec_harness](spec_harness.rs) — tier/mode metadata +//! - [matrix.md](../../docs/testing/specs/matrix.md) — canonical policy index +//! - [Policy semantic testing](../../docs/testing/static-analysis.md) — full harness design and CI +//! +//! ## Multi-crate usage +//! +//! `#[path]`-included by `policy_semantics` (full matrix) and `ttl_integration_test` (LRU +//! subset). Each integration-test binary uses a different subset of models and helpers. +#![allow(dead_code)] + +#[cfg(any( + feature = "policy-arc", + feature = "policy-car", + feature = "policy-clock-pro", + feature = "policy-s3-fifo" +))] +pub mod bounded; +pub mod driver; +pub mod exact; +pub mod spec_harness; + +#[cfg(any( + feature = "policy-fifo", + feature = "policy-heap-lfu", + feature = "policy-lfu", + feature = "policy-lifo", + feature = "policy-mfu", + feature = "policy-mru", + feature = "policy-lru", + feature = "policy-fast-lru", + feature = "policy-lru-k", + feature = "ttl" +))] +pub mod reference; + +use std::collections::HashSet; +use std::hash::Hash; + +use proptest::prelude::*; + +/// Unified trace alphabet for policy semantic tests. +/// +/// Maps to cache API calls in each `policy_semantics/*_tests.rs` adapter. `Peek` must not +/// promote recency; `Get`, `GetMut`, and `Touch` do on LRU-family policies. +#[derive(Debug, Clone, PartialEq, Eq)] +pub enum Op { + Insert(K), + Get(K), + Peek(K), + GetMut(K), + Touch(K), + Remove(K), + EvictOne, +} + +/// Hit/miss classification for the current operation. +/// +/// Exact models use `MustHit` / `MustMiss`. Bounded models and TTL checks may use +/// `MayHitOrMiss` when knowledge is partial. +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub enum HitMiss { + MustHit, + MustMiss, + /// Bounded models and TTL partial-knowledge checks only. + MayHitOrMiss, +} + +/// Expected victim from the reference model. +/// +/// `Exact` — deterministic victim (exact-tier models). `Legal` — any resident key is +/// admissible (bounded-tier). `None` — no victim expectation for this step. +#[derive(Debug, Clone)] +pub enum OracleExpectation { + Exact(K), + /// Reserved for future bounded-tier legal victim sets. + Legal(HashSet), + None, +} + +impl PartialEq for OracleExpectation { + fn eq(&self, other: &Self) -> bool { + match (self, other) { + (Self::Exact(a), Self::Exact(b)) => a == b, + (Self::Legal(a), Self::Legal(b)) => a == b, + (Self::None, Self::None) => true, + _ => false, + } + } +} + +impl Eq for OracleExpectation {} + +/// Observables produced by applying one op to the reference model. +/// +/// Dual-run tests compare each field against the real cache after the same op. +#[derive(Debug, Clone)] +pub struct ModelStep { + pub resident: HashSet, + pub hit: Option, + pub victim: OracleExpectation, + pub evicted_on_insert: Option, +} + +impl ModelStep { + pub fn new(resident: HashSet) -> Self { + Self { + resident, + hit: None, + victim: OracleExpectation::None, + evicted_on_insert: None, + } + } +} + +/// Reference semantics for a cache policy. +/// +/// Each implementation encodes one policy's eviction rule. See [`exact`] and [`bounded`] modules +/// and the [README](README.md) for the per-policy model matrix. +pub trait PolicyModel { + fn capacity(&self) -> usize; + fn resident_set(&self) -> HashSet; + fn apply(&mut self, op: Op) -> ModelStep; + fn peek_victim_key(&self) -> Option; +} + +/// Op strategy without `EvictOne` (policies lacking [`EvictingCache`]). +#[cfg(any( + feature = "policy-two-q", + feature = "policy-slru", + feature = "policy-nru" +))] +pub fn op_strategy_no_evict() -> impl Strategy> { + prop_oneof![ + any::().prop_map(Op::Insert), + any::().prop_map(Op::Get), + any::().prop_map(Op::Peek), + any::().prop_map(Op::Touch), + any::().prop_map(Op::Remove), + ] +} + +/// Default op strategy for policies without `GetMut`. +pub fn op_strategy() -> impl Strategy> { + prop_oneof![ + any::().prop_map(Op::Insert), + any::().prop_map(Op::Get), + any::().prop_map(Op::Peek), + any::().prop_map(Op::Touch), + any::().prop_map(Op::Remove), + Just(Op::EvictOne), + ] +} + +/// Op strategy including `GetMut` (Fast-LRU, S3-FIFO). +#[cfg(any(feature = "policy-fast-lru", feature = "policy-s3-fifo"))] +pub fn op_strategy_with_get_mut() -> impl Strategy> { + prop_oneof![ + 6 => any::().prop_map(Op::Insert), + 4 => any::().prop_map(Op::Get), + 2 => any::().prop_map(Op::Peek), + 2 => any::().prop_map(Op::GetMut), + 2 => any::().prop_map(Op::Touch), + 2 => any::().prop_map(Op::Remove), + 1 => Just(Op::EvictOne), + ] +} + +pub fn standard_capacity() -> impl Strategy { + 1usize..=16 +} + +pub fn standard_op_list() -> impl Strategy>> { + prop::collection::vec(op_strategy(), 0..120) +} + +#[cfg(any(feature = "policy-two-q", feature = "policy-slru"))] +pub fn standard_op_list_no_evict() -> impl Strategy>> { + prop::collection::vec(op_strategy_no_evict(), 0..120) +} + +#[cfg(feature = "policy-nru")] +pub fn short_op_list_no_evict() -> impl Strategy>> { + prop::collection::vec(op_strategy_no_evict(), 0..40) +} + +/// MFU: skip `Remove`/`EvictOne` (stale heap vs debug `validate_invariants`). +#[cfg(feature = "policy-mfu")] +pub fn op_strategy_mfu_safe() -> impl Strategy> { + prop_oneof![ + any::().prop_map(Op::Insert), + any::().prop_map(Op::Get), + any::().prop_map(Op::Peek), + any::().prop_map(Op::Touch), + ] +} + +#[cfg(feature = "policy-mfu")] +pub fn standard_op_list_mfu_safe() -> impl Strategy>> { + prop::collection::vec(op_strategy_mfu_safe(), 0..120) +} diff --git a/tests/abstract_models/reference/fifo.rs b/tests/abstract_models/reference/fifo.rs new file mode 100644 index 0000000..867cbe6 --- /dev/null +++ b/tests/abstract_models/reference/fifo.rs @@ -0,0 +1,126 @@ +//! Spec-derived FIFO reference model. +//! +//! **Source:** [`docs/testing/specs/policies/exact/fifo.md`](../../../docs/testing/specs/policies/exact/fifo.md) · +//! [matrix.md](../../../docs/testing/specs/matrix.md) +//! **Formal spec:** [`docs/testing/specs/formal/fifo/Fifo.tla`](../../../docs/testing/specs/formal/fifo/Fifo.tla) (see +//! [tla-guide.md](../../../docs/testing/specs/tla-guide.md)) +//! **Tier:** reference (spec-first oracle). +//! **Formulation:** `HashSet` + append-only `VecDeque` insertion log with stale skips. + +use std::collections::{HashSet, VecDeque}; +use std::hash::Hash; + +use crate::abstract_models::{HitMiss, ModelStep, Op, OracleExpectation, PolicyModel}; + +#[derive(Debug, Clone)] +pub struct NaiveFifoModel { + store: HashSet, + insertion_order: VecDeque, + capacity: usize, +} + +impl NaiveFifoModel +where + K: Clone + Eq + Hash, +{ + pub fn new(capacity: usize) -> Self { + Self { + store: HashSet::new(), + insertion_order: VecDeque::new(), + capacity, + } + } + + fn collect_resident(&self) -> HashSet { + self.store.clone() + } + + fn evict_oldest(&mut self) -> Option { + while let Some(oldest) = self.insertion_order.pop_front() { + if self.store.contains(&oldest) { + self.store.remove(&oldest); + return Some(oldest); + } + } + None + } + + fn oldest_key(&self) -> Option { + self.insertion_order + .iter() + .find(|k| self.store.contains(*k)) + .cloned() + } +} + +impl PolicyModel for NaiveFifoModel +where + K: Clone + Eq + Hash, +{ + fn capacity(&self) -> usize { + self.capacity + } + + fn resident_set(&self) -> HashSet { + self.collect_resident() + } + + fn peek_victim_key(&self) -> Option { + self.oldest_key() + } + + fn apply(&mut self, op: Op) -> ModelStep { + let mut step = ModelStep::new(self.collect_resident()); + + match op { + Op::Insert(key) => { + if self.store.contains(&key) { + return step; + } + if self.capacity == 0 { + return step; + } + if self.store.len() >= self.capacity { + step.evicted_on_insert = self.evict_oldest(); + } + self.store.insert(key.clone()); + self.insertion_order.push_back(key); + }, + Op::Get(key) => { + step.hit = Some(if self.store.contains(&key) { + HitMiss::MustHit + } else { + HitMiss::MustMiss + }); + }, + Op::Peek(key) => { + step.hit = Some(if self.store.contains(&key) { + HitMiss::MustHit + } else { + HitMiss::MustMiss + }); + }, + Op::GetMut(key) => { + step.hit = Some(if self.store.contains(&key) { + HitMiss::MustHit + } else { + HitMiss::MustMiss + }); + }, + Op::Touch(_) => { + step.hit = Some(HitMiss::MayHitOrMiss); + }, + Op::Remove(key) => { + self.store.remove(&key); + }, + Op::EvictOne => { + if let Some(victim) = self.evict_oldest() { + step.victim = OracleExpectation::Exact(victim); + } + }, + } + + step.resident = self.collect_resident(); + step + } +} diff --git a/tests/abstract_models/reference/heap_lfu.rs b/tests/abstract_models/reference/heap_lfu.rs new file mode 100644 index 0000000..9a4282f --- /dev/null +++ b/tests/abstract_models/reference/heap_lfu.rs @@ -0,0 +1,136 @@ +//! Spec-derived Heap-LFU reference model. +//! +//! **Source:** [`docs/testing/specs/policies/exact/heap-lfu.md`](../../../docs/testing/specs/policies/exact/heap-lfu.md) · +//! [matrix.md](../../../docs/testing/specs/matrix.md) +//! **Tier:** reference (spec-first oracle). +//! **Formulation:** `HashMap` with `Ord` tie-break on key at min frequency; +//! independent of `BinaryHeap` exact model. + +use std::collections::{HashMap, HashSet}; +use std::hash::Hash; + +use crate::abstract_models::{HitMiss, ModelStep, Op, OracleExpectation, PolicyModel}; + +#[derive(Debug, Clone)] +pub struct NaiveHeapLfuModel { + freq: HashMap, + capacity: usize, +} + +impl NaiveHeapLfuModel +where + K: Clone + Eq + Hash + Ord, +{ + pub fn new(capacity: usize) -> Self { + Self { + freq: HashMap::new(), + capacity, + } + } + + fn collect_resident(&self) -> HashSet { + self.freq.keys().cloned().collect() + } + + fn pick_victim(&self) -> Option { + self.freq + .iter() + .min_by(|(k1, f1), (k2, f2)| f1.cmp(f2).then(k1.cmp(k2))) + .map(|(k, _)| k.clone()) + } + + fn bump_freq(&mut self, key: &K) { + if let Some(f) = self.freq.get_mut(key) { + *f += 1; + } + } + + pub fn frequency(&self, key: &K) -> Option { + self.freq.get(key).copied() + } +} + +impl PolicyModel for NaiveHeapLfuModel +where + K: Clone + Eq + Hash + Ord, +{ + fn capacity(&self) -> usize { + self.capacity + } + + fn resident_set(&self) -> HashSet { + self.collect_resident() + } + + fn peek_victim_key(&self) -> Option { + self.pick_victim() + } + + fn apply(&mut self, op: Op) -> ModelStep { + let mut step = ModelStep::new(self.collect_resident()); + + match op { + Op::Insert(key) => { + if self.freq.contains_key(&key) || self.capacity == 0 { + return step; + } + if self.freq.len() >= self.capacity { + if let Some(victim) = self.pick_victim() { + step.evicted_on_insert = Some(victim.clone()); + self.freq.remove(&victim); + } + } + self.freq.insert(key, 1); + }, + Op::Get(key) => { + let hit = self.freq.contains_key(&key); + step.hit = Some(if hit { + HitMiss::MustHit + } else { + HitMiss::MustMiss + }); + if hit { + self.bump_freq(&key); + } + }, + Op::Peek(key) => { + step.hit = Some(if self.freq.contains_key(&key) { + HitMiss::MustHit + } else { + HitMiss::MustMiss + }); + }, + Op::GetMut(key) => { + let hit = self.freq.contains_key(&key); + step.hit = Some(if hit { + HitMiss::MustHit + } else { + HitMiss::MustMiss + }); + if hit { + self.bump_freq(&key); + } + }, + Op::Touch(key) => { + if self.freq.contains_key(&key) { + self.bump_freq(&key); + step.hit = Some(HitMiss::MustHit); + } else { + step.hit = Some(HitMiss::MustMiss); + } + }, + Op::Remove(key) => { + self.freq.remove(&key); + }, + Op::EvictOne => { + if let Some(victim) = self.pick_victim() { + step.victim = OracleExpectation::Exact(victim.clone()); + self.freq.remove(&victim); + } + }, + } + + step.resident = self.collect_resident(); + step + } +} diff --git a/tests/abstract_models/reference/lfu.rs b/tests/abstract_models/reference/lfu.rs new file mode 100644 index 0000000..c6c77ff --- /dev/null +++ b/tests/abstract_models/reference/lfu.rs @@ -0,0 +1,171 @@ +//! Spec-derived LFU reference model. +//! +//! **Source:** [`docs/testing/specs/policies/exact/lfu.md`](../../../docs/testing/specs/policies/exact/lfu.md) · +//! [matrix.md](../../../docs/testing/specs/matrix.md) +//! **Tier:** reference (spec-first oracle). +//! **Formulation:** `HashMap` + append-only `first_seen` log for FIFO tie-break; +//! independent of [`FrequencyBuckets`](cachekit::ds::FrequencyBuckets). + +use std::collections::{HashMap, HashSet, VecDeque}; +use std::hash::Hash; + +use crate::abstract_models::{HitMiss, ModelStep, Op, OracleExpectation, PolicyModel}; + +#[derive(Debug, Clone)] +pub struct NaiveLfuModel { + freq: HashMap, + first_seen: VecDeque, + capacity: usize, +} + +impl NaiveLfuModel +where + K: Clone + Eq + Hash, +{ + pub fn new(capacity: usize) -> Self { + Self { + freq: HashMap::new(), + first_seen: VecDeque::new(), + capacity, + } + } + + fn collect_resident(&self) -> HashSet { + self.freq.keys().cloned().collect() + } + + fn contains_key(&self, key: &K) -> bool { + self.freq.contains_key(key) + } + + fn min_frequency(&self) -> Option { + self.freq.values().copied().min() + } + + /// Last append index for `key` in the tie-break log (re-inserts append again). + fn last_seen_index(&self, key: &K) -> usize { + self.first_seen + .iter() + .rposition(|k| k == key) + .unwrap_or(usize::MAX) + } + + fn peek_victim(&self) -> Option { + let min = self.min_frequency()?; + self.freq + .iter() + .filter(|(_, f)| **f == min) + .map(|(k, _)| k) + .min_by_key(|k| self.last_seen_index(k)) + .cloned() + } + + fn evict_victim(&mut self) -> Option { + let victim = self.peek_victim()?; + self.freq.remove(&victim); + Some(victim) + } + + fn touch(&mut self, key: &K) -> bool { + if let Some(f) = self.freq.get_mut(key) { + *f = f.saturating_add(1); + true + } else { + false + } + } + + fn insert_new(&mut self, key: K) -> Option { + if self.capacity == 0 { + return None; + } + let mut evicted = None; + if self.freq.len() >= self.capacity { + evicted = self.evict_victim(); + } + self.freq.insert(key.clone(), 1); + self.first_seen.push_back(key); + evicted + } + + pub fn frequency(&self, key: &K) -> Option { + self.freq.get(key).copied() + } +} + +impl PolicyModel for NaiveLfuModel +where + K: Clone + Eq + Hash, +{ + fn capacity(&self) -> usize { + self.capacity + } + + fn resident_set(&self) -> HashSet { + self.collect_resident() + } + + fn peek_victim_key(&self) -> Option { + self.peek_victim() + } + + fn apply(&mut self, op: Op) -> ModelStep { + let mut step = ModelStep::new(self.collect_resident()); + + match op { + Op::Insert(key) => { + if self.contains_key(&key) { + return step; + } + step.evicted_on_insert = self.insert_new(key); + }, + Op::Get(key) => { + let hit = self.contains_key(&key); + step.hit = Some(if hit { + HitMiss::MustHit + } else { + HitMiss::MustMiss + }); + if hit { + self.touch(&key); + } + }, + Op::Peek(key) => { + step.hit = Some(if self.contains_key(&key) { + HitMiss::MustHit + } else { + HitMiss::MustMiss + }); + }, + Op::GetMut(key) => { + let hit = self.contains_key(&key); + step.hit = Some(if hit { + HitMiss::MustHit + } else { + HitMiss::MustMiss + }); + if hit { + self.touch(&key); + } + }, + Op::Touch(key) => { + if self.touch(&key) { + step.hit = Some(HitMiss::MustHit); + } else { + step.hit = Some(HitMiss::MustMiss); + } + }, + Op::Remove(key) => { + self.freq.remove(&key); + }, + Op::EvictOne => { + if let Some(victim) = self.evict_victim() { + step.victim = OracleExpectation::Exact(victim); + } + }, + } + + step.resident = self.collect_resident(); + step + } +} diff --git a/tests/abstract_models/reference/lifo.rs b/tests/abstract_models/reference/lifo.rs new file mode 100644 index 0000000..b059438 --- /dev/null +++ b/tests/abstract_models/reference/lifo.rs @@ -0,0 +1,99 @@ +//! Spec-derived LIFO reference model. +//! +//! **Source:** [`docs/testing/specs/policies/exact/lifo.md`](../../../docs/testing/specs/policies/exact/lifo.md) · +//! [matrix.md](../../../docs/testing/specs/matrix.md) +//! **Tier:** reference (spec-first oracle). +//! **Formulation:** `Vec` stack (`push`/`pop` end); independent of `VecDeque` exact model. + +use std::collections::HashSet; +use std::hash::Hash; + +use crate::abstract_models::{HitMiss, ModelStep, Op, OracleExpectation, PolicyModel}; + +#[derive(Debug, Clone)] +pub struct NaiveLifoModel { + stack: Vec, + capacity: usize, +} + +impl NaiveLifoModel +where + K: Clone + Eq + Hash, +{ + pub fn new(capacity: usize) -> Self { + Self { + stack: Vec::new(), + capacity, + } + } + + fn contains_key(&self, key: &K) -> bool { + self.stack.iter().any(|k| k == key) + } + + fn collect_resident(&self) -> HashSet { + self.stack.iter().cloned().collect() + } + + fn newest_key(&self) -> Option { + self.stack.last().cloned() + } +} + +impl PolicyModel for NaiveLifoModel +where + K: Clone + Eq + Hash, +{ + fn capacity(&self) -> usize { + self.capacity + } + + fn resident_set(&self) -> HashSet { + self.collect_resident() + } + + fn peek_victim_key(&self) -> Option { + self.newest_key() + } + + fn apply(&mut self, op: Op) -> ModelStep { + let mut step = ModelStep::new(self.collect_resident()); + + match op { + Op::Insert(key) => { + if self.contains_key(&key) { + return step; + } + if self.capacity == 0 { + return step; + } + if self.stack.len() >= self.capacity { + step.evicted_on_insert = self.stack.pop(); + } + self.stack.push(key); + }, + Op::Get(key) | Op::Peek(key) | Op::GetMut(key) => { + step.hit = Some(if self.contains_key(&key) { + HitMiss::MustHit + } else { + HitMiss::MustMiss + }); + }, + Op::Touch(_) => { + step.hit = Some(HitMiss::MayHitOrMiss); + }, + Op::Remove(key) => { + self.stack.retain(|k| k != &key); + }, + Op::EvictOne => { + if let Some(victim) = self.newest_key() { + step.victim = OracleExpectation::Exact(victim); + self.stack.pop(); + } + }, + } + + step.resident = self.collect_resident(); + step + } +} diff --git a/tests/abstract_models/reference/lru.rs b/tests/abstract_models/reference/lru.rs new file mode 100644 index 0000000..3be5da0 --- /dev/null +++ b/tests/abstract_models/reference/lru.rs @@ -0,0 +1,174 @@ +//! Spec-derived LRU reference model (timestamp formulation). +//! +//! **Source:** [`docs/testing/specs/policies/exact/lru.md`](../../../docs/testing/specs/policies/exact/lru.md) · +//! [matrix.md](../../../docs/testing/specs/matrix.md) +//! **Tier:** reference (spec-first oracle). +//! **Formulation:** `HashMap` access times + monotonic clock; independent of deque model. + +use std::collections::HashMap; +use std::collections::HashSet; +use std::hash::Hash; + +use crate::abstract_models::driver::ModelRecencyRank; +use crate::abstract_models::{HitMiss, ModelStep, Op, OracleExpectation, PolicyModel}; + +#[derive(Debug, Clone)] +pub struct NaiveLruModel { + access: HashMap, + clock: u64, + capacity: usize, +} + +impl NaiveLruModel +where + K: Clone + Eq + Hash + Ord, +{ + pub fn new(capacity: usize) -> Self { + Self { + access: HashMap::new(), + clock: 0, + capacity, + } + } + + fn collect_resident(&self) -> HashSet { + self.access.keys().cloned().collect() + } + + fn bump_clock(&mut self) -> u64 { + self.clock = self.clock.saturating_add(1); + self.clock + } + + fn promote(&mut self, key: K) { + let ts = self.bump_clock(); + self.access.insert(key, ts); + } + + fn lru_victim(&self) -> Option { + self.access + .iter() + .min_by(|(k1, t1), (k2, t2)| t1.cmp(t2).then_with(|| k1.cmp(k2))) + .map(|(k, _)| k.clone()) + } + + fn evict_lru(&mut self) -> Option { + let victim = self.lru_victim()?; + self.access.remove(&victim); + Some(victim) + } + + fn insert_new(&mut self, key: K) -> Option { + if self.capacity == 0 { + return None; + } + let mut evicted = None; + while self.access.len() >= self.capacity { + evicted = self.evict_lru(); + } + self.promote(key); + evicted + } + + fn sorted_resident_keys(&self) -> Vec { + let mut keys: Vec = self.access.keys().cloned().collect(); + keys.sort_by(|a, b| { + let ta = self.access[a]; + let tb = self.access[b]; + tb.cmp(&ta).then_with(|| a.cmp(b)) + }); + keys + } +} + +impl ModelRecencyRank for NaiveLruModel +where + K: Clone + Eq + Hash + Ord, +{ + fn model_recency_rank(&self, key: &K) -> Option { + self.sorted_resident_keys().iter().position(|k| k == key) + } +} + +impl NaiveLruModel +where + K: Clone + Eq + Hash + Ord, +{ + /// Recency rank for assertions (0 = MRU). + pub fn model_recency_rank(&self, key: &K) -> Option { + self.sorted_resident_keys().iter().position(|k| k == key) + } +} + +impl PolicyModel for NaiveLruModel +where + K: Clone + Eq + Hash + Ord, +{ + fn capacity(&self) -> usize { + self.capacity + } + + fn resident_set(&self) -> HashSet { + self.collect_resident() + } + + fn peek_victim_key(&self) -> Option { + self.lru_victim() + } + + fn apply(&mut self, op: Op) -> ModelStep { + let mut step = ModelStep::new(self.collect_resident()); + + match op { + Op::Insert(key) => { + if self.access.contains_key(&key) { + self.promote(key); + } else { + step.evicted_on_insert = self.insert_new(key); + } + }, + Op::Get(key) => { + if self.access.contains_key(&key) { + step.hit = Some(HitMiss::MustHit); + self.promote(key); + } else { + step.hit = Some(HitMiss::MustMiss); + } + }, + Op::Peek(key) => { + step.hit = Some(if self.access.contains_key(&key) { + HitMiss::MustHit + } else { + HitMiss::MustMiss + }); + }, + Op::GetMut(key) => { + if self.access.contains_key(&key) { + step.hit = Some(HitMiss::MustHit); + self.promote(key); + } else { + step.hit = Some(HitMiss::MustMiss); + } + }, + Op::Touch(key) => { + if self.access.contains_key(&key) { + step.hit = Some(HitMiss::MustHit); + self.promote(key); + } else { + step.hit = Some(HitMiss::MustMiss); + } + }, + Op::Remove(key) => { + self.access.remove(&key); + }, + Op::EvictOne => { + if let Some(victim) = self.evict_lru() { + step.victim = OracleExpectation::Exact(victim); + } + }, + } + + step.resident = self.collect_resident(); + step + } +} diff --git a/tests/abstract_models/reference/lru_k.rs b/tests/abstract_models/reference/lru_k.rs new file mode 100644 index 0000000..014077e --- /dev/null +++ b/tests/abstract_models/reference/lru_k.rs @@ -0,0 +1,206 @@ +//! Spec-derived LRU-K reference model. +//! +//! **Source:** [`docs/testing/specs/policies/exact/lru-k.md`](../../../docs/testing/specs/policies/exact/lru-k.md) · +//! [matrix.md](../../../docs/testing/specs/matrix.md) +//! **Tier:** reference (spec-first oracle). +//! **Formulation:** `Vec` cold/hot segments + `HashMap` step history; independent of +//! `VecDeque` exact model. + +use std::collections::{HashMap, HashSet}; +use std::hash::Hash; + +use crate::abstract_models::{HitMiss, ModelStep, Op, OracleExpectation, PolicyModel}; + +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +enum Segment { + Cold, + Hot, +} + +#[derive(Debug, Clone)] +pub struct NaiveLruKModel { + tick: u64, + k: usize, + cold: Vec, + hot: Vec, + segment: HashMap, + history: HashMap>, + capacity: usize, +} + +impl NaiveLruKModel +where + K: Clone + Eq + Hash, +{ + pub fn new(capacity: usize, k: usize) -> Self { + Self { + tick: 0, + k, + cold: Vec::new(), + hot: Vec::new(), + segment: HashMap::new(), + history: HashMap::new(), + capacity, + } + } + + fn collect_resident(&self) -> HashSet { + self.segment.keys().cloned().collect() + } + + fn push_history(&mut self, key: &K, time: u64) { + let h = self.history.entry(key.clone()).or_default(); + h.push(time); + if h.len() > self.k { + let excess = h.len() - self.k; + h.drain(0..excess); + } + } + + fn record_access(&mut self, key: &K) { + self.tick = self.tick.saturating_add(1); + self.push_history(key, self.tick); + } + + fn detach(&mut self, key: &K) { + match self.segment.get(key) { + Some(Segment::Cold) => self.cold.retain(|x| x != key), + Some(Segment::Hot) => self.hot.retain(|x| x != key), + None => {}, + } + } + + fn promote_if_needed(&mut self, key: K) { + let count = self.history.get(&key).map(|h| h.len()).unwrap_or(0); + if count >= self.k { + self.detach(&key); + self.hot.insert(0, key.clone()); + self.segment.insert(key, Segment::Hot); + } + } + + fn move_hot_front(&mut self, key: &K) { + if matches!(self.segment.get(key), Some(Segment::Hot)) { + self.detach(key); + self.hot.insert(0, key.clone()); + } + } + + fn evict_inner(&mut self) -> Option { + if let Some(victim) = self.cold.pop() { + self.segment.remove(&victim); + self.history.remove(&victim); + return Some(victim); + } + if let Some(victim) = self.hot.pop() { + self.segment.remove(&victim); + self.history.remove(&victim); + return Some(victim); + } + None + } + + fn evict_if_needed(&mut self) -> Option { + let mut evicted = None; + while self.segment.len() >= self.capacity { + evicted = self.evict_inner(); + } + evicted + } + + pub fn access_count(&self, key: &K) -> Option { + self.history.get(key).map(|h| h.len()) + } +} + +impl PolicyModel for NaiveLruKModel +where + K: Clone + Eq + Hash, +{ + fn capacity(&self) -> usize { + self.capacity + } + + fn resident_set(&self) -> HashSet { + self.collect_resident() + } + + fn peek_victim_key(&self) -> Option { + self.cold + .last() + .cloned() + .or_else(|| self.hot.last().cloned()) + } + + fn apply(&mut self, op: Op) -> ModelStep { + let mut step = ModelStep::new(self.collect_resident()); + + match op { + Op::Insert(key) => { + if self.segment.contains_key(&key) { + self.record_access(&key); + self.promote_if_needed(key.clone()); + self.move_hot_front(&key); + return step; + } + if self.capacity == 0 { + return step; + } + step.evicted_on_insert = self.evict_if_needed(); + self.tick = self.tick.saturating_add(1); + self.push_history(&key, self.tick); + self.cold.insert(0, key.clone()); + self.segment.insert(key, Segment::Cold); + }, + Op::Get(key) => { + let hit = self.segment.contains_key(&key); + step.hit = Some(if hit { + HitMiss::MustHit + } else { + HitMiss::MustMiss + }); + if hit { + self.record_access(&key); + self.promote_if_needed(key.clone()); + self.move_hot_front(&key); + } + }, + Op::Peek(key) => { + step.hit = Some(if self.segment.contains_key(&key) { + HitMiss::MustHit + } else { + HitMiss::MustMiss + }); + }, + Op::GetMut(key) => { + let hit = self.segment.contains_key(&key); + step.hit = Some(if hit { + HitMiss::MustHit + } else { + HitMiss::MustMiss + }); + if hit { + self.record_access(&key); + self.promote_if_needed(key.clone()); + self.move_hot_front(&key); + } + }, + Op::Touch(_) => { + step.hit = Some(HitMiss::MayHitOrMiss); + }, + Op::Remove(key) => { + self.detach(&key); + self.segment.remove(&key); + self.history.remove(&key); + }, + Op::EvictOne => { + if let Some(victim) = self.evict_inner() { + step.victim = OracleExpectation::Exact(victim); + } + }, + } + + step.resident = self.collect_resident(); + step + } +} diff --git a/tests/abstract_models/reference/mfu.rs b/tests/abstract_models/reference/mfu.rs new file mode 100644 index 0000000..3117c33 --- /dev/null +++ b/tests/abstract_models/reference/mfu.rs @@ -0,0 +1,155 @@ +//! Spec-derived MFU reference model. +//! +//! **Source:** [`docs/testing/specs/policies/exact/mfu.md`](../../../docs/testing/specs/policies/exact/mfu.md) · +//! [matrix.md](../../../docs/testing/specs/matrix.md) +//! **Tier:** reference (spec-first oracle). +//! **Formulation:** `HashMap` frequencies + per-key sequence numbers for heap tie-break; +//! independent of `BinaryHeap` exact model. + +use std::collections::{HashMap, HashSet}; +use std::hash::Hash; + +use crate::abstract_models::{HitMiss, ModelStep, Op, OracleExpectation, PolicyModel}; + +#[derive(Debug, Clone)] +pub struct NaiveMfuModel { + freq: HashMap, + last_seq: HashMap, + seq: u64, + capacity: usize, +} + +impl NaiveMfuModel +where + K: Clone + Eq + Hash, +{ + pub fn new(capacity: usize) -> Self { + Self { + freq: HashMap::new(), + last_seq: HashMap::new(), + seq: 0, + capacity, + } + } + + fn collect_resident(&self) -> HashSet { + self.freq.keys().cloned().collect() + } + + fn record_heap_push(&mut self, key: &K) { + self.seq += 1; + self.last_seq.insert(key.clone(), self.seq); + } + + /// Max-frequency victim; at ties, highest sequence (newest heap entry) is evicted first. + fn pick_victim(&self) -> Option { + let max_freq = *self.freq.values().max()?; + self.freq + .iter() + .filter(|(_, f)| **f == max_freq) + .max_by_key(|(k, _)| self.last_seq.get(*k).copied().unwrap_or(0)) + .map(|(k, _)| k.clone()) + } + + fn bump_freq(&mut self, key: K) { + if let Some(f) = self.freq.get_mut(&key) { + *f += 1; + self.record_heap_push(&key); + } + } + + pub fn frequency(&self, key: &K) -> Option { + self.freq.get(key).copied() + } +} + +impl PolicyModel for NaiveMfuModel +where + K: Clone + Eq + Hash, +{ + fn capacity(&self) -> usize { + self.capacity + } + + fn resident_set(&self) -> HashSet { + self.collect_resident() + } + + fn peek_victim_key(&self) -> Option { + self.pick_victim() + } + + fn apply(&mut self, op: Op) -> ModelStep { + let mut step = ModelStep::new(self.collect_resident()); + + match op { + Op::Insert(key) => { + if self.freq.contains_key(&key) { + self.bump_freq(key); + } else if self.capacity == 0 { + return step; + } else { + while self.freq.len() >= self.capacity { + if let Some(victim) = self.pick_victim() { + if step.evicted_on_insert.is_none() { + step.evicted_on_insert = Some(victim.clone()); + } + self.freq.remove(&victim); + self.last_seq.remove(&victim); + } else { + break; + } + } + self.freq.insert(key.clone(), 1); + self.record_heap_push(&key); + } + }, + Op::Get(key) => { + let hit = self.freq.contains_key(&key); + step.hit = Some(if hit { + HitMiss::MustHit + } else { + HitMiss::MustMiss + }); + if hit { + self.bump_freq(key); + } + }, + Op::Peek(key) => { + step.hit = Some(if self.freq.contains_key(&key) { + HitMiss::MustHit + } else { + HitMiss::MustMiss + }); + }, + Op::GetMut(key) => { + let hit = self.freq.contains_key(&key); + step.hit = Some(if hit { + HitMiss::MustHit + } else { + HitMiss::MustMiss + }); + if hit { + self.bump_freq(key); + } + }, + Op::Touch(_) => { + step.hit = Some(HitMiss::MayHitOrMiss); + }, + Op::Remove(key) => { + self.freq.remove(&key); + self.last_seq.remove(&key); + }, + Op::EvictOne => { + if let Some(victim) = self.pick_victim() { + step.victim = OracleExpectation::Exact(victim.clone()); + self.freq.remove(&victim); + self.last_seq.remove(&victim); + } + }, + } + + step.resident = self.collect_resident(); + step + } +} diff --git a/tests/abstract_models/reference/mod.rs b/tests/abstract_models/reference/mod.rs new file mode 100644 index 0000000..e4c1f4b --- /dev/null +++ b/tests/abstract_models/reference/mod.rs @@ -0,0 +1,32 @@ +//! Spec-derived reference models (independent formulation from operational specs). +//! +//! These models are transcribed from [`docs/testing/specs/`](../../../docs/testing/specs/) +//! only — not from reading `src/policy/`. Cross-model tests in `policy_semantics/` assert +//! agreement with [`exact`](../exact/) models on the same traces. +//! +//! **Not performance references:** use `HashSet`, `VecDeque`, `HashMap`, and timestamps; +//! production code uses slabs, rings, and intrusive lists. + +#[cfg(feature = "policy-fifo")] +pub mod fifo; + +#[cfg(feature = "policy-heap-lfu")] +pub mod heap_lfu; + +#[cfg(feature = "policy-lfu")] +pub mod lfu; + +#[cfg(feature = "policy-lifo")] +pub mod lifo; + +#[cfg(feature = "policy-mfu")] +pub mod mfu; + +#[cfg(feature = "policy-mru")] +pub mod mru; + +#[cfg(any(feature = "policy-lru", feature = "policy-fast-lru", feature = "ttl"))] +pub mod lru; + +#[cfg(feature = "policy-lru-k")] +pub mod lru_k; diff --git a/tests/abstract_models/reference/mru.rs b/tests/abstract_models/reference/mru.rs new file mode 100644 index 0000000..3f333c7 --- /dev/null +++ b/tests/abstract_models/reference/mru.rs @@ -0,0 +1,127 @@ +//! Spec-derived MRU reference model. +//! +//! **Source:** [`docs/testing/specs/policies/exact/mru.md`](../../../docs/testing/specs/policies/exact/mru.md) · +//! [matrix.md](../../../docs/testing/specs/matrix.md) +//! **Tier:** reference (spec-first oracle). +//! **Formulation:** `Vec` with index `0` = MRU victim; independent of `VecDeque` exact model. + +use std::collections::HashSet; +use std::hash::Hash; + +use crate::abstract_models::{HitMiss, ModelStep, Op, OracleExpectation, PolicyModel}; + +#[derive(Debug, Clone)] +pub struct NaiveMruModel { + order: Vec, + capacity: usize, +} + +impl NaiveMruModel +where + K: Clone + Eq + Hash, +{ + pub fn new(capacity: usize) -> Self { + Self { + order: Vec::new(), + capacity, + } + } + + fn contains_key(&self, key: &K) -> bool { + self.order.iter().any(|k| k == key) + } + + fn collect_resident(&self) -> HashSet { + self.order.iter().cloned().collect() + } + + fn mru_key(&self) -> Option { + self.order.first().cloned() + } + + fn promote(&mut self, key: K) { + self.order.retain(|k| k != &key); + self.order.insert(0, key); + } +} + +impl PolicyModel for NaiveMruModel +where + K: Clone + Eq + Hash, +{ + fn capacity(&self) -> usize { + self.capacity + } + + fn resident_set(&self) -> HashSet { + self.collect_resident() + } + + fn peek_victim_key(&self) -> Option { + self.mru_key() + } + + fn apply(&mut self, op: Op) -> ModelStep { + let mut step = ModelStep::new(self.collect_resident()); + + match op { + Op::Insert(key) => { + if self.contains_key(&key) || self.capacity == 0 { + return step; + } + while self.order.len() >= self.capacity { + step.evicted_on_insert = self.order.first().cloned(); + if self.order.is_empty() { + break; + } + self.order.remove(0); + } + self.order.insert(0, key); + }, + Op::Get(key) => { + let hit = self.contains_key(&key); + step.hit = Some(if hit { + HitMiss::MustHit + } else { + HitMiss::MustMiss + }); + if hit { + self.promote(key); + } + }, + Op::Peek(key) => { + step.hit = Some(if self.contains_key(&key) { + HitMiss::MustHit + } else { + HitMiss::MustMiss + }); + }, + Op::GetMut(key) => { + let hit = self.contains_key(&key); + step.hit = Some(if hit { + HitMiss::MustHit + } else { + HitMiss::MustMiss + }); + if hit { + self.promote(key); + } + }, + Op::Touch(_) => { + step.hit = Some(HitMiss::MayHitOrMiss); + }, + Op::Remove(key) => { + self.order.retain(|k| k != &key); + }, + Op::EvictOne => { + if let Some(victim) = self.mru_key() { + step.victim = OracleExpectation::Exact(victim.clone()); + self.order.remove(0); + } + }, + } + + step.resident = self.collect_resident(); + step + } +} diff --git a/tests/abstract_models/spec_harness.rs b/tests/abstract_models/spec_harness.rs new file mode 100644 index 0000000..3834da5 --- /dev/null +++ b/tests/abstract_models/spec_harness.rs @@ -0,0 +1,92 @@ +//! Spec-first harness metadata for contributors. +//! +//! Documentation-first module — not runtime enforcement. See the canonical policy index at +//! [`docs/testing/specs/matrix.md`](../../docs/testing/specs/matrix.md). +//! +//! ## Spec-change checklist +//! +//! When a policy spec changes, update in order: +//! +//! 1. Operational spec in `docs/testing/specs/policies//.md` +//! 2. `reference/.rs` (if a reference model exists) +//! 3. Cross-model test expectations (if behavior changed) +//! 4. `exact/.rs` if the exact model was wrong +//! 5. `formal//` TLA+ module and `tlc.md` alignment notes (if applicable) +//! 6. Row in `docs/testing/specs/matrix.md` +//! +//! ## Harness modes +//! +//! | Mode | When to use | +//! |------|-------------| +//! | [`HarnessMode::DualRun`] | Exact, mirror, composed — `PolicyModel` vs impl | +//! | [`HarnessMode::CrossModel`] | Independent `reference/` vs `exact/` (FIFO, LRU, Fast-LRU, LIFO, LFU, MRU, Heap-LFU, MFU) | +//! | [`HarnessMode::InvariantOnly`] | Bounded — structural invariants only | +//! +//! A policy may use multiple modes (e.g. FIFO: DualRun + CrossModel). +//! +//! ## Cross-model availability +//! +//! `cross_model_available` is true for all exact-tier policies with a `reference/` model. Use +//! [`driver::assert_models_agree`] or [`driver::assert_models_agree_with_recency`] when +//! [`driver::ModelRecencyRank`] is implemented (LRU family). +//! +//! ## Related +//! +//! - [template.md](../../docs/testing/specs/template.md) — new policy spec skeleton +//! - [tla-guide.md](../../docs/testing/specs/tla-guide.md) — optional TLA+ specs + +/// Root path for spec hub docs (grep-friendly). +pub const SPEC_ROOT: &str = "docs/testing/specs"; + +/// Human operational specs by tier (`exact/`, `mirror/`, `bounded/`, `composed/`). +pub const POLICIES_ROOT: &str = "docs/testing/specs/policies"; + +/// TLA+ modules and TLC runbooks (`/Policy.tla`, `tlc.md`). +pub const FORMAL_ROOT: &str = "docs/testing/specs/formal"; + +/// Model tier in the harness. +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub enum SpecTier { + /// Deterministic victim and residency (LFU, LIFO, LRU, …). + Exact, + /// DS-shaped oracle transcribed from implementation (Clock, 2Q, SLRU, NRU). + Mirror, + /// Adaptive victim — invariant-only tests today (ARC, CAR, Clock-PRO, S3-FIFO). + Bounded, + /// Decorator over inner policy (TTL over LRU). + Composed, +} + +/// How the harness validates a policy. +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub enum HarnessMode { + /// `exact/` `PolicyModel` dual-run vs implementation. + DualRun, + /// `reference/` vs `exact/` agreement (FIFO, LRU, Fast-LRU, LIFO, LFU, MRU, Heap-LFU, MFU). + CrossModel, + /// `len <= capacity` + invariant checks (bounded tier). + InvariantOnly, +} + +/// Whether an independent `reference/` model exists for cross-model tests. +pub fn cross_model_available(policy: &str) -> bool { + policy == "fifo" + || policy == "lru" + || policy == "fast-lru" + || policy == "lifo" + || policy == "lfu" + || policy == "mru" + || policy == "heap-lfu" + || policy == "mfu" + || policy == "lru-k" +} + +/// Per-policy harness metadata (documentation-oriented). +#[derive(Debug, Clone, Copy)] +pub struct PolicyHarnessMeta { + pub name: &'static str, + pub tier: SpecTier, + pub modes: &'static [HarnessMode], + pub spec_doc: &'static str, + pub notes: &'static str, +} diff --git a/tests/policy_semantics/arc_tests.rs b/tests/policy_semantics/arc_tests.rs new file mode 100644 index 0000000..56ab26a --- /dev/null +++ b/tests/policy_semantics/arc_tests.rs @@ -0,0 +1,53 @@ +//! ARC invariant-only semantic tests (no `PolicyModel` dual-run). +//! +//! **Model:** none · **Op strategy:** `standard_op_list` (`GetMut`/`Touch`/`EvictOne` no-op) +//! **Asserted:** `len <= capacity`, `debug_validate_invariants` + +use cachekit::policy::arc::ArcCore; +use cachekit::traits::Cache; +use proptest::prelude::*; + +use crate::abstract_models::driver::run_invariant_trace; +use crate::abstract_models::{Op, standard_capacity, standard_op_list}; + +fn apply_arc_op(cache: &mut ArcCore, op: Op) { + match op { + Op::Insert(k) => { + cache.insert(k, k); + }, + Op::Get(k) => { + let _ = cache.get(&k); + }, + Op::Peek(k) => { + let _ = cache.peek(&k); + }, + Op::Remove(k) => { + cache.remove(&k); + }, + Op::GetMut(_) | Op::Touch(_) | Op::EvictOne => {}, + } +} + +fn run_ops(cache: &mut ArcCore, ops: &[Op]) { + run_invariant_trace(cache, ops, apply_arc_op, |cache| { + cache.debug_validate_invariants(); + }); +} + +proptest! { + #![proptest_config(ProptestConfig { cases: 128, ..ProptestConfig::default() })] + + #[cfg_attr(miri, ignore)] + #[test] + fn prop_arc_invariants(capacity in standard_capacity(), ops in standard_op_list()) { + let mut cache = ArcCore::new(capacity); + run_ops(&mut cache, &ops); + } +} + +#[test] +fn smoke_arc() { + let ops = [Op::Insert(1), Op::Insert(2), Op::Get(1), Op::Insert(3)]; + let mut cache = ArcCore::new(2); + run_ops(&mut cache, &ops); +} diff --git a/tests/policy_semantics/car_tests.rs b/tests/policy_semantics/car_tests.rs new file mode 100644 index 0000000..ae5b401 --- /dev/null +++ b/tests/policy_semantics/car_tests.rs @@ -0,0 +1,53 @@ +//! CAR invariant-only semantic tests (no `PolicyModel` dual-run). +//! +//! **Model:** none · **Op strategy:** `standard_op_list` (`GetMut`/`Touch`/`EvictOne` no-op) +//! **Asserted:** `len <= capacity`, `CarCore::debug_validate_invariants` + +use cachekit::policy::car::CarCore; +use cachekit::traits::Cache; +use proptest::prelude::*; + +use crate::abstract_models::driver::run_invariant_trace; +use crate::abstract_models::{Op, standard_capacity, standard_op_list}; + +fn apply_car_op(cache: &mut CarCore, op: Op) { + match op { + Op::Insert(k) => { + cache.insert(k, k); + }, + Op::Get(k) => { + let _ = cache.get(&k); + }, + Op::Peek(k) => { + let _ = cache.peek(&k); + }, + Op::Remove(k) => { + cache.remove(&k); + }, + Op::GetMut(_) | Op::Touch(_) | Op::EvictOne => {}, + } +} + +fn run_ops(cache: &mut CarCore, ops: &[Op]) { + run_invariant_trace(cache, ops, apply_car_op, |cache| { + cache.debug_validate_invariants(); + }); +} + +proptest! { + #![proptest_config(ProptestConfig { cases: 128, ..ProptestConfig::default() })] + + #[cfg_attr(miri, ignore)] + #[test] + fn prop_car_invariants(capacity in standard_capacity(), ops in standard_op_list()) { + let mut cache = CarCore::new(capacity); + run_ops(&mut cache, &ops); + } +} + +#[test] +fn smoke_car() { + let ops = [Op::Insert(1), Op::Get(1), Op::Insert(2), Op::Insert(3)]; + let mut cache = CarCore::new(4); + run_ops(&mut cache, &ops); +} diff --git a/tests/policy_semantics/clock_pro_tests.rs b/tests/policy_semantics/clock_pro_tests.rs new file mode 100644 index 0000000..8547560 --- /dev/null +++ b/tests/policy_semantics/clock_pro_tests.rs @@ -0,0 +1,57 @@ +//! Clock-PRO invariant-only semantic tests (no `PolicyModel` dual-run). +//! +//! **Model:** none · **Op strategy:** `standard_op_list` (`GetMut`/`Touch`/`EvictOne` no-op) +//! **Asserted:** `len <= capacity` + +use cachekit::policy::clock_pro::ClockProCache; +use cachekit::traits::Cache; +use proptest::prelude::*; + +use crate::abstract_models::driver::run_invariant_trace; +use crate::abstract_models::{Op, standard_capacity, standard_op_list}; + +fn apply_clock_pro_op(cache: &mut ClockProCache, op: Op) { + match op { + Op::Insert(k) => { + cache.insert(k, k); + }, + Op::Get(k) => { + let _ = cache.get(&k); + }, + Op::Peek(k) => { + let _ = cache.peek(&k); + }, + Op::Remove(k) => { + cache.remove(&k); + }, + Op::GetMut(_) | Op::Touch(_) | Op::EvictOne => {}, + } +} + +fn run_ops(cache: &mut ClockProCache, ops: &[Op]) { + run_invariant_trace(cache, ops, apply_clock_pro_op, |_| {}); +} + +proptest! { + #![proptest_config(ProptestConfig { cases: 128, ..ProptestConfig::default() })] + + #[cfg_attr(miri, ignore)] + #[test] + fn prop_clock_pro_residency(capacity in standard_capacity(), ops in standard_op_list()) { + let mut cache = ClockProCache::new(capacity); + run_ops(&mut cache, &ops); + } +} + +#[test] +fn smoke_clock_pro() { + let ops = [ + Op::Insert(1), + Op::Get(1), + Op::Insert(2), + Op::Insert(3), + Op::Insert(4), + ]; + let mut cache = ClockProCache::new(3); + run_ops(&mut cache, &ops); +} diff --git a/tests/policy_semantics/clock_tests.rs b/tests/policy_semantics/clock_tests.rs new file mode 100644 index 0000000..702dae2 --- /dev/null +++ b/tests/policy_semantics/clock_tests.rs @@ -0,0 +1,73 @@ +//! Clock dual-run semantic oracle tests. +//! +//! **Model:** `ClockModel` · **Op strategy:** `standard_op_list` +//! **Asserted:** residency, insert eviction + +use cachekit::policy::clock::ClockCache; +use cachekit::traits::{Cache, EvictingCache}; +use proptest::prelude::*; + +use crate::abstract_models::driver::assert_dual_run_step_no_victim; +use crate::abstract_models::exact::clock::ClockModel; +use crate::abstract_models::{Op, PolicyModel, standard_capacity, standard_op_list}; + +fn run_ops(cache: &mut ClockCache, model: &mut ClockModel, ops: &[Op]) { + for op in ops { + let step = model.apply(op.clone()); + match op { + Op::Insert(k) => { + cache.insert(*k, ()); + }, + Op::Get(k) => { + let _ = cache.get(k); + }, + Op::Peek(k) => { + let _ = cache.peek(k); + }, + Op::GetMut(_) | Op::Touch(_) => {}, + Op::Remove(k) => { + cache.remove(k); + }, + Op::EvictOne => { + let _ = cache.evict_one(); + }, + } + assert_dual_run_step_no_victim( + cache, + model, + &step, + |k| cache.contains(k), + |cache, _, step| { + if let Some(e) = &step.evicted_on_insert { + assert!(!cache.contains(e)); + } + }, + ); + } +} + +proptest! { + #![proptest_config(ProptestConfig { cases: 256, ..ProptestConfig::default() })] + + #[cfg_attr(miri, ignore)] + #[test] + fn prop_clock_matches_model(capacity in standard_capacity(), ops in standard_op_list()) { + let mut cache = ClockCache::new(capacity); + let mut model = ClockModel::new(capacity); + run_ops(&mut cache, &mut model, &ops); + } +} + +#[test] +fn smoke_clock() { + let ops = [ + Op::Insert(1), + Op::Get(1), + Op::Insert(2), + Op::Insert(3), + Op::Insert(4), + ]; + let mut cache = ClockCache::new(3); + let mut model = ClockModel::new(3); + run_ops(&mut cache, &mut model, &ops); +} diff --git a/tests/policy_semantics/dual_impl_tests.rs b/tests/policy_semantics/dual_impl_tests.rs new file mode 100644 index 0000000..aaae894 --- /dev/null +++ b/tests/policy_semantics/dual_impl_tests.rs @@ -0,0 +1,161 @@ +//! Dual-implementation equivalence tests (no reference model). +//! +//! **Pairs:** `LruCore` vs `FastLru`, `ClockCache` vs `ClockRing` +//! **Asserted:** residency, `peek_victim`, `recency_rank` agreement + +use std::collections::HashSet; +use std::sync::Arc; + +#[cfg(feature = "policy-clock")] +use cachekit::ds::ClockRing; +#[cfg(feature = "policy-clock")] +use cachekit::policy::clock::ClockCache; +#[cfg(feature = "policy-fast-lru")] +use cachekit::policy::fast_lru::FastLru; +#[cfg(feature = "policy-lru")] +use cachekit::policy::lru::LruCore; +use cachekit::traits::{Cache, EvictingCache, VictimInspectable}; + +use crate::abstract_models::driver::probe_resident; +use crate::abstract_models::{Op, op_strategy}; + +#[cfg(all(feature = "policy-lru", feature = "policy-fast-lru"))] +#[test] +fn dual_lru_core_vs_fast_lru() { + let ops = [ + Op::Insert(1), + Op::Insert(2), + Op::Get(1), + Op::Peek(2), + Op::Touch(1), + Op::Insert(3), + Op::Insert(4), + Op::EvictOne, + Op::Remove(2), + ]; + let mut lru = LruCore::::new(3); + let mut fast = FastLru::new(3); + + for op in &ops { + match op { + Op::Insert(k) => { + lru.insert(*k, Arc::new(*k)); + fast.insert(*k, *k); + }, + Op::Get(k) => { + lru.get(k); + fast.get(k); + }, + Op::Peek(k) => { + lru.peek(k); + fast.peek(k); + }, + Op::Touch(k) => { + lru.touch(k); + fast.touch(k); + }, + Op::Remove(k) => { + lru.remove(k); + fast.remove(k); + }, + Op::EvictOne => { + let _ = lru.evict_one(); + let _ = fast.evict_one(); + }, + Op::GetMut(_) => {}, + } + + for k in 0..=255u8 { + assert_eq!( + lru.contains(&k), + fast.contains(&k), + "contains {k} after {op:?}" + ); + } + assert_eq!( + lru.peek_victim().map(|(k, _)| *k), + fast.peek_victim().map(|(k, _)| *k) + ); + if let (Some(lru_rank), Some(fast_rank)) = (lru.recency_rank(&1), fast.recency_rank(&1)) { + if lru.contains(&1) { + assert_eq!(lru_rank, fast_rank); + } + } + } +} + +#[cfg(feature = "policy-clock")] +#[test] +fn dual_clock_cache_vs_clock_ring() { + let ops = [ + Op::Insert(1), + Op::Get(1), + Op::Insert(2), + Op::Insert(3), + Op::Insert(4), + ]; + let mut cache = ClockCache::::new(3); + let mut ring = ClockRing::new(3); + + for op in &ops { + match op { + Op::Insert(k) => { + cache.insert(*k, ()); + ring.insert(*k, ()); + }, + Op::Get(k) => { + cache.get(k); + let _ = ring.get(k); + }, + Op::Peek(k) => { + cache.peek(k); + ring.peek(k); + }, + Op::Remove(k) => { + cache.remove(k); + ring.remove(k); + }, + _ => {}, + } + let cache_r = probe_resident(|k| cache.contains(k)); + let ring_r: HashSet = ring.keys().copied().collect(); + assert_eq!(cache_r, ring_r, "after {op:?}"); + } +} + +#[cfg(all(feature = "policy-lru", feature = "policy-fast-lru"))] +mod proptests { + use super::*; + use proptest::prelude::*; + + proptest! { + #![proptest_config(ProptestConfig { cases: 64, ..ProptestConfig::default() })] + + #[cfg_attr(miri, ignore)] + #[test] + fn prop_dual_lru_observables(ops in prop::collection::vec(op_strategy(), 0..60)) { + let mut lru = LruCore::::new(8); + let mut fast = FastLru::new(8); + for op in ops { + match op { + Op::Insert(k) => { + lru.insert(k, Arc::new(k)); + fast.insert(k, k); + }, + Op::Get(k) => { lru.get(&k); fast.get(&k); }, + Op::Peek(k) => { lru.peek(&k); fast.peek(&k); }, + Op::Touch(k) => { lru.touch(&k); fast.touch(&k); }, + Op::Remove(k) => { lru.remove(&k); fast.remove(&k); }, + Op::EvictOne => { + let _ = lru.evict_one(); + let _ = fast.evict_one(); + }, + Op::GetMut(k) => { fast.get_mut(&k); }, + } + for key in 0..=255u8 { + assert_eq!(lru.contains(&key), fast.contains(&key)); + } + } + } + } +} diff --git a/tests/policy_semantics/fast_lru_tests.rs b/tests/policy_semantics/fast_lru_tests.rs new file mode 100644 index 0000000..60a6af5 --- /dev/null +++ b/tests/policy_semantics/fast_lru_tests.rs @@ -0,0 +1,139 @@ +//! Fast-LRU dual-run semantic oracle tests. +//! +//! **Model:** `LruOccupancyModel` · **Op strategy:** `op_strategy_with_get_mut` (0..120) +//! **Asserted:** residency, `peek_victim`, recency rank +//! +//! Cross-model: `NaiveLruModel` vs `LruOccupancyModel` (shared LRU reference). naive ≠ exact → fix +//! spec or model; naive = exact but impl fails → fix implementation or adapter. + +use cachekit::policy::fast_lru::FastLru; +use cachekit::traits::{EvictingCache, VictimInspectable}; +use proptest::prelude::*; + +use crate::abstract_models::driver::{ + assert_dual_run_step, assert_models_agree_with_recency, assert_recency_rank, +}; +use crate::abstract_models::exact::lru::LruOccupancyModel; +use crate::abstract_models::reference::lru::NaiveLruModel; +use crate::abstract_models::{Op, PolicyModel, op_strategy_with_get_mut, standard_capacity}; + +fn run_ops(cache: &mut FastLru, model: &mut LruOccupancyModel, ops: &[Op]) { + for op in ops { + let rank_before = match op { + Op::Peek(k) => cache.recency_rank(k), + _ => None, + }; + + let step = model.apply(op.clone()); + + match op { + Op::Insert(k) => { + cache.insert(*k, *k); + }, + Op::Get(k) => { + let _ = cache.get(k); + }, + Op::Peek(k) => { + let _ = cache.peek(k); + }, + Op::GetMut(k) => { + let _ = cache.get_mut(k); + }, + Op::Touch(k) => { + cache.touch(k); + }, + Op::Remove(k) => { + cache.remove(k); + }, + Op::EvictOne => { + if cache.peek_victim().is_some() { + let _ = cache.evict_one(); + } + }, + } + + assert_dual_run_step( + cache, + model, + &step, + |k| cache.contains(k), + |cache, model, step| { + if let Op::Peek(k) = op { + if let Some(rank) = rank_before { + assert_eq!(cache.recency_rank(k), Some(rank)); + } + } + + if matches!(op, Op::Get(_) | Op::GetMut(_) | Op::Touch(_)) { + let key = match op { + Op::Get(k) | Op::GetMut(k) | Op::Touch(k) => *k, + _ => unreachable!(), + }; + assert_recency_rank(cache, model.model_recency_rank(&key), &key); + } + + if let Some(evicted) = &step.evicted_on_insert { + assert!(!cache.contains(evicted)); + } + }, + ); + } +} + +proptest! { + #![proptest_config(ProptestConfig { cases: 256, ..ProptestConfig::default() })] + + #[cfg_attr(miri, ignore)] + #[test] + fn prop_fast_lru_naive_matches_current_model( + capacity in standard_capacity(), + ops in prop::collection::vec(op_strategy_with_get_mut(), 0..120), + ) { + let mut naive = NaiveLruModel::new(capacity); + let mut current = LruOccupancyModel::new(capacity); + assert_models_agree_with_recency(&mut naive, &mut current, &ops); + } + + #[cfg_attr(miri, ignore)] + #[test] + fn prop_fast_lru_matches_model( + capacity in standard_capacity(), + ops in prop::collection::vec(op_strategy_with_get_mut(), 0..120), + ) { + let mut cache = FastLru::new(capacity); + let mut model = LruOccupancyModel::new(capacity); + run_ops(&mut cache, &mut model, &ops); + } +} + +#[test] +fn smoke_fast_lru_naive_agreement() { + let ops = [ + Op::Insert(1), + Op::Insert(2), + Op::GetMut(1), + Op::Peek(2), + Op::Insert(3), + Op::Insert(4), + Op::EvictOne, + ]; + let mut naive = NaiveLruModel::new(3); + let mut current = LruOccupancyModel::new(3); + assert_models_agree_with_recency(&mut naive, &mut current, &ops); +} + +#[test] +fn smoke_fast_lru() { + let ops = [ + Op::Insert(1), + Op::Insert(2), + Op::GetMut(1), + Op::Peek(2), + Op::Insert(3), + Op::Insert(4), + Op::EvictOne, + ]; + let mut cache = FastLru::new(3); + let mut model = LruOccupancyModel::new(3); + run_ops(&mut cache, &mut model, &ops); +} diff --git a/tests/policy_semantics/fifo_tests.rs b/tests/policy_semantics/fifo_tests.rs new file mode 100644 index 0000000..77e40a1 --- /dev/null +++ b/tests/policy_semantics/fifo_tests.rs @@ -0,0 +1,103 @@ +//! FIFO dual-run semantic oracle tests. +//! +//! **Model:** `FifoModel` · **Op strategy:** `standard_op_list` +//! **Asserted:** residency, `peek_victim`, insert eviction + +use cachekit::policy::fifo::FifoCache; +use cachekit::traits::{Cache, EvictingCache}; +use proptest::prelude::*; + +use crate::abstract_models::driver::{assert_dual_run_step, assert_models_agree}; +use crate::abstract_models::exact::fifo::FifoModel; +use crate::abstract_models::reference::fifo::NaiveFifoModel; +use crate::abstract_models::{Op, PolicyModel, standard_capacity, standard_op_list}; + +fn run_ops(cache: &mut FifoCache, model: &mut FifoModel, ops: &[Op]) { + for op in ops { + let step = model.apply(op.clone()); + match op { + Op::Insert(k) => { + cache.insert(*k, *k); + }, + Op::Get(k) => { + let _ = cache.get(k); + }, + Op::Peek(k) => { + let _ = cache.peek(k); + }, + Op::GetMut(_) | Op::Touch(_) => {}, + Op::Remove(k) => { + cache.remove(k); + }, + Op::EvictOne => { + let _ = cache.evict_one(); + }, + } + assert_dual_run_step( + cache, + model, + &step, + |k| cache.contains(k), + |cache, _, step| { + if let Some(e) = &step.evicted_on_insert { + assert!(!cache.contains(e)); + } + }, + ); + } +} + +proptest! { + #![proptest_config(ProptestConfig { cases: 256, ..ProptestConfig::default() })] + + #[cfg_attr(miri, ignore)] + #[test] + fn prop_fifo_naive_matches_current_model( + capacity in standard_capacity(), + ops in standard_op_list(), + ) { + let mut naive = NaiveFifoModel::new(capacity); + let mut current = FifoModel::new(capacity); + assert_models_agree(&mut naive, &mut current, &ops); + } + + #[cfg_attr(miri, ignore)] + #[test] + fn prop_fifo_matches_model(capacity in standard_capacity(), ops in standard_op_list()) { + let mut cache = FifoCache::new(capacity); + let mut model = FifoModel::new(capacity); + run_ops(&mut cache, &mut model, &ops); + } +} + +#[test] +fn smoke_fifo_naive_agreement() { + let ops = [ + Op::Insert(1), + Op::Insert(2), + Op::Insert(3), + Op::Insert(4), + Op::Get(1), + Op::EvictOne, + Op::Remove(2), + ]; + let mut naive = NaiveFifoModel::new(3); + let mut current = FifoModel::new(3); + assert_models_agree(&mut naive, &mut current, &ops); +} + +#[test] +fn smoke_fifo() { + let ops = [ + Op::Insert(1), + Op::Insert(2), + Op::Insert(3), + Op::Insert(4), + Op::Get(1), + Op::EvictOne, + Op::Remove(2), + ]; + let mut cache = FifoCache::new(3); + let mut model = FifoModel::new(3); + run_ops(&mut cache, &mut model, &ops); +} diff --git a/tests/policy_semantics/heap_lfu_tests.rs b/tests/policy_semantics/heap_lfu_tests.rs new file mode 100644 index 0000000..5dc4c69 --- /dev/null +++ b/tests/policy_semantics/heap_lfu_tests.rs @@ -0,0 +1,97 @@ +//! Heap-LFU dual-run semantic oracle tests. +//! +//! **Model:** `HeapLfuModel` · **Op strategy:** `standard_op_list` +//! **Asserted:** residency only (heap rebuild handles staleness) +//! +//! Cross-model: `NaiveHeapLfuModel` vs `HeapLfuModel`. naive ≠ exact → fix spec or model; naive = exact +//! but impl fails → fix implementation or adapter. + +use std::sync::Arc; + +use cachekit::policy::heap_lfu::HeapLfuCache; +use cachekit::traits::{Cache, EvictingCache}; +use proptest::prelude::*; + +use crate::abstract_models::driver::{assert_dual_run_step_no_victim, assert_models_agree}; +use crate::abstract_models::exact::heap_lfu::HeapLfuModel; +use crate::abstract_models::reference::heap_lfu::NaiveHeapLfuModel; +use crate::abstract_models::{Op, PolicyModel, standard_capacity, standard_op_list}; + +fn run_ops(cache: &mut HeapLfuCache, model: &mut HeapLfuModel, ops: &[Op]) { + for op in ops { + let step = model.apply(op.clone()); + match op { + Op::Insert(k) => { + cache.insert(*k, Arc::new(*k)); + }, + Op::Get(k) => { + let _ = cache.get(k); + }, + Op::Peek(k) => { + let _ = cache.peek(k); + }, + Op::GetMut(_) => {}, + Op::Touch(k) => { + cache.increment_frequency(k); + }, + Op::Remove(k) => { + cache.remove(k); + }, + Op::EvictOne => { + let _ = cache.evict_one(); + }, + } + assert_dual_run_step_no_victim(cache, model, &step, |k| cache.contains(k), |_, _, _| {}); + } +} + +proptest! { + #![proptest_config(ProptestConfig { cases: 256, ..ProptestConfig::default() })] + + #[cfg_attr(miri, ignore)] + #[test] + fn prop_heap_lfu_naive_matches_current_model( + capacity in standard_capacity(), + ops in standard_op_list(), + ) { + let mut naive = NaiveHeapLfuModel::new(capacity); + let mut current = HeapLfuModel::new(capacity); + assert_models_agree(&mut naive, &mut current, &ops); + } + + #[cfg_attr(miri, ignore)] + #[test] + fn prop_heap_lfu_matches_model(capacity in standard_capacity(), ops in standard_op_list()) { + let mut cache = HeapLfuCache::new(capacity); + let mut model = HeapLfuModel::new(capacity); + run_ops(&mut cache, &mut model, &ops); + } +} + +#[test] +fn smoke_heap_lfu_naive_agreement() { + let ops = [ + Op::Insert(1), + Op::Insert(2), + Op::Get(1), + Op::Insert(3), + Op::Insert(4), + ]; + let mut naive = NaiveHeapLfuModel::new(3); + let mut current = HeapLfuModel::new(3); + assert_models_agree(&mut naive, &mut current, &ops); +} + +#[test] +fn smoke_heap_lfu() { + let ops = [ + Op::Insert(1), + Op::Insert(2), + Op::Get(1), + Op::Insert(3), + Op::Insert(4), + ]; + let mut cache = HeapLfuCache::new(3); + let mut model = HeapLfuModel::new(3); + run_ops(&mut cache, &mut model, &ops); +} diff --git a/tests/policy_semantics/lfu_tests.rs b/tests/policy_semantics/lfu_tests.rs new file mode 100644 index 0000000..a86d82a --- /dev/null +++ b/tests/policy_semantics/lfu_tests.rs @@ -0,0 +1,110 @@ +//! LFU dual-run semantic oracle tests. +//! +//! **Model:** `LfuModel` · **Op strategy:** `standard_op_list` +//! **Asserted:** residency, frequency, `peek_victim` +//! +//! Cross-model: `NaiveLfuModel` vs `LfuModel`. naive ≠ exact → fix spec or model; naive = exact +//! but impl fails → fix implementation or adapter. + +use std::sync::Arc; + +use cachekit::policy::lfu::LfuCache; +use cachekit::traits::{Cache, EvictingCache}; +use proptest::prelude::*; + +use crate::abstract_models::driver::{assert_dual_run_step, assert_models_agree}; +use crate::abstract_models::exact::lfu::LfuModel; +use crate::abstract_models::reference::lfu::NaiveLfuModel; +use crate::abstract_models::{Op, PolicyModel, standard_capacity, standard_op_list}; + +fn run_ops(cache: &mut LfuCache, model: &mut LfuModel, ops: &[Op]) { + for op in ops { + let step = model.apply(op.clone()); + match op { + Op::Insert(k) => { + cache.insert(*k, Arc::new(*k)); + }, + Op::Get(k) => { + let _ = cache.get(k); + }, + Op::Peek(k) => { + let _ = cache.peek(k); + }, + Op::GetMut(_) => {}, + Op::Touch(k) => { + cache.increment_frequency(k); + }, + Op::Remove(k) => { + cache.remove(k); + }, + Op::EvictOne => { + let _ = cache.evict_one(); + }, + } + assert_dual_run_step( + cache, + model, + &step, + |k| cache.contains(k), + |cache, model, step| { + for k in &step.resident { + assert_eq!(cache.frequency(k), model.frequency(k)); + } + }, + ); + } +} + +#[test] +fn hand_written_lfu_fifo_tie_break() { + let mut cache = LfuCache::new(3); + let mut model = LfuModel::new(3); + let ops = [Op::Insert(1), Op::Insert(2), Op::Insert(3), Op::Insert(4)]; + run_ops(&mut cache, &mut model, &ops); + assert!(!cache.contains(&1)); +} + +proptest! { + #![proptest_config(ProptestConfig { cases: 256, ..ProptestConfig::default() })] + + #[cfg_attr(miri, ignore)] + #[test] + fn prop_lfu_naive_matches_current_model( + capacity in standard_capacity(), + ops in standard_op_list(), + ) { + let mut naive = NaiveLfuModel::new(capacity); + let mut current = LfuModel::new(capacity); + assert_models_agree(&mut naive, &mut current, &ops); + } + + #[cfg_attr(miri, ignore)] + #[test] + fn prop_lfu_matches_model(capacity in standard_capacity(), ops in standard_op_list()) { + let mut cache = LfuCache::new(capacity); + let mut model = LfuModel::new(capacity); + run_ops(&mut cache, &mut model, &ops); + } +} + +#[test] +fn smoke_lfu_naive_agreement() { + let ops = [Op::Insert(1), Op::Insert(2), Op::Insert(3), Op::Insert(4)]; + let mut naive = NaiveLfuModel::new(3); + let mut current = LfuModel::new(3); + assert_models_agree(&mut naive, &mut current, &ops); +} + +#[test] +fn smoke_lfu() { + let ops = [ + Op::Insert(1), + Op::Get(1), + Op::Insert(2), + Op::Insert(3), + Op::Insert(4), + ]; + let mut cache = LfuCache::new(3); + let mut model = LfuModel::new(3); + run_ops(&mut cache, &mut model, &ops); +} diff --git a/tests/policy_semantics/lifo_tests.rs b/tests/policy_semantics/lifo_tests.rs new file mode 100644 index 0000000..97bb336 --- /dev/null +++ b/tests/policy_semantics/lifo_tests.rs @@ -0,0 +1,96 @@ +//! LIFO dual-run semantic oracle tests. +//! +//! **Model:** `LifoModel` · **Op strategy:** `standard_op_list` +//! **Asserted:** residency, `peek_victim` +//! +//! Cross-model: `NaiveLifoModel` vs `LifoModel`. naive ≠ exact → fix spec or model; naive = exact +//! but impl fails → fix implementation or adapter. + +use cachekit::policy::lifo::LifoCore; +use cachekit::traits::{Cache, EvictingCache}; +use proptest::prelude::*; + +use crate::abstract_models::driver::{assert_dual_run_step, assert_models_agree}; +use crate::abstract_models::exact::lifo::LifoModel; +use crate::abstract_models::reference::lifo::NaiveLifoModel; +use crate::abstract_models::{Op, PolicyModel, standard_capacity, standard_op_list}; + +fn run_ops(cache: &mut LifoCore, model: &mut LifoModel, ops: &[Op]) { + for op in ops { + let step = model.apply(op.clone()); + match op { + Op::Insert(k) => { + cache.insert(*k, *k); + }, + Op::Get(k) => { + let _ = cache.get(k); + }, + Op::Peek(k) => { + let _ = cache.peek(k); + }, + Op::GetMut(_) | Op::Touch(_) => {}, + Op::Remove(k) => { + cache.remove(k); + }, + Op::EvictOne => { + let _ = cache.evict_one(); + }, + } + assert_dual_run_step(cache, model, &step, |k| cache.contains(k), |_, _, _| {}); + } +} + +proptest! { + #![proptest_config(ProptestConfig { cases: 256, ..ProptestConfig::default() })] + + #[cfg_attr(miri, ignore)] + #[test] + fn prop_lifo_naive_matches_current_model( + capacity in standard_capacity(), + ops in standard_op_list(), + ) { + let mut naive = NaiveLifoModel::new(capacity); + let mut current = LifoModel::new(capacity); + assert_models_agree(&mut naive, &mut current, &ops); + } + + #[cfg_attr(miri, ignore)] + #[test] + fn prop_lifo_matches_model(capacity in standard_capacity(), ops in standard_op_list()) { + let mut cache = LifoCore::new(capacity); + let mut model = LifoModel::new(capacity); + run_ops(&mut cache, &mut model, &ops); + } +} + +#[test] +fn smoke_lifo_naive_agreement() { + let ops = [ + Op::Insert(1), + Op::Insert(2), + Op::Insert(3), + Op::Insert(4), + Op::EvictOne, + Op::Get(2), + Op::Remove(2), + ]; + let mut naive = NaiveLifoModel::new(3); + let mut current = LifoModel::new(3); + assert_models_agree(&mut naive, &mut current, &ops); +} + +#[test] +fn smoke_lifo() { + let ops = [ + Op::Insert(1), + Op::Insert(2), + Op::Insert(3), + Op::Insert(4), + Op::EvictOne, + Op::Get(2), + Op::Remove(2), + ]; + let mut cache = LifoCore::new(3); + let mut model = LifoModel::new(3); + run_ops(&mut cache, &mut model, &ops); +} diff --git a/tests/policy_semantics/lru_k_tests.rs b/tests/policy_semantics/lru_k_tests.rs new file mode 100644 index 0000000..179ba46 --- /dev/null +++ b/tests/policy_semantics/lru_k_tests.rs @@ -0,0 +1,104 @@ +//! LRU-K dual-run semantic oracle tests. +//! +//! **Model:** `LruKModel` · **Op strategy:** `standard_op_list` +//! **Asserted:** residency, `peek_victim`, access count +//! +//! Cross-model: `NaiveLruKModel` vs `LruKModel`. naive ≠ exact → fix spec or model; naive = exact +//! but impl fails → fix implementation or adapter. + +use cachekit::policy::lru_k::LrukCache; +use cachekit::traits::{Cache, EvictingCache}; +use proptest::prelude::*; + +use crate::abstract_models::driver::{assert_dual_run_step, assert_models_agree}; +use crate::abstract_models::exact::lru_k::LruKModel; +use crate::abstract_models::reference::lru_k::NaiveLruKModel; +use crate::abstract_models::{Op, PolicyModel, standard_capacity, standard_op_list}; + +const K: usize = 2; + +fn run_ops(cache: &mut LrukCache, model: &mut LruKModel, ops: &[Op]) { + for op in ops { + let step = model.apply(op.clone()); + match op { + Op::Insert(k) => { + cache.insert(*k, *k); + }, + Op::Get(k) => { + let _ = cache.get(k); + }, + Op::Peek(k) => { + let _ = cache.peek(k); + }, + Op::GetMut(_) | Op::Touch(_) => {}, + Op::Remove(k) => { + cache.remove(k); + }, + Op::EvictOne => { + let _ = cache.evict_one(); + }, + } + assert_dual_run_step( + cache, + model, + &step, + |k| cache.contains(k), + |cache, model, step| { + for key in &step.resident { + assert_eq!(cache.access_count(key), model.access_count(key)); + } + }, + ); + } +} + +proptest! { + #![proptest_config(ProptestConfig { cases: 256, ..ProptestConfig::default() })] + + #[cfg_attr(miri, ignore)] + #[test] + fn prop_lru_k_naive_matches_current_model( + capacity in standard_capacity(), + ops in standard_op_list(), + ) { + let mut naive = NaiveLruKModel::new(capacity, K); + let mut current = LruKModel::new(capacity, K); + assert_models_agree(&mut naive, &mut current, &ops); + } + + #[cfg_attr(miri, ignore)] + #[test] + fn prop_lru_k_matches_model(capacity in standard_capacity(), ops in standard_op_list()) { + let mut cache = LrukCache::with_k(capacity, K); + let mut model = LruKModel::new(capacity, K); + run_ops(&mut cache, &mut model, &ops); + } +} + +#[test] +fn smoke_lru_k_naive_agreement() { + let ops = [ + Op::Insert(1), + Op::Get(1), + Op::Insert(2), + Op::Insert(3), + Op::Insert(4), + ]; + let mut naive = NaiveLruKModel::new(3, K); + let mut current = LruKModel::new(3, K); + assert_models_agree(&mut naive, &mut current, &ops); +} + +#[test] +fn smoke_lru_k() { + let ops = [ + Op::Insert(1), + Op::Get(1), + Op::Insert(2), + Op::Insert(3), + Op::Insert(4), + ]; + let mut cache = LrukCache::with_k(3, K); + let mut model = LruKModel::new(3, K); + run_ops(&mut cache, &mut model, &ops); +} diff --git a/tests/policy_semantics/lru_tests.rs b/tests/policy_semantics/lru_tests.rs new file mode 100644 index 0000000..8393650 --- /dev/null +++ b/tests/policy_semantics/lru_tests.rs @@ -0,0 +1,149 @@ +//! LRU (`LruCore`) dual-run semantic oracle tests. +//! +//! **Model:** `LruOccupancyModel` · **Op strategy:** `standard_op_list` +//! **Asserted:** residency, `peek_victim`, recency rank (peek must not promote) + +use std::sync::Arc; + +use cachekit::policy::lru::LruCore; +use cachekit::traits::{Cache, EvictingCache, VictimInspectable}; +use proptest::prelude::*; + +use crate::abstract_models::driver::{ + assert_dual_run_step, assert_models_agree_with_recency, assert_recency_rank, +}; +use crate::abstract_models::exact::lru::LruOccupancyModel; +use crate::abstract_models::reference::lru::NaiveLruModel; +use crate::abstract_models::{Op, PolicyModel, standard_capacity, standard_op_list}; + +fn run_ops(cache: &mut LruCore, model: &mut LruOccupancyModel, ops: &[Op]) { + for op in ops { + let rank_before = match op { + Op::Peek(k) => cache.recency_rank(k), + _ => None, + }; + + let step = model.apply(op.clone()); + + match op { + Op::Insert(k) => { + cache.insert(*k, Arc::new(*k)); + }, + Op::Get(k) => { + let _ = cache.get(k); + }, + Op::Peek(k) => { + let _ = cache.peek(k); + }, + Op::GetMut(_) => {}, + Op::Touch(k) => { + cache.touch(k); + }, + Op::Remove(k) => { + cache.remove(k); + }, + Op::EvictOne => { + if let Some((expected, _)) = cache.peek_victim() { + let key = *expected; + let evicted = cache.evict_one(); + assert_eq!(evicted.map(|(k, _)| k), Some(key)); + } else { + assert!(cache.evict_one().is_none()); + } + }, + } + + assert_dual_run_step( + cache, + model, + &step, + |k| cache.contains(k), + |cache, model, step| { + if let Op::Peek(k) = op { + if let Some(rank) = rank_before { + assert_eq!(cache.recency_rank(k), Some(rank)); + } + } + + if matches!(op, Op::Get(_) | Op::Touch(_)) { + if let Some(k) = op_key(op) { + assert_recency_rank(cache, model.model_recency_rank(k), k); + } + } + + if let Some(evicted) = &step.evicted_on_insert { + assert!(!cache.contains(evicted)); + } + }, + ); + } +} + +fn op_key(op: &Op) -> Option<&u8> { + match op { + Op::Get(k) | Op::Peek(k) | Op::Touch(k) => Some(k), + _ => None, + } +} + +proptest! { + #![proptest_config(ProptestConfig { cases: 256, ..ProptestConfig::default() })] + + #[cfg_attr(miri, ignore)] + #[test] + fn prop_lru_naive_matches_current_model( + capacity in standard_capacity(), + ops in standard_op_list(), + ) { + let mut naive = NaiveLruModel::new(capacity); + let mut current = LruOccupancyModel::new(capacity); + assert_models_agree_with_recency(&mut naive, &mut current, &ops); + } + + #[cfg_attr(miri, ignore)] + #[test] + fn prop_lru_core_matches_model( + capacity in standard_capacity(), + ops in standard_op_list(), + ) { + let mut cache = LruCore::new(capacity); + let mut model = LruOccupancyModel::new(capacity); + run_ops(&mut cache, &mut model, &ops); + } +} + +#[test] +fn smoke_lru_naive_agreement() { + let ops = [ + Op::Insert(1), + Op::Insert(2), + Op::Insert(3), + Op::Get(1), + Op::Peek(2), + Op::Touch(3), + Op::Insert(4), + Op::EvictOne, + Op::Remove(2), + ]; + let mut naive = NaiveLruModel::new(3); + let mut current = LruOccupancyModel::new(3); + assert_models_agree_with_recency(&mut naive, &mut current, &ops); +} + +#[test] +fn smoke_lru_core() { + let ops = [ + Op::Insert(1), + Op::Insert(2), + Op::Insert(3), + Op::Get(1), + Op::Peek(2), + Op::Touch(3), + Op::Insert(4), + Op::EvictOne, + Op::Remove(2), + ]; + let mut cache = LruCore::new(3); + let mut model = LruOccupancyModel::new(3); + run_ops(&mut cache, &mut model, &ops); +} diff --git a/tests/policy_semantics/main.rs b/tests/policy_semantics/main.rs new file mode 100644 index 0000000..8623c16 --- /dev/null +++ b/tests/policy_semantics/main.rs @@ -0,0 +1,52 @@ +//! Policy semantic proptests (abstract interpretation oracles). +//! +//! Two test styles: +//! - **Dual-run** (exact/mirror) — `PolicyModel::apply` vs real cache each step +//! - **Invariant-only** (bounded) — `debug_validate_invariants` / `check_invariants` only +//! +//! See [`abstract_models/README.md`](../abstract_models/README.md) for the policy matrix. +//! +//! ```bash +//! cargo test --test policy_semantics --all-features +//! PROPTEST_CASES=1000 cargo test --test policy_semantics --all-features +//! cargo miri test --test policy_semantics --all-features smoke_ -- --test-threads=1 +//! ``` + +#[path = "../abstract_models/mod.rs"] +mod abstract_models; + +#[cfg(feature = "policy-arc")] +mod arc_tests; +#[cfg(feature = "policy-car")] +mod car_tests; +#[cfg(feature = "policy-clock-pro")] +mod clock_pro_tests; +#[cfg(feature = "policy-clock")] +mod clock_tests; +mod dual_impl_tests; +#[cfg(feature = "policy-fast-lru")] +mod fast_lru_tests; +#[cfg(feature = "policy-fifo")] +mod fifo_tests; +#[cfg(feature = "policy-heap-lfu")] +mod heap_lfu_tests; +#[cfg(feature = "policy-lfu")] +mod lfu_tests; +#[cfg(feature = "policy-lifo")] +mod lifo_tests; +#[cfg(feature = "policy-lru-k")] +mod lru_k_tests; +#[cfg(feature = "policy-lru")] +mod lru_tests; +#[cfg(feature = "policy-mfu")] +mod mfu_tests; +#[cfg(feature = "policy-mru")] +mod mru_tests; +#[cfg(feature = "policy-nru")] +mod nru_tests; +#[cfg(feature = "policy-s3-fifo")] +mod s3_fifo_tests; +#[cfg(feature = "policy-slru")] +mod slru_tests; +#[cfg(feature = "policy-two-q")] +mod two_q_tests; diff --git a/tests/policy_semantics/mfu_tests.rs b/tests/policy_semantics/mfu_tests.rs new file mode 100644 index 0000000..bdc11c8 --- /dev/null +++ b/tests/policy_semantics/mfu_tests.rs @@ -0,0 +1,95 @@ +//! MFU dual-run semantic oracle tests. +//! +//! **Model:** `MfuModel` · **Op strategy:** `standard_op_list_mfu_safe` +//! **Asserted:** residency only (skips `Remove`/`EvictOne` to avoid stale heap) +//! +//! Cross-model: `NaiveMfuModel` vs `MfuModel`. naive ≠ exact → fix spec or model; naive = exact +//! but impl fails → fix implementation or adapter. + +use cachekit::policy::mfu::MfuCore; +use proptest::prelude::*; + +use crate::abstract_models::driver::{assert_dual_run_step_no_victim, assert_models_agree}; +use crate::abstract_models::exact::mfu::MfuModel; +use crate::abstract_models::reference::mfu::NaiveMfuModel; +use crate::abstract_models::{Op, PolicyModel, standard_capacity, standard_op_list_mfu_safe}; + +fn run_ops(cache: &mut MfuCore, model: &mut MfuModel, ops: &[Op]) { + for op in ops { + let step = model.apply(op.clone()); + match op { + Op::Insert(k) => { + cache.insert(*k, *k); + }, + Op::Get(k) => { + let _ = cache.get(k); + }, + Op::Peek(k) => { + let _ = cache.peek(k); + }, + Op::GetMut(_) | Op::Touch(_) | Op::Remove(_) | Op::EvictOne => {}, + } + assert_dual_run_step_no_victim(cache, model, &step, |k| cache.contains(k), |_, _, _| {}); + } +} + +proptest! { + #![proptest_config(ProptestConfig { cases: 256, ..ProptestConfig::default() })] + + #[cfg_attr(miri, ignore)] + #[test] + fn prop_mfu_naive_matches_current_model( + capacity in standard_capacity(), + ops in standard_op_list_mfu_safe(), + ) { + let mut naive = NaiveMfuModel::new(capacity); + let mut current = MfuModel::new(capacity); + assert_models_agree(&mut naive, &mut current, &ops); + } + + #[cfg_attr(miri, ignore)] + #[test] + fn prop_mfu_matches_model(capacity in standard_capacity(), ops in standard_op_list_mfu_safe()) { + let mut cache = MfuCore::new(capacity); + let mut model = MfuModel::new(capacity); + run_ops(&mut cache, &mut model, &ops); + } +} + +#[test] +fn smoke_mfu_naive_agreement() { + let ops = [ + Op::Insert(1), + Op::Get(1), + Op::Get(1), + Op::Insert(2), + Op::Insert(3), + Op::Insert(4), + ]; + let mut naive = NaiveMfuModel::new(3); + let mut current = MfuModel::new(3); + assert_models_agree(&mut naive, &mut current, &ops); +} + +#[test] +fn smoke_mfu_reinsert_after_update() { + let ops = [Op::Insert(140), Op::Insert(140), Op::Insert(0)]; + let mut cache = MfuCore::new(1); + let mut model = MfuModel::new(1); + run_ops(&mut cache, &mut model, &ops); +} + +#[test] +fn smoke_mfu() { + let ops = [ + Op::Insert(1), + Op::Get(1), + Op::Get(1), + Op::Insert(2), + Op::Insert(3), + Op::Insert(4), + ]; + let mut cache = MfuCore::new(3); + let mut model = MfuModel::new(3); + run_ops(&mut cache, &mut model, &ops); +} diff --git a/tests/policy_semantics/mru_tests.rs b/tests/policy_semantics/mru_tests.rs new file mode 100644 index 0000000..a743b56 --- /dev/null +++ b/tests/policy_semantics/mru_tests.rs @@ -0,0 +1,107 @@ +//! MRU dual-run semantic oracle tests. +//! +//! **Model:** `MruModel` · **Op strategy:** `standard_op_list` +//! **Asserted:** residency, insert eviction +//! +//! Cross-model: `NaiveMruModel` vs `MruModel`. naive ≠ exact → fix spec or model; naive = exact +//! but impl fails → fix implementation or adapter. + +use cachekit::policy::mru::MruCore; +use cachekit::traits::EvictingCache; +use proptest::prelude::*; + +use crate::abstract_models::driver::{ + assert_dual_run_step_no_victim, assert_models_agree, probe_resident, +}; +use crate::abstract_models::exact::mru::MruModel; +use crate::abstract_models::reference::mru::NaiveMruModel; +use crate::abstract_models::{Op, PolicyModel, standard_capacity, standard_op_list}; + +fn run_ops(cache: &mut MruCore, model: &mut MruModel, ops: &[Op]) { + for op in ops { + let before = probe_resident(|k| cache.contains(k)); + let step = model.apply(op.clone()); + match op { + Op::Insert(k) => { + cache.insert(*k, *k); + }, + Op::Get(k) => { + let _ = cache.get(k); + }, + Op::Peek(k) => { + let _ = cache.peek(k); + }, + Op::GetMut(_) | Op::Touch(_) => {}, + Op::EvictOne => { + let _ = cache.evict_one(); + }, + Op::Remove(k) => { + cache.remove(k); + }, + } + assert_dual_run_step_no_victim( + cache, + model, + &step, + |k| cache.contains(k), + |cache, _, step| { + if let (Op::Insert(k), Some(evicted)) = (op, &step.evicted_on_insert) { + if !before.contains(k) { + assert!(!cache.contains(evicted)); + } + } + }, + ); + } +} + +proptest! { + #![proptest_config(ProptestConfig { cases: 256, ..ProptestConfig::default() })] + + #[cfg_attr(miri, ignore)] + #[test] + fn prop_mru_naive_matches_current_model( + capacity in standard_capacity(), + ops in standard_op_list(), + ) { + let mut naive = NaiveMruModel::new(capacity); + let mut current = MruModel::new(capacity); + assert_models_agree(&mut naive, &mut current, &ops); + } + + #[cfg_attr(miri, ignore)] + #[test] + fn prop_mru_matches_model(capacity in standard_capacity(), ops in standard_op_list()) { + let mut cache = MruCore::new(capacity); + let mut model = MruModel::new(capacity); + run_ops(&mut cache, &mut model, &ops); + } +} + +#[test] +fn smoke_mru_naive_agreement() { + let ops = [ + Op::Insert(1), + Op::Get(1), + Op::Insert(2), + Op::Insert(3), + Op::Insert(4), + ]; + let mut naive = NaiveMruModel::new(3); + let mut current = MruModel::new(3); + assert_models_agree(&mut naive, &mut current, &ops); +} + +#[test] +fn smoke_mru() { + let ops = [ + Op::Insert(1), + Op::Get(1), + Op::Insert(2), + Op::Insert(3), + Op::Insert(4), + ]; + let mut cache = MruCore::new(3); + let mut model = MruModel::new(3); + run_ops(&mut cache, &mut model, &ops); +} diff --git a/tests/policy_semantics/nru_tests.rs b/tests/policy_semantics/nru_tests.rs new file mode 100644 index 0000000..6771ca9 --- /dev/null +++ b/tests/policy_semantics/nru_tests.rs @@ -0,0 +1,60 @@ +//! NRU dual-run semantic oracle tests. +//! +//! **Model:** `NruModel` · **Op strategy:** `short_op_list_no_evict` +//! **Asserted:** residency only (O(n) eviction; no `EvictingCache`) + +use cachekit::policy::nru::NruCache; +use cachekit::traits::Cache; +use proptest::prelude::*; + +use crate::abstract_models::driver::assert_dual_run_step_no_victim; +use crate::abstract_models::exact::nru::NruModel; +use crate::abstract_models::{Op, PolicyModel, short_op_list_no_evict, standard_capacity}; + +fn run_ops(cache: &mut NruCache, model: &mut NruModel, ops: &[Op]) { + for op in ops { + let step = model.apply(op.clone()); + match op { + Op::Insert(k) => { + cache.insert(*k, *k); + }, + Op::Get(k) => { + let _ = cache.get(k); + }, + Op::Peek(k) => { + let _ = cache.peek(k); + }, + Op::GetMut(_) | Op::Touch(_) | Op::EvictOne => {}, + Op::Remove(k) => { + cache.remove(k); + }, + } + assert_dual_run_step_no_victim(cache, model, &step, |k| cache.contains(k), |_, _, _| {}); + } +} + +proptest! { + #![proptest_config(ProptestConfig { cases: 256, ..ProptestConfig::default() })] + + #[cfg_attr(miri, ignore)] + #[test] + fn prop_nru_matches_model(capacity in standard_capacity(), ops in short_op_list_no_evict()) { + let mut cache = NruCache::new(capacity); + let mut model = NruModel::new(capacity); + run_ops(&mut cache, &mut model, &ops); + } +} + +#[test] +fn smoke_nru() { + let ops = [ + Op::Insert(1), + Op::Insert(2), + Op::Get(1), + Op::Insert(3), + Op::Insert(4), + ]; + let mut cache = NruCache::new(3); + let mut model = NruModel::new(3); + run_ops(&mut cache, &mut model, &ops); +} diff --git a/tests/policy_semantics/s3_fifo_tests.rs b/tests/policy_semantics/s3_fifo_tests.rs new file mode 100644 index 0000000..9c5a36c --- /dev/null +++ b/tests/policy_semantics/s3_fifo_tests.rs @@ -0,0 +1,67 @@ +//! S3-FIFO invariant-only semantic tests (no `PolicyModel` dual-run). +//! +//! **Model:** none · **Op strategy:** `op_strategy_with_get_mut` (0..80) +//! **Asserted:** `len <= capacity`, `check_invariants`, smoke residency bound + +use cachekit::policy::s3_fifo::S3FifoCache; +use proptest::prelude::*; + +use crate::abstract_models::driver::{probe_resident, run_invariant_trace}; +use crate::abstract_models::{Op, op_strategy_with_get_mut, standard_capacity}; + +fn apply_s3_fifo_op(cache: &mut S3FifoCache, op: Op) { + match op { + Op::Insert(k) => { + cache.insert(k, k); + }, + Op::Get(k) => { + let _ = cache.get(&k); + }, + Op::Peek(k) => { + let _ = cache.peek(&k); + }, + Op::GetMut(k) => { + let _ = cache.get_mut(&k); + }, + Op::Touch(_) | Op::EvictOne => {}, + Op::Remove(k) => { + cache.remove(&k); + }, + } +} + +fn run_ops(cache: &mut S3FifoCache, ops: &[Op]) { + run_invariant_trace(cache, ops, apply_s3_fifo_op, |cache| { + #[cfg(debug_assertions)] + cache.check_invariants().expect("s3-fifo invariants"); + }); +} + +proptest! { + #![proptest_config(ProptestConfig { cases: 256, ..ProptestConfig::default() })] + + #[cfg_attr(miri, ignore)] + #[test] + fn prop_s3_fifo_invariants( + capacity in standard_capacity(), + ops in prop::collection::vec(op_strategy_with_get_mut(), 0..80), + ) { + let mut cache = S3FifoCache::new(capacity); + run_ops(&mut cache, &ops); + } +} + +#[test] +fn smoke_s3_fifo() { + let ops = [ + Op::Insert(1), + Op::GetMut(1), + Op::Insert(2), + Op::Insert(3), + Op::Insert(4), + ]; + let mut cache = S3FifoCache::new(3); + run_ops(&mut cache, &ops); + let resident = probe_resident(|k| cache.contains(k)); + assert!(resident.len() <= cache.capacity()); +} diff --git a/tests/policy_semantics/slru_tests.rs b/tests/policy_semantics/slru_tests.rs new file mode 100644 index 0000000..a943da7 --- /dev/null +++ b/tests/policy_semantics/slru_tests.rs @@ -0,0 +1,55 @@ +//! SLRU dual-run semantic oracle tests. +//! +//! **Model:** `SlruModel` · **Op strategy:** `standard_op_list_no_evict` +//! **Asserted:** residency only (no `EvictingCache`) + +use cachekit::policy::slru::SlruCore; +use proptest::prelude::*; + +use crate::abstract_models::driver::assert_dual_run_step_no_victim; +use crate::abstract_models::exact::slru::SlruModel; +use crate::abstract_models::{Op, PolicyModel, standard_capacity, standard_op_list_no_evict}; + +const PROBATIONARY_FRAC: f64 = 0.25; + +fn run_ops(cache: &mut SlruCore, model: &mut SlruModel, ops: &[Op]) { + for op in ops { + let step = model.apply(op.clone()); + match op { + Op::Insert(k) => { + cache.insert(*k, *k); + }, + Op::Get(k) => { + let _ = cache.get(k); + }, + Op::Peek(k) => { + let _ = cache.peek(k); + }, + Op::GetMut(_) | Op::Touch(_) | Op::EvictOne => {}, + Op::Remove(k) => { + cache.remove(k); + }, + } + assert_dual_run_step_no_victim(cache, model, &step, |k| cache.contains(k), |_, _, _| {}); + } +} + +proptest! { + #![proptest_config(ProptestConfig { cases: 256, ..ProptestConfig::default() })] + + #[cfg_attr(miri, ignore)] + #[test] + fn prop_slru_matches_model(capacity in standard_capacity(), ops in standard_op_list_no_evict()) { + let mut cache = SlruCore::new(capacity, PROBATIONARY_FRAC); + let mut model = SlruModel::new(capacity, PROBATIONARY_FRAC); + run_ops(&mut cache, &mut model, &ops); + } +} + +#[test] +fn smoke_slru() { + let ops = [Op::Insert(1), Op::Get(1), Op::Insert(2), Op::Insert(3)]; + let mut cache = SlruCore::new(4, 0.25); + let mut model = SlruModel::new(4, 0.25); + run_ops(&mut cache, &mut model, &ops); +} diff --git a/tests/policy_semantics/two_q_tests.rs b/tests/policy_semantics/two_q_tests.rs new file mode 100644 index 0000000..56ae35e --- /dev/null +++ b/tests/policy_semantics/two_q_tests.rs @@ -0,0 +1,61 @@ +//! 2Q dual-run semantic oracle tests. +//! +//! **Model:** `TwoQModel` · **Op strategy:** `standard_op_list_no_evict` +//! **Asserted:** residency only (no `EvictingCache`) + +use cachekit::policy::two_q::TwoQCore; +use proptest::prelude::*; + +use crate::abstract_models::driver::assert_dual_run_step_no_victim; +use crate::abstract_models::exact::two_q::TwoQModel; +use crate::abstract_models::{Op, PolicyModel, standard_capacity, standard_op_list_no_evict}; + +const PROBATION_FRAC: f64 = 0.25; + +fn run_ops(cache: &mut TwoQCore, model: &mut TwoQModel, ops: &[Op]) { + for op in ops { + let step = model.apply(op.clone()); + match op { + Op::Insert(k) => { + cache.insert(*k, *k); + }, + Op::Get(k) => { + let _ = cache.get(k); + }, + Op::Peek(k) => { + let _ = cache.peek(k); + }, + Op::GetMut(_) | Op::Touch(_) | Op::EvictOne => {}, + Op::Remove(k) => { + cache.remove(k); + }, + } + assert_dual_run_step_no_victim(cache, model, &step, |k| cache.contains(k), |_, _, _| {}); + } +} + +proptest! { + #![proptest_config(ProptestConfig { cases: 256, ..ProptestConfig::default() })] + + #[cfg_attr(miri, ignore)] + #[test] + fn prop_two_q_matches_model(capacity in standard_capacity(), ops in standard_op_list_no_evict()) { + let mut cache = TwoQCore::new(capacity, PROBATION_FRAC); + let mut model = TwoQModel::new(capacity, PROBATION_FRAC); + run_ops(&mut cache, &mut model, &ops); + } +} + +#[test] +fn smoke_two_q() { + let ops = [ + Op::Insert(1), + Op::Get(1), + Op::Insert(2), + Op::Insert(3), + Op::Insert(4), + ]; + let mut cache = TwoQCore::new(5, 0.4); + let mut model = TwoQModel::new(5, 0.4); + run_ops(&mut cache, &mut model, &ops); +} diff --git a/tests/proptest-regressions/lfu_tests.txt b/tests/proptest-regressions/lfu_tests.txt new file mode 100644 index 0000000..66f4995 --- /dev/null +++ b/tests/proptest-regressions/lfu_tests.txt @@ -0,0 +1,7 @@ +# Seeds for failure cases proptest has generated in the past. It is +# automatically read and these particular cases re-run before any +# novel cases are generated. +# +# It is recommended to check this file in to source control so that +# everyone who runs the test benefits from these saved cases. +cc f72f930ec978aeef20e7fff4770cb0b26954eec56cafbacc009106bb7a3edf7f # shrinks to capacity = 2, ops = [Insert(58), EvictOne, Insert(0), Insert(58)] diff --git a/tests/ttl_integration_test.rs b/tests/ttl_integration_test.rs index 2c993db..0999a67 100644 --- a/tests/ttl_integration_test.rs +++ b/tests/ttl_integration_test.rs @@ -8,6 +8,9 @@ #![cfg(feature = "ttl")] +#[path = "abstract_models/mod.rs"] +mod abstract_models; + use std::time::Duration; use cachekit::builder::{CacheBuilder, CachePolicy}; @@ -202,7 +205,7 @@ fn dyn_expiring_cache_purge_expired_works_via_builder_path() { // --------------------------------------------------------------------------- mod proptests { - use std::collections::{HashMap, VecDeque}; + use std::collections::HashMap; use std::time::Duration; use cachekit::policy::expiring::Expiring; @@ -211,107 +214,90 @@ mod proptests { use cachekit::traits::{Cache, ExpiringCache}; use proptest::prelude::*; + use crate::abstract_models::exact::lru::LruOccupancyModel; + use crate::abstract_models::{Op, PolicyModel}; + /// Operations the reference model and the cache will both execute. #[derive(Debug, Clone)] - enum Op { + enum TtlOp { Insert { key: u8, ttl_ms: u32 }, Get { key: u8 }, Advance { delta_ms: u32 }, Purge, } - /// Reference: same physical occupancy and LRU order as `FastLru` - /// (MRU at front of `lru`), plus deadlines mirroring - /// `Expiring::deadline_from`. - #[derive(Default)] + /// TTL reference: `LruOccupancyModel` for physical LRU order + deadline map. struct RefModel { - /// MRU at front, LRU at back — matches `FastLru` head/tail semantics. - lru: VecDeque, + lru: LruOccupancyModel, deadlines: HashMap, now: u64, - capacity: usize, } impl RefModel { fn new(capacity: usize) -> Self { Self { - capacity, - ..Default::default() + lru: LruOccupancyModel::new(capacity), + deadlines: HashMap::new(), + now: 0, } } fn insert(&mut self, key: u8, ttl_ms: u32) { if ttl_ms == 0 { self.deadlines.remove(&key); - self.lru.retain(|&k| k != key); + let _ = self.lru.apply(Op::Remove(key)); return; } - // Saturating arithmetic mirrors `Expiring::deadline_from`. let deadline = self.now.saturating_add(ttl_ms as u64).min(u64::MAX - 1); - let exists = self.lru.iter().any(|&k| k == key); - if exists { + if self.lru.resident_set().contains(&key) { self.deadlines.insert(key, deadline); - Self::touch_key(&mut self.lru, key); - return; - } - - if self.capacity == 0 { + self.lru.touch_key(key); return; } - while self.lru.len() >= self.capacity { - let Some(victim) = self.lru.pop_back() else { - break; - }; + let step = self.lru.apply(Op::Insert(key)); + if let Some(victim) = step.evicted_on_insert { self.deadlines.remove(&victim); } - self.deadlines.insert(key, deadline); - self.lru.push_front(key); } fn advance(&mut self, delta_ms: u32) { self.now = self.now.saturating_add(delta_ms as u64); } - /// Mirror `Expiring::get` + `FastLru::get`: purge expired residents or - /// promote live hits to MRU. fn observe_get(&mut self, key: u8) { - if !self.lru.iter().any(|&k| k == key) { + if !self.lru.resident_set().contains(&key) { return; } let expired = match self.deadlines.get(&key) { Some(&d) => d <= self.now, None => { - self.lru.retain(|&k| k != key); + let _ = self.lru.apply(Op::Remove(key)); return; }, }; if expired { self.deadlines.remove(&key); - self.lru.retain(|&k| k != key); + let _ = self.lru.apply(Op::Remove(key)); } else { - Self::touch_key(&mut self.lru, key); + self.lru.touch_key(key); } } - fn touch_key(lru: &mut VecDeque, key: u8) { - lru.retain(|&k| k != key); - lru.push_front(key); - } - - /// Apply `purge_expired`-style removal for deadlines `<= now`. fn purge_dead_expired(&mut self) { let now = self.now; self.deadlines.retain(|_, d| *d > now); - self.lru.retain(|k| self.deadlines.contains_key(k)); + for key in self.lru.resident_set().iter().copied().collect::>() { + if !self.deadlines.contains_key(&key) { + let _ = self.lru.apply(Op::Remove(key)); + } + } } - /// `Some(true)` if the key is physically resident with deadline `> now`; - /// `Some(false)` if resident but expired; `None` if not physically present. fn is_definitely_live(&self, key: u8) -> Option { - if !self.lru.iter().any(|&k| k == key) { + if !self.lru.resident_set().contains(&key) { return None; } match self.deadlines.get(&key) { @@ -322,12 +308,12 @@ mod proptests { } } - fn op_strategy() -> impl Strategy { + fn op_strategy() -> impl Strategy { prop_oneof![ - (any::(), 1u32..2_000).prop_map(|(k, t)| Op::Insert { key: k, ttl_ms: t }), - any::().prop_map(|k| Op::Get { key: k }), - (1u32..500).prop_map(|d| Op::Advance { delta_ms: d }), - Just(Op::Purge), + (any::(), 1u32..2_000).prop_map(|(k, t)| TtlOp::Insert { key: k, ttl_ms: t }), + any::().prop_map(|k| TtlOp::Get { key: k }), + (1u32..500).prop_map(|d| TtlOp::Advance { delta_ms: d }), + Just(TtlOp::Purge), ] } @@ -346,11 +332,11 @@ mod proptests { for op in ops { match op { - Op::Insert { key, ttl_ms } => { + TtlOp::Insert { key, ttl_ms } => { cache.insert_with_ttl(key, (), Duration::from_millis(ttl_ms as u64)); model.insert(key, ttl_ms); } - Op::Get { key } => { + TtlOp::Get { key } => { let hit = cache.get(&key).is_some(); if let Some(true) = model.is_definitely_live(key) { prop_assert!( @@ -366,11 +352,11 @@ mod proptests { } model.observe_get(key); } - Op::Advance { delta_ms } => { + TtlOp::Advance { delta_ms } => { cache.clock().advance(Duration::from_millis(delta_ms as u64)); model.advance(delta_ms); } - Op::Purge => { + TtlOp::Purge => { let _ = cache.purge_expired(); model.purge_dead_expired(); }