开源操作系统的LoongArch移植—seL4微内核：proj97-la-seL4。
欢迎充满热情的你，关注💖💖💖LoongArch国产指令集和seL4开源项目💖💖💖
如果你觉得本团队的移植工作有参考价值😊，请不要吝惜你的⭐
- 工程量大。seL4官方有55个仓库，编写或运行程序往往需要关联多个仓库。团队工作不仅涉及elfloader、cmake等程序或工具的移植，还涉及微内核、测试程序、形式化验证等仓库的移植。
- seL4移植资料少。相比于xv6教学操作系统，seL4的官方指导资料和技术博客较少，官方只提供了架构无关的设计**，团队需要充分理解riscv等架构代码才能移植seL4到龙芯平台。
- 龙芯演示资料少。龙芯指令集在2021年发布，教学资料和技术博客较少，可供参考示例程序不多。
-
展示文档
- 2022.09.16，龙芯版seL4微内核通过所有sel4test测试用例，视频。
- 2022.08.15，决赛项目文档。建议下载阅读，github在线阅读pdf可能有问题。
- 2022.08.15，决赛演示视频：百度网盘链接或github链接。
- 2022.08.07，项目分享会（8月7日第十场）：分享会视频和分享会PPT。
- （初赛）2022.05.30，初赛文档-la-seL4-项目调研_设计_展示文档。
- （初赛）2022.05.15，初赛中期-设计和展示文档。
- （初赛）2022.05.15，初赛中期-演示视频及文字说明。
-
技术文档等资源
- 项目构建、编译、调试方法和调试脚本：项目构建、编译、调试方法和调试脚本。
- 用于自动化测试的龙芯版本docker镜像：镜像功能见项目资源，现构建出：la-seL4，la-l4v，la-cparser-builder，la-cparser-run。
- cmake框架分析图：cmake框架分析图。
- seL4源码结构图：seL4源码结构图。
- seL4-comments，团队的seL4内核源码仓库注释仓库：seL4-comments。
- seL4_tools-comments，团队的seL4-elfloader源码注释仓库：seL4-tools-comments。
- 开发中积累的技术文档：os-comp-Problem-Solutions。
- commit规范：Angular团队commit message规范。
- 许可证：GPL，已通过seL4的CI workflow许可证和版权信息检查。
- 决赛进展：
- 内核移植完成，完善内存管理、中断与例外模块，正常引导用户空间程序。
- 进入sel4test测试程序，通过15个测试样例。
- 构建龙芯版本docker，移植自动化测试程序(github workflow)：通过Compile workflow、C Parser workflow、CI workflow和RefMan workflow检查。
- 初赛进展：
- cmake文件中，关于LoongArch的部分。
- 完成elfloader移植的移植，引导微内核启动。
- 完成虚拟内存映射。
- 配置好中断与例外框架。
- 成功编译出内核。
- 微内核初始化完成，调试到激活线程的位置。
在seL4微内核官方仓库里，包含微内核等55个相关仓库。为实现seL4微内核移植和用户程序测试，我们fork并修改了其中10个官方仓库（并在gitlab建立镜像），还使用了seL4_projects_libs和projects_libs仓库，这些仓库的介绍和链接如下。
| 仓库名 | 仓库描述 | gitlab地址 | github地址 |
|---|---|---|---|
| la-seL4 | seL4微内核代码 | 当前仓库 | la-seL4 |
| la-sel4test | seL4测试代码（用户空间程序） | la-sel4test | la-sel4test |
| la-seL4_tools | seL4构建工具，如cmake，elfloader等 | la-seL4_tools | la-seL4_tools |
| la-musllibc | 轻量级C语言库 | la-musllibc | la-musllibc |
| la-sel4runtime | 运行C语言兼容程序的最小runtime系统 | la-sel4runtime | la-sel4runtime |
| projects_libs | 用户程序库 | —— | 使用官方仓库 |
| seL4_projects_libs | 用户程序库 | —— | 使用官方仓库 |
| la-util_libs | 用户程序库 | la-util_libs | la-util_libs |
| la-seL4_libs | 用户程序库 | la-seL4_libs | la-seL4_libs |
| la-seL4-ci-actions | 自动化测试程序仓库 | la-seL4-ci-actions | la-seL4-ci-actions |
| la-l4v | seL4形式化证明工具仓库 | la-l4v | la-l4v |
| la-seL4-CAmkES-L4v-dockerfiles | docker镜像构建仓库 | la-seL4-CAmkES-L4v-dockerfiles | la-seL4-CAmkES-L4v-dockerfiles |
为促进操作系统教学，推进龙芯生态建设，扩大seL4开源社区影响力，特分享本项目资源：
- 团队资源
- tyyteam org：15个git仓库，含移植笔记、代码注释、CI仓库、docker仓库等。
- 龙芯版docker镜像：
- la-seL4:latest：该镜像包含单独编译内核的所有依赖（包括龙芯交叉编译工具），支持编译龙芯版seL4内核。
- la-l4v:latest：该镜像包含构建l4v的所有工具和依赖（包括龙芯版本脚本），也是构建la-cparser-builder镜像、形式化验证等工作的基础镜像。
- la-cparser-builder:latest：该镜像包含cparser源码编译分析工具（包括龙芯版本），也是la-cparser-run等镜像的基础镜像。
- la-cparser-run:latest：该镜像包含上述基础镜像和其他seL4官方镜像、脚本，能对内核源码执行更严格的语法检查，为形式化验证工作做准备。
- 技术文档：见文档和演示。
- 龙芯资源
- seL4资源
感谢团队成员（刘庆涛，雷洋和陈洋）彼此给予的支持鼓励😊😊😊
更加感谢指导老师（张福新老师和高燕萍老师）的辛勤付出👍👍👍
还要感谢徐淮，胡起，袁宇翀，谢本壹，梁思远的帮助和建议，感谢seL4技术团队（Kent McLeod，Axel Heider，Jashank Jeremy，Gernot Heiser，Gerwin Klein等）在github issue上的指导和支持💖💖💖
React
Typescript
Django
Laravel
Facebook
Microsoft
Google
Alibaba
D3
Tencent