#osc14tk 聴講メモ 秘密結社Metasepi作戦会議 – #NetBSD のデバイスドライバを #Haskell で書いてみよう！
秘密結社Metasepi作戦会議 – NetBSDのデバイスドライバをHaskellで書いてみよう！
-
2014-03-01 (土) 15時15分
-
Rewrite NetBSD kernel driver using Ajhc Haskell compiler. – YouTube
▶ #osc14tk 秘密結社#Metasepi 作戦会議 — #NetBSD のデバイスドライバを #Haskell で書いてみよう！ – YouTube
自己紹介
DEMO
-
NetBSDはヘッドホンが刺さるとunsol というログがでる
-
音を出す場所を変えられる
-
ブレークポイントを付けられる
-
再度ヘッドホンを刺すと、Haskell の関数が呼ばれた
-
デモの動画 http://bit.ly/netbsdajhc
デモのアーキテクチャー
- Demo architecture
Ajhc とは
Metasepi とは
-
UNIXライクなOSを型言語で作りたい
-
既存の言語でカーネル開発が大変な為、それらを解決するのが目的
-
カーネルのバグを再現するだけで半年とかかけるのが無駄
-
カーネルのソースをforkするとソースをチェックする人が減って質が下がる
Type safety
-
Less runtime errors.
-
数理科学的バグ撲滅方法論
-
型を協力にした方が出荷前に見つかるバグが増える
Type safetyは誰の為？
-
いまはCでカーネルが作られている
-
カーネルにバグがあるとシステム停止
-
カーネルのデザインにこそ慎重さ、型が必要
そのためには強い型のコンパイラが必要
- C言語と同等の柔軟性も必要
いろんな型コンパイラの吐き出すバイナリを比べる
- jhcが小さい
jhcは Haschell → c → binary のトランスレーター
関数型言語で作られたカーネルは数多く提案されてきた
- 実用化されるまでには長い道のりが
そのために Snatch
-
モジュールごとに強い型付け言語＋そのランタイムで置き換えてまとめてパッケージ化する
-
少しづつ置き換えられる
この手法で作られたのがデモ
Cの構造体をHaskellで見られるコードを自動生成するツール
ajhc でカーネル開発してみてどうだったか？
-
強い最適化によってデバッグが困難
-
カーネルデバッガが展開されたcのコードベースでしか行えない
次は ATSコンパイラで開発を試行してみる
-
MLライクな言語
-
GCは無い
-
その為に http://jats-ug.metasepi.org/ を作った
-
ATS作者（ボストン大学准教授）は5年前にATSをNetBSDで作ろうとしたことがあった為、この取り組みを支持してくれている。
-
C言語の問題は正しく書き下すことが出来ない。ATSは正しく書けるようにする為に作った。
型言語で真の安全性のあるOSを作る
関連記事
