2018 Fiscal Year Annual Research Report
A reversible debugging model for real-time concurrent programs
| Project/Area Number |
17H01722
|
|---|
| Research Institution | Nagoya University |
|---|
Principal Investigator |
結縁 祥治 名古屋大学, 情報学研究科, 教授 (70230612)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
西田 直樹 名古屋大学, 情報学研究科, 准教授 (00397449)
関 浩之 名古屋大学, 情報学研究科, 教授 (80196948)
中澤 巧爾 名古屋大学, 情報学研究科, 准教授 (80362581)
|
|---|
| Project Period (FY) |
2017-04-01 – 2021-03-31
|
| Keywords | 逆計算モデル / バックトラック逆計算 / 構造操作意味規則 / 因果無矛盾性 / 実時間プログラム |
|---|
| Outline of Annual Research Achievements |
本年度は、並行プログラミング言語に逆計算機構を導入する手法および実時間を考慮したプログラムカリキュラスの提案を中心にして研究を進めた。前者については、バックトラックに基づく逆計算機構をプログラミング言語を導入する計算について、欧州Cost Action(IC1405)プロジェクトのメンバーと共同して研究を実施した(結縁)。ここでは、構造的操作意味定義に基づく手続き、関数定義、ループ構造など、実用的なプログラムに対して、アノテーションを加えてバックトラックに基づく逆計算を定義した。後者については、TimedRCCSを提案した。時間についてのプログラムカリキュラスに関する研究は、既存研究のRCCSを拡張する形で実施した（結縁）。さらに、CCSKの時間拡張についても研究を行った。その他に、逆計算の操作意味定義に関する拡張(結縁)、関数型並行分散プログラミング言語Erlangの逆計算意味(西田)について研究をすすめた。さらに、逆計算デバッグのための情報圧縮技術についても研究を実施した(関)。
逆計算については、バックトラックに基づいて情報を蓄積する方法については単一のスタックにもとづいて巻き戻す方法について検討し、時間については時間の経過が持つ特性を活かした意味論を展開することを試みた。後者については、今年度の研究ではプログラムの並行構造にもとづく逆計算情報のデータ蓄積方法が複雑であり、並行構造の反映には限界があることがわかった。合成可能性という観点から、より扱いやすいモデルの提案が必要であることがわかった。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
本年度は、より技術的な内容について検討を進めた。逆計算を並行プログラミング言語、時間を考慮した体系への拡張について知見を得た。逆計算においては、単純に実行した経路を巻き戻すバックトラック型の逆計算に加えて、因果無矛盾性を保存する逆計算を考慮する必要がある。逐次計算において、この両者に違いはないが、並行分散計算機構を持つ場合は、デバッグという観点においては後者の方がより自然である。これは、通信などの同期機構によって分散計算が行われる場合、全体の状態をまとめて状態を正確に定義することが懇談であるという並行分散計算の本質に基づく。また、これらのアイデアに基づくプログラミング言語定義との関係について一定の知見を得た。
|
| Strategy for Future Research Activity |
今後は、因果無矛盾性に基づく逆計算機構を研究する。デバッグの観点から、技術的に興味深い点は、因果無矛盾性にもとづくデバッグ機構の定式化である。バックトラックに基づく逆計算では、デバッグが必要になるポイントが明確に定義できない場合がある。例えば、問題のあるスレッドに到達するまでの他のスレッドの実行は多数の組み合わせがあり、要求された性質が成り立たなくなるポイントが明確でない。デバッグの原因となるポイントを詳細に解析するには、バックトラックよりも制約条件を緩めた因果無矛盾性にもとづいて、デバッグポイントを指摘する方が自然である。今後は、因果無矛盾性に基づくデバッグ手法を検討し、並行プログラミングにおいて実際的なモデルを考案する観点から、データを直接的に扱うためのデバッグモデルを考案する。
時間経過を含めた逆計算の意味の定義を研究する過程で得られた知見として、従来Ulidowskiらによって提案されている枠組みを拡張する必要があることが判明したため、順方向の時間経過意味から逆方向計算を導き出すことが可能なクラスの同定に関する研究を実施する。また、時間経過とオートマトンモデルにおけるデータの扱いについての関係を明らかにすることによって、時間経過の逆方向計算のメカニズムを明らかにする。
|
