广西网站建设公司哪家好_app公司开发_浙江企业网站建设_关键词搜索排名优化

seL4 Dynamic Libraries: initialisation & threading

本教程提供了代码示例和练习，用于使用SEL4_LIBS中的动态库来引导系统并启动线程。
本教程非常有用，因为它解决了两种不同类型的开发人员的概念问题：

经验丰富的内核开发人员的思维被预先编程为“一个地址空间等于一个进程”，并开始引入 seL4 CSpace 与 VSpace 模型。
新的内核开发人员，教程将提示他们阅读哪些内容。

不要删除main() 之前声明的全局变量 - 它们是为了你的便利而声明的，以便你可以掌握一些基本的数据结构。这篇教程的目的旨在让读者掌握以下内容：

了解内核的启动过程。
了解内核以某些对象和这些对象的功能为中心。
了解库的存在是为了自动化 seL4 API 的细粒度特性，并大致了解其中一些库。
了解内核如何将控制权移交给用户空间。
了解 seL4 API 如何使开发人员能够操作他们遇到的能力所引用的对象。
了解如何在 seL4 中生成新线程，以及线程具有 TCB、VSpace 和 CSpace 的基本思想，并且是教程中需要填写的内容。

Initialising

# For instructions about obtaining the tutorial sources see https://docs.sel4.systems/Tutorials/#get-the-code
#
# Follow these instructions to initialise the tutorial
# initialising the build directory with a tutorial exercise
./init --tut dynamic-1
# building the tutorial exercise
cd dynamic-1_build
ninja

Exercises

首次运行本教程时，您应该看到以下输出：

Booting all finished, dropped to user space
main@main.c:89 [Cond failed: info == NULL]
Failed to get bootinfo.

Obtain BootInfo

引导系统后，seL4 内核将控制权移交给 root 任务，即一个初始化线程。该线程从内核接收一个结构体，该结构体描述了机器上所有可用的资源。这个结构体称为BootInfo结构体。它包括有关所有 IRQ、内存和 IO 端口 (x86) 的信息。该结构还告诉 init 线程某些重要的能力引用在哪里。这一步将教您如何获得该结构。
seL4_BootInfo* platsupport_get_bootinfo(void) 是返回 BootInfo 结构的函数。它还设置 IPC 缓冲区，以便可以执行一些系统调用，例如 name_thread 使用的 seL4_DebugNameThread。
下面是源码可以详细的看一下：

bootinfo_types.h
bootinfo.c

基于以上的两个链接，任务一就是获取启动信息：

// 比较简单只需要一行代码
/* TASK 1: get boot info */
info = platsupport_get_bootinfo();

此时的输出如下：
在这里插入图片描述

Initialise simple

libsel4simple提供了线程引导环境的抽象。在使用它之前，需要使用某种默认状态对其进行初始化。

simple-default.h

 /* TASK 2: initialise simple object 用底层数据结构info去初始化simple，以简化开发*/simple_default_init_bootinfo(&simple,info);

这一步成功输出也不会改变。

Use simple to print BootInfo

使用一个简单的函数打印出seL4_BootInfo函数的内容。

/* TASK 3: print out bootinfo and other info about simple */
// 看了一下源码，simple里的成员大多数都是函数指针，函数指针的赋值是在simple_default_init_bootinfo这个里面进行的
// simple_print是在调用simple函数指针指向的函数时进行了一层检查和封装
simple_print(&simple);

此时会格式化输出一堆信息：
在这里插入图片描述
可以看出来，simple对象是对info对象的一种封装，方便程序员使用，方便编程。在这段输出的背后仍然有错误的输出信息。

Initialise an allocator

