SoftWare Abstraction 6.4.3 Cache Memory

models/book/chapter6/memory/CacheMemory.alsを改変。
loadの対象となるアドレスをmainにありかつ、対象をキャッシュに載ってないものから弱化したものにした。

module chapter6/memory/cacheMemory [Addr, Data] ----- the model from page 219

sig CacheSystem {
 main, cache: Addr -> lone Data
 }

pred init [c: CacheSystem] {
 no c.main + c.cache
 }

pred write [c, c': CacheSystem, a: Addr, d: Data] {
 c'.main = c.main
 c'.cache = c.cache ++ a -> d
 }

pred read [c: CacheSystem, a: Addr, d: Data] {
 some d
 d = c.cache [a]
 }

pred load [c, c': CacheSystem] {
 some addrs: Addr |
  c'.cache = c.cache ++ addrs <: c.main
 c'.main = c.main
 }

pred flush [c, c': CacheSystem] {
 some addrs: some c.cache.Data {
  c'.main = c.main ++ addrs <: c.cache
  c'.cache = c.cache - addrs -> Data
  }
 }

// This command should not find any counterexample
LoadNotObservable: check {
 all c, c', c": CacheSystem, a1, a2: Addr, d1, d2, d3: Data |
  {
  read [c, a2, d2]
  write [c, c', a1, d1]
  load [c', c"]
  read [c", a2, d3]
  } implies d3 = (a1=a2 => d1 else d2)
 }

これを実行すると、a1 ≠ a2 => d3 = d2を満たさないという反例が出る。

writeの結果キャッシュ上のa2はd2を指すようになったのだが、loadの対象にa2が選ばれる事によりc'の時点でmainが指すd1をc''の時点で指すようになってしまっている。
これを解釈した結果が本文での「flushされる前にloadされた」なのだが、そのような見方がしっくりくるまでかなり手間取ったというお話。