close
Showing posts with label microkernel. Show all posts
Showing posts with label microkernel. Show all posts

Saturday, June 24, 2017

[Update] seL4/RISC-V SMP support | seL4/RISC-V Tutorials Release

Updates (since 03062017)

 

A new unofficial 24062017 release of seL4, libraries and seL4 Tutorials.


  • SMP support, tested on Spike with 2 - 9 cores:
    • seL4 is using a big kernel lock.
    • Only reschedule IPI (set affinity) is provided.
    • Relying on SBI to do other remote operations.
    • SBI doesn't provide VADDR-> ASID -> HART operation.
    • Using tp register to hold per-core IPC buffer addresses.
  • Ported seL4-tutorias to RISC-V. This means:
    • People can learn more about both seL4/RISC-V doing the tutorials.
    • Lack of RISC-V/Spike user-level timer (or another S-timer) is an issue. seL4 (being a microkernel) is not supposed to provide a timer API, rather, user-level apps should have their own HW timer and device drivers.
  • More tests are passing on sel4test now after:
    • SMP support.
    • Re-adding a supervisor timer (for seL4 scheduling).
    • [154/154] Tests pass (8 more tests pass after multicore and timer support).
    • All libraries, kernel are rebased to latest seL4's revisions.

seL4 Tutorials 

 

sel4-tutorials [1] is the first recommended entry point for people who want to learn and get hands-on experience on seL4 and its libraries.  This repo [1] contains slides, docs and code tutorials with commented instructions and tasks that take you from writing a seL4 hello world application to doing IPC in a multithreading environment, now on RISC-V.

BERJAYA
hello-3 exercise showing 2 threads doing IPC communication

 [1] https://github.com/heshamelmatary/sel4-tutorials/tree/RISCVUnofficialRelease-24062017

seL4test

 

seL4test is a comprehensive unit and functional testing suite for seL4 and can be useful when porting to new platforms or adding new features.

It can be used as a reference how to develop a big project on seL4. A new riscv_smp_defconfig config file for RISC-V is added to test SMP support. Instructions how to run it are provided in this blog post.

For this release that contains SMP, use:

$repo init -u git@github.com:heshamelmatary/sel4riscv-manifest.git -m sel4test-24062017.xml

Note

 

This work is my personal/independent effort (during spare time) and it's not related to Data61/CSIRO/TS Group (that maintains seL4), until it gets upstream.

Friday, July 17, 2015

seL4 runs on Rocket Chip (RISCV/FPGA)


Abstract

After running on Spike simulator, seL4 can now run on the latest up-to-date version of Rocket Chip code on FPGA, the first hardware platform that seL4/RISC-V port can run on. Moreover, seL4 runs on the online jor1k emulator [1]. This can be considered as a starting point for both RISC-V and seL4 to experiment some new security-related and/or scalability solutions based on the flexibility to easily modify the hardware according to seL4 requirements (or vice versa), given that both are open-source, and under research development.

Details

Previously seL4/RISC-V was only running on RV32 (RISC-V 32-bit mode) which assumes SV32 (Page-Based 32-bit Virtual-Memory Systems) to work on. SV32 was only supported by Spike simulator, and that's why seL4 could, previously, only run there. The 32-bit seL4 has been progressing till the point that it is able to run, not only a hello world application, but it can run another simple operating system above it [2] that can fork other applications. That seems to be a good progress, but it would be better to have it running on a real hardware.

The issue was that the only open-source RISC-V hardware is currently Rocket Chip, which doesn't support 32-bit (SV32) mode, only RV64 (SV39 and SV48 virtual memory systems that run only on RISC-V 64-bit mode), and since there's no 64-bit support on seL4 (yet), it would have been hard and time-consuming to re-factor the entire seL4 code to run 64-bit code (including pointers, variables, data structures, scripts, etc).

How does 32-bit seL4 run on RV64/SV39?


The workaround was to keep running 32-bit seL4, but with modifications to the RISC-V low-level target-dependent MMU handling code to run on RV64/SV39 memory system without touching the target-independent seL4 code. This was possible because both RV32 and RV64 execute 32-bit fixed instructions. So basically, only the memory configuration was required (apart from HTIF code) to be modified to make this step possible, including initialization and page-tables layout. This means that seL4 is still being built and compiled using riscv32-* toolchain.

