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
