15.4. Offline caching

This section formalizes the offline caching problem of CLRS §15.4 and the farthest-in-future (Belady) eviction policy: the cache model with policies, hits and misses, the next-use function, the farthest-in-future selection, and the finite-trace exchange proof that the policy is optimal.

Main results:

• Policy / Policy.step / misses: the caching model (CLRS §15.4)

• nextUse: the next request position of a page at or after a position

• Farther: the "at least as far in the future" order

• farthestInFuture cache σ i: the resident page whose next use is farthest

• fifoPolicy σ: the farthest-in-future eviction policy

• fifo_step_of_mem / fifo_step_fault: the policy's cache transitions

• LegalTrace: a policy-independent certificate for a legal cache execution

• fifo_optimal: for every nonempty initial cache and finite request sequence, the farthest-in-future policy incurs no more misses than any policy (CLRS Theorem 15.5)

Completion boundary:

• The mathematical offline-caching optimality theorem is complete. The result is stated for finite request lists and a nonempty finite initial cache. Pointer-level cache mutation, RAM costs, and hardware caching behavior are separate implementation refinements and are not claimed here.

Notation conventions used in this section:

• C : cache (a Finset Page of resident pages)

• σ : request sequence

• i : position of the fault

• π : eviction policy

Implementation details

The section is split into the following sub-modules:

• Cache Model

• Farthest-In-Future Eviction

• Optimality

• Optimality proof overview

• Trace-coupling proof

• Legal cache traces

• Exact one-page cache difference

• Recursive coupling core

• Coupling correctness

• One-step FIF exchange

• Finite exchange iteration