Hi Karl, Please see my answers inline. If you have further questions or need more detail than I have provided, don't hesitate to ask. I live and breathe this stuff so my explanations may be more succinct than is required for understanding. Cheers, Anna. On 2/12/2015 3:30 am, Karl Apsite wrote:

Ahoy there!

I'm working on a Zynq 7000 - ZC702 dev board. I've setup a capability associated with the GPIO buffer, and have successfully ran a small test in the root process that could read a button's state via GPIO. The next step is to send the capability to a second process so that it can read the button's state. I'm having some trouble understanding how I should go about using the IPC calls to achieve this transfer.

I'll try to give a summary of my efforts, to clear up where I am, and what I've done so far. To start:

I borrowed (heavily) from the 4th tutorial that established two separate processes Main: https://github.com/seL4-projects/sel4-tutorials/blob/master/solutions/hello-... App:

I felt inclined to inform the second process about the whereabouts of the new endpoint as opposed to making an assumption as to where it was allocated. I crammed the address into the argc/argv constructs as the process starts, and it seems to be able to continue just fine.

1. Is that an OK thing to do? I understand that I shouldn't be too willing to share vital information freely between both processes, and I'm not sure if abusing argc/argv to inform the second process is appropriate here.

Yes.

I left the main thread in seL4_Wait(). My idea is: other processes are expected to send a message representing a command that main can respond to. Main can check the message, badge(s), and privileges as necessary, and respond with the capability if it so desires. With the capability in hand, and a tag with extracaps set to one, I was NOT able to successfully send the cap. The second process would only receive a tag with extra caps set to zero, so it must be failing somewhere along the way.

I loaded the cap into the first slot using seL4_SetCap(0, my_cap) and the cap was functioning previously, so I doubt it's erroring when I send. I expect an error on the receiving end somewhere.

I have NOT been able to prepare a path for a capability in the second process, and notify seL4 of the location using seL4_GetCapReceivePath(root_node, new_cap, 32).

2. How should the second process obtain a reference to its root cnode?

libsel4utils by default puts the root cnode in slot 2, and the endpoint in slot 1. See sel4utils_cspace_layout: https://github.com/seL4/seL4_libs/blob/master/libsel4utils/include/sel4utils... I agree it is nasty to assume a process "knows" automatically where capabilities are - you can also transmit the slots in argv/argc as you are. Or you can make your app depend on libsel4utils and get the constants from there, or you can define your own protocol elsewhere. A key distinction is who is managing the processes cspace? You can use your initial thread to fully manage the cspace, or allow the process to manage it's own cspace. Without a reference to its root cnode, a process cannot successfully receive caps over IPC.

3. How should the second process allocate a new cnode?

You can allocate the cnode in your main process and use sel4utils_copy_cap_to_process: https://github.com/seL4/seL4_libs/blob/master/libsel4utils/include/sel4utils... Or you copy an untyped capability to the second process and let it create it's own allocator. You can see an example of this in sel4test: https://github.com/seL4/sel4test/blob/master/apps/sel4test-tests/src/main.c#...

I think the new_process_t structure in the main process has the addresses I'm after (to obtain the root cnode at least, and maybe allow me to a new cnode?), but I don't understand the implications of informing the second process about the information in the new_process_t structure.

4. Is the new process expected to know all of that information? 5. Is there an API to establish this sort of information (along with the IPC endpoint that I had to cram into argc/argv earlier?)

Not really. There are a few options: * send the initial slots (endpoint, cspace_root, cspace size) to the process in argv/argc and transmit the rest of the information over IPC using your own protocol. This is how sel4test does it, but it is a very slow way of doing it, but a good way to get your head around IPC. * send the info via shared memory, and tell the process in argv/argc where to look for it. https://github.com/seL4/seL4_libs/blob/master/libsel4vspace/include/vspace/v... can set this up.

_______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel

________________________________ The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.