日本ソフトウェア科学会第 33 回大会 (2016 年度) 講演論文集

OS を関数型言語のみで開発するための検討と試作
徳永 航平

上野 雄大

大堀 淳

本論文では，関数型言語で OS を実装することに向けて行っている一連の検討と試作の経緯と現状を報告する．OSの実現には，レジスタやメモリなどのハードウェアの直接制御が必要不可欠である．従って主要な OS の開発は C言語やアセンブリ言語を用いて行われてきた．一方，より高級な言語，特に関数型言語で記述すれば，モジュール性や安全性などの点で有益である．C との直接連携機能を持つ SML#ならば，プリミティブをいくつか導入するだけで，ハードウェアレベルのコードを記述でき，OS 全体も SML#のみで記述できると期待できる．著者らはこれまでに，PC/AT 互換機上で動作し，割り込み制御，32bit アドレス空間，コンソール制御機能を持つプログラムをSML#とアセンブリ言語で実装した．現在，同様の試みを ARMv8 プロセッサを内蔵する Raspberry Pi 上で行っている．これら試みの結果と現状を報告し，展望を述べる．

考えられる．実際に，関数型言語を用いた OS 開発の1 はじめに試みがいくつか報告されている． [1] [2]OS の実現には，レジスタやメモリなどのハード著者らは，OS の開発言語として，関数型言語の中ウェアの直接制御が不可欠である．従って，これまででも特に SML# [3] に着目している．SML#は，東主要なオペレーティングシステム（OS）の開発は C

北大学で開発を進めている関数型言語で，他の関数言語やアセンブリ言語を用いて行われてきた．一方，型言語と同様に，静的な型検査による高い安全性と，OS はあらゆるプログラムが動作するための基盤であモジュール性の高さを持つ．さらに，SML#が扱うり，その構成には高い信頼性が要求される．C 言語やデータは，ハードウェアのネイティブなデータ表現とアセンブリ言語は，プログラムの正しさを検査する枠同じである．すなわち，ハードウェアが要求する様々組みが弱いため，それらの言語を用いて高い信頼性をなデータ構造を SML#のコード上でそのまま扱うこ確保しながら OS を開発することは難しい．この問題とが可能である．また，C との直接連携機能により，に対する根本的な解決策のひとつは，C 言語より強C 言語で記述された関数を SML#コードにリンクし，い型システムを持ち，整合性を検査する機構が内包呼び出すことができる．これにより，機械語命令に直されているプログラミング言語を用いることである．

接対応するいくつかのプリミティブを C 言語で記述

そのような言語のなかでも，関数型言語は，様々な言し，導入するだけで，機械語命令やレジスタ，特定の語機能の研究開発が行われ応用可能性が期待されてメモリ番地への直接アクセスが得られ，SML#で直おり，安全性の高い OS をより効率的に開発できると接ハードウェアレベルのコードを記述することができると期待できる．これら SML#の機能を駆使するな

Kohei Tokunaga, 東 北 大 学 大 学 院 情 報 科 学 研 究 科,
Graduate School of Information Sciences, Tohoku
University.
Katsuhiro Ueno, Atsushi Ohori, 東北大学電気通信研究所, Research Institute of Electrical CommunicationTohoku University.

らば，コントロールレジスタの設定や割り込み制御を含む，今日の OS では C 言語で書くような箇所のほぼ全てを，SML#でも書くことができるはずである．
著者らはこれまで，以上の方針に基づき，SML#による OS 開発の可能性を検討し，SML#による試作を続けてきた．これまでの経緯は以下の通りである．

上を対象に現在行っている試みとして，同程度の機能

まず，仮想マシン上で，Intel x86 プロセッサ向けの，を有するプログラムの，実装戦略および実装の現状をコンソール機能を提供するプログラムをスクラッチか詳細に述べる．最後に第 4 節で本論文をまとめ，今ら試作した．このプログラムは，起動直後に GDT な後の展望について述べる．

どを適切に構築することで 32bit アドレス空間を設定し，割り込みテーブルに SML#で書かれたキーボード割り込みハンドラを設定した後，キー入力の内容

2 SML#とアセンブリ言語による，Intelx86 プロセッサにおける試作をディスプレイにそのまま出力するプログラムに制

本節では，関数型言語による OS の開発にむけて最御を渡す．以上の全てのコードは，ブートローダや，初に試作した，仮想マシン上で動作する，Intel x86

GDT や VRAM へのアクセスや割り込み発生時のレプロセッサ [4] 向けの，コンソール機能を提供するプ

ジスタ退避を行うアセンブリコードを除いて，全てログラムの実装について述べる．はじめに，SML#でSML#で書かれている．この試作を通じて，ディス記述された関数ととアセンブリ言語で記述された関プレイやキーボードなどのデバイス制御や，割り込数が互いに呼び出しを行う機構と，それを利用したみベクタの設定と割り込み処理ルーチンなど，ハーハードウェア資源へのアクセスについて述べる．次

