学生の研究紹介

学生が取り組むテーマは各学生とスタッフが話し合って決めています．以下はその一例です．

Webアプリケーションは，ユーザから送られてきたリクエストから動的にWebページの生成を行うアプリケーションです．近年，コンピュータやスマートフォンの所有者が増え，インターネットが広く普及したことで，Webアプリケーションの需要は大きくなりました．しかし，一からWebアプリケーションを実現するためには，データベースとの連携等，様々な技術を複合させる必要があります．Webアプリケーションフレームワークは，このような困難性を取り除き，少ないコード量でユーザがWebアプリケーションを開発できるような支援をします．

本研究では，関数型言語SML#による型安全でかつ宣言的な記述が可能であるようなWebアプリケーションフレームワークの実現を目指します．

SML#サーバーの実現

Cのサーバー機能埋め込みライブラリであるlibmicrohttpd を利用し，SML#でサーバー機能を利用するためのライブラリを構築しました．Webサーバーは，以下の型を持つ関数によって記述することができます．

main : (request -> response) -> unit

型付きテンプレートエンジンの実現

リクエストを送信することで，サーバーからレスポンスを得ることができます．この結果から動的にWebページを生成するためには，得られた値をWebページに埋め込む必要があります．一般に，このような値の埋め込み作業はテンプレートエンジンを用いて行います．テンプレートエンジンは，テンプレートファイルに記述されるテンプレートと呼ばれる構造を読み込み，その中に含まれる「ホール」と呼ばれる変数に対して値を埋め込むことで，Webページの動的な生成を行います．

しかし，誤ってホール名を誤って指定した場合，値が埋め込まれず，意図した結果が得られません．このような場合，テンプレートエンジンはホール名の誤りを報告しないため，テンプレートのサイズによっては，埋め込み失敗の検出が困難となります．そこで，テンプレートに型を与え，型チェックを行うことでホール名の不整合を検出し，この問題を防ぐことを考えます．テンプレートは以下の4つの操作で扱うものとします．

1. import ： テンプレートを読み込む．
2. templateAs ：読み込んだテンプレートに対して動的な型チェックを行い，静的なビューを与える．
3. fill：テンプレートのホールに対して，型付きの操作として値の埋め込みを行う．
4. export：全てのホールに値が埋め込まれた結果を出力する．（ホールが全て埋まっているかどうかの確認も行う）

このようなテンプレートエンジンの実現のために，CのテンプレートテンプレートライブラリであるClearSilverを用いました．また，テンプレートに型を与える上で，部分動的レコード[Buneman, Ohori, TODS'96][Ohori, Ueno, Sasaki, Kikuchi, ECOOP'16]を用いました．

