Basic questions about ssel4utils processes and setting up IPC between them

New to seL4
1

I’m new to seL4 but am struggling with transferring caps from the root task to a process created with sel4utils_spawn_process_v. Initially the process(es) should get the endpoint of the root task and that is working well. Now, I would like to add the possibility for a process to request an IPC endpoint from the root-task, so I’d call the root-task which allocates a new endpoint and transfers it back by reply:

    // child
    seL4_SetCapReceivePath(CSPACE, RECV_CAP, CDEPTH);
    seL4_MessageInfo_t ret = seL4_Call(parent_ep, msg);
    seL4_Uint64 extra_caps = seL4_MessageInfo_get_extraCaps(ret);

but what should CSPACE be? There is no such thing as the boot-info, hm should I add more arguments to the process? Then the root task:

    // root
    vka_alloc_endpoint(&vka, &app_ep);

    cspacepath_t ep_cap_path;
    vka_cspace_make_path(&vka, app_ep.cptr, &ep_cap_path);

    seL4_CPtr new_ep_cap = sel4utils_mint_cap_to_process(pcb, ep_cap_path,
                                               seL4_AllRights, APP_BADGE);

    seL4_MessageInfo_t info = seL4_MessageInfo_new(0, 0, 1, 1);
    seL4_SetCap(0, new_ep_cap);
    seL4_SetMR(0, 0x2E2E2E2E);
    seL4_Reply(info);

(full code main.c and app.c which can both be used within the dynamic-3 build-context of the tutorials)

However on the client extra caps are not set. I tried many different ways, also with sel4utils_copy_cap_to_process. But I am not sure I understand most of it nor with how to proceed, also what are the pcb->thread.ipc_buffer?

Can someone help me with finding a working, clean solution for spawning process(es) that may ask for their IPC? And why is my code not transferring at least the caps?

Also: Once the child dies, I’d assume the root-task needs to do some cleanup (eg. that cspace path allocated). Is this managed by the process abstraction or (if not) what are the necessary steps?

I’m sorry for all those questions, there’s a lot of new parts and I cannot find many resources (or even code examples, the ipc tutorial or refos does not make use of the sel4utils processes - should I even use them?).

2

Edited: So still after passing app_pcb.cspace via argv, it was also not really working and would always print out extra caps of 0. I’m really at a loss here.

Now, I tried with sel4utils_copy_cap_to_process and passed the resulting cap in the child’s cspace via MR:

app

    // get parent_ep and cspace from argv
    parent_ep = (seL4_CPtr)atol(argv[0]);
    cnode = (seL4_CPtr)atol(argv[1]);

    // message just has a 0-label to init a synchronous ep
    seL4_MessageInfo_t msg = seL4_MessageInfo_new(0, 0, 0, 0);

    // call the root-task to request ep
    seL4_MessageInfo_t ret = seL4_Call(parent_ep, msg);

    // check extraCaps (for some reason always 0)
    seL4_Uint64 extra_caps = seL4_MessageInfo_get_extraCaps(ret);
    printf("app got reply: extraCaps=%d, r0=0x%x\n", extra_caps, seL4_GetMR(0));

    // if that worked, get the cap
    seL4_CPtr ep = seL4_GetMR(0);
    printf("ep got cap: 0x%x\n", ep);

    // .. and listen on it
    seL4_Word badge;
    msg = seL4_Recv(ep, &badge);
    printf("mesage from %d: 0x%x\n", badge, seL4_GetMR(0));

main

    // args, and spawn the process
    char string_args[2][WORD_STRING_SIZE];
    char *argv[2];
    sel4utils_create_word_args(string_args, argv, 2, ep, app_pcb.cspace);

    printf("starting %s\n", name);
    error = sel4utils_spawn_process_v(pcb, &vka, &vspace, 2, argv, 1);
    ZF_LOGF_IFERR(error, "failed to spawn process %s\n", name);

    // ...

    seL4_CPtr cap = sel4utils_copy_cap_to_process(pcb, &vka, app_ep.cptr);
    seL4_MessageInfo_t info = seL4_MessageInfo_new(0, 0, 0, 1);
    seL4_SetMR(0, cap);
    seL4_Reply(info);

Which prints message from 0: 0xdead, neat! Is this the correct approach though? Also what sort of book keeping do I need to do (eg. endpoint, path and copied cap)?

The working code: sel4utils process endpoints · GitHub (feedback appreciated!)

3

The sel4utils process abstractions are primarily used for supporting the sel4test and sel4bench applications or for other prototyping activities.

The capability tutorial tries to introduce the concept of CSpaces and copying caps between slots within CSpaces.

In order to receive a cap, the seL4_SetCapReceivePath needs to be given a CSlot address (Using direct CSpace addressing described here). When using the sel4utils process module to create a process, the CSpace has a defined initial layout that contains the CSpace for the process. The layout is defined here: https://github.com/seL4/seL4_libs/blob/master/libsel4utils/include/sel4utils/process.h#L62-L92

So in your first post, the seL4_SetCapReceivePath arguments would be something like:

  • CSPACE = SEL4UTILS_CNODE_SLOT,
  • RECV_CAP = SEL4UTILS_FIRST_FREE (A CPtr to an empty slot in the CNode of the receiving process)
  • CDEPTH = seL4_WordBits (The number of bits of address to resolve)

Then when you send the cap over IPC the kernel will copy the cap from the source slot (referred to by the arg to seL4_SetCap) to the destination slot (referred to by the arg to seL4_SetCapReceivePath) assuming that the access rights are all sufficient and the cap allows transfer.

In your other approach, the cap is transferred to the same destination slot, but uses the seL4_CNode_Copy() and is performed by the parent that still has access to both CSpace root capabilities.

Is this the correct approach though? Also what sort of book keeping do I need to do (eg. endpoint, path and copied cap)?

This depends on what your design goals are. The second approach is used when the child process isn’t expected to be able to modify it’s own CSpace (although the sel4utils process module doesn’t intend to restrict this), and so all CSpace operations are delegated to the higher-authority parent. In frameworks like CAmkES or the seL4 Core Platform, which are used for static designs, only the initial loader is able to modify CSpaces and once the system is initialized, the rights to CSpace modifications aren’t given to any of the running processes.

The first approach can be used when there are reasons to want to send and receive caps between threads that don’t have access to each other’s CSpace caps, eg a process and some anonymous memory resource server. If the server were to use the second approach, it would likely end up with CSpace caps to all of its clients which would also give it the authority to copy caps out of the client CSpace essentially giving it all of the access rights of all of its clients. Using the first approach instead here would allow it to have a reduced set of access rights while enabling dynamic transfer of capabilities throughout a system after initialization.

1 Like