Hi Michal,
There are currently two ways to run rump kernels on seL4:
- A single process, created and started by a small root task that gets passed caps to most resources in the system. This is what the blog post and thesis refers to. It currently only supports running one rumpkernel in the system. The rumprun-sel4-demoapps repository contains some examples (This is the repo referred to in the blogpost). - Using CAmkES, which allows multiple rumpkernel instances, each of which are in their own address space and can be connected through dataports and events. Examples of this exist in the camkes repository: rumprun_ethernet, rumprun_hello, rumprun_pthreads. To support multiple rump kernels the baseline devices they require access to is a serial output, and timer to program timeout interrupts. The rumprun_platform_layer provides these through a serial server and a timer server, and you can only have one, but it supports multiple rump kernel connections. I realise that it should probably have a different name because rumprun platform layer can also refer to the per rump kernel platform layer.
So to answer your questions:
1: In the CAmkES environment, other than sharing a timer server and serial server, the rump kernels are separated. As for threading, all the rump kernel threads run on a single seL4 thread. There is an additional seL4 thread that receives timer interrupts, and a third that receives other hardware interrupts and marks a rump kernel thread as runnable to process the interrupt.
2: You can only have one rumprun_platform_layer per application. I guess if you wanted to completely isolate some rump kernel instances you could set up equivalent timer and serial server instances that use different hardware. (The CAmkES component definitions and CPP macros that get expanded can be found in ./libs/rumprun/platform/sel4/camkes if you want to change them)
3: For a CAmkES rump kernel component, you write POSIX programs and the rump kernel provides your libc, pthreads, backing syscall implementation and drivers. This is similar to how normal CAmkES components function, only the muslc that they use doesn't have very many implemented syscalls or backing drivers to support them. This is to say, that a rust binary built with the x86_64 rumprun target should work in a CAmkES rump kernel component without any additional configuration. Where you can configure the rump kernels is to specify what NetBSD driver modules they get linked with. The way that Rumprun does this is to provide a few different preset named configurations. For seL4 these are "sel4_generic" and "sel4_ethernet", and can be selected in the CAmkES ADL on a per component basis. A new configuration can be specified by adding it to the libs/rumprun/app-tools/rumprun-bake.conf file and rebuilding. This is how the rumprun_ethernet app uses rump kernel ethernet and networking stack drivers. To run the rust app in the hello app, you should be able to do it by modifying the make rule here (https://github.com/seL4/camkes/blob/master/apps/rumprun_hello/components/hel...) to change to a rust cargo source directory, build the app, and then copy the resulting binary to the camkes build directory. Something like: cd $(RUST_SOURCE_DIR) && cargo build --target=x86_64-rumprun-netbsd && cp $(RUST_SOURCE_DIR)/target/x86_64-rumprun-netbsd/debug/$(rust appname) $(BUILD_DIR)/$@ The CAmkES generated build rules will then bake that image into the rump kernel configuration you specify and provide a final loadable image. As for how to use CAmkES dataports in your rust app, you would somehow have to convince rust to build with FFI functions that are weak symbols. I haven't tried to do this yet and don't know if it is possible or not. Exercise for the reader?
Hopefully this helps, thanks for your feedback.
Kind regards, Kent McLeod
From: Devel devel-bounces@sel4.systems on behalf of Michal Podhradsky mpodhradsky@galois.com Sent: Saturday, August 5, 2017 7:32 AM To: devel@sel4.systems Subject: [seL4] rumprum and camkes
Hello all, mostly Kent,
I read your blog post about rumpkernels on sel4: https://research.csiro.au/tsblog/using-rump-kernels-to-run-unmodified-netbsd...
and after experimenting with the rumprun apps (such as the ethernet one) I think it is a great addition to sel4.
So I have few questions. I need to run two different rumpkernels, each with its own address space, connected only through dataports/events.
1- does the current rumpkernel backend support having this separation? According to your thesis, all rumpkernel threads run in a single sel4 thread - is that correct?
2- Right now, I can combine multiple rumprun components in one application (lets say runmprun_hello and rumprun_pthreads). butI can have only one rumprYun_platform_layer per application, correct? An example below:
assembly { composition { component rumprun_platform_layer rrpl; component rumprun hello; RUMPRUN_META_CONNECTION(hello, rrpl)
component rumprun_pthreads pthreads; RUMPRUN_META_CONNECTION(pthreads, rrpl) }
configuration { hello.rump_config = {"cmdline": "hello World!" }; RUMPRUN_COMPONENT_CONFIGURATION(hello, 0)
pthreads.rump_config = {"cmdline": "./pthreads_test 4" }; RUMPRUN_COMPONENT_CONFIGURATION(pthreads, 1) } }
If I instantiate another rumprun_platform component, it wont compile.
3 - how can I go around defining/adding my own rumpkernels? Lets say I want to build a rumpkernel with rust support (you have an sel4 example here) and integrate it with the rumprun_hello app.
Regards Michal