The seL4 components that had to be changed are:
  • vspace.c
  • elfloader
vspace.c is an architecture-dependent core file (for all seL4 ports) for MMU handling in seL4 microkernel. A new file, vspace64.c was added to run on RV64 mode. The difference between the 32-bit version is that the 4KiB pages should now follow 3 levels page-tables implementation instead of just 2 levels (SV32).

elfloader is just statically mapping the seL4 microkernel image at 2-level page-table, 2MiB pages granularity, while it maps seL4 at 4MiB granularity (just one level page-table) on SV32
 
RV32/SV32 implementation of seL4 can cover 4GiB address space, while RV64/SV39 extends this to 2^9 GiB. seL4 port only uses 256 MiB, so this amount of SV39 memory wasn't needed. This made it simpler by using only two entries in the first-level page-table: one for the first GiB (reserved for applications use), and the second one for the kernel page-tables. The first-level page-table (AKA page-directory) is then shared between all applications, but write accesses is only  exclusive to seL4 microkernel. New applications (address spaces) are just allocating/filling 2nd-level (and if necessary 3rd-level to provide 4KiB pages) page-tables without worrying about the first level. During context switches, address space change is done by writing the address of the second-level page table (allocated by applications) into the first entry of the page-directory rather than updating the sptbr register. This solution has a limitation of restricting application address space mapping to the first GiB virtual address range, but it has the benefit of optimizing both memory and time. Memory optimization is achieved by the fact that there is no need to allocate 3-level page-tables when creating a new task, only two (or even one) as with SV32. From timing perspective, seL4 is copying the kernel mapping for each created task, this is no longer needed since this kernel mapping lies on a separate 2nd entry, covering the 256 MiB of the second GiB virtual memory of the page directory. The SV39 mapping of seL4 is shown in the next figure.

BERJAYA
seL4 mapping on RV64/SV39



Next, I will be working on cleaning up the code, writing some tutorials how to build and run seL4 on different RISC-V platforms, fixing bugs and adding more features.

References

Monday, June 8, 2015

seL4 on RISC-V is running SOS (Simple Operating System)

BERJAYA
SOS running on seL4 on RISC-V

Abstract 


Following the first status update of my project (Porting seL4 to RISC-V), this post reveals more updates, most notably, the port is now mature enough to run SOS (Simple Operating System) which is recommended by the seL4 getting started guide [1] [2] to learn about seL4 programming. Given that SOS is used part of an advanced operating system course offered by UNSW and currently only runs on Sabre Lite ARM-based board, seL4 on RISC-V can be considered the second supported platform for SOS, and the first all-open-source seL4 system, providing that seL4 (and its components), RISC-V ISA, Spike simulator (and hopefully soon Rocket-Chip/lowRISC on FPGA) are all open-source.

Details 


Running SOS on seL4/RISC-V platform proves that the port is continually making a steady progress, and asserting that most of seL4/RISC-V API and internals are known to work fine. As mentioned before, a seL4 microkernel port itself wouldn't be interesting without some use cases. So, rather than unit testing each seL4 function itself, I preferred to port an existing (and interesting) use-case like SOS, that's entirely dependent on the seL4 API, and heavily utilizes many of its features. This gives me a better understanding of how a real-world seL4-based application would need/act, and how the seL4 microkernel implementation should react, debugging from the very highest level of a seL4 system (applications running on SOS which in turn runs on seL4) down to the very lowest-level of RISC-V hardware implementation. So what's SOS, and what was needed to run it on the seL4/RISC-V port?

What's SOS


"simple operating system (SOS) is a server running on top of the seL4 microkernel. The SOS server is expected to provide a specified system call interface to its clients (Specified in libs/libsos/include/sos.h)." [2] The SOS framework is described in the following figure.

BERJAYA
SOS framework


