Can We Make Operating Systems Reliable and Secure? via enbug diary
あーなるほろ。L4Linux てそういう構造だったのね。QNX とかみたいな single-server だと思ってたので、どこでそんなに IPC cost が問題になるのか不思議だったけど、これで納得。Xen てこれに近いことするもんなんだろうか。よくわかってないんだけど。
;; BSD とか Hurd とかを放りこんで Xen を試したいが為にさっさと hard disk を入れ換えたがってるのだ
;; とか考えると、あーまた SigScheme とか弄る気が…orz
EROS/Coyotos が無視されてる理由はよくわからないけど、EROS は目的がちょっとずれてる, Coyotos はまだ設計がハッキリしてない + MINIX 3 と被るからじゃないですかね。この記事の project は主に OS を作る人の programmer error から operational semantics を守る事を目的としてますが、*1EROS は (私が勘違いしてなければ) cracking に対して守備的な設計になってて、fault isolation は privilege factorization の一部みたいな感じですし。
しかし気になるのはこの Sing# 言語。この contract-base の verifiability というのは私が better C として妄想してる物と mechanics がほぼ等しい (利用目的は全然違う)。真面目に作る気になるようならこの辺の論文を読み漁る必要がありそう。
