線形論理に基づく並列計算の枠組み及びプログラミング言語の設計・実装に関する研究

1995 Fiscal Year Annual Research Report

• Project/Area Number: 06452389
• Research Institution: University of Tokyo
• Principal Investigator: 米澤 明憲 東京大学, 大学院・理学系研究科, 教授 (00133116)
• Co-Investigator(Kenkyū-buntansha): 松岡 聡 東京大学, 大学院・工学系研究科, 講師 (20221583) ; 小林 直樹 東京大学, 大学院・理学系研究科, 助手 (00262155)
• Keywords: 並列言語 / 並列オブジェクト / 静的解析 / 線型タイプ

Research Abstract

本年度は、昨年度から行なってきた線形論理に基づく型付並列言語HACLのコンパイラのシングルプロセッサ上への作成をほぼ完成させ、さらにワークステーションクラスタ上の分散処理系の設計およびプロトタイプコンパイラの作成を行なった。我々はHACLをそれ自身有用な並列プログラミング言語としてと同時に、その上に高レベルなプログラミング言語を作成するための核言語としても位置付けており、実際に並列オブシェクトなどの高レベルの機能が効率良く実現できることを作成したコンパイラを通して検証した。
さらに我々は、HACLを含めた非同期通信に基づく並列言語のより効率のよい実現のために、いくつかの静的解析技法を考案した。具体的には並列プログラムの効率の鍵となるプロセス間通信の効率をあげるために、(1)各通信チャネルに一度にたまるメッセージ数の上限の解析、(2)各通信チャネルが通信に使用される回数の解析、を行なった。(1)については関数型言語のエフェクト解析の手法を応用した解析手法を示し、それが正しいことを理論的に証明するとともに、解析プログラムのプロトタイプを作成して予備実験を行なった。(2)については線形タイプの概念を利用した解析手法を示すとともに、その正しさの理論的証明、および解析でえられた結果を利用したプログラム変換を正当化するためのプロセス等価性の理論を開発した。これにより、例えば関数型言語における末尾再帰呼び出しの除去に相当する最適化が並列言語においても可能になった。また、(2)の解析は効率の向上だけでなく、並列プログラムの安全性を向上させるのにも役立つことがわかった。

Research Products

• [Publications] Naoki Kobayashi and Akinori Yonezawa: "Asynchronous Communication Model Based on Linear Logic" Formal Aspects of Computing, Springer-Verlag. 7. 113-149 (1995)
• [Publications] Naoki Kobayashi, Motoki Nakade, and Akinori Yonezawa: "Static Analysis of Communication for Asynchronous Concurrent Programming Languages" International Static Analysis Symposium(SAS'95), Springer-Verlag LNCS. 983. 225-242 (1995)
• [Publications] Naoki Kobayashi, Benjamin C Pierce, and David N.Turner: "Linearity and the Pi-Calculus" Proceedings of ACM SIGACT/SIGPLAN Symposium on Principles of Programming Languages(POPL'96). 358-371 (1996)