#osc14tk 聴講メモ 秘密結社Metasepi作戦会議 – #NetBSD のデバイスドライバを #Haskell で書いてみよう!


秘密結社Metasepi作戦会議 – NetBSDのデバイスドライバをHaskellで書いてみよう!

▶ #osc14tk 秘密結社#Metasepi 作戦会議 — #NetBSD のデバイスドライバを #Haskell で書いてみよう! – YouTube

自己紹介

DEMO

  • NetBSDはヘッドホンが刺さるとunsol というログがでる

  • 音を出す場所を変えられる

  • ブレークポイントを付けられる

  • 再度ヘッドホンを刺すと、Haskell の関数が呼ばれた

  • デモの動画 http://bit.ly/netbsdajhc

デモのアーキテクチャー

  • Demo architecture

Ajhc とは

Metasepi とは

  • http://metasepi.org/

  • 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を作る

シェアする

  • このエントリーをはてなブックマークに追加
  • 0

フォローする

コメントをどうぞ

メールアドレスが公開されることはありません。 * が付いている欄は必須項目です

CAPTCHA