Hi I have recently started with working on sel4 and I have a couple of questions. i) Can a process be spawned or configured only from the root task? (using sel4_configure_process) ii) How to enable or locate prints of ZF_LOGE in kernel? I have enabled kernel prints and debug in make menuconfig. iii) I have followed the tutorial for IPC between a spawned process and root task. The setup is done as follows from the root task: /* create an endpoint */ vka_object_t ep_object = {0}; error = vka_alloc_endpoint(&vka, &ep_object); assert(error == 0); /* * make a badged endpoint in the new process's cspace. This copy * will be used to send an IPC to the original cap */ /* make a cspacepath for the new endpoint cap */ cspacepath_t ep_cap_path; seL4_CPtr new_ep_cap; vka_cspace_make_path(&vka, ep_object.cptr, &ep_cap_path); /* copy the endpont cap and add a badge to the new cap */ new_ep_cap = sel4utils_mint_cap_to_process(&new_process, ep_cap_path, seL4_AllRights, seL4_CapData_Badge_new(EP_BADGE)); assert(new_ep_cap != 0); However, I want to establish communication between two spawned processes. In that case I need to copy the badged endpoint capability of one process into another process. But in the spawned process I wouldn't have access to the pointer (sel4utils_process_t of new process), so how can i use mint_cap_to_process. Can someone help me with these. Thanks in advance. Regards Mark
On Sun, Oct 16, 2016 at 12:32 PM, Mark Reus <markreusva@gmail.com> wrote:
i) Can a process be spawned or configured only from the root task? (using sel4_configure_process)
This one I can answer, though I'm not too familiar with the sel4_libs. :-) Any thread can spawn another thread (or a process with separate address space) if it has the appropriate capabilities. All of the raw materials for a thread or process can be built directly from untyped objects... and that's all you need -- enough untypeds to slice and dice into a CSpace, maybe a VSpace, TCB, probably an Endpoint, etc. (I know the simple library has some stuff to make this easier, but hopefully the theory helps guide you!) Thanks, Jeff
Hi Mark, To answer your questions: i) Processes can be spawned and created from any task that has the caps to do so. ii) ZF_LOG* is only currently used at user level, it would be nice in the kernel. You can use printf in the kernel. iii) See below. Essentially you need to decide on a protocol for your cspace layout and communicate this to your launched processes. sel4bench provides a basic example of how to do this, where the benchmarking app comes with a library (libsel4benchsupport) that is shared between the initial task and the processes it launches. See [1] for the setup and [2] for the shared header. Sel4utils also has default locations for some of the capabilities it creates [3]. All of the benchmark apps then call the same function [4] to set up their own allocators. I hope this example helps! Please feel free to follow up with further q’s. Cheers, Anna. [1] https://github.com/seL4/sel4bench/blob/master/apps/sel4bench/src/main.c#L139 [2] https://github.com/seL4/sel4bench/blob/master/libsel4benchsupport/include/cs... [3] https://github.com/seL4/seL4_libs/blob/master/libsel4utils/include/sel4utils... [4] https://github.com/seL4/sel4bench/blob/master/libsel4benchsupport/src/suppor... From: Devel [mailto:devel-bounces@sel4.systems] On Behalf Of Mark Reus Sent: Sunday, 16 October 2016 12:32 PM To: devel@sel4.systems Subject: [seL4] General Questions Hi I have recently started with working on sel4 and I have a couple of questions. i) Can a process be spawned or configured only from the root task? (using sel4_configure_process) ii) How to enable or locate prints of ZF_LOGE in kernel? I have enabled kernel prints and debug in make menuconfig. iii) I have followed the tutorial for IPC between a spawned process and root task. The setup is done as follows from the root task: /* create an endpoint */ vka_object_t ep_object = {0}; error = vka_alloc_endpoint(&vka, &ep_object); assert(error == 0); /* * make a badged endpoint in the new process's cspace. This copy * will be used to send an IPC to the original cap */ /* make a cspacepath for the new endpoint cap */ cspacepath_t ep_cap_path; seL4_CPtr new_ep_cap; vka_cspace_make_path(&vka, ep_object.cptr, &ep_cap_path); /* copy the endpont cap and add a badge to the new cap */ new_ep_cap = sel4utils_mint_cap_to_process(&new_process, ep_cap_path, seL4_AllRights, seL4_CapData_Badge_new(EP_BADGE)); assert(new_ep_cap != 0); However, I want to establish communication between two spawned processes. In that case I need to copy the badged endpoint capability of one process into another process. But in the spawned process I wouldn't have access to the pointer (sel4utils_process_t of new process), so how can i use mint_cap_to_process. Can someone help me with these. Thanks in advance. Regards [Image removed by sender.]Mark
participants (3)
-
Anna.Lyons＠data61.csiro.au -
Jeff Waugh -
Mark Reus