ドウェアに肉薄した処理についても，ほぼ SML#でに，本試作で実装したプログラムの，機能ごとの実装記述できる確信を得た．この結果を受けて，我々は現の詳細を述べる．そして，SML#プログラムの実行

在，仮想マシンでない本物のハードウェアを直接制御に必要なランタイム関数の実装について述べたあと，する本格的な OS を SML#で開発することに取り組

本試作で得られた見通しについて述べる．

んでいる．さらに，上述の試作ではアセンブリコー
ドで記述したルーチンを詳細に分析し，そのうちのごくわずかなアセンブリコードを除いて SML#で記

2. 1 SML#とアセンブリ言語の連携と，ハードウェア資源へのアクセス述し，SML#による記述箇所をさらに増やすことを開発言語として，SML#とアセンブリ言語を使用目指している．具体的な目標は，ARMv8 プロセッサした．開発にあたって，特定のレジスタ，メモリ領域を内蔵する Raspberry Pi で動作する，簡単な組み込の特定番地，特定の I/O ポートへのアクセスを提供

みアプリケーションを実行するための，小さいながするプリミティブをアセンブリ言語で記述し，導入しらも必要十分な機能を提供する OS を，ごくわずかた．SML#コードからは，これらプリミティブを通じなアセンブリコードと大部分の SML#コードで構成て，メモリや I/O ポートへの直接アクセスが可能ですることである．現在，その第一歩として，OS を記ある．SML#とアセンブリ言語で OS を記述するに述するのに必要なすべての機械語命令をラップする

は，SML#で記述された関数とアセンブリ言語で記

SML#ライブラリと，最初の試作と同程度の機能を述された関数が互いに呼び出しを行うための機構が必Raspberry Pi の実機上で実現するプログラムの開発要である．SML#コードからは，C との直接連携機を進めている．

能を使用し，アセンブリ言語で記述された関数を呼び

本発表では，これら一連の検討と試作を報告し，展望を述べる．

出すことが可能である．このとき，アセンブリ言語関数は，引数が格納されるレジスタやスタック，caller

本論文の構成は次のとおりである．まず，第 2 節

save および callee save なレジスタ，返り値を格納すで，仮想マシン上で行った Intel x86 プロセッサ向けるレジスタやスタックなどに関する呼び出し規約にの，割り込み制御，32bit アドレス空間，コンソール従って記述される必要がある．アセンブリコードから制御機能を持つプログラムの試作と，得られた見通し

SML#で記述された関数の呼び出しは SML#コンパについて述べる．3 節では，前章で得られた洞察を生イラによってサポートされていないため，新たに機構かし，ARMv8 プロセッサを内蔵する Raspberry Piを導入する必要があった．本試作で導入した機構は，

以下のとおりである．

• SML#で記述された関数に対応する，ID を導入した．

レイ上のある位置への文字表示が行われる．VRAM領域の制御を行うこれらの処理は，文字列を受け取って画面への文字表示を行う関数として，アセンブリ• アセンブリコードから呼び出したい SML#関数言語で記述した．しかし，VRAM 領域はメモリ上にに対応する ID を格納するための，変数を用意マップされた領域であるため，特定番地へのメモリアした．

クセスを提供するプリミティブを利用すれば，この処• アセンブリ言語コードからは，SML#で記述さ理は SML#でも記述可能である．

れた関数が以下の手順で呼び出される．なお，こ2. 2. 3 キーボード割り込み制御の実装の間，すべて割り込みは禁止される．

割り込みが発生すると，CPU は，IDT と呼ばれる，

1. アセンブリコードから呼び出したい SML#割り込み処理ルーチンの先頭アドレスの配列を読み，関数に対応する ID を上述の ID 格納用変数

割り込みを発生させたデバイスに対応する割り込みに格納する．

処理ルーチンに制御を移す．割り込み処理ルーチンを2. SML#コードのエントリポイントにジャンプする．

実行する前に，割り込み発生前のレジスタ状態を保存する必要がある．割り込み処理ルーチンの実行後，3. SML#コードのエントリポイントでは，ID保存しておいたレジスタ状態を復帰し，割り込みに格納用変数を参照し，格納されている ID によって中断されていた処理から実行が再開する．本試

対応する関数を呼び出す．

作におけるキーボード割り込みハンドラは，IDT と，レジスタ状態の保存，復帰処理を除いて，SML#で2. 2 機能ごとの実装の詳細記述されている．なお，IDT は，メモリ上の配列で，本試作で開発したプログラムについて，ブートロー

