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/cspace.h

[3] https://github.com/seL4/seL4_libs/blob/master/libsel4utils/include/sel4utils/process.h#L54

[4] https://github.com/seL4/sel4bench/blob/master/libsel4benchsupport/src/support.c#L265

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

Mark