高級並列言語の様々な安全性を保証するプログラム進化支援つき汎用型システムの研究

2001 Fiscal Year Annual Research Report

• Project/Area Number: 13780203
• Research Category: Grant-in-Aid for Encouragement of Young Scientists (A)
• Research Institution: The University of Tokyo
• Principal Investigator: 五十嵐 淳 東京大学, 大学院・総合文化研究科, 助手 (40323456)
• Keywords: 型システム / 並行プログラム / 安全性 / Java / プログラム進化 / 資源使用解析

Research Abstract

ここ数年のインターネットおよびWorld Wide Web(WWW)の普及,また並列計算機の普及に伴い分散/並列環境上でのプログラミング技術が注目を集めている。本研究では,分散/並列プログラミングにおける様々な安全性(デッドロック/競合状態が起きないこと,計算資源が正しく使われること)を保証するための統一的な枠組みを構築することを目的としている.本年度の研究成果は以下の通り.
1.計算資源に対するアクセス方法の正しさの検証のための型システムの考案
計算機システムにおいては,プログラムは記憶領域(メモリ),ネットワーク,CPU,ファイルなどさまざまな資源を共有して動作しており,あるプログラムが不正に資源にアクセスを行うと,計算機システム全体の動作に悪影響を与える.本研究では各プログラムが正しいプロトコルで資源にアクセスすることを検証するための型システムの確立に成功した.この型システムを用いることにより例えば,(1)新たにメモリを獲得したらいずれそのメモリを解放する.すでに解放したメモリ領域への読み書きを行わない,(2)ファイルを開いたらいずれ閉じる.閉じたあとは読み書きを行わない,(3)ある資源にアクセスする前には必ずその資源に関するロックを獲得してから行う.ロックを獲得したらいずれ解放する.
2.プログラム進化支援のための型システムの形式化
一般的に,すでに流通している言語へ新しい機能(ここでは先進的型システム)を組み込む場合には,新しい機能を仮定せずに書かれた既存のプログラム部品を,を最小限の書き換えで,新しい環境下での部品と組み合わせ実行できることが望ましい.この目的のために,既存のraw typesという技術を基礎にする方向であるが,これは比較的新しい技術であるため,理論的な基盤を確立する必要がある.本年度はraw typesの理論の研究を行い,raw typesを実際に使っている既存の言語処理系の不具合を発見することに成功した.

Research Products

• [Publications] A.Igarashi, N.Kobayashi: "Resource Usage Analysis"Proceedings of ACM SIGPLAN/SIGACT Symposium on Principles of Programming Languages(POPL2002). 331-342 (2002)
• [Publications] A.Igarashi, B.C.Pierce, P.Wadler: "Featherweight Java : A Minimal Core Calculus for Java and GJ"ACM Transactions of Programming Languages and Systems. 23(3). 396-450 (2001)