组织介绍

组织介绍

OpenMicrokernel是由北京大数据先进技术研究院、清华大学、上海交通大学和西北工业大学共同研究开发的微内核与微内核操作系统项目。目标是满足泛在计算场景对强实时、高可靠、高效率操作系统的需求,对分布式微内核操作系统理论与关键技术展开深入研究,构建安全、可靠、高效的微内核操作系统。

国家自然科学基金重点项目“分布式微内核操作系统理论与关键技术”(批准号: 62332012)资助项目

技术架构

OpenMicrokernel遵从分层设计,从下向上依次为:硬件体系结构层、虚拟机监视器hypervisor层、内核层、操作系统框架层和应用层。

硬件体系结构层

系统在硬件体系结构层面提供了较为多样的ISA指令集支持,目前支持x86_64/ARM/RISC-V/LOONGARCH四种硬件体系结构,充分满足了泛在异构场景的应用需求。
ARM是一种精简指令集(RISC)架构,广泛用于移动设备、嵌入式系统和服务器等领域。ARM架构以低功耗、高性能著称,采用精简指令集设计,使其在能效方面表现突出。ARM公司主要采用授权模式,许多厂商如苹果、高通和三星等都会基于ARM架构设计自己的芯片,推动了ARM生态的广泛发展。

RISC-V是一种开源的RISC架构,由加州大学伯克利分校开发,并由RISC-V基金会管理。与ARM不同,RISC-V采用开源许可,允许任何公司和个人自由使用和扩展其指令集,降低了芯片开发的门槛。这种开放性促进了RISC-V在嵌入式、AI、服务器等多个领域的快速发展,吸引了众多科技企业和学术机构的关注。

LoongArch是由龙芯中科(Loongson Co,Ltd)公司自主研发的一种指令集架构,旨在减少对国外架构的依赖。它基于RISC思想设计,并兼容多种软件生态,如Linux和国产操作系统,支持向量计算、虚拟化等特性。LoongArch的推出标志着中国在自主可控计算架构方面迈出了重要一步,有助于推动国内信息产业的独立发展。

虚拟机监视器hypervisor层

NPU负责

内核层

OpenMicrokernel采用了seL4作为其内核,seL4目前首个经过全面形式化验证的通用操作系统内核。选择seL4作为内核,能够有效地提升整体系统的安全性,为高可靠计算环境提供坚实的基础。

然而,seL4在泛在计算中的实际应用也面临一些挑战,尤其是在进程间通信(IPC)方面。我们发现OS框架层系统服务之间耦合度很高,互相过程调用频繁,其性能明显受制于seL4默认的端点(Endpoint)模型:引入了一次性回复权能(Single-use Reply Capability)来支持过程调用,但其通用性设计导致了大量不必要的合法性检查,忽略了系统服务间天然相互信任、明确识别的特点。

为此,我们提出了基于权能旁路的同步IPC快速路径(Synchronous IPC Fastpath based on Capability-Bypass)。该方案允许系统服务向内核申请通信保护密钥,并注册一个处理函数作为入口点。内核在执行IPC时,仅需切换堆栈/指令寄存器并保留堆栈现场,利用硬件寄存器传递调用参数,从而避免冗余的权能操作。相比传统的seL4 IPC机制,该方法极大地减少了进程间通信的开销,使得系统服务过程调用的延迟大幅降低,同时具备较好的硬件适配性。

这一优化方案不仅提升了seL4 在泛在计算场景下的适用性,也为上层操作系统框架(Genode)提供了更加高效的 IPC 机制,同时兼容底层Hvisor虚拟化环境的扩展需求。

在内核层,相关开发资源与开发支持有:

seL4 microkernel
sel4 resources
sel4 tutorials
Archived community seL4 on Loongarch64 platform

优化后的seL4微内核
优化后的高效内核(x86/ARM/RISCV架构)
优化后的高效内核(Loongarch 架构)

操作系统框架层

sjtu负责

https://gitee.com/open-microkernel/GenodePlus

网络结构层

北京大数据研究院负责的网络结构部分

如何加入

(临时)请发送申请邮件至yiming_zhou2002@163.com

联系

(临时)邮箱: yiming_zhou2002@163.com

成就
0
Star
0
Fork
成员(5)
lr
yimingzhou2002
Zoran
xj
qizhenlin

搜索帮助