Skip to content

Latest commit

 

History

History
238 lines (172 loc) · 18.1 KB

初赛中期-设计和展示文档.md

File metadata and controls

238 lines (172 loc) · 18.1 KB

目标描述

本项目将seL4微内核移植到LoongArch平台上。

  • 搭建交叉编译环境，在QEMU模拟器上调试微内核。
  • 移植相关测试程序。
  • 最终实现龙芯机器上的微内核调试。

资料调研

seL4微内核，是L4微核家族的经典实现版本，也是首个通过完整形式化验证的微核。它具有安全可靠、高性能等特点，通常用作安全系统的底层模块。

相比于xv6等教学操作系统或应用广泛的linux系统，seL4微核的底层架构文档较少。针对本赛题，团队调研资料如下：

系统框架设计--待完善

  • 虚拟地址设计 虚拟地址空间设计 图：虚拟地址空间设计

物理地址空间：

  1. 内存空间分为低地址段和高地址段，当前我们在qemu模拟使用4GB内存，对应的地址段分别为0x00000000-0x0FFFFFFF（低256MB），0x90000000-0x17FFFFFFF（剩余4GB-256MB），内核的装载地址为0x900000000
  2. IO地址段基地址位0x1FE00000

虚拟地址空间：

  1. 低128TB为用户空间，采用页表映射
  2. 内核空间采用直接映射窗口，0x9000_0000_0000_0000-0x9000_FFFF_FFFF_FFFF配置为直接映射装窗口，抹去高位的9后和物理地址空间一一对应，因此KERNEL_ELF_BASE为0x9000_0000_9000_0000，KDEV_BASE为0x9000_0000_1FE0_0000，抹去高位的9后就得到Kernel和IO基址的实际物理地址
  3. 其余未使用的虚拟地址空间为非法地址，其中顶部的这块非法空间可以用来捕获出错的负数地址
  • 例外与中断

现有代码是参考龙芯架构linux的例外和中断，但是结构比较复杂。接下来打算参考xv6-riscv等操作系统，实现基础的例外和中断处理。

  • cmake分析 cmake1 图：cmake分析(1) cmake分析(1)图是启动sel4test（微内核测试框架-以riscv-spike为例）项目构建的cmake执行逻辑，其中标注的是各脚本和cmake的一些主要行为，后半部分是sel4微内核测试框架依赖的sel4官方开源的库的cmake设置，因和内核关联不大，这里没有记录。

cmake2 图：cmake分析(2) cmake分析(2)图是sel4内核部分的cmake执行逻辑，其中很多配置会通过脚本和cmake宏或者函数生成头文件，供根据具体架构和平台构建的的微内核使用。cmake过程中的具体逻辑请查阅图片中各节点的叙述。

  • 代码目录结构图 seL4源码目录结构图 图：seL4源码目录结构图

各仓库源码见文档seL4仓库及镜像说明。

  • riscv-loongarch寄存器和重点汇编指令对照表

表：riscv-loongarch寄存器映射方式

RISCV LA RISCV LA
s1 s0 t4 t4
s2 s1 t5 t5
s3 s2 t6 t6
s4 s3 t7 t7
s5 s4 ra ra
s6 s5 sp sp
s7 s6 gp r21(保留，不可分配)
s8 s7 tp tp
s9 s8 a0 a0
s0 s9 a1 a1
s10 t7 a2 a2
s11 t8 a3 a3
t0 t0 a4 a4
t1 t1 a5 a5
t2 t2 a6 a6
t3 t3 a7 a7

表：riscv-loongarch重点汇编指令对照表

