LRU Cache

위키 빌드 파이프라인에서 파싱 결과와 렌더링 결과를 캐싱한다. 수천 개의 마크다운 파일을 매번 파싱하면 빌드 시간이 길어지므로, 변경되지 않은 파일의 결과를 메모리에 유지하여 증분 빌드를 지원한다.

Least Recently Used 정책을 사용하는 이유는 위키 편집 패턴에 있다: 최근 편집한 문서가 다시 편집될 확률이 높으므로, 오래 접근하지 않은 항목부터 제거하는 것이 합리적이다. Map의 삽입 순서를 활용하여 별도 자료구조 없이 O(1) get/set을 제공한다.

캐시의 핵심 불변량: (1) 저장된 항목 수는 maxSize를 초과할 수 없고, (2) 용량 초과 시 가장 오래 접근되지 않은 항목이 제거되며, (3) get은 항목을 최근 위치로 승격하지만, has는 순서에 영향을 주지 않는다.

구현은 Map의 삽입 순서를 활용한다: get 시 delete 후 재삽입으로 끝으로 이동하고, has는 Map.has만 호출하여 순서를 변경하지 않는다. 이 구분이 깨지면 has 호출만으로 항목이 eviction에서 살아남게 된다.

module lru

sig Key {}

sig Entry {
  key: one Key,
  order: one Int
}

sig Cache {
  entries: set Entry,
  maxSize: one Int
}

-- maxSize는 항상 양수
fact positiveCapacity {
  all c: Cache | c.maxSize > 0
}

-- key는 캐시 내에서 유일
fact uniqueKeys {
  all c: Cache | all disj e1, e2: c.entries | e1.key != e2.key
}

-- 항목 수는 maxSize 이하
fact capacityBound {
  all c: Cache | #c.entries <= c.maxSize
}

-- order로 LRU 순서를 표현: 작은 값이 오래된 항목, 값은 유일
fact distinctOrder {
  all c: Cache | all disj e1, e2: c.entries | e1.order != e2.order
}

-- get은 항목을 최근 위치로 승격 (order를 최대로)
pred promoteOnGet[c: Cache, e: Entry] {
  e in c.entries
  all other: c.entries | e.order >= other.order
}

-- eviction 대상: 가장 작은 order
pred evictLRU[c: Cache, victim: Entry] {
  #c.entries = c.maxSize
  victim in c.entries
  all e: c.entries | victim.order <= e.order
}

-- eviction 대상은 항상 유일
assert uniqueEviction {
  all c: Cache, v1, v2: Entry |
    (evictLRU[c, v1] and evictLRU[c, v2]) implies v1 = v2
}

-- get으로 승격된 항목은 절대 eviction 대상이 아님
assert promotedNotEvicted {
  all c: Cache, e: Entry |
    (promoteOnGet[c, e] and #c.entries > 1)
    implies not evictLRU[c, e]
}

check uniqueEviction for 5 but 6 Int
check promotedNotEvicted for 5 but 6 Int

alloy:model(lru)

Eviction 정책

용량 초과 시 가장 오래 사용되지 않은 항목이 제거된다. 이 동작이 캐시의 핵심이다 — 새 항목이 들어올 때 가장 오래된 항목이 밀려나야 메모리를 제한하면서도 최근 작업의 캐시 적중률을 유지할 수 있다.

용량 2에 a, b, c 순서 삽입 → a가 제거됨

import { LRUCache } from './src/lib/cache.ts'
const c = new LRUCache(2)
c.set('a', 1)
c.set('b', 2)
c.set('c', 3)
console.log(JSON.stringify({ hasA: c.has('a'), hasB: c.has('b'), hasC: c.has('c') }))

evict={"hasA":false,"hasB":true,"hasC":true}

run:wiki

expr	expected
.hasA	false
.hasB	true
.hasC	true

LRU 순서 갱신

get으로 조회하면 해당 항목이 최근 사용 항목으로 승격된다. 이후 eviction 시 조회하지 않은 항목이 먼저 제거된다.

이 승격이 없으면 "조회만 반복하는 항목"이 삽입 순서에 따라 밀려나게 되어, 자주 참조되는 문서의 캐시가 무효화되는 문제가 발생한다.

a, b 삽입 후 get('a')로 승격 → c 삽입 시 b가 제거됨 (a 아님)

import { LRUCache } from './src/lib/cache.ts'
const c = new LRUCache(2)
c.set('a', 1)
c.set('b', 2)
c.get('a')
c.set('c', 3)
console.log(JSON.stringify({ hasA: c.has('a'), hasB: c.has('b') }))

$evict={"hasA":false,"hasB":true,"hasC":true}

promote={"hasA":true,"hasB":false}

run:wiki

expr	expected
.hasA	true
.hasB	false