The components shown in the picture above are:
  • Harware: The hardware described in our case is the RISC-V platform. Currently only the Spike simulator is supported.
  • seL4 microkernel: this is the seL4 RISC-V port of the kernel (and the third port after IA-32 and ARM). It provides the functionalities needed to run our SOS project in the sort of memory management, scheduling, IPC, etc.
  • SOS: a stub operating system running on top of seL4 microkernel. It's intended to be developed and enhanced by students and/or people who are interested to learn about seL4. SOS initializes a synchronous endpoint capability for its clients/applications to use for communication. Interrupts are delivered using an asynchronous endpoint (seL4 has two types of endpoint capability: synchronous and asynchronous).
  • tty_test: it serves as a simple application running on top of SOS that simply prints out a hello word message. 
The application level would need to issue system calls to SOS using the seL4 endpoint capabilities. An example of such a system call is tty_test application requesting (from SOS) some data to be printed out. SOS on the other hand monitors the system call requests from its clients (using seL4_Wait system call), serves it, and sends replies. Refer to [3] to get more details about the SOS framework.

What's needed to support running SOS


Other than the seL4 microkernel internals, almost all of the current seL4 user-level libraries had to be supported to build SOS and its applications, the following picture is captured from the high-level Kconfig file of the project.

BERJAYA
Project Kconfig file

To be able to build/run SOS, the following components are involved:
  • seL4 microkernel, it now supports memory management capabilities, context switch, traps from user applications, and a lot (than what has been discussed here) more architecture-dependent functions were implemented.  
  • libseL4: This is the user-level library for applications to deal with seL4 microkernel via system calls. It defines the format of the system calls, kernel objects definitions, user-level context and it exposes them all to the user.
  • libmuslc: The C library that seL4 and its libraries depend on. It has been ported to RISC-V part of this project, and now it's working pretty fine as expected.
  • libsel4muslcsys: A minimal muslc implementation for the root task to bootstrap, it provides stdio related system call handlers and it's part of the bootstrap procedure of the root task, defining the system call table and entry point for muslc-based applications.
  • libplatsupport: Some platform related functions (BSP) for seL4 supported platforms. For example serial driver initialization and console driver functions for a given board are provided there. libsel4platsupport depends on it. I had to add Spike platform with very basic implementation just to get over build dependencies.
  • libsel4platsupport: For RISC-V it has to be ported to provide the bootstraping and the exe entry point __sel4_start for the root task. It gets the boot frame address from the seL4 microkernel, constructs the stack vector as muslc expects, and then jumps to the normal muslc _start entry, enabling it to populate the libc environment's data-structures with its details, initializes TLS, files and stdio handlers, etc. Finally the muslc task bootstrap procedure jumps to the user's main() function, or the root task, which in our use case is SOS.
  • libcpio: used by SOS to parse the cpio archive, searching for user binaries.
  • libelf: This one is used by SOS to parse the ELF binaries extracted from the cpio archive. Hence SOS can read the ELF's section headers, and do the loading/mapping consequently.
  • libsel4cpace: a library provided to abstract away the details of seL4 CSpace management, this library had to also be ported for RISC-V. It's used by SOS to construct tasks' CSpace.
  • mapping: SOS comes with mapping.c file that's needed in conjunction with elf.c to load/map the user ELF binaries. It's ported to RISC-V and it invokes  the newly provided RISC-V system calls like seL4_RISCV_Page_Map and seL4_RISCV_PageTable_Map
Other libraries had to be modified to be aware of the new RISC-V architecture (CONFIG_ARCH_RISCV) and just modified to be built, again to get over other required libraries dependency.

BERJAYA
seL4/SOS bootstrap procedure

What's next 

Next I'll be working on 64-bit support, IRQ handling, seL4test project, and see how we can take the port to the FPGA-level. The project repos are listed below [4] [5].

References


[1] Getting Started with seL4
[2] Advanced Operating Systems Course | Project: A Simple Operating System
[3] SOS framework
[4] [Github] seL4 RISC-V por
[5] [Github] seL4 project containing SOS

Sunday, May 24, 2015

Porting seL4 to RISC-V | Status Report No.1

Introduction 


