seL4环境配置

      转载声明:希望大家能够从这里收获知识之外,也能够体会到博主撰写博客的辛苦。个人博客势单力薄,对于强转甚至转载博客访问量高于原文的例子不在少数。

  希望能够得到大家关注的同时,也能够稍微体谅一下博主的不易。

  

  既然奔着seL4来的,那么对于宏内核与微内核的区别应该是很清楚的了,在此就简单地介绍两者的区别,本文主要用来完成seL4环境配置工作

   对于小白来说,自己独自完成对seL4微内核的阅读和理解真的很困难,目前跟着老师助教一起进行对seL4微内核的分析和理解。所以准备长期更新seL4学习的博客,希望大家多多支持,错误之处还请各位帮忙指出改正。

       对于两者的区别也就简单提一下,相关的资料十分充足可以自行查找满足自己的需求。

        微内核:所有的服务器都相对独立并且运行在各自的地址空间。通过进程间通信机制(IPC)实现进程之间的通讯,互换“服务”。服务器的独立运行避免了一个服务器崩溃或及其他的服务器。

        宏内核:也称为单内核,将内核从整体上作为一个大过程实现,并且同时运行在一个单独的地址空间。这也意味所有的内核服务之间可以直接调用函数,简单高效。

下图为宏内核与微内核架构图:

1.微内核与宏内核

seL4 官网:http://sel4.systems/

seL4 wiki:https://wiki.sel4.systems/

seL4 项目主页:http://ts.data61.csiro.au/projects/seL4/

在安装和运行seL4系统之前,需要在机器上安装必要的安装包。这里假设大家都安装在Linux系统之上,并且下面的示例均为Ubuntu14.04版本(64-bit)或者可以安装在Ubuntu16.04版本(64-bit),当然也可以尝试其他的Unix系统(包括Mac OS)等。

下图为进行第一个实验的要求:

image

下面进行第一个seL4实验:

image

下面为获取代码以及第一个实验执行hello1的指令

image

首先先将需要的seL4程序从git上面clone下来,指令如下所示:

>git clone https://github.com/zpfbuaa/seL4.git

其中后面的程序地址可以是其他的只要是源码就行了,上面是指提供一个方便大家的链接。

为了避免链接失败,下面再多给些地址:

https://github.com/xcgxg/sel4-tutorials-manifest.git(和上述指令相同)

http://pan.baidu.com/s/1jIsdVTG (直接下载到Linux机器上就可以了)

http://pan.baidu.com/s/1kV2RkVH(直接下载就可以了)

该步目的在于完成对源码的clone工作,为后期的源码阅读做准备。

假设大家都已经准备好了上述源码的工作。

对于文件怎样

下面需要对源码进行一系列的配置操作。

https://github.com/SEL4PROJ/sel4-tutorials/blob/master/Prerequisites.md

可以参照上述的链接。不过出现的问题就是安装的东西有点多,甚至有些不必要安装,看到上述的指令不要想就知道很麻烦。

下图为代码下载解压之后的文件,其中rebuild.sh文件可能不存在,只是自己写的一个指令脚本,用来对代码进行clean等操作。

image

下面为rebuild.sh文件的内容

image

下图解释每个指令的作用:

image

上述rebuild.sh文件的执行指令为:

> sh rebuild.sh

通过上述指令,可以重新build项目。

image

之后执行下述指令

产生错误信息如下所示:

02E49CM4$BX6QYDR930TL@K

原因是src/main.o以及src/util.o文件缺少,其中main.o以及util.o文件都是通过相对应的.c文件经过编译得到的,也就是意味着main.c以及util.c文件出现了错误。所以下一步需要对src/main.c以及src/util.o文件经行必要的修改,来完成我们的第一个实验hello1。

具体的文件路径如下图所示:

image

下面我们查看main.c文件,可以使用指令gedit main.c同样也可以使用vim main.c

image

通过上述的提示,告诉我们需要添加一个main函数用来打印一条消息,因为我们的第一个实验就是hello1嘛,所以就直接让程序打印HelloWorld未尝不可。

image

这样经过上述的操作,我们就可以开心地运行我们的helloworld程序了。

首先还是先运行sh rebuild.sh,重建项目。

下图为需要进行的实验hello-1的运行指令:

image

运行该指令文件结果如下所示:

其中会在下面这个地方稍微等待一下:

image

接着程序进行编译,编译结果如下:

image

这样我们就可以运行我们的hello1程序了,运行指令如下:

> qemu-system-i386 -nographic -m 512 -kernel images/kernel-ia32-pc99 -initrd images/hello-1-image-ia32-pc99

注意这里可能报错,如果之前工作没有错误的话,这里报的错误应该就是缺少程序包。由于已经安装时错误截图没有保留,所以没法给大家看具体的错误截图了。

如果没记错的话,缺少的安装包应该就是这个qemu-system-x86,如果不是这个的话,大家按照提示缺少的安装包进行安装即可。

> sudo apt-get install qemu-system-x86

修复上述问题之后,运行结果如下所示:

image

image

image

经过上述的操作,对于seL4的基本配置已经告一段落。

接下来就开始对seL4源码的阅读分析。

原文地址:https://www.cnblogs.com/zpfbuaa/p/6063633.html