RISCV指令 LA指令 riscv指令解释 LA指令解释
ecall syscall 0 从S切换到M 0是保留错误码
mv rd, rs move rd, rs x[rs]->x[rd] x[rs]->x[rd]
wfi idle level 当前硬件线程可以被暂停直到需要处理一个中断 处理器核停止取指令，进入等待状态，直至被中断唤醒或被复位，然后执行idle指令的下一条指令
STORE_S rd, offset(rs) st.d rd, rs, offset x[rd] -> M[ x[rs]+offset ] x[rd] -> M[ x[rs]+offset ]
LOAD_S rd, offset(rs) ld.d rd, rs, offset LOAD_S宏展开后是LOAD字符串，M[x[rs] +offset] -> x[rd] ,M表示内存 M[ x[rs]+offset ] -> x[rd]
j offset b offset 跳转到pc+offset 同左
jalr x1, 0(rs1) 用法：jalr rs1 jirl rd, rj, offs16 等效用法：jirl ra, rj, 0 此处ra特指返回地址寄存器，rj等效于左侧rs1 pc+4存入x[1](ra中)，跳转到rs1处。 pc+4存入rd中，跳转地址：rj的值+offs16逻辑左移两位再符号扩展。
li rd, imm li.w/li.d rd, imm load立即数 同左
bne rs1, rs2, offset 同左 不相等时分支（x[rs1] != x[rs2]） 同左
rdtime rd rdtime.d rd, rj 读出时间相关寄存器到rd 读出时间相关寄存器到rd，需要返回；rj保存counter ID号，可以不返回，
rdcycle rd 暂时用rdtime替代
sfence.vma x0, rj invtlb 0x4,rj,r0 vaddr=x0, asid=rj即不为0时，作用于指定asid的各级页表访问操作，不包括全局映射 见参考资料-龙芯指令集卷1-4.2.4.7，该指令不在此展开。r0是特指，rj是泛指某寄存器。0x4表示G=0，指定asid=rj的页表项
sfence.vma invtlb 0x0,r0,r0 作用于所有地址空间的各级页表访问操作 见参考资料-龙芯指令集卷1-4.2.4.7，该指令不在此展开。r0是特指r0寄存器。0x0表示清除所有页表项
fence.i ibar 0 在 Fence.I 之后所有指令的取指令操作，一定能够观测到在 Fence.I 之前所有指令造成的访存结果 用于单核内部store操作与取指操作之间的同步。确保该指令之后的取值一定能够观察到该指令之前所有store操作的执行效果。Load Barrier 读屏障。在读指令前插入该指令，可以让高速缓存中的数据失效，重新从主内存加载数据
jal offset bl offset pc+4存入ra，pc=pc+offset 同左
bnez rj, offset bnez rj, offset 不等于0跳转 同左
bnqz rj, offset bnqz rj, offset 等于0跳转 同左
beq rj, rd, offset beq rj, rd, offset 相等时跳转 同左
beqz rj, offset beqz rj, offset rj==0，跳转到offset 同左
jr rj jirl zero, rj, 0 寄存器跳转 pc=x[] 同左
la la 加载符号地址 同左

seL4仓库及镜像说明

在seL4微内核官方仓库里，包含微内核仓库、sel4test测试仓库等个仓库。为实现seL4移植和基础测试，我们fork了其中7个官方仓库，并在gitlab建立镜像，这7个仓库的功能和链接如下。

仓库名 仓库描述 gitlab地址(dev) github地址(dev)
la-seL4 seL4微内核代码 当前仓库 la-seL4-dev
la-sel4test seL4测试代码（用户空间程序） la-sel4test-dev la-sel4test-dev
la-seL4_tools 构建seL4项目的工具，包含cmake，elfloader等 la-seL4_tools-dev la-seL4_tools-dev
la-musllibc 提供代码静态链接和动态链接的轻量级C语言库 la-musllibc-dev la-musllibc-dev
la-sel4runtime 运行C语言兼容程序的最小runtime系统 la-sel4runtime-dev la-sel4runtime-dev
la-seL4_libs 在seL4微内核上编写用户程序的程序库 la-seL4_libs-dev la-seL4_libs-dev
la-util_libs seL4微内核使用的程序库，包括pci驱动库、驱动程序库、设备树库等 la-util_libs-dev la-util_libs-dev

