seL4之hello-3征途

seL4之hello-3征途 #

回顾上周

  • 了解seL4的启动流程和初始化线程
  • 了解seL4的几种内核对象和权能机制
  • 完成hell0-2的运行.

补充上周

1.找到根任务(初始化线程)的创建具体的位置(那一个函数)

这个函数在kernel/src/kernel/boot.c中

具体查找的截图如下:

2.找出内核中bootinfo的定义,和为根任务创建 bootinfo的代码

查找方法:使用cscope 查找关键字seL4_BootInfo
查找结果如下所示

### 3.阅读手册,找出seL4中有哪些类型的对象,列出全部对象类型,并简要介绍其作用 ### ![](http://files.cnblogs.com/files/zpfbuaa/3.bmp)

查找代码结果


介绍本周

  • 了解seL4的启动流程和初始化线程
  • 了解seL4的几种内核对象和权能机制

2016年11月28日23:20:18

来自伊甸一点的温馨提醒:注意本周内容较多,建议分多次练习,并记录下实验结果

1.提供本次必要的实验手册 ###

文件信息

File: C:UsersPengFei_ZhengDesktopseL4之hello-3征途.zip
Size: 13713128 bytes
Modified: 2016年11月28日, 23:22:24
MD5: 6AF7C2002EF47F60BBCD9D7A12F34937
SHA1: 6B1DC165E95D5E5FBA6AD2697B8C81C8667167DD
CRC32: 9B6CEDED
### 2.详细介绍实验步骤 ###

来自伊甸一点的温馨提示:手册在刚刚下载的文件

#### 0. 查看手册明确实验内容 ####

1. 初始化hello-3状态 ####

执行命令 make ia32_hello-3_defconfig

运行结果截图:


2. 进入hello-3目录下 ####

  • 执行命令如下图所示:

  • 进入文件main.c: gedit main.c

需要做的就是完成当中对TODO1 ~ TODO15的修改.

solution的路径如下所示:

3. 生成hello-3 ####

生成hello-3的指令: make

运行截图


4. 运行hello-3 ####

运行指令如下所示:
qemu-system-i386 -nographic -m 512 -kernel images/kernel-ia32-pc99 -initrd images/hello-3-image-ia32-pc99

来自伊甸一点的温馨提醒:指令有点长,注意不要copy错了

小白的我给的运行部分截图:

退出模拟器的指令: Ctrl+a 松开之后再按 x

### 3.IPC的概念与演化 ###
  • L4的IPC有同步和异步两种,它们的区别是什么?试举例说明。

L4的IPC同步机制 synchronous IPC 避免了内核中的缓冲以及与其相关的管理和复制成本。它也是直接进程切换和临界映射优化的先决条件。

L4的IPC异步机制 asynchronous IPC,在seL4中将该模型定义为异步端点 asynchronous endpoints

下面的例子估计北航的才会深有体会:

你去食堂吃饭。假如你要点香锅,你需要先排队点菜,之后拿到一个号码牌。这样你就可以回到你的座位上等着了,并且你可以回到座位上和妹子聊聊天什么的。一直到你听到你的号码被叫到,你才过去把饭拿回来。(这就是异步)

还是去食堂吃饭,不过这次去了学二食堂,人很多。你找到你想吃的那个窗口对应的队就排着了,然后你一直在队里面等啊等啊等(这里不排除和妹子聊天的可能,但是在seL4中既然你都进队了,就得准守规则好好等着不许聊天)。这时候你就在里面直到你前面没有人了并且还有饭菜剩下,你才能成功拿到自己的饭。(这就是同步)

更多有关IPC请移步该文档

  • L4最初采用的IPC方法不是endpoint,而是叫做 Clans & Chiefs模型,简要描述一下是什么是 Clans & Chiefs。相比 endpoint,它有哪些缺点?

下图为嵌套的clans,嵌套的clans内部通信是自由的,但是对于嵌套的clans外部依旧需要通过chief的重定位通信。

下图为task tree的构造

这里的task tree不能当做一个整体来看待了,只知道某一个clan中的task但是无法确定内部的task都是哪些。

即clans是相互独立的。上图的右部显示出了之前的task tree独立。

也就是我们所说的:我的附属的附属不是我的附属。当然也可以换成:我的随从的随从不是我的随从。

下面是对task tree的独立性解释

4.seL4中的IPC接口 ###

  • 阅读文档,列举seL4提供的用于IPC的接口,简要描述他们的作用和区别。

内核提供的系统调用:

  • 你在hello3中调用了seL4_Call函数,找到这个函数。这个函数体是C语言吗?如果不是C语言,想想为什么?

使用cscope找到seL4_Call函数

可以看到里面的关键字有register也就是寄存器,既然是直接对寄存器进行操作的,那么应该使用的就是汇编语言了。现在我们举一个例子找一下是不是这样子的。

查找asm

找到__asm__的定义如下:

嗯嗯,确实这里用的是汇编语言。具体的含义不是很清楚,里面有指令mov 数据传送指令以及 adrp 地址生成指令。使用会汇编语言可以提高通信速度吧。

2016年12月2日10:33:14

对上述进行修改和更正,尤其是上面提到的汇编语言可以提高通信速度这一说法:

seL4_Call 里面那个asm后面的确实是汇编,这种写法叫C语言嵌入汇编inline assembly。不过使用汇编最主要不是为了性能,主要是为了通过sysenter指令进行系统调用。

C语言是没法系统调用的。 比如我们编程时候调的什么open、read等系统级函数,他们的实现就跟seL4_Call 很相似,也是inline assembly。

想了解更多关于介绍指令的内容请移步该博客

5.endpoint的代码 ###

2016年11月29日12:51:09

(⊙v⊙)嗯 未完待续...

  • 在内核代码中找到 endpoint对象(结构体)的定义。并指出它占几个字节。

  • 一个 endpoint对象有多种状态,阅读代码,找找 endpoint有哪几种状态。尝试理 解各种状态的含义

  • 分析endpoint结构体各个字段的含义,就像上次作业分析 cap 的字段含义等,最好画图表示。

  • 上次我们了解了TCB对象,其中有两个指针成员,分别叫 做 tcbEPNext和 tcbEPPrev,这两个字段是什么含义?与 endpoint有什么关系?

  • 上面找的都是同步端点,找找内核代码中异步端点的定义

6.seL4 IPC初步分析 ###

  • 找到seL4_Call函数,考虑一下这个函数执行完之后,会发生什么,下一行要执行的代码在哪里?

  • 如果你完成了上一步,尝试把接下来发生的事情(函数调用过程) 表示出来(例如:funcA->funcB->funcC等)。

7.hello4实验 ###

转载注意 ###

转载请注明原作者:伊甸一点

转载请以链接形式注明文章地址

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