This year I am participating in GSoC with a new umbrella organization called lowRISC aiming to produce a completely open-source SoC (System-on-Chip). lowRISC is based on the new open RISC-V ISA, designed by UC Berkeley. I'll be performing a complete RISC-V port of the new formally-verified microkernel seL4.

Details

 The project basically involves working with seL4 and RISC-V. The next section will introduce some related details about each.

RISC-V

RISC-V is an open ISA, which is designed to help with computer architecture education and research. It supports both 32-bit and 64-bit modes and is powerful enough to run Linux. UC Berkeley team has implemented this ISA (64-bit RISC-V Rocket core) and showed off some interesting comparison between it and ARM Cortex-A5. 

BERJAYA
64-bit RISC-V Rocket Chip and ARM Cortex-A5 comparison [1]

QEMU and Spike are the main simulators that enable running/debugging RISC-V software. 

Recently, a new draft of the RISC-V privileged ISA specification has been released [2], which describes rich and nice features. Notably, the draft introduces new four modes that RISC-V can run at (before that, there were only supervisor and user modes). The four modes are user, supervisor, hypervisor (however it's not implemented yet) and machine mode. This new design takes the RISC-V architecture to a new level where virtualization can be supported and easily researched.

seL4

seL4 is a new open-source L4 microkernel developed by NICTA and now owned by General Dynamics C4 Systems. It gained its popularity being "The world's first operating-system kernel with an end-to-end proof of implementation correctness and security enforcement is now open source." seL4 developers believe that it's the state-of-art microkernel currently. The following figure shows the history of microkernels in general and their implementations.

BERJAYA
L4 microkernels history [3]


L4 simplicity concept has been greatly achieved in seL4 given that it has about 10K lines on C code, compared to Fiasco.OC which has 36K lines of C/C++ code.

Currently seL4 is ported to only two architectures: ARM and IA-32. Only the ARM port is formally verified, and both support only 32-bit implementation, however the 64-bit implementation is still a work in progress. The IA-32 port supports booting in multi-kernel mode unlike the ARM port.

seL4 microkernel itself wouldn't be of much interest without user-land applications and libraries. There are many libraries and projects that build on seL4 microkernel:
  • verification, the seL4 proofs.
  • seL4test, a test suite for seL4, including a Library OS layer.
  • CAmkES, a component architecture for embedded systems based on seL4. See the CAmkES pages for more documentation about CAmkES.
  • VMM a componentised virtual machine monitor for ia32 platforms using Intel VT-X and VT-D extensions.
  • RefOS, a reference example of how one might build a multi-server operating system on top of seL4. It was built as a student project.

seL4 on RISC-V

Porting seL4 to RISC-V needs a knowledge of both seL4 microkernel and RISC-V design/implementation. The project aims to perform a complete port of seL4 microkernel that enables some of the previously mentioned projects to run on it, mainly, the seL4test project that has over 120 tests asserting the seL4 microkernel API, features and behaviour. There have been some implementation trade-offs regarding the project, described below.

32-bit or 64-bit?

Both! As already mentioned, seL4 only supports 32-bit currently, on the other hand, RISC-V has been focusing on 64-bit implementations right from the start with a little support for 32-bit; UC Berkeley team has only 64-bit Rocket chip and there is no 32-bit hardware implementation so far (except for some simple educational repos). Luckily, Spike has recently supported 32-bit mode (with a new --isa flag). It will be easier to port seL4 for 32-bit architecture trying to follow/imitate ARM/IA-32 ports. 64-bit implementation would be more challenging as most of the seL4 data structures and scripts assume 32-bit environment. As there's no 32-bit hardware implementation of RISC-V yet, the port wouldn't have the chance to run on real hardware. Hence, we decided to start with 32-bit porting, make it run on Spike first, and from there we can evolve to 64-bit that can run on Spike, or Rocket Chip--hopefully both!

Rocket Chip vs. Spike and/or QEMU

Again, this is closely related to the previous trade-off of 32/64 bit implementations. So if we ended up with a 64-bit seL4 working on Spike, this can easily run on the 64-bit Rocket Chip. Rocket Chip and Spike are up-to-date with the latest ISA privileged specification, however QEMU isn't. Consequently, we chose to work with Spike as the main simulator. Spike is also more similar to the hardware implementation in that it's simulating the HTIF interface and can communicate with the shared library riscv-fesvr (front-end server) like the Rocket Chip.
 

Working in which mode?

The latest privileged specification introduces 4 modes that RISC-V software can run in. Conceptually, seL4 might run in any of the three privileged modes separately, or even two or three of them simultaneously. The next figure shows the possible seL4, guest OSes and applications configurations regarding to which modes they can run at.

BERJAYA
seL4 in which RISC-V mode trade-off

   
The number of which modes to run seL4 microkernel in was narrowed down to two by the fact that there is no hypervisor implementation yet. These two modes are: machine (M-mode), and supervisor (S-mode) modes. The M-mode supports physical access control and Base-and-Bounds checking, i.e, no mapping or address translation (SV32, SV39 and SV48), only S-mode does. seL4 microkernel on the other hand expects that it would run in an address-translation-based mode, and would map its kernel image, IPC buffers, bootframe and other areas of memory during bootstrap. So we followed the current seL4 ports for now to work in S-Mode.

Loading the image(s) and mapping pages

The bare seL4 system basically consists of: 1) the kernel image, 2) applications. Current ARM and IA-32 seL4 ports differ in the way they load the kernel image and applications. Since IA-32 port can boot in multi-kernel mode, it loads the images in way similar to grub. So the kernel is the first part that takes control of the physical resources, and it loads/maps the application images itself. The ARM port behaves differently in that it archives the kernel and application images in cpio format. There's a separate elfloader tool that reads the ELF images from the cpio archive, loads it to the available physically-adjacent memory, sets up the VM environment and finally maps the ELF images according to their ELF's section VMAs. Hence, the elfloader is the first to take control of the physical resources, and then it passes control to the kernel (which works in a VM environment right from the start) with some information passed to it about the loading addresses of the kernel image itself and the user image(s). The final image for the seL4/ARM system then contains: 1) elfloader tool, 2) libelf, 3) libcpio, 4) kernel image and 5) user applications. We followed the ARM port as it's more hardware agnostic, and as a start the RISC-V wouldn't need to support multi-kernel mode.

