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
[Image removed by sender.]Mark
_______________________________________________
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel

Reply via email to