开发进度和计划

  • 2022.02.25 - 2022.02.28 调研学习阶段，虚拟机环境配置、软件安装与sel4的尝试运行。
  • 2022.03.01 - 2022.03.03 调研学习阶段，尝试交叉编译不同架构下的sel4微内核并试运行，调研官方文档，建立开发仓库。
  • 2022.03.04 - 2022.03.07 调研学习阶段，继续调研，确定了要将sel4test(sel4微内核测试框架)项目移植到龙芯平台。
  • 2022.03.09 - 2022.03.11 调研学习阶段，学习sel4官方网站的资料，熟悉sel4设计模式和特点。
  • 2022.03.12 - 2022.03.22 准备阶段，，完成龙芯交叉编译调试环境的配置，完成sel4官方网站给出的示例教程，阅读官方文档。
  • 2022.03.23 - 2022.03.26 准备阶段，明确了参考sel4在RISCV架构下的设计，将其移植到龙芯平台的开发模式，搜集调研RISCV和龙芯开发文档，并尝试开始启动调试。建立了各思维导图(虚拟地址设计图、sel4源码目录结构图、sel4启动流程图等)、龙芯linux和sel4的源码注释仓库等，开始从阅读源码入手移植。
  • 2022.03.27 - 2022.03.29 准备阶段，开会明确分工，刘、陈主要负责sel4龙芯架构相关技术细节设计，并从sel4内核启动开始移植，雷主要负责从cmake项目构建和编译开始移植。
  • 2022.03.30 - 2022.04.12 移植阶段，补充龙芯架构缺少的文件，完成了从运行脚本到架构相关的项目的构建流程。
  • 2022.04.13 - 2022.05.03 移植阶段，基本完成了龙芯架构相关技术细节的设计和移植，并调试通过了ninja编译。
  • 2022.05.04 - 2022.05.15 调试和完善阶段，进行gdb调试，且已经成功进入内核。进行相关技术文档的撰写，迎接中期检查。
  • 2022.05.16 - 2022.05.31 调试和完善阶段，进一步调试和完善，争取在五月底完成移植工作，使sel4test成功运行。
  • 2022.06 - 以后 尝试增加更多细节以加以完善，如中断，运行示例等。

更加详细的开发日志请见腾讯文档，如没有权限查看请联系小组成员。

重要进展

待完善

遇到的主要问题和解决方法

团队从调研学习到调试阶段的问题和解决方案，全部记录在github仓库oscompProblemSolutions，请切换分支查看各队员的记录。

分工和协作

刘庆涛：添加设备树文件、uart驱动；编码中断模块；设计虚拟地址；参与项目调研、源码注释、内核调试和文档撰写。

雷洋：分析项目的cmake构建流程并添加龙芯架构支持；编写脚本简化项目构建、初始化和开发流程；参与项目调研、源码注释、内核调试和文档撰写。

陈洋：设计虚拟地址空间、编码内存管理模块；调试内核启动源码；移植elfloader；参与项目调研、源码注释、内核调试和文档撰写。

导师沟通及指导情况

在2022年3月，团队与项目指导教师（张福新老师）开始交流比赛信息，选择proj97-la-seL4赛题。

团队成员经常在腾讯会议和微信群中与张老师交流赛题内容和代码细节，并根据老师提供的龙芯交叉编译工具、龙芯开发手册、L4相关论文等资料（具体见参考资料）逐步移植seL4微内核。

非常感谢张老师为seL4移植工作给予的指导。

项目构建和编译方法

seL4官方给出的依赖包：Dependencies(seL4 docs)。

创建并进入sel4test目录，用repo命令获取官方库：

mkdir sel4test
cd sel4test
repo init -u https://github.com/seL4/sel4test-manifest.git
repo sync

在sel4test目录下，用wget获取并执行init_loongarch_seL4-test_dev.sh：

wget home.ustc.edu.cn/~le24/shell/init_loongarch_seL4-test_dev.sh
chmod u+x init_loongarch_seL4-test_dev.sh
./init_loongarch-seL4-test_dev.sh ssh

在sel4test目录下，创建build_3A5000文件夹：

mkdir build_3A5000
cd build_3A5000
../init-build.sh -DPLATFORM=3A5000 -DLoongarch64=1 -DSIMULATION=1

编译：

ninja

如果需要拉取和推送代码，我们在这里提供脚本帮助简化这一过程。

中期开发状态

点击此处查看演示视频及文字说明

参考资料

seL4官方资料(包括设计思想、API，seL4环境配置，项目构建和编译方法)

龙芯开源文档

张老师提供的龙芯资料

循序渐进，学习开发一个RISC-V上的操作系统 - 汪辰

qemu文档

gcc文档

2021年操作系统大赛参赛队的开源作品