seo企业网站源码,新网站建设需要注意,崇左网页设计,网站维护费用官网链接#xff1a;link
求解
代码中的很多方法例如这一个教程里面的seL4_GetMR(0)#xff0c;我在官方给的手册和API中都搜不到#xff0c;想问一下大家这些大家都是在哪里搜的#xff01;#xff01;
IPC
seL4中的IPC和一般OS中讲的IPC概念相差比较大#xff0c;根…官网链接link
求解
代码中的很多方法例如这一个教程里面的seL4_GetMR(0)我在官方给的手册和API中都搜不到想问一下大家这些大家都是在哪里搜的
IPC
seL4中的IPC和一般OS中讲的IPC概念相差比较大根据官方的意思是理解seL4的IPC的时候最好忘记IPC的概念起这个名字只是为了标准上对齐但是理解的时候最好将其当作专有名词来理解。
背景知识
进程间通信IPC是用于在进程之间同步传输少量数据和能力的微内核机制。在seL4中称为端点的小型内核对象促成了IPC端点充当的是通讯的端口。端点对象的调用通常被用于收发IPC数据。 端点们由一系列的等待收发信息的线程组成。为了理解这一点思考一个案例n个线程正在一个端点上等待一个信息。如果n个端点在一个端点上发送信息那么n个在该端点上等待信息的线程都将会收到这些信息且被唤醒。如果此时有第n1个发送者发送一个信息那么这个发送者将会排队等待。
系统调用
线程可以通过系统调用seL4_Send在端点上发送信息一直阻塞到信息被其他线程接收的时候。seL4_NBSend也可以用它执行轮询发送该发送仅当已经有一个线程阻塞等待一个信息的时候才会发送成功否则就失败。为了避免出现反向通道seL4_NBSend不返回指示消息是否已发送的结果。 seL4_Recv 可用于接收消息seL4_NBRecv 可用于轮询消息。 seL4_Call是一个系统调用本质上结合了seL4_Send和seL4_Recv但是有一个主要区别在接收阶段使用此函数的线程被阻塞在一个一次性能力上称为回复能力reply capability而不是在端点本身上。在client-server场景下客户端使用seL4_Call发出请求服务器可以显式的回复正确的客户端。 回复能力reply capability内部存储在接收者的线程控制块TCB中。系统调用 seL4_Reply 会调用这个能力向客户端发送一个进程间通信IPC并将其唤醒。seL4_ReplyRecv 也执行相同操作但它在一个组合的系统调用中发送回复并阻塞在提供的端点上。 由于线程控制块TCB只有一个空间来存储回复能力reply capability如果服务器需要处理多个请求例如在硬件操作完成后再进行回复可以使用 seL4_CNode_SaveCaller 将回复能力保存到接收者的 CSpace 中的一个空槽中。
方法说明seL4_Send发送后阻塞直到对方接收之后才会取消阻塞seL4_NBSend非阻塞发送发送后继续往下执行但不告知发送结果防止反向通道seL4_Call立即发送阻塞等待回复该回复不是说对方发消息的回复而是使用seL4_Reply进行回复才会取消阻塞继续往下执行seL4_Reply响应的功能只有他能唤醒call调用的阻塞也可唤醒seL4_Recv的阻塞seL4_Recv阻塞等待直到有消息到达这个消息可以是回复Send、NBSend也可以是响应Reply
反向通道 back channel
back channel反向通道 指的是一种非预期的或隐藏的信息传递路径可能会导致信息泄露或安全问题。通常在操作系统或安全系统中设计者希望确保通信通道只能按照预期的方式工作防止信息通过其他途径即“反向通道”泄露。在 seL4_NBSend 的情况下如果系统返回了消息是否成功发送的结果发送者就能通过这个结果推断接收者的状态例如接收者是否正在等待消息。这就可能成为一个反向通道允许一个线程获取另一个线程的状态信息而这类信息可能会被滥用。因此seL4_NBSend 不返回结果来避免这种潜在的安全隐患。
IPC Buffer
每个线程都有一个Buffer被称之为IPC Buffer它包含IPC消息是由数据和能力组成的。发送发指定消息长度内核在发送方和接收放IPC缓冲区之间复制此有界长度。
Data transfer
IPC 缓冲区包含用于在 IPC 上传输数据的消息寄存器 (MR) 有界区域。每个寄存器都是机器字大小最大消息大小可在 libsel4 提供的 seL4_MsgMaxLength 常量中找到。 可以使用seL4_SetMR 将消息加载到IPC 缓冲区中并使用seL4_GetMR 提取消息。小消息在寄存器中发送不需要复制操作。适合寄存器的字数可在 seL4_FastMessageRegisters 常量中获得。 所传输的数据量根据所使用的消息寄存器的数量必须设置为 seL4_MessageInfo_t 数据结构中的长度字段。
消息寄存器和IPC缓冲区之间的关系
1、消息寄存器
消息寄存器是 seL4 内核用于短消息传递的一个内部概念。在 seL4 中系统为每个线程分配了一些虚拟寄存器用于存储发送和接收的消息数据。这些消息寄存器主要用于传递少量数据例如几字节到几百字节。在处理简单的 IPC 传递时寄存器用来保存消息内容。seL4_GetMR(index) 函数的作用就是访问某个消息寄存器中的数据。index 代表消息寄存器的索引号比如 0 代表第一个消息寄存器。
2、IPC buffer
IPC buffer 是 seL4 中的一个内存区域用于消息传递。当消息过大、超出了消息寄存器的容量时IPC buffer 才被使用。IPC buffer 位于线程控制块 (TCB) 中线程可以通过这个缓冲区来传递大消息或能力等复杂的数据结构。也就是说小消息存储在消息寄存器中而大消息存储在 IPC buffer 中。
3、二者之间的关系
当 seL4 处理 IPC 消息时它首先会使用消息寄存器来传递较小的消息这比访问内存中的 IPC buffer 更快。如果消息的大小超过了消息寄存器的容量系统会将它分片后存入 IPC buffer寄存器中只保存与此消息相关的元数据或控制信息。
Cap transfer
除了数据之外IPC 还可用于在每个消息的进程之间发送能力。这称为能力转移。正在传输的能力数量在 seL4_MessageInfo_t 结构中编码为 extraCaps。下面是通过 IPC 发送能力的示例
seL4_MessageInfo info seL4_MessageInfo_new(0, 0, 1, 0);
seL4_SetCap(0, free_slot);
seL4_Call(endpoint, info);以前是玩过单片机看到这个寄存器的时候十分敏感总觉得是硬件寄存器。此处的寄存器指的是IPC消息的能力槽位(capability slot)中。所以上面的seL4_SetCap(0, free_slot) 的作用是把free_slot这个能力放到IPC消息info的第一个能力槽位中槽位索引为0。 若想要接收能力接收者必须指定一个 cspace 地址来放置该能力。这如下面的代码示例所示
seL4_SetCapReceivePath(cnode, badged_endpoint, seL4_WordBits);
seL4_Recv(endpoint, sender);接收到的能力的访问权限与接收者对端点拥有的权限相同。请注意虽然发送方可以发送多种功能但接收方一次只能接收一种功能。
Capability unwrapping 能力解包
在进程间通信IPC中seL4 也可以对能力capability进行解包unwrapping。如果消息中的第 n 个能力引用了用于发送消息的端点endpoint那么该能力会被解包它的徽章badge会被放置在接收者的 IPC 缓冲区的第 n 个位置在 caps_or_badges 字段中同时内核会将 seL4_MessageInfo_t 中 capsUnwrapped 字段的第 n 位从最低有效位开始计数设置为 1。 解释一下 在 seL4 系统中能力capability是线程访问系统资源例如端点、内存等的权限。在 IPC 通信中发送方可以通过消息传递这些能力给接收方。解包unwrapping 是指内核自动将发送方传递的能力标识符从能力对象中提取出来并放置在接收方的 IPC 缓冲区中供接收方使用。 具体来说如果消息中第 n 个能力引用了用于发送消息的端点指的是在 IPC 消息中第 n 个能力是与消息发送的那个端点相关联的能力。换句话说这个能力能够访问发送消息的端点或者与其进行交互。那么 seL4 会对这个能力进行特殊处理它会提取出这个能力的 badge徽章并将其放在接收方的 IPC 缓冲区中相应的位置。同时内核会通过设置 capsUnwrapped 字段中的位来标记哪些能力被解包了。
Message Info
seL4_MessageInfo_t 数据结构用于将 IPC 消息的描述编码为单个字。它用于描述要发送到seL4的消息并让seL4描述发送到接收者的消息。它包含以下字段
length 消息中消息寄存器数据的数量seL4_MsgMaxLength 最大值extraCaps 消息中的能力数量 (seL4_MsgMaxExtraCaps)capsUnwrapped 标记被内核解包的能力label 从发送方传输到接收方的未经内核修改的数据
Badges 徽章
除了消息内核还会传递发送者调用以发送消息的端点能力的徽章badge。端点可以通过 seL4_CNode_Mint 或 seL4_CNode_Mutate 来进行标记。一旦端点被徽章标记接收到该端点消息的任何接收者都会获得该端点的徽章。下面的代码示例演示了这一点
seL4_Word badge;
seL4_Recv(endpoint, badge);
// once a message is received, the badge value is set by seL4 to the
// badge of capability used by the sender to send the messageFastpath
快速 IPC 对于基于微内核的系统至关重要因为服务通常彼此分离以进行隔离而 IPC 是客户端和服务之间通信的核心机制之一。因此IPC 有一个快速路径——内核中经过高度优化的路径——它允许这些操作非常快。为了使用快速路径IPC 必须满足以下条件
必须使用seL4_Call或seL4_ReplyRecv消息中的数据必须适合 seL4_FastMessageRegisters 寄存器。进程必须具有有效的地址空间不传送能力调度程序中没有比被 IPC 解除阻塞的线程优先级更高的其他线程可以运行。
额还是想吐槽太复杂了
实操
这篇教程中有几个由capDL loader设置好的进程两个clients一个server。所有进程都拥有对同一个端点能力访问的权限该能力提供了对同一个端点对象的访问。看了上面的背景知识仍然不是很能搞懂下面插一节补充。
补充
IPC 缓冲区每个线程TCB都有自己专属的 IPC 缓冲区用于发送和接收消息。这个缓冲区通常是在线程的用户地址空间内通过 seL4_SetIPCBuffer 设置。在执行 IPC 操作时内核会自动将消息放入该线程的 IPC 缓冲区端点endpoint端点是 seL4 中用于线程之间通信的对象。多个线程可以共享同一个端点能力这意味着它们可以通过这个端点进行通信。例如两个线程可以都向同一个端点发送或接收消息从而实现消息的交换或同步
在对端点的解释中说向同一个端点发送或接收消息这句话令人很摸不着头脑下面基于五个对象线程A、线程B、端点A、线程A的IPC缓冲区、线程B的IPC缓冲区举一个IPC通信的完整例子辅助理解。 场景
线程A需要向线程B发送一个消息。线程A和线程B通过端点A来实现通信。每个线程都有自己的IPC缓冲区来存储消息。对象
线程A发送消息的线程。线程B接收消息的线程。端点A线程A 和线程B 用于通信的共享端点。线程A的IPC缓冲区用于存储线程A发送或接收的消息内容。线程B的IPC缓冲区用于存储线程B接收的消息内容。
IPC流程
创建端点A 系统中创建一个端点对象 端点A它用来作为通信通道供线程A 和线程B 通过它进行消息的传递。两者共享这个端点。线程A向端点A发送消息线程A 将消息放入自己的 IPC缓冲区并使用系统调用 seL4_Send(endpointA) 来发送消息。这个系统调用会将消息从 线程A的IPC缓冲区 发送到 端点A。端点A 在这个时候相当于一个“信箱”等待另一个线程线程B来取消息。线程B等待接收消息线程B 通过调用 seL4_Recv(endpointA) 在 端点A 上等待消息。这时线程B 阻塞等待消息到达。当消息到达时内核会通过端点讲消息从线程A的IPC缓冲区 拷贝到 线程B的IPC缓冲区。消息传递完成当消息被传递到 线程B的IPC缓冲区 后线程B 不再阻塞恢复运行并可以从它的 IPC 缓冲区读取消息。
流程如下
线程A的IPC缓冲区 --- 端点A --- 线程B的IPC缓冲区上面的流程给人一种端点A存储了通信的信息的感觉实际上端点A本身并不存储消息。但是它实际上是一个同步机制用于协调消息在不同线程之间的传递。在seL4中消息通过IPC机制在不同线程之间传递端点A起的是“连接”作用而不是数据存储作用。
IPC的工作机制
当 线程A 调用 seL4_Send(endpointA) 发送消息时消息被存储在线程A的IPC缓冲区中。当 线程B 调用 seL4_Recv(endpointA) 接收消息时内核会将消息从 线程A的IPC缓冲区 复制到 线程B的IPC缓冲区通过端点A作为中介来协调消息的传递。 也就是说端点A起到的是协调消息传递的作用它不存储数据而是促使内核将数据从发送者的缓冲区拷贝到接收者的缓冲区。
所以端点的作用是什么
内核通过它判断哪些线程在等待消息或发送消息。当线程B准备好接收消息时内核会在后台完成消息从 线程A的IPC缓冲区 到 线程B的IPC缓冲区 的数据拷贝端点A 是一个信号机制用于确定消息何时可以被传递。它不存储消息也没有持有对线程A IPC缓冲区的访问权限。
回到教程
在这篇教程中你将会创建一个服务器输出由客户端发送过来的信息内容。你还讲更改客户端回复的顺序以获得正确的消息。当你运行代码的时候输出差不多是这样子的输出的顺序可能不太一样 在初始化时两个客户端使用以下协议它们在提供的端点上等待通过能力转移发送给它们的带徽章的端点。之后客户端发送的所有消息都使用带徽章的端点以便服务器能够识别客户端。然而服务器当前并没有发送带徽章的能力我们提供了代码来给端点能力加徽章并回复客户端。 练习我们的任务是设置能力传送这样客户端才能成功的接收到带徽章的端点能力。看一下代码
seL4_Word badge seL4_GetMR(0);//这个函数用于从当前线程的消息寄存器中读取指定索引位置的值。索引从 0 开始因此 seL4_GetMR(0) 返回的是第一个消息寄存器的值。// server在自己的地址空间复制了一个带徽章的端点能力下面需要做的是将这个能力传给发送者看完下面方法的详解就能看懂这个方法是干啥的了
seL4_Error error seL4_CNode_Mint(cnode, free_slot, seL4_WordBits,cnode, endpoint, seL4_WordBits,seL4_AllRights, badge);
printf(Badged %lu\n, badge);// TODO use cap transfer to send the badged cap in the reply 将这个徽章标记的端点能力发出去/* reply to the sender and wait for the next message */
seL4_Reply(info);/* now delete the transferred cap */
error seL4_CNode_Delete(cnode, free_slot, seL4_WordBits);
assert(error seL4_NoError);/* wait for the next message */
info seL4_Recv(endpoint, sender);看一下seL4_CNode_Mint这个方法其作用是拷贝一个能力同时设置其权限和徽章。 现在我们来梳理一下一个server和两个client的逻辑。 对于server.c而言 在初始的时候会调用seL4_Recv阻塞住自己等待client发送信息过来在之前我们说过这个阻塞只要对方有消息过来就会被唤醒当有消息过来了之后进入一个死循环以下是死循环的内容判断有没有badge。如果没有badge则取收到的消息第一个寄存器的内容作为badge复制一个带badge的endpoint将能力放在free_slot插槽里面创建一个IPC消息体使用reply传回这个消息体然后删除掉新创建的能力然后阻塞等待下一条消息进行下一次循环回到3如果有badge暂时是空的指的是原代码里面的内容需要我们填充回到3 对于client.c而言两个client的逻辑完全相同只挑一个说 设置好收到的能力放置在哪个槽里面第一个消息寄存器中填入值创建一个IPC消息体使用call发送出去然后阻塞等待reply等到了reply之后将定义在数组中的单词放置在消息寄存器中发出去然后阻塞等待回复直到所有的单词发完为止 上面理清楚了之后做第一个TODO
// TODO use cap transfer to send the badged cap in the reply
// 只发送一个能力
info seL4_MessageInfo_new(0, 0, 1, 0);
// 消息体的能力槽中指定要传送的能力
seL4_SetCap(0,free_slot);运行之后输出如下 运行到这里的时候两个client都会因为call的调用而阻塞住而server端因为运行到了else里面是空的所以我们需要继续填充else中的内容。 进行下一个TODO
// TODO use printf to print out the message sent by the client
seL4_Word length seL4_MessageInfo_get_length(info);//seL4_MessageInfo_get_length这个方法是我搜出来的
for (int i 0; i length; i)
{seL4_Word character seL4_GetMR(i); // 获取每个消息寄存器中的字符printf(%c, (char)character); // 将其作为字符打印
}
// followed by a new line
printf(\n); // 打印换行符输出如下 做下一个TODO
// TODO reply to the client and wait for the next message
// info seL4_MessageInfo_new(0, 0, 0, 0);
seL4_Reply(info);
info seL4_Recv(endpoint, sender);输出如下 不知道为啥报错。 有知道的请留言seL4_CNode_SaveCaller这个没用谁用了请留言交流一下。