What has been done so far

So far, the basic microkernel port can bootstrap and jump to the user image on Spike in 32-bit mode working only in S-mode. 

BERJAYA
seL4 microkernel running on Spike


To be able to achieve this, I had to work on the following seL4 components.
  • libmuslc: libelf depends on libmuslc. I performed a very basic port of musl c library to RISC-V architecture, enough to build it successfully and produce the .a library.
  • libelf: This one is portable and architecture-independent. It has to be included part of the elf loading process. 
  • libcpio: like libelf, libcpio is also architecture-independent and is used to read the cpio archive containing the kernel image and user images.
  • elfloader: This tool is developed by seL4 team for the ARM port, I had to port it to RISC-V. It has to work in M-mode and it's acting as riscv-pk, that is, any system calls from seL4 microkernel are redirected to elfloader code, which handles it and returns (apart from its main purpose which is loading the kernel/user images). elfloader currently only supports write and exit system calls (to be able to get some printf output and exit the spike simulator).
  • seL4 microkernel: The project is mainly about the seL4 microkernel. The port basically followed ARM port and even a lot of code is copied from it. seL4 microkernel runs in S-mode right from the start as mentioned previously. Some architecture-level capability data structures had to be modified according to the RISC-V ISA, and the low-level RISC-V VM handling code is now implemented to map the kernel image, kernel frames, initial task and user images properly. 
  • Build system: The build system for seL4 projects is the Linux Kconfig/Kbuild build system. The existing Kconfig/Kbuild files had to be modified to allocate a new entry for RISC-V architecture with a new Spike platform (that runs on Spike simulator). New riscv_defconfig, project-riscv.mk, makefiles and other files were added to enable building a complete seL4/RISC-V system (elfloader, libcpio, libelf, seL4 mircokernel, user image) like in seL4tests project and other seL4 projects.