近年，膨大な量のウェブページのページランクを計算するなど，巨大なグラフを扱う機会が増えています．このような巨大なグラフを並列処理することを目的として，頂点主体プログラミングモデルや，そのモデルを採用したPregelシステム[Malewicz et al., SIGMOD'10]が提案されました．

当研究室では，SML#からPregelシステムを駆動させる研究に取り組んでいます．

Pregelシステムのオープンソース実装であるPregel+[Yan et al., WWW'15]のSML#バインディングを作成しました．SML#はC言語向け外部関数インターフェースを持つので，非常に容易にバインディングを作成することが出来ます．

Pregel+のSML#バインディングを用いて，SML#の頂点主体プログラミングライブラリを作成しました．これにより，SML#で頂点主体プログラミングを行うことが出来ます．

当研究室の既存の研究として，等式集合（連立方程式）をデータとして扱い，等式集合の変形によって計算を行うという研究があります．[Nishimura, Ohori, JFP'99] 等式集合の変形を計算モデルとして，Pregelシステムを高水準に駆動させる研究に取り組んでいます．

SML#に実装されているCとの直接連携機能の概要

SML#の主な機能の1つに，Cとの直接連携があります．SML#では，整数や浮動小数点データなどの全てのデータは，計算機アーキテクチャが定める標準のデータフォーマットでメモリ上に格納されます．このため，データ変換を一切行わずにSML#のデータをC関数に直接引数として渡すことができます．このような機能は，プログラム中の全てのデータにおける実行時表現をCと同様な自然なものにするコンパイル技術[Nguyen and Ohori, PPDP'06]と，MLとCとの間でのコールバックを含む関数の呼び出しを可能にする外部関数とのインターフェース技術[上野, 大堀, コンピュータソフトウェア'10]によって実現されています．これにより，SML#では関数名とその関数の型を宣言するだけで，C関数を呼び出すことができます．例えば，Cの標準ライブラリ関数putsは以下のように宣言することで，SML#から呼び出すことができます．

val puts = _import “puts” : string -> int

Cとの直接連携機能に残されている課題

SML#のCとの直接連携機能を利用することで，多くのライブラリ関数を特別なデータ変換をすることなくSML#にインポートすることができます．しかし，現在のSML#に実装されているCとの連携機能には主に2種類の課題が残されています．1つは，インポートしたC関数に対応するSML#の関数型が，C関数を使いこなすための有用な情報を含まないため，関数の可読性が低下するという課題です．具体的には，構造体へのポインタ型をタプル型に対応付けているため，Cの構造体型が持つメンバ名が失われます．また同様に，C関数の引数の並びをタプル型に対応付けているため，同じ型の引数が複数並ぶと，ユーザはその型から各引数の意図を区別することが難しくなります．もう1つの課題は，SML#でサポートしていないCの型があり，SML#にインポートできないC関数が存在するということです．特に共用体型については一切サポートされていないため，共用体を受け取るC関数をインポートすることはできません．本研究室ではこれらの課題を解決し，SML#におけるより利便性の高いCとの直接連携機能の実現を目的とした研究開発を進めています．

構造体により厳密に対応する型の導入

フィールドの順序をラベルの一部として指定できる順序付きレコード型を導入しました．例えば，以下の順序付きレコード型は，最初のフィールドがstring型で，次のフィールドがint型であるレコード型です．

{1_name : string, 2_age : int}

ラベルの先頭に含まれる自然数によって，フィールドの順序を指定できます．

この順序付きレコード型を構造体へのポインタ型に対応する型として，Cとの連携機能に実装することで，構造体のメンバ名を失うことなく構造体を受け取る関数をインポートすることができます．本手法によって，int型の9つのメンバを持つ構造体を受け取る標準ライブラリ関数asctimeは以下のようにインポートすることができます．

val asctime = _import "asctime" :
(1_tm_sec: int, 2_tm_min: int, 3_tm_hour: int, 4_tm_mday: int,
 5_tm_mon: int, 6_tm_year: int, 7_tm_wday: int, 8_tm_yday: int, 9_tm_isdst: int) -> char ptr

提案手法では，レコードラベルに構造体のメンバ名が含まれるため，関数の可読性が向上します．

ラベル付きの型による引数の並びの表現

上で述べた順序付きレコード型をC関数の引数の並びにも応用することで，ラベルとして引数名を関数型に含めることが可能となります．例えば，float型の4つの引数を受け取るOpenGLのglClearColor関数は以下のようにインポートすることができます．

 val glClearColr = _import "glClearColor" :
(1_red: Real32.real, 2_green: Real32.real, 3_green: Real32.real, 4_alpha: Real32.real) -> ()

提案手法では，関数の型にラベルとして引数名を含んでいるため，可読性が向上します．

共用体型のサポートに関する検討

共用体型は，複数のメンバが同じメモリ領域を共有し，代表で1つのメンバをデータ表現とします．これと同じような性質を持つSML#の型にヴァリアント型があります．ヴァリアント型は，SML#では以下のように宣言します．

datatype A = Dog of string | Cat of string

各ヴァリアントに対するデータの格納は，タグ(この例だとDogやCat)をキーとして行われます．例えば，Dog “Pochi” のようにしてヴァリアントにデータを格納します．このタグの有無を除けば，ヴァリアント型は共用体型に近いデータ型であると言えます．本研究室では，ヴァリアント型と同様な使い方ができる共用体型に限り，共用体型をSML#にインポートする方針を検討しています．

レコードとは名前と値のペアを集めた汎用的なデータ構造です．基本的なMLの枠組みではレコードに対する操作は選択および更新しか扱えず，現実世界のデータを扱う際には力不足と感じることがあります．本研究ではレコード同士の結合演算といった，よりリッチな演算を扱うための理論的枠組み，ならびに実装方式の構築を目的とした研究開発を進めています．

現在は特にレコード上の自然結合演算の実現に向けた研究を進めております．自然結合演算とは，部分的な記述を統合し，より詳細な記述とする演算です．

理論的枠組みについては，型については以下に示すようにMLの基本的な型システムを制約集合で拡張することで比較的容易に導入が可能であると考えております．より実装に適した枠組みとするため，制約の妥当性の確認は遅延させる戦略を採っております．この枠組みはOhoriらによるシステム[Ohori, Buneman, LFP '88]をHM(X)[Odersky, Sulzmann, Wehr, TAPOS'99]スタイルで拡張したものです．

値の評価に関しては以下の大小関係の下で上限を計算する演算の特殊な場合として定義できます．これはBunemanらによる成果[Bunema, Jung, Ohori, TCS'91]に基づくものです．

実装方式の構築については，現在取り組んでいる主な課題となっております．自然結合を実行するためには対象となるレコードの各値に対応した名前の情報，すなわちレコードの型情報が必要となりますが，この情報はプログラムの実行時には残っていません．現在，型情報を実行時にも残す方針を軸に実装方式の検討を進めています．

関数型言語によるハードウェア資源の直接制御

オペレーティングシステム(OS)の実現には，レジスタやメモリなどハードウェアの直接制御が不可欠です．我々は，OSの開発言語として，C言語やアセンブリ言語より強い型システムを持ち，整合性を検査する機構が内包されている関数型言語の中でも特にSML#に着目しています．SML#の以下の特徴が，ハードウェアレベルプログラミングにおいて有用です．

• SML#が扱うデータは，ハードウェアのネイティブなデータ表現と同じです．
• Cとの直接連携機能により，Cで記述された関数をSML#コードにリンクし，呼び出すことができます．

我々はこれまで，SML#によるOS開発の可能性を検討し，SML#による試作を続けてきました．

x86プロセッサを対象にした試作

最初の試作として，仮想マシン上で動作する，Intel x86プロセッサ向けの，コンソール機能を提供するプログラムを実装しました．このプログラムは，ブートローダや，GDTやVRAMへのアクセスや割り込み発生時のレジスタ退避を行うアセンブリコードを除いて，SML#で書かれています．

インフラ的機能とコンソール機能の実装

SML#によるハードウェアプログラミングを実践するにあたって，以下のインフラ的機能を整備しました．

• SML#コードとアセンブリ言語コード間の呼び出し機構
  • SML#コードからのアセンブリ言語関数の呼び出しについては，SML#の，Cとの直接連携機能を利用しました．
  • アセンブリ言語コードからのSML#関数の呼び出しについては，呼び出しプロトコルをSML#とアセンブリ言語で実装しました．
• ハードウェアアクセスのためのインタフェース
  • 特定のレジスタ，メモリ領域の特定番地，特定のI/Oポートへのアクセスを提供するプリミティブをアセンブリ言語で記述し，導入しました．
• SML#コードのラインタイム関数
  • SML#コードのランタイム関数は，OSによるサポートを前提としている為，いくつかをスタブ関数として定義したり，ハードウェアレベルプログラムに対応すコードに変更しました．

コンソール機能として，以下の機能を実装しました．

• ブートローダおよび32bitアドレス空間の設定
• ディスプレイ制御
• キーボード割り込み制御

これらは，上述のプリミティブを利用し，SML#とアセンブリ言語で実装しました．

本試作における検討

この試作を通じて，ディスプレイやキーボードなどのデバイス制御や，割り込みベクタの設定と割り込み処理ルーチンなど，ハードウェアに肉薄した処理についても，ほぼSML#で記述できる確信を得ました．

ARMプロセッサを対象にした試作

上述の結果を受けて，我々は現在，Raspberry Pi上で動作するOSのSML#での開発に取り組んでいます．その第一歩として，最初の試作と同程度の機能を持ち，Raspberry Pi上で動作するプログラムを，SML＃での記述箇所を増やすことを目指し，試作しています．

インフラ的機能とコンソール機能の実装

本試作では，上述のインフラ的機能の，以下の点について改良しました．

• ハードウェアアクセスを提供するプリミティブの改良
• SML#コンパイラからARMをターゲットとしたコードを生成するための改良

最初の試作と同程度の機能をRaspberry Pi実機上で実現するには，以下の機能を実装します．

• ブートローダとファームウェア
• 仮想アドレス空間
• 割り込みベクタテーブルとキーボード割り込み制御
• ディスプレイ制御