Hello sel4-devs, I came across the rumprun-sel4-demo apps [1] repo. There seems to be some bitrot as the kernel version keeps moving forward, But after moving the kernel back to 12.0 and some cmake fixes, I could get many apps(LevelDB, Redis, Memcached) to compile. Though "hello" ran fine, the few others I tried failed with various errors in the simulate step(such as page faults and invalid syscall number). I plan to debug these at some point, but I had a few questions about the setup before that.
1. Is this repo considered abandoned? 2. Is the rumpkernel+app running as a Virtual Machine or as a user process in this setup? Phrased differently, is seL4 acting like an OS or a Hypervisor? 3. Is there a known effort to run another libOS on seL4, such as Unikraft?
The current mental model I have for running real apps on seL4 is something like this diagram below:
3. App+LibOS(Redis + rump) ------------------------------------- 2. RootTask + other services* ------------------------------------- 1. sel4 ===================== 0. Hardware
Most of my contributions would be in layer-2, i.e. (rootTask + other services). I would then want to expose these new functionalities to the libc inside layer 3. The kernel itself should be mostly untouched.
Thanks, Sid [1] https://github.com/seL4/rumprun-sel4-demoapps