その先頭アドレスを特定のレジスタに格納することでダおよび 32bit アドレス空間の設定，ディスプレイ制定義されるため，特定へのレジスタ，メモリ領域の特御，キーボード割り込み制御の実装の詳細を述べる．

定番地へのアクセスを提供するプリミティブを利用す

2. 2. 1 ブートローダおよび 32bit アドレス空間

れば，IDT の定義は SML#でも記述可能である．割の設定処理の実装
ブートローダには，プログラム本体のロード，32bitアドレス空間の設定，プロテクトモードへの移行，レり込みハンドラの実装は，以下のとおりである．

• メモリ上に，入力されたキー情報を格納するためのバッファを用意した．

ジスタの初期化を行った後，SML#とアセンブリ言語• キーボード入力要求フラグを導入した．このフで記述されたカーネル本体へジャンプする処理を記述

ラグが立っている時のみ，入力されたキー情報がした．これらの処理は Intel x86 プロセッサの仕様上，バッファに格納される．

16bit コードで記述する必要があり，これは SML#コ• 割り込みハンドラは，以下の手続きで動作する．

ンパイラで生成することができないため，アセンブリ1. レジスタ状態を保存する．

言語で記述した．32bit アドレス空間は，GDT と呼2. 入力要求フラグが立っていれば，3. へ進む．

ばれる配列をメモリ上に配置し，その先頭アドレスを入力要求フラグが立っていなければ，4. へ

特定のレジスタに格納することで定義される．GDT進む．の定義も，アセンブリ言語で記述した．

3. キーボードコントローラから入力キー情報

2. 2. 2 ディスプレイ制御の実装を取得し，解析して，バッファに入力キーのディスプレイ制御として，画面への文字表示機能を文字コードを格納し，ディスプレイ上の現在実装した．ビデオコントローラがメモリ上にマップしのカーソル位置に文字を表示する．ている，VRAM 領域中の，画面位置に対応する番地

4. レジスタ状態を復帰する．に文字コードと色情報等を書き込むことで，ディスプ

5. 割り込みハンドラからリターンする．

2. 3 SML#プログラムの実行に必要なランタイム関数の実装ように，アドレス空間の設定もメモリ上のページテー
ブルやいくつかのアドレス空間設定用レジスタで，可SML#で，OS のサポートなしにハードウェアレベ能であるため，これらの記述も，本ライブラリを利用

ルのプログラミングを行うためには，SML#のランして SML#で行う．この方針に従い，最初の試作でタイム関数を OS に依存しないように改造する必要がアセンブリ言語で実装していたテーブルの定義やディあった．これらは，スタブ関数としてアセンブリ言語

スプレイの制御等も，大部分を SML#で記述する．

で記述した．ヒープ領域の管理を行う関数は，ヒープ領域の先頭からメモリのアロケーションのみを行い，

3. 2 機能ごとの実装の現状一度アロケーションをしたら解放しないように実装

最初の試作と同程度の機能を Raspberry Pi 実機上した．

で実現するには，ブートローダ，仮想アドレス空間の定義，割り込みベクタテーブルの定義，後述する

2. 4 本試作で得られた見通し

mailbox 機構と framebuﬀer 機構を通じたディスプレ

本試作では，VRAM の制御，GDT や IDT の設定イ制御，キーボード割り込みハンドラを実装する必要などをアセンブリ言語で記述した．しかし，特定のレがある．また，SML#コンパイラが ARMv8 コード

ジスタ，メモリ領域の特定番地，特定の I/O ポートへを生成するように，コンパイラの設定を行う必要がのアクセスを提供するプリミティブを利用すれば，アある．SML#で記述する対象は，カーネルに対象をセンブリ言語で記述した処理のほとんどが，SML#で絞り，ブートローダ及び GPU ファームウェアには，記述することが可能であるという確信を，割り込みハ

ARMv8 プロセッサ用の Linux のコードを使用する．

ンドラなどいくつかの機能の SML#での実装を通じなお，SML#で記述した関数と C 言語で記述した関て，得られた．

数の互いの呼び出しの機構は，最初の試作と同様にする．実装の現状を以下に述べる．

3 SML#と C による，ARMv8 プロセッサにおける試作の現状

3. 2. 1 仮想アドレス空間の定義
仮想アドレス空間は，メモリ上にページテーブル

本節では，現在行っている試作として，最初の試作を配置し，仮想アドレス空間の設定用レジスタでアと同程度の機能をもち，ARMv8 プロセッサ [5] を内クセス権などを設定し，ページテーブルの先頭アド蔵する，Raspberry Pi の実機上で動作するプログラ

レスを特定のレジスタに格納することで定義できる．

ムについて述べる．はじめに，本試作における実装の特定のレジスタに対する読み書きや，メモリの特定番方針について述べ，次に各機能の実装の現状について地への読み書きを提供する上述のライブラリを利用述べる．

