Reduce repeated decoding and codec admission in summary histories
The 32-case summary property repeatedly decodes identical authenticated filesystem pages and checks each codec charge twice. Reuse the existing bounded decoded cache in LogicalObjectStore, avoid hot budget copies, and let the codec's atomic charge perform its own admission. All generated inputs, real parent turns, capture/publication/authenticated reads, 32 cases and shrinking are unchanged.
Profile
The original per-case profile measured 6.705 s: parent creation/compaction 3.975 s (59.3%), capture 1.192 s, publication 0.545 s, preparation 0.414 s, summary authentication 0.170 s and child reads 0.124 s. Of 350 subsequent debugger samples, 198 were under parent turns, including 122 in staging and 67 in path resolution. Repeated decoded-page work was one concrete cost. After caching, parent decode samples fell from 16 to 1 in a later diagnostic profile. A further 500-sample profile of the cache/copy candidate found JSON Writer in 77 samples, codec charging in 59, its preflight/charge helper in 56, WorkCounters admission in 31 and memcpy in 44. These samples locate work; timings below measure the gain.
Decisions
- Parent histories are not equivalent: all five generated strings enter their actual inputs, responses and compaction. Sharing a completed parent would lose that coverage, so the fixture is unchanged.
- Share the existing disposable decoded cache across store clones, with its existing 4,096-entry/256 MiB defaults. Keys retain object identity, decoder type and decode limits. Changing the provider object-byte limit creates a fresh cache so a warm hit cannot bypass a tighter limit. Cold admission uses the existing shared-owner custody charges; authority results are not cached.
- Inline the three profiled accounting bridges. Replace two full standalone-budget tuple queries used only as native-mode predicates with the existing native-work predicate. Codec charging already checks cancellation, scope and allowance before updating the ledger under its guard; remove its redundant separate preflight. Keep direct native charging so an exhausted allocation allowance returns the original typed denial.
- Move unchanged cache I/O bodies into private modules to keep touched source under 800 lines. Its actual mutex uses the crate-local sync shim. Cache/view precedes retained payload custody; no cache guard spans provider I/O.
- The exhaustive Loom model uses two actors, two immutable identities and one-entry/eight-byte residency. One actor publishes; the other looks up the distinct identity then publishes. One entry forces eviction at the first distinct replacement. Additional admissions serialize through the same mutex; larger residency repeats eviction inside that guard. Join precedes terminal observations. No preemption or exploration caps. The claim covers decoded identity/admission/eviction, not backend I/O-flight wakeups.
- Independent input oracles cover LRU histories (Vec identities, 64 shrinking histories with mandatory hits/misses/limit separation/eviction/clear) and codec counters (64 shrinking cases, owned/native histories, complete receipt after every event, cancellation/denial/overflow). Controls alias identity, omit eviction, split the capacity check/insertion, reuse a narrowed store's cache, omit/double a codec charge, or mutate a rejection. Every control's targeted assertion was deleted in a diagnostic copy; the corresponding fault then completed.
Paired bb1 timings
20 alternating pairs, seeds 750-769, normal repository debug/test profile, all 32 generated histories and shrinking per arm. Empirical nearest-rank p95. The property is faster in 20/20 pairs; median paired reduction 32.4%.
| Observation | Before | After |
|---|---|---|
| Generated property median | 7.966 s | 5.155 s |
| Generated property p95 | 11.248 s | 7.061 s |
| Generated property maximum | 13.652 s | 8.163 s |
| Full three-test filter median | 9.461 s | 6.359 s |
| Full three-test filter p95 | 13.299 s | 8.309 s |
| Full three-test filter maximum | 15.100 s | 10.721 s |
Including the six preceding codec-isolation measurements, all 26 updated property runs have p95 8.163 s and maximum 9.456 s. No updated property run reached 10 s. The earlier six-pair full-filter maximum was 11.258 s; that aggregate includes the original regression and negative-control test in addition to the generated property. It is retained rather than claimed below 10 s.
The before comparator is the saved native binary with temporary decoded-cache hooks disabled, before the accounting-copy/codec changes. It retains an empty cache constructor, so it is a controlled uncached-path comparator, not an unmodified-main binary. Both arms run identical property/regression source and generated seeds. Instrumentation and deletion copies are absent from committed source. Absolute updated p95/max come directly from the final binary.
All 20 paired runs (seconds)
| Seed | Property before | Property after | Full filter before | Full filter after |
|---|---|---|---|---|
| 750 | 10.124 | 5.013 | 11.857 | 6.280 |
| 751 | 13.652 | 4.826 | 15.100 | 5.948 |
| 752 | 7.018 | 4.557 | 8.646 | 5.651 |
| 753 | 8.160 | 4.476 | 9.495 | 5.467 |
| 754 | 7.195 | 4.711 | 8.617 | 5.710 |
| 755 | 6.939 | 4.678 | 8.275 | 5.673 |
| 756 | 6.957 | 5.267 | 8.367 | 6.228 |
| 757 | 7.673 | 5.521 | 9.267 | 6.678 |
| 758 | 7.696 | 7.061 | 9.117 | 8.309 |
| 759 | 9.328 | 4.921 | 10.850 | 6.024 |
| 760 | 8.227 | 8.163 | 9.906 | 10.721 |
| 761 | 7.413 | 5.200 | 8.862 | 6.438 |
| 762 | 7.906 | 5.996 | 9.427 | 7.310 |
| 763 | 11.248 | 4.873 | 12.655 | 5.989 |
| 764 | 8.172 | 5.610 | 9.902 | 6.823 |
| 765 | 9.752 | 5.242 | 11.209 | 6.457 |
| 766 | 10.422 | 5.915 | 13.299 | 6.958 |
| 767 | 8.026 | 6.781 | 10.187 | 7.929 |
| 768 | 7.411 | 5.027 | 8.847 | 6.106 |
| 769 | 7.139 | 5.111 | 8.599 | 6.647 |
Intermediate failures remain recorded: the cache-only candidate later took 11.467 s for the full filter; the cache/copy candidate reached 12.307 s for the property. Neither was published as solved. The final codec change addresses the remaining duplicated admission. The one-page retention prototype had no gain (8.578 -> 9.136 s median) and is excluded; #764 stays closed.
Validation
- Codec oracle/control module: 2 / 0.00585 s; assertion-deletion copy: 2 / 0.00549 s, including all six owned/native fault cases. Existing preparation tests: 4 / 0.012 s. Native allocation-prefix properties/regression: 3 tests, slowest 0.471 s; typed denials, physical allocation charges and retirement remain checked. Summary metadata: 9 / 0.026 s. Each paired run passes all three production-path publication tests, including the five existing controls.
- FS accounting/closure/adapter/cache histories: 1+23+6+2, each group below 0.015 s. Unchanged point/path/persistent-I/O/residency/native-custody/batch/flight groups pass below 0.013 s. LRU deletion: 2 / 0.004 s; adapter original/deletion: 4 / 0.006 s.
- Actual-lock Loom: 3 / 0.0060 s. Identity deletion: 3 / 0.0065 s; capacity deletion: 3 / 0.0076 s. Dedicated command:
cargo +nightly-2026-07-01 test --locked -p acyclic-fs --lib --features model-checking --no-run,RUSTFLAGS='--cfg acyclic_fs_loom --cfg acyclic_loom'(both required by the existing shared-backend guard). Those model/cache sources are unchanged by subsequent accounting/codec commits. - Final Windows GNU cross-check on bb1: passed in 82.1 s using repo-pinned stable 1.98.1,
cargo check --locked -p acyclic-harness -p acyclic-fs --lib --tests --features acyclic-harness/terminal,acyclic-harness/filesystem-local,acyclic-harness/native-execution,acyclic-harness/grpc,acyclic-harness/test-support,acyclic-harness/search-http --target x86_64-pc-windows-gnu. No local compile proof. The initial nightly cross-check lacked that toolchain's GNU std target and reached no source error. - Signed head
3d74fe350288236c4f5545e1df429b8b0bb47efd. Source is LF and within line limits. No renamed/removed API. Full paginated current #515/#526 paths checked; no overlap, including the activehistory.rs.
Summary by cubic
Previously, the 32-case summary property repeatedly decoded identical authenticated filesystem pages and charged each codec once; it now reuses a bounded decoded cache in LogicalObjectStore and lets the codec's atomic charge perform its own admission. Median property time falls from 7.97s to 5.16s in 20 paired runs.
Refactors
LogicalObjectStoreshares a bounded decoded cache; tightening the object-byte limit creates a fresh cache so a warm hit cannot bypass the new bound.- Cache keys retain object identity and decoder limits; authority results are not cached.
- Inlined accounting bridges avoid copying standalone budget state; native work predicates replace standalone-only tuple queries.
- Codec charging now performs its own admission under the ledger guard, removing the redundant preflight charge while keeping typed native denials.
- Added proptest histories for cache LRU and codec counters, plus Loom models and negative controls that fail when a cache mutation or codec charge is skipped.