2011年11月8日火曜日

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された」なのだが、そのような見方がしっくりくるまでかなり手間取ったというお話。

2011年4月26日火曜日

存在限量子を解釈する際に勘違い

松坂の集合位相入門P.19あたりにある集合系のすべての要素を対象にした和集合をCoqの帰納型で表現しようとしたが、それを使って本文の命題を証明するときに問題が発生した。

本文中では

∪V = {x|∃ A∈V (x∈A)}

というような∃量化を使った定義だったが、これをCoqで使われるような表記に直す際に

forall x:U, exists A:Ensemble U, A∈V -> x∈A

という解釈をしてしまい、AがVに含まれない場合を考慮しなければならなくなった。集合系Vに含まれる筈の集合Aを議論する際にそれはないだろうと。

本文中の式を日本語で「定義されるXの全ての要素に対して、xを含むようなVの元Aが存在する」というように解釈すると、なんとなく後半が含意でなく論理積を表現しているようなにおいがするんだけど・・・∃より∀の方が使い慣れているので、こちらを使った定義でよく使われる含意を使った形式につられてしまったのだろうか