L4 - oraccha/omicron GitHub Wiki

L3の後継プロジェクトとして[http://l4ka.org/team/jochen/ Jochen Liedtke] 教授らによって研究されているカーネル．いろいろなカーネルの実装や周辺プロジェクトがあるみたい．

  • L3のさらに前はEumelというOSで，1979年にプロジェクトが開始され，最初のターゲットプロセッサはZ80だったそうな．
  • Jochen Liedtke 教授は今年(2001年)の6月に亡くなっていたらしい．

Machを第1世代のマイクロカーネルとするとL4やExokernelは第2世代のマイクロカーネル，エクステンシブルカーネルなどと呼ばれ，必要最小限のハードウェアの仮想化，高速なIPCが特徴である．

  • [http://os.inf.tu-dresden.de/L4/ 本家] (TU Dresden)
  • [http://l4hq.org/ L4HQ]

L4を最初に知ったとき，システムコールが7つしかないことに衝撃を受けた．

  • ipc，fpage_unmap，task_new，id_nearest， lthread_ex_regs，thread_switch，thread_schedule

基本的なコンセプト

  • タスクとスレッド

  • IPC . メッセージ通信． すべてのIPCは同期型でバッファリングされない． メッセージに含まれるデータはレジスタまたはメッセージバッファによる値渡し(in-line)と，仮想記憶機構を利用した参照渡し(out-of-line)の方法がある．

  • アドレス空間 . 再帰的にマッピングすることが可能． map/grant/flush というプリミティブが用意されている． mapとgrantはsenderのアドレス空間からreceiverのアドレス空間にページがマップされる点は同じであるが，mapがsenderのページを保持し続けるのに対して，grantはsenderのページをアンマップしてしまう．

  • clan/chief . タスクの階層(親子)関係によるセキュリティ機構． タスクの親を chief と呼び，同じ chief から生成されたタスクの集合を clan と呼ぶ． clan 間の IPC は，chief を介してリダイレクトされる．

L4上のOS構成

  • OSサーバはクライアントの chief になる．
  • OSサーバは単一もしくは複数のタスクから構成される．
  • クライアントのシステムコールはライブラリのスタブルーチンによりOSサーバへのRPCへと翻訳される．
  • OSサーバはクライアントの要求を他のサーバへリダイレクトする．

実装いろいろ

  • [http://os.inf.tu-dresden.de/fiasco/ Fiasco] (TU Dresden) . x86，ARM，UX (Linux のユーザプロセスとして動作)．

    • 2005-09-26: 1.2 がリリースされている．

  • [http://os.inf.tu-dresden.de/drops/ DROPS] (TU Dresden)

    • [http://www.osnews.com/story.php?news_id=15176 A Developer's Insight Into DROPS] (OSNews 2006-07-13)

  • [http://l4ka.org/ L4Ka](Univ. of Karlsruhe) . x86，ARMに対する実装が存在する．

    • [http://i30www.ira.uka.de/mailarchives/[email protected]/ MLアーカイブ]
    • Hazelnut/Pistachio というコード名のカーネルがあり，それをベースとしたOSプロジェクトがいくつか存在する(Pistachio はまだリリースされていない)．
      • すでにメインは Pistachio っぽいな．
    • 前者の API は version X.0 であり，後者はその後継である version 4(version X.2) の API を実装したカーネルらしい．64bit プロセッサ，SMP対応あたりが目玉なのだろうか?
      • [http://l4ka.org/documentation/files/l4-x2.pdf Reference Manual Version X.2]

  • http://www.cse.unsw.edu.au/~disy/L4/MIPS/ L4/MIPS . OSの講義としても使われているみたい．

    • [http://om.cse.unsw.edu.au/lxr/l4mips/http/source/?v=79g L4/MIPS Cross Reference] . LXR を使って HTML 化されている．
    • [http://www.cse.unsw.edu.au/~cs9242/project/project.html Project: A Simple Operating System]

  • [http://www.cse.unsw.edu.au/~pleb/gauntlet.html Gauntlet] . ARMへの実装．

  • Mungi . L4上に単一アドレス空間を提供するOSパーソナリティを構築するプロジェクト．

  • [http://os.inf.tu-dresden.de/L4/LinuxOnL4 L4Linux] . L4のOSパーソナリティとしてLinuxを載せるプロジェクト． . そう言えば，MkLinuxなんてあったね．

    • Hurd を載せるという話もあるらしい．

  • SawMill (IBM) . A Highly-Configurable Operating System

  • ChacmOS . L4上にIDL使ってファイルサーバー、タスクサーバー、メモリサーバー、 ネームサーバー（っていってもいわゆるネームスペースを提供する物だと思う）。 ファイルサーバーはext2だとか。--有野

    • 似たようなコンセプトのOSに[http://l4ka.org/projects/SCOS/ SC/OS]がある．両者の違いは IDL4 を利用するか Flick を利用するかの違い?

  • [http://research.nii.ac.jp/H2O/index-e.html H2O Project] (NII) . NII にお邪魔したときに見せてもらった．VMWare 上で開発しているそうだ．

    • [http://www.nii.ac.jp/hrd/HTML/Journal/pdf/03/03-05.pdf 高信頼制御システムのための拡張型分散 OS]
    • [http://research.nii.ac.jp/H2O/L4minix.html L4/Minix]

  • NomadBios

  • [http://os.inf.tu-dresden.de/l4env/ L4Env] . Linux のデバドラを動かそうともしているらしい．

  • [http://journeyos.sourceforge.net/ JourneyOS]

  • [http://www.disy.cse.unsw.edu.au/Software/Wombat/ Wombat] (UNSW) . L4 の上に Linux OS パーソナリティを動かすプロジェクト．

  • [http://opensource.bleepsoft.com/index.php/Main/L4BSD L4::BSD]

  • [http://www.ertos.nicta.com.au/software/darbat/ L4/Darwin (aka Darbat)]

    • [http://www.ertos.nicta.com.au/downloads/darbat/ReleaseNotes-0.2.pdf Darbat Release 0.2 Notes] . Intel Mac で動くのね．

  • [http://www.dcl.info.waseda.ac.jp/l4vm/ L4VM] (早大)

  • [http://wiki.ok-labs.com/ OKL4] (Open Kernel Labs) . 商用利用。

2001-12-15 . L4Ka プロジェクトの Hazelnut を DL して動かしてみた．

  • [http://sourceforge.net/cvs/?group_id=8798 CVS] (SourceForge)

RedHat 7.2 でコンパイルした rmgr (カーネルローダに相当する)が実行可能ファイルじゃないとか Grub に言われてブートできなくてはまったが，結局，Kondara/MNU 2.0 でコンパイルすると OK だった． file コマンドの出力結果も正しそうだし，gcc のバージョンは 2.96 で同じなんだけどなぁ．binutils の違いかな．2.11.90.0.8 と 2.10.91 だけど．う〜む．

でも，gcc の 2.96 って曰く付きのバージョンなんだよね． なんか C++ の mangling ルールが 3.0 互換(?)だから "#if (GNUC >= 3)" みたいなチェックが効かない(ような気がする)．

  • ちなみに Grub のエントリはこんな感じ． {{{ title L4Ka root (hd0,1) kernel=(hd0,1)/boot/l4ka/rmgr -sigma0 module=(hd0,1)/boot/l4ka/x86-kernel module=(hd0,1)/boot/l4ka/sigma0 module=(hd0,1)/boot/l4ka/root_task }}}
  • rmgr はリソースマネジャ，sigma0 はルートページャらしい．
    • rmgr のコードを見るとモジュールのロードに OSKit を利用しているみたい．

L4Ka には clan/chief が実装されていないのね．

[http://japan.cnet.com/news/ent/story/0,2000056022,20398361,00.htm 豪研究所、カーネルの安全性を数学的に検証する手法を開発(CNET)]. Secure Embedded L4をIsabelleという検証系でチェックした、という話。汎用OSカーネルの、初の形式的検証とのこと.