Section 15.4 optimality: legal cache traces
This file separates the semantic notion of a legal cache execution from the
Policy representation. It is the first layer of the trace-coupling proof of
farthest-in-future optimality.
namespace CLRSopen Finsetopen scoped BigOperatorsnamespace Caching
A legal cache execution on σ, with cache states at request boundaries.
structure LegalTrace (C₀ : Finset Page) (σ : List Page) where
cache : ℕ → Finset Page
evict : ℕ → Page
init : cache 0 = C₀
step : ∀ t, t < σ.length →
cache (t + 1) =
if σ.getD t 0 ∈ cache t then cache t
else insert (σ.getD t 0) ((cache t).erase (evict t))
evict_mem : ∀ t, t < σ.length →
σ.getD t 0 ∉ cache t → evict t ∈ cache t
The miss indicator of a legal trace at request position t.
def traceFaultAt (T : LegalTrace C₀ σ) (t : ℕ) : ℕ :=
if σ.getD t 0 ∈ T.cache t then 0 else 1The total number of misses of a legal trace over the request sequence.
def traceMisses (T : LegalTrace C₀ σ) : ℕ :=
∑ t ∈ Finset.range σ.length, traceFaultAt T tOn a hit, a legal trace leaves the cache unchanged.
lemma LegalTrace.cache_succ_of_mem (T : LegalTrace C₀ σ)
(t : ℕ) (ht : t < σ.length) (hrequest : σ.getD t 0 ∈ T.cache t) :
T.cache (t + 1) = T.cache t := by
rw [T.step t ht, if_pos hrequest]On a fault, a legal trace evicts its recorded resident and loads the request.
lemma LegalTrace.cache_succ_of_not_mem (T : LegalTrace C₀ σ)
(t : ℕ) (ht : t < σ.length) (hrequest : σ.getD t 0 ∉ T.cache t) :
T.cache (t + 1) =
insert (σ.getD t 0) ((T.cache t).erase (T.evict t)) := by
rw [T.step t ht, if_neg hrequest]The legal trace generated by an eviction policy.
def policyTrace (π : Policy) (C₀ : Finset Page) (σ : List Page)
(hC₀ : C₀.Nonempty) : LegalTrace C₀ σ where
cache := cacheSeq π C₀ σ
evict := fun t => π.evict t (cacheSeq π C₀ σ t) (σ.getD t 0)
init := rfl
step := by
intro t _ht
rfl
evict_mem := by
intro t _ht hmiss
exact π.evict_mem t (cacheSeq π C₀ σ t) (σ.getD t 0) hmiss
(cacheSeq_nonempty π C₀ σ t hC₀)The legal trace generated by farthest-in-future.
noncomputable def fifoTrace (C₀ : Finset Page) (σ : List Page)
(hC₀ : C₀.Nonempty) : LegalTrace C₀ σ :=
policyTrace (fifoPolicy σ) C₀ σ hC₀A policy trace has the same pointwise miss indicator as the policy run.
lemma traceFaultAt_policyTrace (π : Policy) (C₀ : Finset Page)
(σ : List Page) (hC₀ : C₀.Nonempty) (t : ℕ) :
traceFaultAt (policyTrace π C₀ σ hC₀) t = faultAt π C₀ σ t := by
rflA policy trace has exactly the policy's miss count.
lemma traceMisses_policyTrace (π : Policy) (C₀ : Finset Page)
(σ : List Page) (hC₀ : C₀.Nonempty) :
traceMisses (policyTrace π C₀ σ hC₀) = misses π C₀ σ := by
rflThe farthest-in-future trace has exactly the policy-level FIF miss count.
lemma traceMisses_fifoTrace (C₀ : Finset Page) (σ : List Page)
(hC₀ : C₀.Nonempty) :
traceMisses (fifoTrace C₀ σ hC₀) = misses (fifoPolicy σ) C₀ σ := by
rflEvery reachable cache boundary in a legal trace preserves cache size.
lemma legalTrace_card (T : LegalTrace C₀ σ) (hC₀ : C₀.Nonempty)
(t : ℕ) (ht : t ≤ σ.length) :
(T.cache t).card = C₀.card := by
induction t with
| zero => simpa using congrArg Finset.card T.init
| succ t ih =>
have htlt : t < σ.length := Nat.lt_of_succ_le ht
have htprev : t ≤ σ.length := Nat.le_trans (Nat.le_succ t) ht
rw [T.step t htlt]
by_cases hrequest : σ.getD t 0 ∈ T.cache t
· rw [if_pos hrequest]
exact ih htprev
· rw [if_neg hrequest]
have hevict : T.evict t ∈ T.cache t := T.evict_mem t htlt hrequest
have hnotmem : σ.getD t 0 ∉ (T.cache t).erase (T.evict t) := by
intro hmem
exact hrequest (Finset.mem_erase.mp hmem).2
rw [Finset.card_insert_of_notMem hnotmem]
rw [Finset.card_erase_of_mem hevict]
rw [ih htprev]
have hpos : 0 < C₀.card := Finset.card_pos.mpr hC₀
omegaend Cachingend CLRS