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