Competitive paging

DefinitionOne LRU step#✓fully proved

For a capacity \(k\), a cache \(c\) (a list of pages, most recently used first) and a requested page \(p\), the LRU step removes the first occurrence of \(p\) from \(c\) (if any), puts \(p\) at the front, and keeps the first \(k\) pages of the result. On a miss with a cache of exactly \(k \ge 1\) pages, this evicts the last page, the least recently used one.

def lruStep (k : ℕ) (c : List α) (p : α) : List α := (p :: c.erase p).take k
Used by 12
Used byLRU as an online pager · Cache after LRU serves a request sequence · Number of LRU misses · LRU is \(k\)-competitive · LRU misses at most \(k - |S|\) times in the rest of a phase · LRU as an online pager has LRU's miss count · The recency invariant for a repeated page · The recency invariant for a new page · Each LRU step is a legal transition · The LRU trace · LRU is a legal cache manager · LRU as a policy on list caches

DefinitionCache after LRU serves a request sequence#✓fully proved

For a capacity \(k\), a cache \(c\) (a list of pages, most recently used first) and a request sequence \(\sigma\), this is the cache obtained from \(c\) by applying one LRU step with capacity \(k\) for each request of \(\sigma\), in order.

def lruCache (k : ℕ) (c : List α) (σ : List α) : List α := σ.foldl (lruStep k) c
Uses 1 · Used by 2
Statement usesOne LRU step
Used byLRU is \(k\)-competitive · LRU is a legal cache manager

DefinitionNumber of LRU misses#✓fully proved

For a capacity \(k\), a cache \(c\) and a request sequence \(\sigma\), this is the number of requests of \(\sigma\) that are not in the current cache when they are served, where the cache starts at \(c\) and after each request is updated by one LRU step with capacity \(k\).

def lruMisses (k : ℕ) : List α → List α → ℕ
  | _, [] => 0
  | c, p :: σ => (if p ∈ c then 0 else 1) + lruMisses k (lruStep k c p) σ
Uses 1 · Used by 5
Statement usesOne LRU step
Used byLRU is \(k\)-competitive · LRU misses at most \(k - |S|\) times in the rest of a phase · LRU as an online pager has LRU's miss count · LRU is a legal cache manager · LRU as a policy on list caches

TheoremThe recency invariant for a repeated page#✓fully proved

Let \(k\) be a capacity, \(c\) a cache (most recently used first) and \(S\) a list of at most \(k\) pages equal to the first \(|S|\) pages of \(c\). If \(p \in S\), then after one LRU step with capacity \(k\) serving \(p\), the first \(|S|\) pages of the cache are \(p\) followed by \(S\) with the first occurrence of \(p\) removed.

theorem lruStep_take_of_mem {k : ℕ} {c S : List α} {p : α} (hS : c.take S.length = S)
    (hk : S.length ≤ k) (hp : p ∈ S) :
    (lruStep k c p).take S.length = p :: S.erase p
Uses 1 · Used by 1
Statement usesOne LRU step
Used byLRU misses at most \(k - |S|\) times in the rest of a phase

TheoremThe recency invariant for a new page#✓fully proved

Let \(k\) be a capacity, \(c\) a cache (most recently used first) and \(S\) a list with \(|S| + 1 \le k\) equal to the first \(|S|\) pages of \(c\). If \(p \notin S\), then after one LRU step with capacity \(k\) serving \(p\), the first \(|S| + 1\) pages of the cache are \(p\) followed by \(S\).

theorem lruStep_take_of_not_mem {k : ℕ} {c S : List α} {p : α} (hS : c.take S.length = S)
    (hk : S.length + 1 ≤ k) (hp : p ∉ S) :
    (lruStep k c p).take (S.length + 1) = p :: S
Uses 1 · Used by 1
Statement usesOne LRU step
Used byLRU misses at most \(k - |S|\) times in the rest of a phase

DefinitionSplitting off a phase#✓fully proved