Next, I'll be working on the seL4 system calls API, timer and IRQ support and 64-bit mode. You can follow my blog to get more updates about the project as well as my github repo(s) [4] [5] [6].

References


[3] Elphinstone, Kevin, and Gernot Heiser. "From L3 to seL4 what have we learnt in 20 years of L4 microkernels?." Proceedings of the Twenty-Fourth ACM Symposium on Operating Systems Principles. ACM, 2013.

Thursday, February 19, 2015

Thoughts on Supporting Rump Kernels on RTEMS

Introduction 

So, once I had heard about Rump kernels [1] from Gedare Bloom (one of RTEMS maintainers), I started to do some research about it, and whether RTEMS can have a support for such a new architecture. Rump kernel is a way to run unmodified NetBSD kernel drivers virtually anywhere. So, for a platform that can support Rump kernelsa developer can just pick up some NetBSD drivers (that have been tested and proven to work properly), compile and link it without any modifications to the source code or the host kernel itself. Moreover, these drivers can be even upgraded from NetBSD upstream without any significant effort. So, what's exactly Rump kernel, Anykernel and a so-called platform?

Rump kernel is not a fully-featured OS neither a complete virtual machine like KVM or VirtualBox. It's a minimal thin implementation that enables the host platform (see the platform section) to emulate the system calls layer that NetBSD drivers expect/call. Rump kernel is hardware-agnostic, meaning that it does not depend on specific hardware features like virtualization and cache-coherence. For example, kernel drivers need some way of allocating memory (using rumpuser_malloc), it doesn't really matter whether this is a virtual/logical memory (allocated address space using page-table), or fixed physical addresses; it depends on the platform, what concerns Rump kernels is to freely allocate, use and free this area of memory. That's, Rump kernels try to make use of the underlying software platform features as possible as could be in parallel with giving the illusion (and of course working work-arounds) to the drivers that they get what they need! At this point you may be wondering about the structure of Rump kernels and how it depends/relates to the platform. The following figure [2] may make it clearer. Please note that libc and the layers above it are optional.

BERJAYA
Figure 1: Rump Kernel Environment

As you can see, the Rump kernel support is stacked. At the top of the stack comes the application that can be POSIX-compliant. In the next section some of these stack components are illustrated and how RTEMS (as an example platform) can and Rump kernels work together.

Platform


So what's the platform? Basically, the platform can be anything like a raw hardware, Virtual Machines or an OS like Linux. Actually, there are currently some implementations for such platforms. So, Rump kernels can run on some POSIX userspace like "Linux, Android, NetBSD, FreeBSD, OpenBSD, Dragonfly BSD, Solaris (+ derivates) and Windows (via Cygwin)" [3]. There are some implementations that run on bare-metal machines like KVM,VirtualBox or hypervisors like Xen. Genode OS has been modified to support Rump kernel [4] and similarly Minix. So, can RTEMS be the next platform? The simple answer is yes!

RTEMS is an POSIX-compliant RTOS, so with a small effort, Rump Kernel can run above this RTEMS/POSIX environment. However, it would make more sense from performance, control and code density perspectives to discard this POSIX dependency and write the whole hypercall layer (see figure 1). Userspace POSIX platforms here [5] have another POSIX library (userpsace libraries on the previous figure) as well as the host POSIX library. As the authors of Rump Kernels say, it's enough for a platform to just implement the hypercall layer to support the whole Rump kernel stack. So, theoretically, if RTEMS implemented this very thin ~1000-lines-of-code hypercall layer, all other NetBSD code can be imported, providing NetBSD drivers, libc, and even unmodified POSIX library.


The hypercall (AKA rumpuser) layer [7] is divided into basic and IO operations. The complete interface can be found here [6]. Almost all of the functions mentioned in that link can be implemented by using/wrapping existing RTEMS features. Some of the interfaces are mentioned below.

Memory Allocation