在 seL4 中，内存管理大部分委托给用户空间，每个线程使用自定义分页器管理自己的页面错误。如果不使用 allocman 库和 VKA 库，您必须手动分配一个页帧，然后将该帧映射到页表中，然后才能在地址空间中使用新内存。在本教程中，您不会经历该过程，但稍后您会遇到它。现在，使用 allocman 和 VKA 分配系统。 allocman 库需要一些初始内存来引导其元数据。完成此步骤。这两个时辅助程序员进行内存管理的。

 /* TASK 4: create an allocator */// allocman_t 是 seL4 中的资源分配管理器（Allocator Manager）的核心结构体，用于管理系统的能力（capabilities）和内存资源。allocman 通过对资源的跟踪、分配和回收，来确保系统运行过程中能够有效利用资源。// bootstrap_use_current_simple：用于将系统的资源信息封装到 simple_t 中，并传递给 allocman，为系统初始化做好准备。allocman = bootstrap_use_current_simple(&simple, ALLOCATOR_STATIC_POOL_SIZE, allocator_mem_pool);ZF_LOGF_IF(allocman == NULL, "Failed to initialize alloc manager.\n""\tMemory pool sufficiently sized?\n""\tMemory pool pointer valid?\n");

此时的输出应该是这样：
在这里插入图片描述

Obtain a generic allocation interface (vka)

libsel4vka 是一个 seL4 类型感知对象分配器，它将为您分配新的内核对象。 seL4 中的术语“分配新内核对象”是“重新类型化”先前未类型化内存的更详细过程。 seL4 认为所有未明确指定用途的内存都是“无类型的”，并且为了将任何内存重新调整为有用的对象，您必须为其指定特定于 seL4 的类型。这就是重新输入，除其他外，VKA 库还为您简化了这一过程。
vka.h

/* TASK 5: create a vka (interface for interacting with the underlying allocator) */
allocman_make_vka(&vka, allocman);

完成这一步输出不会改变。

Find the CSpace root cap

/* TASK 6: get our cspace root cnode */
cspace_cap = simple_get_cnode(&simple);

这就是 seL4 和当代内核之间的差异开始显现的地方。您“重新类型化”的每个内核对象都将使用能力引用交给您。 seL4 内核保留了这些能力的多个树。每个单独的能力树称为“CSpace”。每个线程可以有自己的CSpace，也可以在多个线程之间共享CSpace。 “进程”之间的界限没有明确定义，因为 seL4 没有任何真正的“进程”概念。它处理线程。共享和隔离基于 CSpaces（共享与非共享）和 VSpaces（共享与非共享）。 “进程”的想法可能涉及这样一个事实：在硬件级别，共享同一 VSpace 的线程在传统意义上是兄弟姐妹，但从逻辑上讲，在 seL4 中，实际上并不存在“进程”的概念。
因此，您必须获取对线程 CSpace 根“CNode”的引用。 CNode 是构成 CSpace 的众多功能块之一。这一步成功输出结果也不会改变

Find the VSpace root cap

/* TASK 7: get our vspace root page diretory */
seL4_CPtr pd_cap;
pd_cap = simple_get_pd(&simple);

正如上一步一样，您需要获取对线程 CSpace 根的引用，现在您需要获取对线程 VSpace 根的引用。这一步成功输出结果也不会改变。

Allocate a TCB Object

//typedef struct vka_object {
//    seL4_CPtr cptr;
//    seL4_Word ut;
//    seL4_Word type;
//    seL4_Word size_bits;
//} vka_object_t;
/* TASK 8: create a new TCB */
vka_object_t tcb_object = {0};
vka_alloc_tcb(&vka, &tcb_object);//这里要取地址
ZF_LOGF_IFERR(error, "Failed to allocate new TCB.\n""\tVKA given sufficient bootstrap memory?");

为了管理在 seL4 中创建的线程，seL4 内核跟踪 TCB（线程控制块）对象。其中每一个都代表一个可调度的可执行资源。与其他当代内核不同，seL4 不会代表您分配堆栈、虚拟地址空间 (VSpace) 和其他元数据。此步骤创建一个 TCB，这是一个非常简单的原始资源，仍然需要您手动填写。
完成此任务后，错误应该消失，并且您应该看到以下输出：
在这里插入图片描述

