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

• Item type: Trans(1)
• 公開日: 2009-08-28
• タイトル: リターンバリア型実時間ごみ集めの抽象モデル検査
• タイトル / 言語: en
• タイトル: Abstract Model Checking of Real-time Garbage Collection with Return Barriers
• 言語: jpn
• キーワード / 主題Scheme: Other
• キーワード / 主題: 通常論文
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_6501
• 資源タイプ: journal article
• 著者所属: 京都大学大学院情報学研究科，現在，任天堂株式会社
• 著者所属: 京都大学大学院情報学研究科
• 著者所属: 京都大学大学院情報学研究科
• 著者所属: 京都大学大学院情報学研究科
• 著者所属(英): en
• 著者所属(英): Graduate School of Informatics, Kyoto University / Presently with Nintendo Co., Ltd.
• 著者所属(英): en
• 著者所属(英): Graduate School of Informatics, Kyoto University
• 著者所属(英): en
• 著者所属(英): Graduate School of Informatics, Kyoto University
• 著者所属(英): en
• 著者所属(英): Graduate School of Informatics, Kyoto University
• 著者名: 藤川, 浩光; 馬谷, 誠二; 八杉, 昌宏; 湯淺, 太一
• 著者名(英): Hiromitsu, Fujikawa; Seiji, Umatani; Masahiro, Yasugi; Taiichi, Yuasa
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: 実時間ごみ集めアルゴリズムの代表的なものとしてスナップショット方式があげられるが，このアルゴリズムのルート挿入を改良したものに，リターンバリアという手法がある．スナップショット方式のルート挿入では，プログラムの実行を止める必要があった．この停止時間はスタックの大きさに依存していたが，リターンバリア方式ではスタックをフレーム単位で分割してルート挿入することにより，より停止時間を短縮することができる．我々は簡略化したリターンバリア型実時間ごみ集めの安全性の証明に成功した．ここでの簡略化とは，通常ならヒープ領域のセルが 2 つ以上のポインタを持てるところを，1 つに限定したということである．さらに，実際の処理系ではルート挿入の間にもスタックが伸び縮みするが，証明を複雑にする可能性があったので，スタックが伸び縮みしない処理系モデルを対象とした．安全性とは使用中のセルを誤ってごみとして回収しないという保証である．現在，様々な実時間ごみ集めアルゴリズムが提案されており，プログラムの停止時間が短くなるよう改良されている．しかしアルゴリズムは複雑さを増しており，一見して安全性があるのか分かりにくいことも多い．モデル検査で安全性を証明されたアルゴリズムであれば，より安心して実用的に使うことができる．先行研究として，簡略化したスナップショット方式ごみ集めの安全性が，抽象モデル検査とよばれる手法で証明されている．本研究ではこれに基づいて抽象モデル検査を行い，リターンバリアを使う場合と使わない場合の比較を行った．また，抽象化が正しく行われていることも定理証明系である Isabele/HOL を用いて証明した．
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: Snapshot GC (garbage collection) is one of the most popular real-time GC algorithms and “return barrier” is the method that improves root insertion of the snapshot GC algorithm. The original snapshot GC algorithm required to stop the running program during root insertion. This pause time of programs depends on the size of the stack. GC with return barriers can shorten the pause time by dividing root insertion. We proved the safety of a simplified version of the real-time GC with return barriers. Here, “simplified” means two things. One is that we assume each cell in the heap area contains at most one pointer whereas each cell in general has multiple pointers. The second is that we used a processor model that does not support dynamic changes of the stack size. “Safety” guarantees that GC never collects cells in use as garbage. So far, various real-time GC algorithms have been proposed, which reduce the pause time of programs. However, these algorithms are complex and it is often difficult to judge their safety at a glance. We can safely use such an algorithm if we can prove its safety with model checking. We checked the algorithm based on this method, and compared the abstract systems for GC with return barriers and for the original snapshot GC. We also proved the validity of abstraction using the theorem prover Isabelle/HOL.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AA11464814
• 書誌情報: 情報処理学会論文誌プログラミング（PRO）; 巻 2, 号 4, p. 13-32, 発行日 2009-08-28
• ISSN / 収録物識別子タイプ: ISSN
• ISSN / 収録物識別子: 1882-7802
• 出版者 / 言語: ja
• 出版者: 情報処理学会