なんかAlloyでいろいろできそうな気がしてきたので、参照カウント式GCでメモリリークがあることを検証してみます。
とりあえず、こんな感じでモデルを作ります。今回は、参照のカウントはとらずに、参照があるかないかで判断することにします。
module exec/refgc
abstract sig メモリ{
参照: set 割り当て
}
one sig ルート extends メモリ{
}
sig 割り当て extends メモリ{
}
pred show{
}
run show
「割り当て」というのが、なにかに割り当てられたメモリです。
こんなインスタンスがでました。
あと、こんな感じで、どこからも参照されてない割り当ても存在できてます。
ということで、割り当てメモリは必ずどこからか参照されることにします。つまり、どこからも参照されてないメモリをGCするということです。
fact{
all a:割り当て | some m:メモリ |
a in m.参照
}
書き下すと「すべての割り当てについて、どこかのメモリの参照に含まれている」となります。
そうすると、こんな感じ
他の例をみても、すべての割り当てがどこかから参照されてます。
ただ、自己参照は絵的に面白くないので、自己参照は含めないことにします。
fact{
all a:割り当て | some m:メモリ |
not a in a.参照 and
a in m.参照
}
これで自己参照なくなった。
ここまでで、生成されたインスタンスを全部みてるとルートから浮いた割り当てメモリがあることはわかるんですが、それをちゃんとAlloyさんにみつけてもらいましょう。
ルートから参照でたどれない割り当ては存在しない、というassertをcheckしてみます。
assert ルートからたどれる{
no a:割り当て |
not a in ルート.^参照
}
check ルートからたどれる
そうすると、こんな反例がでました。
割り当て０と割り当て１が相互に参照しあっています。
ということで、参照されているかどうかを基準にメモリを回収しようとしても、循環参照してる割り当てメモリは残ってしまうことがわかりました。
Alloy、おもしろくなってきました。慣れると小さい仕様ならヒアリングしながらでも検証できたりしそうです。たぶん無駄に検証したりしそうです。おもしろがって。
ソースはこんな感じになりました。
module exec/refgc
abstract sig メモリ{
参照: set 割り当て
}
one sig ルート extends メモリ{
}
sig 割り当て extends メモリ{
}
fact{
all a:割り当て | some m:メモリ |
not a in a.参照 and
a in m.参照
}
assert ルートからたどれる{
no a:割り当て |
not a in ルート.^参照
}
check ルートからたどれる
pred show{
}
run show
