非決定的並列プログラム検証のための論理時間に基づく再演機構

点击翻译按钮获取中文摘要

本年度行った研究の実績は次の通りである。(1)イベント及び論理時間の定義とその検証並列オブジェクト指向言語プログラムの実行において、メッセージの通信、各ノードプロセッサ上でのコンテクスト切り替えなど、処理の区切りとなるものをイベントとして定義し、イベント間の半順序関係をもとに論理時間を定義した。(2)論理時間に基づく再演実行機構の設計提案する方式の要点は、イベントを計測しながらテスト実行を行い、イベント記録をもとに、各イベントの論理時間を定めるとともに、再演時には論理時間によって再演実行の順序を決定するものである。(3)デバッガの設計、試作(1)、(2)に基づく並列プログラムデバッガを設計し、研究室で試作したマルチコンピュータ上に実現した。各ノードはイベントが発生するたびにこれを記録し、一定の時間間隔でホストに送信する。デバッガの試作に当たっては、各ノード上のファームウェアを活用して、できるだけプローブ効果を抑える工夫をした。(4)実験による評価実験によって、イベントに基づく論理時間の定義を基本とする記録、表示、再演のための機構の有効性が明らかになった。特に、使用者から見ると、非同期的な現象をあたかも同期的な現象のように扱えるため、極めてデバッグしやすくなる。また、デバッグ機能の付加に伴う動的な負荷は、イベント記録について、1イベント当り平均0.04ms、記憶容量において約35Bであり、リプレイの実行性能が1論理時間に対する表示に0.94sと十分実用に耐えるものであることを確かめた。(5)成果報告本研究の成果については、添付の研究発表に示すように、電子情報通信学会論文誌、及びSpringer社Lecture Notes in Computer Science1107などに掲載となった。また、関連する研究成果の報告を添付の文献リストに示すように行った。