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