しながら，SML#で実装中である．

3. 2. 2 割り込みベクタテーブルの定義
3. 1 本試作における実装の方針

ARMv8 プロセッサのアーキテクチャでは，割り込

本試作では，最初の試作の結果を受けて，OS を実

みベクタテーブルは割り込み処理ルーチンの先頭ア装するのに必要なハードウェアにアクセスするためにドレスの配列ではない．割り込みベクタテーブルは割必要な機械語命令をラップする最小限のライブラリり込み処理ルーチンそのものの配列である． [6] つまを C で実装し，これを効率的に利用することで可能

り，割り込みベクタテーブルに，機械語でハンドラをな限り SML#による記述箇所を増やす．本ライブラ

直接記述する形式をとっている．このため，割り込みリでは，番地を指定するメモリアクセスに加えて，リベクタテーブルはアセンブリ言語で記述する必要がンクレジスタ，アドレス空間設定用のレジスタ，フラある．現在，実装方針を検討中である．

グレジスタ等へのアクセスも提供する．I/O デバイスのレジスタはメモリ上にマップされており，後述する

3. 2. 3 ディスプレイ制御の実装の現状

ロセッサを内蔵する Raspberry Pi 上で，試作を行っディスプレイ制御には，GPU の制御が必要となる．ている．SML#による記述箇所を最初の試作よりも増本試作では，上述の GPU ファームウェアで提供されやすために，機械語命令をラップする SML#ライブている mailbox 機構 [7]，および framebuﬀer 機構 [8]ラリを実装した．これを利用して，最初の試作でアセを利用する．これらの機構を利用すれば，メモリ上にンブリ言語で記述していた箇所についても，SML#でマップされたデータ構造を通じて，GPU の制御が可実装する．

能となる．この機構を通じて，GPU を制御する処理

今後の展望としては，最初の試作と同程度の機能をを，メモリの特定番地への読み書きを提供する上述のRaspberry Pi の実機上で実現するプログラムを完成

ライブラリを利用しながら，SML#で実装中である．

させ，コード量比較などの観点から実装方式について

3. 2. 4 キーボード割り込み制御の実装再度検討を行う．その後，簡単な組み込みアプリケーキーボード割り込みの制御は，USB を通じて行う．

ションを実行するための，小さいながらも十分な機能

この実装は，方針を模索中である．

3. 2. 5 SML#コンパイラの ARMv8 コード生成への対応を有する OS を，大部分を SML#で実装する．
謝辞 本研究の一部は JSPS 科研費 25280019「ML系多相型言語 SML#の実用化技術に関する基礎研究」

SML#コンパイラは，バックエンドに LLVM を用および 15K15964「実用プログラミング言語のためのいている．SML#コンパイラから ARMv8 をターゲッ系統的言語開発基盤の実現」の助成を受けて実施されトとしたコードを生成するには，LLVM のターゲットたものである．

を ARMv8 に設定すれば可能である．現在，ARMv8コード生成への対応に向けて，取り組んでいる．

4 まとめと今後の展望
最初の試作では，SML#とアセンブリ言語で，Intelx86 プロセッサ向けの，コンソール機能を提供するプログラムを試作した．この試作から，SML#とアセンブリ言語を用いてハードウェア制御を行うために導入が必要な機構について考察を行うことができ，ハードウェア制御において SML# が有用であることを確認できた．この試作ではディスプレイ制御やテーブルの定義など多くの箇所がアセンブリ言語で記述されていたが，それらの箇所についても大部分が SML#で実装可能であることの確信を得ることができた．
最初の試作の結果を受けて，実機で動作する，同程度のプログラムを開発するために，現在，ARMv8 プ

参 考 文 献[1] 井上翔太, 大山恵弘. Ocaml による os の実装. 研究
報告システムソフトウェアと オペレーティング・シス
テム（OS）2010-OS-113(4), 1-8, 2010-01-20, 2010.
[2] Thomas Hallgren, Mark P Jones, Rebekah Leslie,
and Andrew Tolmach. A principled approach to operating system construction in haskell. ICFP 05
September 26-28, 2005, Tallinn, Estonia., 2005.
[3] SML# compiler.
http://www.pllab.riec.tohoku.ac.jp/smlsharp/.
[4] Intel Corporation. Intel 64 and IA-32 Architectures Software Developer Manuals.
[5] ARM. ARM Architecture Reference Manual.
[6] ARM. ARM Cortex-A Series Programmer s
Guide for ARMv8-A Chapter 10. AArch64 Exception Handling.
[7] Mailbox framebuﬀer interface raspberrypi/firmware
wiki github. https://github.com/raspberrypi/firmware/wiki.
[8] Rpi framebuﬀer - elinux.org.
http://elinux.org/RPi Framebuﬀer.