This is an issue that I have thought about before, but haven't had a chance to fix properly. As you point out, the underlying issue is that Camkes threading model maps one camkes thread to one seL4 thread (obviously camkes threads are just seL4 threads) while the rumprun threading model is inherently unicore and the single core is mapped to a seL4 thread. Because of this, any blocking camkes connector involving a rumprun component is not going to work without locking the rumprun system as you point out. Supporting what you want to requires using non blocking connectors and implementing the blocking in the rumprun component similar to interrupt handling.

If you look at this rumprun kernel module: https://github.com/SEL4PROJ/rumprun/tree/master/platform/sel4/librumpsel4_stdio it has an example of blocking a rumprun thread implemented by using notification objects and shared memory to do synchronous calls to another seL4 component. (It's not in camkes however, just calling back to the root task). You may be able to use it for inspiration. The rumprun thread blocks on a rumpkernel synchronisation primitive after notifying the other seL4 process. The response from the other process is passed through via the same mechanism as hardware interrupts where the interrupt thread will wake up the rumprun thread from within the rumpkernel.

The other approach you mention of using multiple seL4 threads requires adding multicore support to rumprun unikernel which is likely going to be harder than implementing a new seL4 rump kernel platform layer that has multicore support designed in from the start.

We've been looking into adding better mixed-threading-model component support in Camkes as we have requirements to build CakeML components which are single threaded. Some of these new mechanisms could end up being used to better create rumprun Camkes connectors, but there are no concrete plans at this stage.

From: Devel <devel-bounces@sel4.systems> on behalf of Jason Wenger <jcwenger@rockwellcollins.com>
Sent: Thursday, September 20, 2018 1:00 AM
To: devel@sel4.systems
Subject: [seL4] seL4 and rump kernel synchronization primitives limitations

I think I've uncovered an interesting problem involving IPC between rump kernels and seL4, and I'm curious if anyone has any thoughts on mitigating it.

My use case is that I want a CAmkES component to be able to notify the rump component to send a network packet.

However, as far as I can see:

CAmkES connector, mutex, and semaphore threads that run in a rump component
• can wait on their seL4 synchronization primitives
• ... but they can't call rump function calls because they're not rump threads.

You can try to call, becuase you're running in the same address space as the rump kernel, but if you call a rumpkernel function, the CAmkES thread crashes when it reaches curlwp() becuase the calling thread is unknown to the NetBSD kernel. Therefore you can't call sendto() inside, for example, a notification callback or an seL4RPCCall handler, unless you can work out a way to signal to the NetBSD kernel that you're calling into the kernel from a foreign thread. Is this somehow possible through use of rump_schedule() and rump_unschedule()?

... and the other possible path I can see also has problems:

rumpkernel created userspace threads (pthreads)
• can wait on seL4 synchronization primitives
• ... but if they do wait, they also unschedule the entire rest of the rump kernel and userspace because every single rump thread (both kernel and user) all run in one seL4 thread.

Therefore you can't do

while(true) {

semaphore_wait();
sendto(...);

}

without unscheduling the entire rump component when you hit the wait(). For this to work, there would need to be a way to have multiple seL4 threads for rump kernel execution so that one could block while the others continue. That is done for interrupt and timer handling, but there's no way I can see to set it up from a rump userspace program.

The only other possible path appears to be busy-wait polling which is obviously very inefficient.

Any thoughts?

--Jason C. Wenger