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