问题标签 [sel4]

我在 Google 上搜索了很多关于 L4 微内核的信息，发现 L4 上的资源非常少。

1. 我可以参考哪些好的链接？
2. L4 是否有任何应用（即在哪里使用）？

我想在 seL4 上构建一个系统，我不想从头开始编写驱动程序。我知道 L4linux 设法通过 fiasco.OC 提升了整个 linux 内核，包括驱动程序。

理想情况下，我想要一个驱动程序包装器，它允许我在 sel4 上将 linux 驱动程序作为独立任务运行。

我愿意编写很多代码。但我想避免阅读硬件规格表和重写驱动程序。

我们能否拥有针对桌面用户的具有微内核架构的操作系统？我在这个网站上读到过旧的微内核可能比单体内核慢 50%，而像 L4 这样的更高版本只比单体内核慢 2% 或 4%。L4内核以其性能而闻名。

为什么我们没有针对桌面用户的基于微内核架构的操作系统？我们将来能有这样的操作系统吗？

我正在尝试在用户空间中为 sel4 编写示例 USB 驱动程序。任何人都可以对 sel4 用户空间驱动程序有任何想法，请与我分享...如果有人有 sel4 用户空间驱动程序的示例代码（示例驱动程序），请与我分享...

最初我认为 Fuchsia 是第一个广泛使用基于能力的安全性的内核，但看起来在 seL4 中它们也是主要的安全原语。

简而言之：

我正在尝试在 x86_64 虚拟机中运行 sel4 微内核，但无法使以太网接口正常工作。在 sel4 微内核上获得 Internet 连接（通过 vitio-net 以太网设备）的正确程序是什么？什么是正确的（内存）地址？

长版：

我已经使用 e1000 网络设备尝试了 camkes (picoserver) 示例，但无法让它们工作，所以我决定学习一些新东西并从头开始。此外，我决定使用 virtio-net（与 vhost 一起）而不是模拟 e1000 设备以获得更好的性能。我的计划是使用ethif_virtio_pci_init初始化一个eth_driver结构，然后将该结构传递给 picoTCP。现在我可以在 sel4 中找到 virtio PCI 设备，但我不确定如何正确访问它并ethif_virtio_pci_config_t为ethif_virtio_pci_init.

来自 libethdrivers virtio_pci.h 的一些信息：

所以ethif_virtio_pci_config_t我需要一个 uint16_t io_base 地址和一个指向 MMIO 基址的指针。

这是我到目前为止获得的信息：

据我了解，我现在需要将物理地址映射到虚拟地址。为此，我创建了一个 IO-mapper，但我不确定要映射什么。从 0x8000000 开始的整个 dma 区域还是只是 virtio 设备的地址？据我了解，新的虚拟地址将是我的 MMIO 基指针，但 uint16_t io_base 是什么？

到目前为止，这是我的代码，我不确定的部分在最后：

我读了很多关于 sel4 内核的文章，但我对 sel4 微内核（和 Linux 内核）的大多数概念仍然很陌生，所以我非常感谢任何提示和建议。我通常使用嵌入式、微控制器和更多“裸机”平台，想学习一些新的东西，但现在很多东西都很混乱。

为什么页面全局目录中的条目会偏移？如果有的话，偏移量的意义是什么？

页面全局目录

为什么不在 0x80036000 的位置 0 开始条目？

RISC-V (sv39) 的 Linux 和 seL4 使用三级页表，该页表具有页全局目录 (PGD)、页中间目录 (PMD) 和页表条目 (PTE)。PTE 条目指向可执行数据。正是这样：http ://www.science.unitn.it/~fiorella/guidelinux/tlk/node34.html

每个表为 4096 字节或 0x1000。每个条目是 64 字节。每个表可以有 512 个条目 (0x200)。一些表——特别是 PGD 和 PMD 有偏移的条目。换句话说，条目不是从表中的位置 0 开始，而是在表中途甚至 3/4 处为 0。我试图理解为什么会这样。

问题是关于表格中的位置而不是位置的内容。这就是为什么从 0x80036c00 开始而不是 0x2000d401 的含义？我知道 0x2000d401 指向 PMD 中的一个条目，该条目指向 PTE 中的一个条目，最后指向可执行代码。

我可以毫无问题地在概念上遍历页表。我的问题是我已经在我的二进制文件中移动了有效负载并修改了页表以使用 4KB 而不是 2MB 页面。这适用于特殊情况，但不适用于一般情况，我试图了解原因。我怀疑基于我得到的 QEMU 输出的页表有问题。