Skip to content

Furthest-in-future caching

18 fully proved

Offline Caching

InductiveCache events#✓fully proved

A cache event over a type \(\alpha\) of blocks records how one request is served: either a hit on the requested block \(r \in \alpha\), or a miss on the requested block \(r\) together with an optional evicted block \(v \in \alpha\), absent when nothing is evicted.

public inductive CacheEvent (α : Type u) where
  | hit (request : α)
  | miss (request : α) (evicted : Option α)
  deriving Repr, DecidableEq
Used by 35
Used byLegal cache transitions · Legal cache traces preserve valid caches · Legal cache transitions preserve valid caches · Furthest-in-future caching · One step of the furthest-in-future manager · The furthest-in-future manager produces legal traces · Optimality of furthest-in-future caching · Furthest-in-future caching has the fewest misses · Furthest-in-future on no requests · Furthest-in-future serves exactly the requests · Furthest-in-future caching with zero capacity · Miss indicator · Number of misses in a trace · A legal trace misses at least once · Page served by a cache event · A legal trace without misses serves only cached pages · A legal step caches the served page · 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 · The event of an LRU step · LRU is \(k\)-competitive · LRU is \(k\)-competitive against the offline optimum · Each LRU step is a legal transition · The LRU trace · LRU is a legal cache manager · Hits do not change the offline strategy's misses · The offline trace misses at most once every \(k\) requests · No deterministic online pager is better than \(k\)-competitive · Offline paging step · Each offline step is a legal transition · Offline paging trace · The offline trace is legal · A policy that misses at most \(k\) times per phase is \(k\)-competitive

DefinitionLegal cache transitions#✓fully proved