int rumpuser_malloc(size_t len, int alignment, void **memp
void rumpuser_free(void *mem, size_t len)
These functions can easily be mapped to RTEMS libcsupport implementation of (malloc/free). Other memory managers like Partition and Region managers can also be used.

Files and IO

int rumpuser_open(const char *name, int mode, int *fdp)
int rumpuser_close(int fd)
int rumpuser_getfileinfo(const char *name, uint64_t *size, int *type)
void rumpuser_bio(int fd, int op, void *data, size_t dlen, int64_t off,
     rump_biodone_fn biodone, void *donearg)
int rumpuser_iovread(int fd, struct rumpuser_iovec *ruiov, size_t iovlen,
     int64_t off, size_t *retv)
int rumpuser_iovwrite(int fd, struct rumpuser_iovec *ruiov,
     size_t iovlen, int64_t off, size_t *retv
int rumpuser_syncfd(int fd, int flags, uint64_t start, uint64_t len) 
The previous IO functions can be implemented by wrapping IMFS and some stubs, most embedded system applications do not need a complete featured file system, but if it's needed, the option of wrapping the correct RTEMS filesystem is still there. How to configure and enable Rump kernel features is an implementation tradoff, but currently rump-posix is doing it by starting a Rump kernel server with a command line flag of which features are needed from the Rump Kernel. For example this command line does such a job (loading a filesystem driver when starting the server)
rumpremote (unix:///tmp/rumpctrlsock)$ ./rumpdyn/bin/rump_server -lrumpvfs unix:///tmp/rumpctrlsock

Clocks

"The hypervisor should support two clocks, one for wall time and one for monotonically increasing time, the latter of which may be based on some arbitrary time (e.g. system boot time). If this is not possible, the hypervisor must make a reasonable effort to retain semantics." [6]
All of the required clock services are provided by RTEMS such as _Watchdog_Ticks_since_boot. RTEMS provides enough time management libraries like Watchdog, Time, Clock manager, Timer benchmark (which may or may not depend on the Clock manager) and CPU Counter (deprecated?). Hence, there are more than enough implementation to support Clocks interface part of the hypercall.

Console output 

"Console output is divided into two routines: a per-character one and printf-like one. The former is used e.g. by the rump kernel's internal printf routine. The latter can be used for direct debug prints e.g. very early on in the rump kernel's bootstrap or when using the in-kernel rou- tine causes too much skew in the debug print results (the hypercall runs outside of the rump kernel and therefore does not cause any locking or scheduling events inside the rump kernel)." [6]
 Both are there!


Threads

int rumpuser_thread_create(void *(*fun)(void *), void *arg,
const char *thrname, int mustjoin, int priority, int cpuidx,
void **cookie)
void rumpuser_thread_exit(void)
int rumpuser_thread_join(void *cookie)
void rumpuser_curlwpop(int enum_rumplwpop, struct lwp *l)

Mainly, all thread management is directly mapped to the host threading implementation. So, when Rump kernel driver creates a thread, the host will actually create this thread and schedule it according to its policy. It does not matter how the host implements threading. For RTEMS, all of these functions can be easily mapped to corresponding ones, no big deal.

Synchronization and Mutexes

Normal mutex operations are provided by RTEMS. There is also a need for Read/Write locks and conditional variables. 

What then?

If we had this hypercall layer on RTEMS, there's no other effort needed. The other BIG NetBSD code can be linked AS IS! At this stage we can try out some NetBSD drivers. We can have some fun by making use of Rump Kernel Remote/Client mode which separates the kernel from the clients (applications). So, for example we can have a bare-metal client connecting to Rump Kernels on RTEMS or vice versa communicating using IPC and TCP/IP. This platform can be setup using some simulators or real hardware. 

One other interesting way is using Rump Kernels to tackle the scalability issues that RTEMS currently faces, providing another solution other than the complex fine-grained locking. We can have cores with attached IO devices that can have Rump kernels on it, and act as servers for other clients (on other cores), communicating together (using inter-processor interrupts, message passing, shared-memory communication or whatever). 

References


[1] http://rumpkernel.org/
[2] Rump Kernels No OS? No Problem!
[3] Rump Kernels Platforms
[4] Genode OS and Rump Kernels.
[5] Userspace (POSIX) Rump kernel.
[6] rumpuser - NetBSD Manual Pages
[7] https://github.com/rumpkernel/buildrump.sh/issues/59