L4操作系统（L4/Fiasco介绍）
linuxvae 2012-11-11
我们学习操作系统课程的时候，一直在讲微内核，说什么“微内核是现代操作系统的主流”（时间太久，记不清了，如果说错了，不要拍我）。可是事实上，真正进入工业级别应用的微内核操作系统并不多，Microsoft的系统虽然宣称是微内核，但是应该不是，因为从来没有见过一个人可以把XP或者2000系统裁减到50M以内（95/98可以做小，这个可以从网络搜索到相关资料，但是它们是DOS的封装，这里不谈）。但是Linux不是微内核，而是 monolitic，这是大家都公认的，Linux的前辈Unix当然也不是微内核。具体说来，这个分歧主要是学术界和工业届的分歧。学术界认为，微内核是操作系统发展的主流方向，但是工业界却不这样认为。这也许是当linus推出Linux以后，和他的老师Andy Taonenbau(写Minix的牛人)互相拍砖头的缘由。
不过确切的说，microkernel的整体性能不如monolitic，这对于追求性价比的厂商而言，采用monolitic也是有道理的。不过microkernel也有自己的长处，就是稳定。相对而言，microkernel比monolitic的依赖更为简单，所以它更稳定。不过第一代microkernel真的很令人失望，到了JochenLiedtke（German），他设计了第二代microkernel，称为L4，为了追求效率，所有的L4用汇编语言实现（牛人吧，用汇编写操作系统），但是这样的结果是在追求效率的同时，使得第一代L4只能运行在486和pentium上面。但是目前L4已经变成微内核的一个设计标准，围绕这个标准，有很多的L4的实现（http://os.inf.tu-dresden.de/L4/impl.html）。最初的由Jochen设计的L4目前称之为L4/X86，现在最活跃的两个分别是Pistachio和Fiasco。前者是普通的microkernel，后者是专门为实时系统设计的microkernel，实现了L4V2（L4APIVersion2）。由于Fiasco跟L4的这种关系，所以平时Fiasco也被称做L4/Fiasco，以强调它是L4的一个implementation。
现在，终于开讲Fiasco，Fiasco的意思是“失败“，好像是从意大利语里面借来的（不知道他们为什么去这么一个名字，不过听起来还蛮上口的）。Fiasco是DresdenReal-TimeOperatingSystemsProject（德累斯敦大学实时操作系统项目）的核心子项目，它是一个具备实时功能的microkernel。我们知道，在一个实时系统里面，通常有两种任务，一种是real-time的，另一种是time-sharing的。real-time部分由Fiasco提供，在time-sharing部分，开发者们利用了Linux。平常Linux都是跑在某一种硬件平台（X86，ARM，PowerPC，MIPS），而在Fiasco/L4里面，开发者对Linux进行了修改，使得Linux能够运行在L4/Fiasco，这部分叫做L4Linux。目前，L4Linux的最新版本已经到了L4Linux-2.6.17,这是现行的最新的Linux-2.6的稳定版本。
下面，我们说说L4/Fiasco中的服务模式（程序架构），这个我认为比较有意思。如果没有任何module被加载，单纯一个microkernel那是什么事情也做不了的。所以基于L4/Fiasco有好多的module被设计出来，这些module以server的形式为后面加载的module提供服务，就好似多个C/S嵌套起来一样。
最后，讲一下microkernel跟monolitic的区别，前面说Fiasco的时候，也说到module，大家在编译Linux kernel的时候，也会有module。这两个地方的module是不一样的。前面的module是彼此之间是隔离的，具有不同的address space，而后者之间共享同一个address space。Operating System Based L4-Like Microkernel
关于L4系统，一般来讲，目前公认的L4系统有2个特点，FastIPC和Sigma0协议。Sigma0是一种基于IPC的内存管理协议，使用Sigma0，内存管理呈现出一种层次状。举例：有A和B两个程序，如果程序B想使用程序A的内存。如果使用Sigma0，那么很容易实现，只要把A设置为B的pager,并提供B的pagefaulthandler程序就可以。在这种情况下，程序A和程序B依然具有不同的AddressSpace，A和B之间互相隔离（关于这种层次式的内存管理，请参考Thesawmillframeworkforvirtualmemorydiversity）。但是如果使用Linux来实现这种模式，除非使用sharememory，我想不出其它更好的办法，但是sharememory使得A和B之间有的AddressSpace有了交集，从security和safety两个方面来讲，都不是很好的解决方法。近年来，越来越多的L4系统开始支持一种新的特性-Capability,Capability是为了提高操作系统安全性而设计的，Capability和要访问的Resource之间的关系类似于文件描述符号和文件之间的关系一样，要访问一个Resource，必须通过Capability来进行，Capability里面规定了那么资源可以被访问等安全特性，Capability
允许被grant（从一个用户转移到另外一个用户），总之，Capability是比AccessControlList更好的一种增强系统安全性的方法。
LiveSystem
1,PikeOS/ELinOS德国SYSGOAG公司的商用非开源系统，它提供了很好的ResourceIsolation机制，使用ParaVirtualization，让每一个OSPersonality运行在一个VM里面，可以支持Java和Ada的应用程序。PikeOS不但具有SpatialIsolation，还具有很好的TemporalIsolation，因此也支持Real-Timeapplication。ELinOS是移植到PikeOS的嵌入式Linux系统（2.4和2.6)，支持众多硬件平台和开发板。PikeOS通过ARINIC653，D0-178B认证，因此被用于军工航天等Safety-Critical和SecureApplication。PikeOS是从98年开始开发的，近几年Sysgo已经成为欧洲增长最快嵌入式厂商，ELinOS也成为比较流行的嵌入式Linux开发环境。因为是商用系统，可参考的资料很少。(www.sysgo.com，http://en.wikipedia.org/wiki/PikeOS）
2，Fiasco/L4Env/L4LinuxFiasco是TUDOperatingSystemGroup(os.inf.tu-dresden.de)开发的Real－Time微内核，支持L4V2.0和L4X.0标准(L4的接口标准），Fiasco是由C＋＋实现的典型L4系统，Fiasco提供众多L4系统调用以及Fiasco的实时扩展，请点击FiascoSyscalls。L4Env是一套基于Fiasco的服务程序，包括roottask,sigma0,log,names,dm_phys,l4vfs,l4io,dope,con等各种server，L4Env是一种典型SawMillMulti－ServerOS（参考paperTheSawMillmultiserverapproach）,关于L4Env的一些基本情况，请点击L4EnvManual。L4Linux是基于L4Env移植的Linux系统，Linux－2.0,Linux-2.2,Linux-2.4,Linux-2.6前后分别被移植到L4Env上面，目前L4Linux版本更新到2.6.26，L4Linux相当于一种基于“L4CPU”的Linux系统，对Linux系统的修改都存放在arch/l4目录下面，较好地维持了Linux系统semanticintegrity。关于Fiasco/L4Env/L4Linux的设计，请参考PaperThePerformanceofµ-Kernel-BasedSystems,这个Paper也是微内核领域最著名的Paper之一。值得注意的是，基于Fiasco和L4Linux，有2个很重要的研究成果，DROPS实时系统是一种面向服务质量需求的实时系统，可以提供某种程度的保证(guarantee)。L4/Nizza，一种面向TrustedComputing的基于微内核的系统架构，这也是最早利用L4微内核进行securitysystem研究的工作，可以参考Paper:SecurityArchitectureRevisited。此外，他们维护一个IDLforL4，称为Dice。
3,Pistachio/AfterBurnerPistachio是目前最好的L4微内核之一，它由卡尔斯鲁尔大学系统体系结构研究组和新南威尔士州立大学操作系统研究小组共同开发的微内核。跟所有的研究机构一样，一开始大家都是单干，卡尔斯鲁尔作Hazelnut,新南威尔士州立做L4/MIPS,L4/Alpha。后来，大家联合起来，做成了Pistachio。不过微内核之上的部分大家一直单干，各有各的系统。卡尔斯鲁尔的Pistachio小组在很长的时间内，一直使用来自TUD的L4Linux作为基于Pistachio的虚拟化技术，直到Pistachio的Afterburner技术出现为止才有了改观。AfterBurning是该小组研发的一种Pre-Virtulization技术(Pre-Virtualization是一种兼顾Para-Virtulization的高性能和Modularity的可维护性而出现的一种尝试，具体来说，是把一种sourcecode可以根据需求编译出不同的系统，同样的Linux，可以编译出适用于Xen的GuestOS，也可以编译出使用L4:Pistachio的VirtualMachine。由于这项工作是在编译阶段完成的，因此诸多优化也可以同时生效，而避免了Para-Virtualization的单一性。比如L4Linux只能应用用Fiasco，XenLinux只适合于Xen等等），因为是通过编译来完成的，所以性能会更好一些。比较有趣的是，他们有一个BurnNT技术，可以支持Multi-Windows，网站上面提供源代码下载。他们关于DeviceDriverVirtualization有一篇Paper是OSDI的，UnmodifiedDeviceDriverReuse,是近几年L4领域一篇少有的佳作。其主要思想是把每一个VirtualLinux当作一个DeviceDriverServer，从而提供DependableSystem.
4,OKL4/IguanaOKL4是L4:Pistachio-Embedded的延续，它目前有OpenKernelLabs公司维护，但是研究工作基本上都是在ERTOS完成的。目前OKL4的市场化推广作的不错，已经有很多产品使用了OKL4，包括基于OKL4的OpenMoko，也已经面世。相当于TU-D和UniKarlsruhe的L4小组，ERTOS规模显得很庞大，他们网站上面的项目也很多，各种项目都有。主要有：1）基本系统维护，OKL4+Iguana+Magpie＋Wombat,Iguana类似于L4Env,Magpie类似于Dice,Wombat类似于L4Linux，一一对应。2）SecurityseL4+L4.Verified，我分不清楚2个项目的目标有什么不同，seL4是securityEmbeddedL4的意思，总之，其核心内容即使使用formalmethod来验证OKL4issecurekernel，似乎他们现在已经达到验证机器码的程度，大概步骤就是使用Haskell重新实现OKL4的API，然后使用Isabela进行证明，在这个方面，KernelVerification，他们作的很成功，这也是他们可以赢得众多工业厂商青睐的一个原因3）Real-Time既然是面向Embedded的，Real-Time自然是要用；Component-basedMicrokernel；PowerManagement，这些也都是目前OS研究的一些Hotopic.
5,Coyotos首先，Coyotos不是L4，但是Coyotos和L4之间的关系之密切远远胜过了其他微内核和L4之间的关系。比如FastIPC，Capability-BasedOS,IDL。Coyotos是KeyKOS和EROS(ExtremelyReliableOS)的改进版本，从EROS的名称或许可以看出，这个系统和以上的系统有些不同，它强调reliable，所以EROS刚开始的时候，被应用于一些军用系统，但是后来发现SynchronousIPC会导致一个DenialofService的Bug，这个Bug存在于所有基于SynchronousIPC的系统中，当然也包括所有的L4，在VulnerabilityInSynchronousIPCdesign中有详细的描述。当然，现在这个Bug也已经被修正。Coyotos的目标应该是提供具有军用级别的（EAL7=EvaluationAssuranceLevel）的microkernel,它使用一种新的称为BitC(类似于Haskell的SafetyLanguage)来实现这个系统，而且整个系统采用一种类似于OOP的形式（所有的L4系统都是OOP的，Fiasco和Pistachio都是C++的）。CoyotosisstillpersistantandtransactionalmicrokernelOS。从概念上来讲，Coyotos更为先进，Capability也是在该系统上面首次被应用，所以有志于研发3rdMicrokernel的不妨多多关注这个Microkernel.
6，MungiMungi是ERTOS小组开发的persistantSASOS(singleaddressspaceoperatingsystem),这个项目已经停止。但是作为第一个利用L4/Microkernel来开发不同类型的OS，仍然可以给我们提供很多新的idea,尤其是persistant，即使到目前为止，应该有值得研究的价值。http://www.coyotos.org/官网上面有很多该Microkernel的设计文档，值得一看。
7,M.D.Bennett《AKernelForIMASystems》这是UniversityofYork的以为PH.D基于L4尝试构建IMA系统，IMA全程是Integrated_Modular_Avionics，也就是面向航空航天控制的系统，这也是我能找到的基于L4所作的safetycriticalsystem的唯一一次尝试，因为我自己是倾向于作这个方向的，所以列举这个Kernel在这里。因为UniversityOfYork是safetycriticalsystem的大本营，所以这篇paper应该不错。
8, Genode OS Framework. 一个recursive hierarchical constructive os framework. 目前基于L4/Fiasco开发，主页: genode.org