Given a capacity \(k\) and a list \(s\) of pages (the pages already in the current phase, most recent first), a request sequence \(\sigma\) is split into a phase and a remainder as follows. The empty sequence splits into two empty parts. For a sequence \(p\) followed by \(\sigma'\): if \(p\) is in \(s\), then \(p\) joins the phase and \(\sigma'\) is split with \(s\) replaced by \(p\) followed by \(s\) with its first occurrence of \(p\) removed; if \(p\) is not in \(s\) and \(s\) has fewer than \(k\) entries, then \(p\) joins the phase and \(\sigma'\) is split with \(p\) added at the front of \(s\); otherwise the phase is empty and the remainder is the whole sequence.

When \(s\) has no repetitions and at most \(k\) pages, the phase is the longest prefix of \(\sigma\) whose distinct pages, together with those of \(s\), number at most \(k\).

def phaseSplit (k : ℕ) : List α → List α → List α × List α
  | _, [] => ([], [])
  | seen, p :: rest =>
      if p ∈ seen then
        let r := phaseSplit k (p :: seen.erase p) rest
        (p :: r.1, r.2)
      else if seen.length < k then
        let r := phaseSplit k (p :: seen) rest
        (p :: r.1, r.2)
      else ([], p :: rest)
Used by 6
Used byFIFO is k-competitive · FIFO misses at most k times per phase · LRU is \(k\)-competitive · LRU misses at most \(k - |S|\) times in the rest of a phase · A phase ends only on a \((k + 1)\)-st distinct page · A policy that misses at most \(k\) times per phase is \(k\)-competitive

TheoremLRU misses at most \(k - |S|\) times in the rest of a phase#✓fully proved

Let \(k\) be a capacity, \(c\) a cache (most recently used first) and \(S\) a duplicate-free list of at most \(k\) pages equal to the first \(|S|\) pages of \(c\). For every request sequence \(\sigma\), let \(\pi\) be the phase that the phase split cuts from \(\sigma\) with \(S\) as the pages already in the phase: the longest prefix of \(\sigma\) whose distinct pages, together with those of \(S\), number at most \(k\). Then the number of LRU misses with capacity \(k\) serving \(\pi\) from \(c\), plus \(|S|\), is at most \(k\).

theorem lruMisses_phase (k : ℕ) : ∀ (seen c σ : List α), c.take seen.length = seen →
    seen.Nodup → seen.length ≤ k →
    lruMisses k c (phaseSplit k seen σ).1 + seen.length ≤ k
Uses 5 · Used by 1
Statement usesNumber of LRU misses · Splitting off a phase
Proof usesOne LRU step · The recency invariant for a repeated page · The recency invariant for a new page
Used byLRU is \(k\)-competitive

TheoremA phase ends only on a \((k + 1)\)-st distinct page#✓fully proved

Let \(k\) be a capacity, let \(s\) be a list of pages without repetitions with at most \(k\) pages (the pages already in the current phase), and let \(\sigma\) be a request sequence. If the remainder left after splitting off a phase from \(\sigma\) given \(s\) starts with a page \(q\), then there is a list \(S\) of exactly \(k\) pairwise distinct pages, none equal to \(q\), each of which lies in \(s\) or in that phase.

theorem phaseSplit_snd_cons (k : ℕ) : ∀ (seen σ : List α) (q : α) (rest : List α),
    seen.Nodup → seen.length ≤ k → (phaseSplit k seen σ).2 = q :: rest →
    ∃ S : List α, S.Nodup ∧ S.length = k ∧ q ∉ S ∧
      ∀ x ∈ S, x ∈ seen ∨ x ∈ (phaseSplit k seen σ).1
Uses 1 · Used by 2
Statement usesSplitting off a phase
Used byLRU is \(k\)-competitive · A policy that misses at most \(k\) times per phase is \(k\)-competitive

DefinitionThe event of an LRU step#✓fully proved

For a capacity \(k\), a cache \(c\) (a list of pages, most recently used first) and a requested page \(p\), the LRU event is a hit on \(p\) if \(p \in c\). Otherwise it is a miss on \(p\) that evicts the last page of \(c\) (the least recently used one) if \(c\) is nonempty, \(k > 0\) and \(c\) has at least \(k\) pages, and a miss on \(p\) without eviction in all other cases.

def lruEvent (k : ℕ) (c : List α) (p : α) : CacheEvent α :=
  if p ∈ c then .hit p
  else if h : c ≠ [] ∧ k ≤ c.length ∧ 0 < k then .miss p (some (c.getLast h.1))
  else .miss p none
Uses 1 · Used by 3
Statement usesCache events
Used byEach LRU step is a legal transition · The LRU trace · LRU is a legal cache manager

DefinitionThe LRU trace#✓fully proved

Given a capacity \(k\), a cache \(c\) and a request sequence \(\sigma\), the events LRU emits on \(\sigma\) from \(c\): nothing on the empty sequence, and on a sequence \(p\) followed by \(\sigma'\), the event LRU emits when serving \(p\) from \(c\), followed by the events LRU emits on \(\sigma'\) from the cache after one LRU step with capacity \(k\) serving \(p\) from \(c\).

def lruTrace (k : ℕ) : List α → List α → List (CacheEvent α)
  | _, [] => []
  | c, p :: σ => lruEvent k c p :: lruTrace k (lruStep k c p) σ
Uses 3 · Used by 3
Statement usesCache events · The event of an LRU step · One LRU step
Used byLRU is \(k\)-competitive · LRU is \(k\)-competitive against the offline optimum · LRU is a legal cache manager

TheoremEach LRU step is a legal transition#✓fully proved

Let \(k\) be a capacity and \(c\) a duplicate-free cache with at most \(k\) pages. For every page \(p\), the cache system with capacity \(k\) has a transition from \(c\), labelled by the LRU event for \(p\) at \(c\), to the cache produced by one LRU step with capacity \(k\) serving \(p\).

theorem lru_tr {k : ℕ} {c : List α} (p : α) (hnd : c.Nodup) (hck : c.length ≤ k) :
    (cacheLTS k).Tr c (lruEvent k c p) (lruStep k c p)
Uses 4 · Used by 1
Statement usesCache events · Legal cache transitions · The event of an LRU step · One LRU step
Used byLRU is a legal cache manager

TheoremLRU is a legal cache manager#✓fully proved

Let \(k\) be a capacity, \(c\) a cache given as a list of pages without repetitions with at most \(k\) pages, and \(\sigma\) a request sequence. Then the sequence of events that LRU emits when serving \(\sigma\) from \(c\) is a run of the cache system with capacity \(k\) from \(c\) to the cache LRU holds after serving \(\sigma\); the pages requested by these events are exactly \(\sigma\), in order; and the number of misses among these events equals the number of misses of LRU on \(\sigma\) from \(c\).

theorem lruTrace_spec {k : ℕ} : ∀ (c σ : List α), c.Nodup → c.length ≤ k →
    (cacheLTS k).MTr c (lruTrace k c σ) (lruCache k c σ) ∧
      (lruTrace k c σ).map CacheEvent.request = σ ∧
      misses (lruTrace k c σ) = lruMisses k c σ
Uses 11 · Used by 1
Statement usesCache events · Page served by a cache event · Legal cache transitions · Number of misses in a trace · Cache after LRU serves a request sequence · Number of LRU misses · The LRU trace
Proof usesMiss indicator · The event of an LRU step · One LRU step · Each LRU step is a legal transition
Used byLRU is \(k\)-competitive

TheoremLRU is \(k\)-competitive#✓fully proved

Let \(k \ge 1\) and let \(c\) be a duplicate-free cache with at most \(k\) pages. Let \(e\) be a legal trace of the cache system with capacity \(k\) that starts from a duplicate-free cache with at most \(k\) pages, and let \(m\) be its number of misses. Then the trace that LRU with capacity \(k\) emits when serving, from \(c\), the requests of \(e\) in order has at most \(k m + k\) misses.

This is the bound of Sleator and Tarjan for an online and an offline cache of the same size.

theorem lruMisses_le {k : ℕ} (hk : 1 ≤ k) {c : List α} (hc : c.Nodup) (hcl : c.length ≤ k)
    {c0 cf : List α} {es : List (CacheEvent α)} (hes : (cacheLTS k).MTr c0 es cf)
    (hnd : c0.Nodup) (hck : c0.length ≤ k) :
    misses (lruTrace k c (es.map CacheEvent.request)) ≤ k * misses es + k
Uses 17 · Used by 1
Statement usesCache events · Page served by a cache event · Legal cache transitions · Number of misses in a trace · The LRU trace
Proof usesMiss indicator · Legal cache traces preserve valid caches · Legal cache transitions preserve valid caches · A legal trace misses at least once · A legal step caches the served page · Cache after LRU serves a request sequence · Number of LRU misses · LRU misses at most \(k - |S|\) times in the rest of a phase · One LRU step · LRU is a legal cache manager · Splitting off a phase · A phase ends only on a \((k + 1)\)-st distinct page
Used byLRU is \(k\)-competitive against the offline optimum

TheoremLRU is \(k\)-competitive against the offline optimum#✓fully proved

Let \(k \ge 1\), and let \(c\) and \(c_0\) be duplicate-free caches with at most \(k\) pages each. For every request sequence \(\sigma\), the trace that LRU with capacity \(k\) emits when serving \(\sigma\) from \(c\) has at most \(k m + k\) misses, where \(m\) is the number of misses of the furthest-in-future manager with capacity \(k\) serving \(\sigma\) from \(c_0\).

Furthest-in-future misses no more often than any legal trace serving the same requests from the same cache, so it is the offline optimum.

theorem lruMisses_le_furthestInFuture {k : ℕ} (hk : 1 ≤ k) {c : List α} (hc : c.Nodup)
    (hcl : c.length ≤ k) (requests : List α) {c0 : List α} (hnd : c0.Nodup)
    (hck : c0.length ≤ k) :
    misses (lruTrace k c requests) ≤ k * misses (furthestInFuture k requests c0).1 + k
Uses 9
Statement usesCache events · Furthest-in-future caching · Number of misses in a trace · The LRU trace
Proof usesPage served by a cache event · Legal cache transitions · The furthest-in-future manager produces legal traces · Furthest-in-future serves exactly the requests · LRU is \(k\)-competitive

StructureDeterministic online paging algorithm#✓fully proved

A deterministic online paging algorithm with cache size k: a state machine whose cache never holds more than k pages. Its moves need not be legal transitions; the lower bound holds for any such machine.

structure OnlinePager.{u, v} (α : Type u) (k : ℕ) where
  /-- Internal states. -/
  State : Type v
  /-- The initial state. -/
  init : State
  /-- The pages cached in a state. -/
  cache : State → List α
  /-- The state after serving a request. -/
  step : State → α → State
  /-- The cache holds at most `k` pages. -/
  cache_le : ∀ q, (cache q).length ≤ k
Used by 12
Used byThe paging adversary · The adversary forces \(n\) misses while the optimum misses at most \(k + \lceil n / k \rceil\) times · FIFO is k-competitive · FIFO is k-competitive against the offline optimum · The ratio k is tight for FIFO · FIFO paging as an online pager · FIFO as an online pager misses as often as the FIFO step policy · LRU as an online pager · LRU as an online pager has LRU's miss count · Misses of an online pager · The pager misses every request · No deterministic online pager is better than \(k\)-competitive

DefinitionMisses of an online pager#✓fully proved

For an online pager \(A\), a state \(q\) and a request sequence \(\sigma\), the number of misses of \(A\) from \(q\) on \(\sigma\) counts the requests of \(\sigma\) that are not in the cache of the current state, where the run starts at \(q\) and each request moves \(A\) to its next state.

def misses : A.State → List α → ℕ
  | _, [] => 0
  | q, p :: σ => (if p ∈ A.cache q then 0 else 1) + misses (A.step q p) σ
Uses 1 · Used by 8
Statement usesDeterministic online paging algorithm
Used byThe adversary forces \(n\) misses while the optimum misses at most \(k + \lceil n / k \rceil\) times · FIFO is k-competitive · FIFO is k-competitive against the offline optimum · The ratio k is tight for FIFO · FIFO as an online pager misses as often as the FIFO step policy · LRU as an online pager has LRU's miss count · The pager misses every request · No deterministic online pager is better than \(k\)-competitive

DefinitionLRU as an online pager#✓fully proved

LRU as an online pager.

def lruPager.{u} (α : Type u) [DecidableEq α] (k : ℕ) : OnlinePager.{u, u} α k where
  State := {c : List α // c.length ≤ k}
  init := ⟨[], Nat.zero_le _⟩
  cache q := q.1
  step q p := ⟨lruStep k q.1 p, List.length_take_le _ _⟩
  cache_le q := q.2
Uses 2 · Used by 1
Statement usesDeterministic online paging algorithm · One LRU step
Used byLRU as an online pager has LRU's miss count

TheoremLRU as an online pager has LRU's miss count#✓fully proved

For every cache \(c\) of at most \(k\) pages and every request sequence \(\sigma\), the number of misses of LRU with capacity \(k\), viewed as an online pager and started in the state with cache \(c\), on \(\sigma\) equals the number of misses of LRU with capacity \(k\) started with cache \(c\) on \(\sigma\).

theorem lruPager_misses {α : Type*} [DecidableEq α] {k : ℕ} :
    ∀ (q : (lruPager α k).State) (σ : List α), (lruPager α k).misses q σ = lruMisses k q.1 σ
Uses 5
Statement usesDeterministic online paging algorithm · Misses of an online pager · Number of LRU misses · LRU as an online pager
Proof usesOne LRU step

DefinitionOutside page of a cache#✓fully proved

For a natural number \(k\) and a list \(c\) of pages from \(\{0, \dots, k\}\), the outside page of \(c\) is the smallest \(x \in \{0, \dots, k\}\) that does not occur in \(c\), or \(0\) if every page of \(\{0, \dots, k\}\) occurs in \(c\).

def outside {k : ℕ} (c : List (Fin (k + 1))) : Fin (k + 1) :=
  ((List.finRange (k + 1)).find? fun x => x ∉ c).getD 0
Used by 4
Used byThe paging adversary · The adversary forces \(n\) misses while the optimum misses at most \(k + \lceil n / k \rceil\) times · The pager misses every request · The outside page is not cached

TheoremThe outside page is not cached#✓fully proved

Let \(k\) be a natural number and let \(c\) be a list of at most \(k\) pages from \(\{0, \dots, k\}\). Then the outside page of \(c\) does not occur in \(c\).

theorem outside_not_mem {k : ℕ} {c : List (Fin (k + 1))} (hc : c.length ≤ k) : outside c ∉ c
Uses 1 · Used by 1
Statement usesOutside page of a cache
Used byThe pager misses every request

DefinitionThe paging adversary#✓fully proved

Let \(A\) be a deterministic online pager with cache size \(k\) on the \(k + 1\) pages \(0, \dots, k\). From a state \(q\) of \(A\), the adversary's sequence of \(n\) requests is empty for \(n = 0\); for \(n + 1\) it first requests the smallest page not in the cache of \(q\) (page \(0\) if there is none) and then continues with the adversary's sequence of \(n\) requests from the state that \(A\) reaches from \(q\) by serving that request.

def adversary {k : ℕ} (A : OnlinePager (Fin (k + 1)) k) : ℕ → A.State → List (Fin (k + 1))
  | 0, _ => []
  | n + 1, q => outside (A.cache q) :: adversary A n (A.step q (outside (A.cache q)))
Uses 2 · Used by 3
Statement usesDeterministic online paging algorithm · Outside page of a cache
Used byThe adversary forces \(n\) misses while the optimum misses at most \(k + \lceil n / k \rceil\) times · The pager misses every request · No deterministic online pager is better than \(k\)-competitive

TheoremThe pager misses every request#✓fully proved

The pager misses every request of the adversary's sequence.

theorem misses_adversary {k : ℕ} (A : OnlinePager (Fin (k + 1)) k) :
    ∀ n q, A.misses q (adversary A n q) = n
Uses 5 · Used by 1
Statement usesDeterministic online paging algorithm · Misses of an online pager · The paging adversary
Proof usesOutside page of a cache · The outside page is not cached
Used byThe adversary forces \(n\) misses while the optimum misses at most \(k + \lceil n / k \rceil\) times

DefinitionOffline paging step#✓fully proved

Given a cache size \(k\), a cache \(c\) (a list of pages), a requested page \(p\) and the list \(f\) of future requests, the offline step returns an event and a new cache. If \(p \in c\), it is a hit on \(p\) and the cache is unchanged. Otherwise, if \(c\) has fewer than \(k\) pages, it is a miss on \(p\) with no eviction and the new cache is \(p\) followed by \(c\). Otherwise, if some page of \(c\) does not occur among the first \(k - 1\) entries of \(f\) (no entries at all when \(k = 0\), and all of \(f\) when \(f\) is shorter), it is a miss on \(p\) evicting the first such page \(v\) in \(c\), and the new cache is \(p\) followed by \(c\) with the first occurrence of \(v\) removed. If there is no such page, it is a miss on \(p\) with no eviction and the new cache is \(p\) followed by \(c\).

def optStep (k : ℕ) (c : List α) (p : α) (future : List α) : CacheEvent α × List α :=
  if p ∈ c then (.hit p, c)
  else if c.length < k then (.miss p none, p :: c)
  else match c.find? (fun x => x ∉ future.take (k - 1)) with
    | some v => (.miss p (some v), p :: c.erase v)
    | none => (.miss p none, p :: c)
Uses 1 · Used by 5
Statement usesCache events
Used byHits do not change the offline strategy's misses · The offline trace misses at most once every \(k\) requests · Each offline step is a legal transition · Offline paging trace · The offline trace is legal

DefinitionOffline paging trace#✓fully proved

Given a cache size \(k\), the offline trace from a cache \(c\) on a list of requests is defined by recursion on the list: on the empty list it is empty, and on a list with first request \(p\) and remaining requests \(r\) it is the event of the offline step with cache size \(k\) on \(c\), \(p\) and \(r\), followed by the offline trace on \(r\) from the new cache of that step.

def optTrace (k : ℕ) : List α → List α → List (CacheEvent α)
  | _, [] => []
  | c, p :: rest => (optStep k c p rest).1 :: optTrace k (optStep k c p rest).2 rest
Uses 2 · Used by 4
Statement usesCache events · Offline paging step
Used byThe adversary forces \(n\) misses while the optimum misses at most \(k + \lceil n / k \rceil\) times · Hits do not change the offline strategy's misses · The offline trace misses at most once every \(k\) requests · The offline trace is legal

TheoremA full cache has a page outside the next \(k - 1\) requests#✓fully proved

Let \(k \ge 1\), let \(c\) be a list of \(k\) distinct pages and let \(f\) be any list of requests. Then the search through \(c\) for the first page that does not occur among the first \(k - 1\) entries of \(f\) succeeds; in particular, some page of \(c\) does not occur there.

theorem find?_isSome {k : ℕ} (hk : 1 ≤ k) {c : List α} (hnd : c.Nodup) (hck : c.length = k)
    (future : List α) : ∃ v, c.find? (fun x => x ∉ future.take (k - 1)) = some v
Used by 2
Used byThe offline trace misses at most once every \(k\) requests · Each offline step is a legal transition

TheoremEach offline step is a legal transition#✓fully proved

Let \(k \ge 1\), let \(c\) be a cache of at most \(k\) distinct pages, let \(p\) be a requested page and let \(f\) be the list of future requests. Then the event and the new cache produced by the offline step with cache size \(k\) on \(c\), \(p\) and \(f\) form a legal transition from \(c\) of the caching system with capacity \(k\).

theorem optStep_tr {k : ℕ} (hk : 1 ≤ k) {c : List α} (hnd : c.Nodup) (hck : c.length ≤ k)
    (p : α) (future : List α) :
    (cacheLTS k).Tr c (optStep k c p future).1 (optStep k c p future).2
Uses 4 · Used by 1
Statement usesCache events · Legal cache transitions · Offline paging step
Proof usesA full cache has a page outside the next \(k - 1\) requests
Used byThe offline trace is legal

Let \(k \ge 1\), let \(c\) be a cache of at most \(k\) distinct pages and let \(\sigma\) be a list of requests. Then the offline trace with cache size \(k\) from \(c\) on \(\sigma\) is a legal run of the caching system with capacity \(k\) from \(c\) to some final cache, and the pages served by its events are, in order, exactly \(\sigma\).

theorem optTrace_legal {k : ℕ} (hk : 1 ≤ k) : ∀ (c σ : List α), c.Nodup → c.length ≤ k →
    (∃ cf, (cacheLTS k).MTr c (optTrace k c σ) cf) ∧ (optTrace k c σ).map CacheEvent.request = σ
Uses 7 · Used by 1
Statement usesCache events · Page served by a cache event · Legal cache transitions · Offline paging trace
Proof usesLegal cache transitions preserve valid caches · Offline paging step · Each offline step is a legal transition
Used byThe adversary forces \(n\) misses while the optimum misses at most \(k + \lceil n / k \rceil\) times

TheoremHits do not change the offline strategy's misses#✓fully proved

Let \(k\) be a capacity, let \(c\) be a cache and let \(w\) be a request sequence all of whose requests lie in \(c\). Then for every request sequence \(\tau\), the offline strategy with capacity \(k\) (on a miss with a full cache, evict the first cached page not among the next \(k - 1\) requests, if there is one) started with cache \(c\) misses as many times on \(w\) followed by \(\tau\) as on \(\tau\) alone.

theorem misses_optTrace_hits {k : ℕ} : ∀ (w τ c : List α), (∀ x ∈ w, x ∈ c) →
    misses (optTrace k c (w ++ τ)) = misses (optTrace k c τ)
Uses 5 · Used by 1
Statement usesNumber of misses in a trace · Offline paging trace
Proof usesCache events · Miss indicator · Offline paging step
Used byThe offline trace misses at most once every \(k\) requests

TheoremAfter a miss on a full cache, every page except the evicted one is present#✓fully proved

Let \(c\) be a list of \(k\) distinct pages among the \(k + 1\) pages \(0, \dots, k\), let \(p\) be a page not in \(c\), and let \(v\) be any page. Then every page \(x \neq v\) lies in the cache obtained from \(c\) by removing \(v\) and adding \(p\).

theorem mem_of_full {k : ℕ} {c : List (Fin (k + 1))} (hnd : c.Nodup) (hck : c.length = k)
    {p v : Fin (k + 1)} (hp : p ∉ c) {x : Fin (k + 1)} (hx : x ≠ v) :
    x ∈ p :: c.erase v
Used by 1
Used byThe offline trace misses at most once every \(k\) requests

TheoremThe offline trace misses at most once every \(k\) requests#✓fully proved

Let \(k \ge 1\) and consider the \(k + 1\) pages \(0, 1, \dots, k\). Let \(N\) be a natural number, \(\sigma\) a sequence of \(n \le N\) requests to these pages, and \(c\) a cache of \(|c| \le k\) distinct pages. Then the number of misses of the offline trace with cache size \(k\) from \(c\) on \(\sigma\) is at most \((k - |c|) + \lfloor (n + k - 1) / k \rfloor = (k - |c|) + \lceil n / k \rceil\): after at most \(k - |c|\) misses filling the cache, at most one miss every \(k\) requests.

theorem misses_optTrace_le {k : ℕ} (hk : 1 ≤ k) : ∀ (N : ℕ) (σ : List (Fin (k + 1))),
    σ.length ≤ N → ∀ c : List (Fin (k + 1)), c.Nodup → c.length ≤ k →
    misses (optTrace k c σ) ≤ (k - c.length) + (σ.length + k - 1) / k
Uses 8 · Used by 1
Statement usesNumber of misses in a trace · Offline paging trace
Proof usesCache events · Miss indicator · A full cache has a page outside the next \(k - 1\) requests · After a miss on a full cache, every page except the evicted one is present · Hits do not change the offline strategy's misses · Offline paging step
Used byThe adversary forces \(n\) misses while the optimum misses at most \(k + \lceil n / k \rceil\) times

TheoremThe adversary forces \(n\) misses while the optimum misses at most \(k + \lceil n / k \rceil\) times#✓fully proved

The adversary forces \(n\) misses while the optimum misses at most \(k + \lceil n / k \rceil\) times. Let \(k \ge 1\) and let \(A\) be a deterministic online pager with cache size \(k\) on the \(k + 1\) pages \(0, \dots, k\). For every \(n\), on the adversary's sequence of \(n\) requests started from the initial state of \(A\), the pager \(A\) started in its initial state misses exactly \(n\) times, and the furthest-in-future strategy with capacity \(k\) started with an empty cache misses at most \(k + \lceil n / k \rceil\) times.

theorem adversary_vs_optimum {k : ℕ} (hk : 1 ≤ k) (A : OnlinePager (Fin (k + 1)) k) (n : ℕ) :
    A.misses A.init (adversary A n A.init) = n ∧
      misses (furthestInFuture k (adversary A n A.init) []).1 ≤ k + (n + k - 1) / k
Uses 14 · Used by 1
Statement usesCache events · Furthest-in-future caching · Number of misses in a trace · Deterministic online paging algorithm · Misses of an online pager · The paging adversary
Proof usesPage served by a cache event · Legal cache transitions · Furthest-in-future caching has the fewest misses · The pager misses every request · The offline trace misses at most once every \(k\) requests · Offline paging trace · The offline trace is legal · Outside page of a cache
Used byNo deterministic online pager is better than \(k\)-competitive

TheoremNo deterministic online pager is better than \(k\)-competitive#✓fully proved

Let \(k \ge 1\) and let \(A\) be a deterministic online pager with cache size \(k\) on the \(k + 1\) pages \(0, \dots, k\). For a request sequence \(\sigma\), write \(A(\sigma)\) for the number of misses of \(A\) started in its initial state on \(\sigma\), and \(\mathrm{OPT}(\sigma)\) for the number of misses of the furthest-in-future strategy with capacity \(k\) started with an empty cache on \(\sigma\). Then for all natural numbers \(c\), \(d\) with \(c < kd\) and every natural number \(b\), there is a request sequence \(\sigma\) with \(c \cdot \mathrm{OPT}(\sigma) + b < d \cdot A(\sigma)\). That is, the pager misses more than \(c / d\) times the optimum plus \(b / d\).

theorem not_competitive_of_lt {k : ℕ} (hk : 1 ≤ k) (A : OnlinePager (Fin (k + 1)) k) {c d : ℕ}
    (hc : c < k * d) (b : ℕ) : ∃ σ : List (Fin (k + 1)),
      c * misses (furthestInFuture k σ []).1 + b < d * A.misses A.init σ
Uses 7 · Used by 1
Statement usesCache events · Furthest-in-future caching · Number of misses in a trace · Deterministic online paging algorithm · Misses of an online pager
Proof usesThe paging adversary · The adversary forces \(n\) misses while the optimum misses at most \(k + \lceil n / k \rceil\) times
Used byThe ratio k is tight for FIFO

DefinitionMisses of a paging policy on list caches#✓fully proved

Let a paging policy be given by its step function, which maps a cache (a list of pages) and a requested page to the next cache. Starting from a cache \(c\), the policy serves a request sequence \(p_1, \dots, p_n\) by setting \(c_0 = c\) and \(c_i = \mathrm{step}(c_{i-1}, p_i)\) for each \(i\); its number of misses is the number of indices \(i\) with \(p_i \notin c_{i-1}\).

def policyMisses (step : List α → α → List α) : List α → List α → ℕ
  | _, [] => 0
  | c, p :: σ => (if p ∈ c then 0 else 1) + policyMisses step (step c p) σ
Used by 5
Used byFIFO is k-competitive · FIFO misses at most k times per phase · FIFO as an online pager misses as often as the FIFO step policy · A policy that misses at most \(k\) times per phase is \(k\)-competitive · LRU as a policy on list caches

TheoremA policy that misses at most \(k\) times per phase is \(k\)-competitive#✓fully proved

Let \(k \ge 1\) and consider a paging policy on list caches, given by its step function. Suppose that, started from any cache, the policy misses at most \(k\) times on the first phase of every request sequence (the longest prefix of the sequence with at most \(k\) distinct pages). Let \(T\) be a legal trace of caching with capacity \(k\) (a run of the cache transition system) whose initial cache is a list of at most \(k\) pages with no page repeated, and let \(m\) be the number of misses in \(T\). Then, started from any cache, the policy misses at most \(km + k\) times on the sequence of requests served by \(T\).

theorem policyMisses_le (step : List α → α → List α) {k : ℕ} (hk : 1 ≤ k)
    (hphase : ∀ c σ : List α, policyMisses step c (phaseSplit k [] σ).1 ≤ k) (c : List α)
    {c0 cf : List α} {es : List (CacheEvent α)} (hes : (cacheLTS k).MTr c0 es cf)
    (hnd : c0.Nodup) (hck : c0.length ≤ k) :
    policyMisses step c (es.map CacheEvent.request) ≤ k * misses es + k
Uses 12 · Used by 1
Statement usesCache events · Page served by a cache event · Legal cache transitions · Number of misses in a trace · Misses of a paging policy on list caches · Splitting off a phase
Proof usesMiss indicator · Legal cache traces preserve valid caches · Legal cache transitions preserve valid caches · A legal trace misses at least once · A legal step caches the served page · A phase ends only on a \((k + 1)\)-st distinct page
Used byFIFO is k-competitive

TheoremLRU as a policy on list caches#✓fully proved

For every capacity \(k\), the misses of the paging policy whose step is the LRU step with capacity \(k\) coincide with the LRU misses with capacity \(k\), from every starting cache and on every request sequence.

theorem policyMisses_lruStep (k : ℕ) : policyMisses (lruStep (α := α) k) = lruMisses k
Uses 3
Statement usesMisses of a paging policy on list caches · Number of LRU misses · One LRU step

DefinitionOne step of FIFO paging#✓fully proved

The cache is a list of pages, oldest first, and \(k\) is the capacity. On a request for a page \(p\) already in the cache \(c\), the cache stays \(c\). Otherwise \(p\) is appended at the back of \(c\); if \(c\) had fewer than \(k\) pages, that is the new cache, and if not, the front page, the one loaded earliest, is removed as well.

def fifoStep (k : ℕ) (c : List α) (p : α) : List α :=
  if p ∈ c then c else if c.length < k then c ++ [p] else (c ++ [p]).tail
Used by 6
Used byFIFO keeps the cache legal on every request sequence · FIFO is k-competitive · FIFO misses at most k times per phase · FIFO paging as an online pager · FIFO as an online pager misses as often as the FIFO step policy · One FIFO step keeps the cache legal

If a list \(c\) of pages has no duplicates and at most \(k\) entries, then for every page \(p\) the cache produced from \(c\) by one FIFO step with capacity \(k\) on request \(p\) also has no duplicates and at most \(k\) entries.

theorem fifoStep_legal {k : ℕ} {c : List α} (hnd : c.Nodup) (hck : c.length ≤ k) (p : α) :
    (fifoStep k c p).Nodup ∧ (fifoStep k c p).length ≤ k
Uses 1 · Used by 2
Statement usesOne step of FIFO paging
Used byFIFO keeps the cache legal on every request sequence · FIFO paging as an online pager

TheoremFIFO misses at most k times per phase#✓fully proved

Let \(S\) be a list of at most \(k\) distinct pages (the pages already in the current phase), let \(c\) be any list of pages (a FIFO cache, oldest page first), and let \(L\) be a list of distinct pages, each of them in \(S\), that is a suffix of \(c\). For every request sequence \(\sigma\), let \(P\) be the phase split off from \(\sigma\) given \(S\): the longest prefix of \(\sigma\) whose distinct pages, together with those of \(S\), number at most \(k\). Then the number of misses of the FIFO step policy with capacity \(k\) serving \(P\) from \(c\), plus the length of \(L\), is at most \(k\).

The pages loaded so far in the phase (\(L\), in load order) stay at the back of the queue: each miss appends one, and an eviction removes the front, which is not among them while at most \(k\) pages have been loaded. So a page of the phase is missed at most once, and a phase has at most \(k\) distinct pages.

theorem fifoMisses_phase (k : ℕ) : ∀ (seen c L σ : List α), L <:+ c → L.Nodup →
    (∀ x ∈ L, x ∈ seen) → seen.Nodup → seen.length ≤ k →
    policyMisses (fifoStep k) c (phaseSplit k seen σ).1 + L.length ≤ k
Uses 3 · Used by 1
Statement usesOne step of FIFO paging · Misses of a paging policy on list caches · Splitting off a phase
Used byFIFO is k-competitive

For a type \(\alpha\) of pages and a capacity \(k \in \mathbb{N}\), a legal cache is a list of pages of \(\alpha\) with no duplicates and at most \(k\) entries.

abbrev LegalCache (α : Type*) (k : ℕ) := {c : List α // c.Nodup ∧ c.length ≤ k}
Used by 1
Used byFIFO paging as an online pager

If a list \(c\) of pages has no duplicates and at most \(k\) entries, then for every finite request sequence \(\sigma\) the cache obtained from \(c\) by serving the requests of \(\sigma\) in order, each with one FIFO step of capacity \(k\), also has no duplicates and at most \(k\) entries.

theorem fifoCache_legal {k : ℕ} : ∀ (c : List α) (σ : List α), c.Nodup → c.length ≤ k →
    (σ.foldl (fifoStep k) c).Nodup ∧ (σ.foldl (fifoStep k) c).length ≤ k
Uses 2
Statement usesOne step of FIFO paging
Proof usesOne FIFO step keeps the cache legal

DefinitionFIFO paging as an online pager#✓fully proved

The online pager with capacity \(k\) whose states are the legal caches of capacity \(k\) (lists of at most \(k\) distinct pages, oldest first), whose initial state is the empty cache, whose cache in a state is that list itself, and which serves a request \(p\) by one FIFO step with capacity \(k\).

def fifoPager (α : Type*) [DecidableEq α] (k : ℕ) : OnlinePager α k where
  State := LegalCache α k
  init := ⟨[], List.nodup_nil, Nat.zero_le k⟩
  cache q := q.1
  step q p := ⟨fifoStep k q.1 p, fifoStep_legal q.2.1 q.2.2 p⟩
  cache_le q := q.2.2
Uses 4 · Used by 4
Statement usesLegal cache · One step of FIFO paging · One FIFO step keeps the cache legal · Deterministic online paging algorithm
Used byFIFO is k-competitive · FIFO is k-competitive against the offline optimum · The ratio k is tight for FIFO · FIFO as an online pager misses as often as the FIFO step policy

TheoremFIFO as an online pager misses as often as the FIFO step policy#✓fully proved

For every legal cache \(q\) of capacity \(k\) (at most \(k\) distinct pages) and every request sequence \(\sigma\), the number of misses of the FIFO online pager started in \(q\) and serving \(\sigma\) equals the number of misses of the policy given by the FIFO step with capacity \(k\) serving \(\sigma\) from the cache \(q\).

theorem fifoPager_misses {k : ℕ} :
    ∀ (q : (fifoPager α k).State) (σ : List α),
      (fifoPager α k).misses q σ = policyMisses (fifoStep k) q.1 σ
Uses 5 · Used by 1
Statement usesFIFO paging as an online pager · One step of FIFO paging · Misses of a paging policy on list caches · Deterministic online paging algorithm · Misses of an online pager
Used byFIFO is k-competitive

TheoremFIFO is k-competitive#✓fully proved

FIFO is k-competitive (Sleator and Tarjan). Let \(k \ge 1\), and let \(\tau\) be a legal trace of the caching system with capacity \(k\) that starts from a cache \(c_0\) of at most \(k\) distinct pages; let \(m\) be its number of misses. Then the FIFO online pager with capacity \(k\), started in any legal cache (at most \(k\) distinct pages) and serving the requests of \(\tau\) in order, misses at most \(k m + k\) times.

theorem fifoMisses_le {k : ℕ} (hk : 1 ≤ k) (q : (fifoPager α k).State) {c0 cf : List α}
    {es : List (CacheEvent α)} (hes : (cacheLTS k).MTr c0 es cf) (hnd : c0.Nodup)
    (hck : c0.length ≤ k) :
    (fifoPager α k).misses q (es.map CacheEvent.request) ≤ k * misses es + k
Uses 13 · Used by 1
Statement usesCache events · Page served by a cache event · Legal cache transitions · Number of misses in a trace · FIFO paging as an online pager · Deterministic online paging algorithm · Misses of an online pager
Proof usesFIFO misses at most k times per phase · FIFO as an online pager misses as often as the FIFO step policy · One step of FIFO paging · Misses of a paging policy on list caches · A policy that misses at most \(k\) times per phase is \(k\)-competitive · Splitting off a phase
Used byFIFO is k-competitive against the offline optimum

TheoremFIFO is k-competitive against the offline optimum#✓fully proved

Let \(k \ge 1\), let \(\sigma\) be a finite request sequence, and let \(c_0\) be a list of at most \(k\) distinct pages. Let \(m\) be the number of misses of the furthest-in-future manager with capacity \(k\) serving \(\sigma\) from the cache \(c_0\). Then the FIFO online pager with capacity \(k\), started in any legal cache (at most \(k\) distinct pages), misses at most \(k m + k\) of the requests of \(\sigma\).

theorem fifoMisses_le_furthestInFuture {k : ℕ} (hk : 1 ≤ k) (q : (fifoPager α k).State)
    (requests : List α) {c0 : List α} (hnd : c0.Nodup) (hck : c0.length ≤ k) :
    (fifoPager α k).misses q requests ≤ k * misses (furthestInFuture k requests c0).1 + k
Uses 11
Statement usesCache events · Furthest-in-future caching · Number of misses in a trace · FIFO paging as an online pager · Deterministic online paging algorithm · Misses of an online pager
Proof usesPage served by a cache event · Legal cache transitions · The furthest-in-future manager produces legal traces · Furthest-in-future serves exactly the requests · FIFO is k-competitive

TheoremThe ratio k is tight for FIFO#✓fully proved

Let \(k \ge 1\) and let \(c\) and \(d\) be natural numbers with \(c < k d\). For every natural number \(b\) there is a finite request sequence \(\sigma\) over \(k + 1\) pages with \(c \cdot m + b < d \cdot f\), where \(m\) is the number of misses of the furthest-in-future manager with capacity \(k\) serving \(\sigma\) from the empty cache, and \(f\) is the number of misses of the FIFO online pager with capacity \(k\) serving \(\sigma\) from its initial, empty cache.

So no ratio \(c / d < k\) makes FIFO \(c / d\)-competitive, whatever the additive constant.

theorem fifo_not_competitive_of_lt {k : ℕ} (hk : 1 ≤ k) {c d : ℕ} (hc : c < k * d) (b : ℕ) :
    ∃ σ : List (Fin (k + 1)), c * misses (furthestInFuture k σ []).1 + b <
      d * (fifoPager (Fin (k + 1)) k).misses (fifoPager (Fin (k + 1)) k).init σ
Uses 7
Statement usesCache events · Furthest-in-future caching · Number of misses in a trace · FIFO paging as an online pager · Deterministic online paging algorithm · Misses of an online pager
Proof usesNo deterministic online pager is better than \(k\)-competitive
45 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.