リターンバリア型実時間ごみ集めの抽象モデル検査

概要

論文の詳細を見る
実時間ごみ集めアルゴリズムの代表的なものとしてスナップショット方式があげられるが,このアルゴリズムのルート挿入を改良したものに,リターンバリアという手法がある.スナップショット方式のルート挿入では,プログラムの実行を止める必要があった.この停止時間はスタックの大きさに依存していたが,リターンバリア方式ではスタックをフレーム単位で分割してルート挿入することにより,より停止時間を短縮することができる.我々は簡略化したリターンバリア型実時間ごみ集めの安全性の証明に成功した.ここでの簡略化とは,通常ならヒープ領域のセルが 2 つ以上のポインタを持てるところを,1 つに限定したということである.さらに,実際の処理系ではルート挿入の間にもスタックが伸び縮みするが,証明を複雑にする可能性があったので,スタックが伸び縮みしない処理系モデルを対象とした.安全性とは使用中のセルを誤ってごみとして回収しないという保証である.現在,様々な実時間ごみ集めアルゴリズムが提案されており,プログラムの停止時間が短くなるよう改良されている.しかしアルゴリズムは複雑さを増しており,一見して安全性があるのか分かりにくいことも多い.モデル検査で安全性を証明されたアルゴリズムであれば,より安心して実用的に使うことができる.先行研究として,簡略化したスナップショット方式ごみ集めの安全性が,抽象モデル検査とよばれる手法で証明されている.本研究ではこれに基づいて抽象モデル検査を行い,リターンバリアを使う場合と使わない場合の比較を行った.また,抽象化が正しく行われていることも定理証明系である Isabele/HOL を用いて証明した.
一般社団法人情報処理学会の論文
2009-08-28

リターンバリア型実時間ごみ集めの抽象モデル検査

スポンサーリンク

概要

著者

関連論文

スポンサーリンク