Configure the new TCB

 /* TASK 9: initialise the new TCB */seL4_TCB_Configure(tcb_object.cptr, seL4_CapNull, cspace_cap, seL4_NilData, pd_cap, seL4_NilData, 0, seL4_CapNull);ZF_LOGF_IFERR(error, "Failed to configure the new TCB object.\n""\tWe're running the new thread with the root thread's CSpace.\n""\tWe're running the new thread in the root thread's VSpace.\n""\tWe will not be executing any IPC in this app.\n");

如果您需要新线程在其自己的隔离地址空间中执行，则必须为新线程创建一个新的 VSpace，并告诉内核您计划让新线程在哪个 VSpace 中执行。这为线程共享 VSpace 提供了选项。以类似的方式，您还必须告诉内核您的新线程将使用哪个 CSpace - 是否会共享当前现有的 CSpace，或者您是否为其创建了一个新的 CSpace。这就是你现在正在做的事情。在这个特定的示例中，您允许新线程共享主线程的 CSpace 和 VSpace。
此外，线程需要设置优先级才能运行。 seL4_TCB_SetPriority(tcb_object.cptr,seL4_CapInitThreadTCB,seL4_MaxPrio);将为您的新线程提供与当前线程相同的优先级，从而允许它在下次调用 seL4 调度程序时运行。每次有内核计时器滴答时都会调用 seL4 调度程序。
成功完成此任务后，输出不应改变。

Name the new TCB

/* TASK 10: give the new thread a name */
NAME_THREAD(tcb_object.cptr, "thread-2");

这是一个便利函数——为 TCB 对象设置名称字符串。
成功完成此任务后，输出不应改变。

Set the instruction pointer

/*
* set start up registers for the new thread:
*/
UNUSED seL4_UserContext regs = {0};
/* TASK 11: set instruction pointer where the thread shoud start running */
sel4utils_set_instruction_pointer(&regs,(seL4_Word)thread_2);

请注意此特定任务之前的行 - 将新的“seL4_UserContext”对象清零的行。正如我们之前所解释的，seL4 要求您手动填写线程控制块。这包括新线程的初始寄存器内容。您可以设置堆栈指针、指令指针的值，如果您想要一点创意，您可以通过其寄存器将一些初始数据传递给新线程。
utils.h
成功完成此任务后，输出不应更改。

Set the stack pointer

/* TASK 12: set stack pointer for the new thread */
sel4utils_set_stack_pointer(&regs, (seL4_Word)(thread_2_stack + THREAD_2_STACK_SIZE - 1));

这个任务只是一些指针算术。堆栈向下增长的警告是为了让您思考算术。处理器堆栈将新值推向递减的地址，因此请考虑一下。
成功完成此任务后，输出不应改变。

Write the registers

/* TASK 13: actually write the TCB registers.  We write 2 registers:
* int seL4_TCB_WriteRegisters(seL4_TCB service, seL4_Bool resume_target, seL4_Uint8 arch_flags, seL4_Word count, seL4_UserContext *regs)
* @param resume_target 	调用该方法之后是否立即恢复这个线程的执行
* @param arch_flags Architecture dependent flags. These have no meaning on either IA-32 or ARM.
* 对于大多数常见架构（如 ARM 和 x86），arch_flags 通常不需要特别设置，设置为 0 就足够了。
* /
seL4_TCB_WriteRegisters(tcb_object.cptr, false, 0, 2, &regs);

如上所述，我们在最后几个操作中填写了新线程的 TCB，因此现在我们将选择的值写入内核中的 TCB 对象。成功完成此任务后，输出不应更改。

Start the new thread

  /* TASK 14: start the new thread running */error = seL4_TCB_Resume(tcb_object.cptr);

最后，我们告诉内核我们的新线程可以运行。从这里开始，内核本身将根据我们赋予线程的优先级以及内核配置的调度策略来选择何时运行线程。成功完成此任务后，输出不应改变。

Print something

    /* TASK 15: print something */printf("aasdasddddddddddddddddas\n"); //\n必须加，不然好像不会输出

为了确认内核已成功执行我们的新线程，我们使其在屏幕上打印一些内容。成功后，应该看到新线程的输出。
在这里插入图片描述

Links to source

sel4_BootInfo
simple_t
vka_t
allocman_t
name_thread()