For a capacity \(k \in \mathbb{N}\), this is the labelled transition system whose states are lists of blocks (the cache contents, in any order) and whose labels are cache events. Write \(|C|\) for the length of a list \(C\), \(x :: C\) for \(C\) with \(x\) prepended, and \(C \setminus v\) for \(C\) with the first occurrence of \(v\) removed. There is a transition from \(C\) to \(C'\) labelled by a hit on \(r\) when \(r \in C\) and \(C'\) is a permutation of \(C\); labelled by a miss on \(r\) with no eviction when \(r \notin C\) and either \(k = 0\) and \(C\) and \(C'\) are both empty, or \(|C| < k\) and \(C'\) is a permutation of \(r :: C\); and labelled by a miss on \(r\) evicting \(v\) when \(k > 0\), \(r \notin C\), \(|C| = k\), \(v \in C\) and \(C'\) is a permutation of \(r :: (C \setminus v)\).

@[expose] public def cacheLTS {α : Type u} [DecidableEq α] (capacity : Nat) :
    Cslib.LTS (List α) (CacheEvent α) where
  Tr before event after := match event with
    | .hit request => request ∈ before ∧ after.Perm before
    | .miss request none => request ∉ before ∧
        ((capacity = 0 ∧ before = [] ∧ after = []) ∨
          (before.length < capacity ∧ after.Perm (request :: before)))
    | .miss request (some victim) =>
        0 < capacity ∧ request ∉ before ∧ before.length = capacity ∧
          victim ∈ before ∧ after.Perm (request :: before.erase victim)
Uses 1 · Used by 19
Statement usesCache events
Used byLegal cache traces preserve valid caches · Legal cache transitions preserve valid caches · The furthest-in-future manager produces legal traces · Optimality of furthest-in-future caching · Furthest-in-future caching has the fewest misses · Furthest-in-future serves exactly the requests · A legal trace misses at least once · A legal trace without misses serves only cached pages · A legal step caches the served page · 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 · LRU is \(k\)-competitive · LRU is \(k\)-competitive against the offline optimum · Each LRU step is a legal transition · LRU is a legal cache manager · Each offline step is a legal transition · The offline trace is legal · A policy that misses at most \(k\) times per phase is \(k\)-competitive

DefinitionFurthest-in-future caching#✓fully proved

Given a capacity \(k\), a sequence of requested pages and an initial cache (a list of pages), the furthest-in-future manager serves the requests in order and returns the list of emitted cache events together with the final cache. A request for a page \(r\) already in the cache is a hit and leaves the cache unchanged. Otherwise it is a miss: if \(k = 0\), nothing is evicted and the cache becomes empty; if the cache holds fewer than \(k\) pages, nothing is evicted and \(r\) is added at the front; otherwise the manager evicts the cached page whose next occurrence among the later requests is furthest away (a page never requested again counts as infinitely far, and ties go to the page listed first in the cache), removes it and adds \(r\) at the front.

public def furthestInFuture {α : Type u} [DecidableEq α]
    (capacity : Nat) (requests initialCache : List α) : List (CacheEvent α) × List α :=
  run capacity requests initialCache
Uses 1 · Used by 12
Statement usesCache events
Used byOne step of the furthest-in-future manager · The furthest-in-future manager produces legal traces · Optimality of furthest-in-future caching · Furthest-in-future caching has the fewest misses · Furthest-in-future on no requests · Furthest-in-future serves exactly the requests · Furthest-in-future caching with zero capacity · The adversary forces \(n\) misses while the optimum misses at most \(k + \lceil n / k \rceil\) times · FIFO is k-competitive against the offline optimum · The ratio k is tight for FIFO · LRU is \(k\)-competitive against the offline optimum · No deterministic online pager is better than \(k\)-competitive

TheoremFurthest-in-future on no requests#✓fully proved

For every capacity \(k\) and every list \(C\) of blocks, the furthest-in-future manager with capacity \(k\) on the empty request list from the initial cache \(C\) emits no events and ends with the cache \(C\), unchanged.

theorem furthestInFuture_nil {α : Type u} [DecidableEq α]
    (capacity : Nat) (initialCache : List α) :
    furthestInFuture capacity [] initialCache = ([], initialCache)
Uses 2
Statement usesCache events · Furthest-in-future caching

TheoremOne step of the furthest-in-future manager#✓fully proved

Write \(x :: L\) for the list \(L\) with \(x\) prepended, \([\,]\) for the empty list, \(|L|\) for the length of \(L\), and \(L \setminus v\) for \(L\) with the first occurrence of \(v\) removed. Write \(\mathrm{FIF}_k(R, C) = (E, D)\) when the furthest-in-future manager with capacity \(k\) on the requests \(R\) from the initial cache \(C\) emits the events \(E\) and ends with the cache \(D\). Write \(\mathrm{hit}(r)\) for a hit on \(r\), \(\mathrm{miss}(r)\) for a miss on \(r\) with no eviction, and \(\mathrm{miss}(r, v)\) for a miss on \(r\) evicting \(v\). Let \(C\) be a duplicate-free list of blocks with \(|C| \le k\), let \(r\) be a block and \(f\) a list of blocks, and for a block \(b\) let \(\nu(b) \in \mathbb{N} \cup \{\infty\}\) be the position of the first occurrence of \(b\) in \(f\), or \(\infty\) if \(b\) does not occur in \(f\). If \(r \in C\), then \(\mathrm{FIF}_k(r :: f, C) = (\mathrm{hit}(r) :: E, D)\) where \((E, D) = \mathrm{FIF}_k(f, C)\). If \(k = 0\), then \(\mathrm{FIF}_k(r :: f, C) = (\mathrm{miss}(r) :: E, D)\) where \((E, D) = \mathrm{FIF}_k(f, [\,])\). If \(r \notin C\) and \(|C| < k\), then \(\mathrm{FIF}_k(r :: f, C) = (\mathrm{miss}(r) :: E, D)\) where \((E, D) = \mathrm{FIF}_k(f, r :: C)\). If \(r \notin C\), \(k > 0\) and \(|C| = k\), and \(v\) is the first entry of \(C\) at which \(\nu\) is maximal on \(C\), then \(\mathrm{FIF}_k(r :: f, C) = (\mathrm{miss}(r, v) :: E, D)\) where \((E, D) = \mathrm{FIF}_k(f, r :: (C \setminus v))\).

Cslib.Algorithms.Lean.OfflineCaching.furthestInFuture_cons · 22 lines 
theorem furthestInFuture_cons {α : Type u} [DecidableEq α]
    (capacity : Nat) (request : α) (future cache : List α)
    (hnodup : cache.Nodup) (hcapacity : cache.length ≤ capacity) :
    (request ∈ cache →
      furthestInFuture capacity (request :: future) cache =
        (.hit request :: (furthestInFuture capacity future cache).1,
          (furthestInFuture capacity future cache).2)) ∧
    (capacity = 0 →
      furthestInFuture capacity (request :: future) cache =
        (.miss request none :: (furthestInFuture capacity future []).1,
          (furthestInFuture capacity future []).2)) ∧
    (request ∉ cache → cache.length < capacity →
      furthestInFuture capacity (request :: future) cache =
        (.miss request none :: (furthestInFuture capacity future (request :: cache)).1,
          (furthestInFuture capacity future (request :: cache)).2)) ∧
    (request ∉ cache → 0 < capacity → cache.length = capacity →
      ∀ victim, List.argmax (β := WithTop Nat) (fun block => future.idxOf? block) cache =
          some victim →
        furthestInFuture capacity (request :: future) cache =
          (.miss request (some victim) ::
            (furthestInFuture capacity future (request :: cache.erase victim)).1,
            (furthestInFuture capacity future (request :: cache.erase victim)).2))
Uses 2
Statement usesCache events · Furthest-in-future caching

Let \(k\) be a capacity, \(R\) a list of requested blocks and \(C\) a duplicate-free list of blocks of length at most \(k\). Let \(E\) be the events and \(D\) the final cache produced by the furthest-in-future manager with capacity \(k\) on \(R\) from the initial cache \(C\). Then \(E\) leads from \(C\) to \(D\) by legal cache transitions for capacity \(k\), the blocks requested by the events of \(E\) are, in order, exactly \(R\), and \(D\) is duplicate-free of length at most \(k\).

theorem furthestInFuture_legal {α : Type u} [DecidableEq α]
    (capacity : Nat) (requests initialCache : List α)
    (hnodup : initialCache.Nodup) (hcapacity : initialCache.length ≤ capacity) :
    let output := furthestInFuture capacity requests initialCache
    (cacheLTS capacity).MTr initialCache output.1 output.2 ∧
      output.1.map (fun event => match event with
        | .hit request => request | .miss request _ => request) = requests ∧
      output.2.Nodup ∧ output.2.length ≤ capacity
Uses 3 · Used by 3
Statement usesCache events · Legal cache transitions · Furthest-in-future caching
Used byFurthest-in-future serves exactly the requests · FIFO is k-competitive against the offline optimum · LRU is \(k\)-competitive against the offline optimum

TheoremFurthest-in-future caching with zero capacity#✓fully proved

Run with capacity \(0\) on a request sequence \(r_1, \dots, r_n\) from the empty cache, the furthest-in-future manager emits exactly the events \(\mathrm{miss}(r_1), \dots, \mathrm{miss}(r_n)\), one miss per request in order and each evicting no page, and its final cache is empty.

theorem furthestInFuture_zero_capacity {α : Type u} [DecidableEq α] (requests : List α) :
    furthestInFuture 0 requests [] =
      (requests.map (fun request => CacheEvent.miss request none), [])
Uses 2
Statement usesCache events · Furthest-in-future caching

TheoremOptimality of furthest-in-future caching#✓fully proved

Let \(k\) be a capacity, \(R\) a list of requested blocks and \(C\) a duplicate-free list of blocks of length at most \(k\). Let \(E'\) be any list of cache events that leads from \(C\) to some final cache by legal cache transitions for capacity \(k\) and whose events request, in order, exactly the blocks of \(R\). Then the furthest-in-future manager with capacity \(k\) on \(R\) from the initial cache \(C\) emits at most as many miss events as \(E'\) contains.

Legal transitions may reorder the list representing the cache, so a competing trace need not keep the manager's order.

theorem furthestInFuture_min_misses {α : Type u} [DecidableEq α]
    (capacity : Nat) (requests initialCache : List α)
    (hnodup : initialCache.Nodup) (hcapacity : initialCache.length ≤ capacity)
    (events : List (CacheEvent α)) (finalCache : List α)
    (hlegal : (cacheLTS capacity).MTr initialCache events finalCache)
    (hrequests : events.map (fun event => match event with
      | .hit request => request | .miss request _ => request) = requests) :
    (furthestInFuture capacity requests initialCache).1.countP
      (fun event => match event with | .hit _ => false | .miss _ _ => true) ≤
      events.countP (fun event => match event with | .hit _ => false | .miss _ _ => true)
Uses 3 · Used by 1
Statement usesCache events · Legal cache transitions · Furthest-in-future caching
Used byFurthest-in-future caching has the fewest misses

Cache Event

DefinitionPage served by a cache event#✓fully proved

The page served by a cache event is the page it requests, whether the event is a hit or a miss.

def request {α : Type u} : CacheEvent α → α
  | .hit r => r
  | .miss r _ => r
Uses 1 · Used by 13
Statement usesCache events
Used byFurthest-in-future caching has the fewest misses · Furthest-in-future serves exactly the requests · A legal trace misses at least once · A legal trace without misses serves only cached pages · A legal step caches the served page · 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 · LRU is \(k\)-competitive · LRU is \(k\)-competitive against the offline optimum · LRU is a legal cache manager · The offline trace is legal · A policy that misses at most \(k\) times per phase is \(k\)-competitive

DefinitionMiss indicator#✓fully proved

The miss indicator of a cache event is true if the event is a miss and false if it is a hit.

def isMiss {α : Type u} : CacheEvent α → Bool
  | .hit _ => false
  | .miss _ _ => true
Uses 1 · Used by 7
Statement usesCache events
Used byNumber of misses in a trace · A legal trace without misses serves only cached pages · LRU is \(k\)-competitive · LRU is a legal cache manager · Hits do not change the offline strategy's misses · The offline trace misses at most once every \(k\) requests · A policy that misses at most \(k\) times per phase is \(k\)-competitive

Offline Caching

DefinitionNumber of misses in a trace#✓fully proved

The number of misses of a finite list of cache events is the number of events in the list that are misses.

def misses {α : Type u} (events : List (CacheEvent α)) : Nat := events.countP CacheEvent.isMiss
Uses 2 · Used by 14
Statement usesCache events · Miss indicator
Used byFurthest-in-future caching has the fewest misses · A legal trace misses at least once · A legal trace without misses serves only cached pages · 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 · LRU is \(k\)-competitive · LRU is \(k\)-competitive against the offline optimum · LRU is a legal cache manager · Hits do not change the offline strategy's misses · The offline trace misses at most once every \(k\) requests · No deterministic online pager is better than \(k\)-competitive · A policy that misses at most \(k\) times per phase is \(k\)-competitive

TheoremLegal cache transitions preserve valid caches#✓fully proved

Let \(k\) be a capacity and let \(C \to C'\) be a legal cache transition for capacity \(k\), labelled by any cache event. If \(C\) has no duplicate entries and length at most \(k\), then \(C'\) has no duplicate entries and length at most \(k\).

theorem cacheLTS_valid {α : Type u} [DecidableEq α] {capacity : Nat} {before after : List α}
    {event : CacheEvent α} (hstep : (cacheLTS capacity).Tr before event after)
    (hnodup : before.Nodup) (hcapacity : before.length ≤ capacity) :
    after.Nodup ∧ after.length ≤ capacity
Uses 2 · Used by 4
Statement usesCache events · Legal cache transitions
Used byLegal cache traces preserve valid caches · LRU is \(k\)-competitive · The offline trace is legal · A policy that misses at most \(k\) times per phase is \(k\)-competitive

TheoremLegal cache traces preserve valid caches#✓fully proved

Let \(k\) be a capacity and suppose a finite sequence of cache events leads from the cache \(C\) to the cache \(C'\) by legal cache transitions for capacity \(k\). If \(C\) has no duplicate entries and length at most \(k\), then \(C'\) has no duplicate entries and length at most \(k\).

theorem cacheLTS_mtr_valid {α : Type u} [DecidableEq α] {capacity : Nat} {before after : List α}
    {events : List (CacheEvent α)} (h : (cacheLTS capacity).MTr before events after)
    (hnodup : before.Nodup) (hcapacity : before.length ≤ capacity) :
    after.Nodup ∧ after.length ≤ capacity
Uses 3 · Used by 2
Statement usesCache events · Legal cache transitions
Proof usesLegal cache transitions preserve valid caches
Used byLRU is \(k\)-competitive · A policy that misses at most \(k\) times per phase is \(k\)-competitive

TheoremA legal step caches the served page#✓fully proved

Let \(k > 0\) be a capacity. If a legal transition for capacity \(k\) takes a cache \(C\) to a cache \(C'\) by a cache event, then the page served by that event lies in \(C'\).

theorem request_mem_of_tr {α : Type u} [DecidableEq α] {capacity : Nat} (hpos : 0 < capacity)
    {before after : List α} {event : CacheEvent α}
    (h : (cacheLTS capacity).Tr before event after) : event.request ∈ after
Uses 3 · Used by 2
Statement usesCache events · Page served by a cache event · Legal cache transitions
Used byLRU is \(k\)-competitive · A policy that misses at most \(k\) times per phase is \(k\)-competitive

TheoremA legal trace without misses serves only cached pages#✓fully proved

Let \(k\) be a capacity. If a legal trace of cache events for capacity \(k\) starts from a cache \(C\) and contains no miss, then every page served by an event of the trace lies in \(C\).

theorem request_mem_of_misses_eq_zero {α : Type u} [DecidableEq α] {capacity : Nat}
    {before after : List α} {events : List (CacheEvent α)}
    (h : (cacheLTS capacity).MTr before events after) (h0 : misses events = 0) :
    ∀ event ∈ events, event.request ∈ before
Uses 5 · Used by 1
Statement usesCache events · Page served by a cache event · Legal cache transitions · Number of misses in a trace
Proof usesMiss indicator
Used byA legal trace misses at least once

TheoremA legal trace misses at least once#✓fully proved

Let \(k\) be a capacity and \(C\) a cache listing at most \(k\) pages, and consider a legal trace of cache events for capacity \(k\) that starts from \(C\). Let \(p\) be a page in \(C\). If at least \(k + 1\) distinct pages are each equal to \(p\) or served by some event of the trace, then the trace contains at least one miss.

theorem one_le_misses {α : Type u} [DecidableEq α] {capacity : Nat} {before after : List α}
    {events : List (CacheEvent α)} (h : (cacheLTS capacity).MTr before events after)
    (hcapacity : before.length ≤ capacity) {p : α} (hp : p ∈ before) {distinct : List α}
    (hdistinct : distinct.Nodup) (hlength : capacity + 1 ≤ distinct.length)
    (hsub : ∀ x ∈ distinct, x = p ∨ x ∈ events.map CacheEvent.request) : 1 ≤ misses events
Uses 5 · Used by 2
Statement usesCache events · Page served by a cache event · Legal cache transitions · Number of misses in a trace
Proof usesA legal trace without misses serves only cached pages
Used byLRU is \(k\)-competitive · A policy that misses at most \(k\) times per phase is \(k\)-competitive

TheoremFurthest-in-future caching has the fewest misses#✓fully proved

Let \(k\) be a capacity, \(R\) a list of requested blocks and \(C\) a duplicate-free list of blocks of length at most \(k\). Let \(E'\) be any list of cache events that leads from \(C\) to some final cache by legal cache transitions for capacity \(k\) and whose events serve, in order, exactly the blocks of \(R\). Then the number of misses among the events emitted by the furthest-in-future manager with capacity \(k\) on \(R\) from the initial cache \(C\) is at most the number of misses of \(E'\).

theorem furthestInFuture_misses_le {α : Type u} [DecidableEq α]
    (capacity : Nat) (requests initialCache : List α)
    (hnodup : initialCache.Nodup) (hcapacity : initialCache.length ≤ capacity)
    (events : List (CacheEvent α)) (finalCache : List α)
    (hlegal : (cacheLTS capacity).MTr initialCache events finalCache)
    (hrequests : events.map CacheEvent.request = requests) :
    misses (furthestInFuture capacity requests initialCache).1 ≤ misses events
Uses 6 · Used by 1
Statement usesCache events · Page served by a cache event · Legal cache transitions · Furthest-in-future caching · Number of misses in a trace
Proof usesOptimality of furthest-in-future caching
Used byThe adversary forces \(n\) misses while the optimum misses at most \(k + \lceil n / k \rceil\) times

TheoremFurthest-in-future serves exactly the requests#✓fully proved

Let \(k\) be a capacity, \(R\) a list of requested blocks and \(C\) a duplicate-free list of blocks of length at most \(k\). Then the events emitted by the furthest-in-future manager with capacity \(k\) on \(R\) from the initial cache \(C\) serve, in order, exactly the blocks of \(R\).

theorem furthestInFuture_requests {α : Type u} [DecidableEq α]
    (capacity : Nat) (requests initialCache : List α)
    (hnodup : initialCache.Nodup) (hcapacity : initialCache.length ≤ capacity) :
    (furthestInFuture capacity requests initialCache).1.map CacheEvent.request = requests
Uses 5 · Used by 2
Statement usesCache events · Page served by a cache event · Furthest-in-future caching
Proof usesLegal cache transitions · The furthest-in-future manager produces legal traces
Used byFIFO is k-competitive against the offline optimum · LRU is \(k\)-competitive against the offline optimum

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.