該文會不斷更新，補充
--------------------------------------------------------
L4第二代微內核2005年1月1日為止的最新定義文檔。
http://l4hq.org/docs/manuals/l4-x2-20041209.pdf
L4第二代微內核參考實現的性能評測。
http://os.inf.tu-dresden.de/pubs/sosp97/
Logical Interface: 邏輯接口。硬件無關的接口，數據類型。
Generic Binary Interface: 一般二進制接口。硬件體系相關的接口類型，數據類型。
Generic Programming Interface: 一般程序接口。與具體語言榜定的接口。
ConvenIEnce Programming Interface: 便利程序接口。
基本數據類型 基本數據類型Word指明了一個32位系統上的32位數，一個64位系統上的64位數。
Privileged Thread: 特權線程 有些系統調用只能由特權線程執行。任何與init線程屬於同一個地址空間的線程都是特權線程。
Basic Kernel Interface: 基本內核接口
1.1 內核接口頁通過頁表映射的方式在所有的地址空間裡共享，提供給各個地址空間相關的內核信息。內核接口頁不能映射給其它地址空間，也不能解除內核接口頁在當前空間中的映射。
2.1 線程 THREADCONTROL（特權調用）一個特權thread例如root server可以通過該調用啟動或者刪除一個線程。在創建時，線程可以是active（活動的）或者是inactive（非活動的）。非活動線程在創建後可以被一個同一地址空間中的活動線程激活。
3 調度
3.1 時鐘無論32位平台還是64平台，時鐘變量都是一個64位的無符號整數。單位為一微秒.。
0.000 001 微秒 = 1皮秒
0.001 微秒 = 1納秒
1,000 微秒 = 1毫秒
1,000,000 微秒 = 1秒
SYSTEMCLOCK 獲得當前的系統時刻。該調用不進入內核模式。
THREADSWITCH 調用線程放棄處理器給另一個線程。
SCHEDULE 控制一個線程的運行策略。
該調用只有在目標線程的scheduler被設置成調用線程的情況下才用效。
4 地址空間和映射 Fpage - 是一段地址空間。Fpage最小要比最小物理page相等。
UNMAP(系統調用) - 解除指定的Fpage的映射。
SPACECONTROL(特權系統調用) - 配置地址空間。
5 IPC進程間通訊
5.1 消息和消息寄存器。
IPC （系統調用）
6 雜項
6.1 異常處理線程。
6.2 並行處理標志
6.3 PROCESSOSCONTROL （特權系統調用）
6.3 MEMORYCONTROL （特權系統調用）- 更換指定fpage的屬性。
UTCB - user level thread control block - 用戶級線程控制塊