Linked by Norman Feske on Wed 31st Aug 2016 22:35 UTC
OSNews, Generic OSes

With the just released version 16.08, Genode makes the entirety of the framework's drivers, protocol stacks, and libraries available on the seL4 kernel. Thereby, the vision of a real general-purpose OS built upon a formally verified kernel suddenly becomes a tangible mission. Further highlights of the new version are the use of the framework to run VirtualBox 4 on the Muen separation kernel, an experimental version of VirtualBox 5 on top of the NOVA kernel, the added support for virtual networking and TOR, profound Zynq board support, and new tools for statistical profiling.

The seL4 kernel is universally regarded as the world's most advanced open-source microkernel - not by technical merits alone but by the fact that the kernel is accompanied by formal proofs of its correctness. However, to achieve this high level of assurance, the kernel's responsibilities had to be reduced to an extreme that goes even beyond traditional microkernels. In particular, the kernel leaves the problem of managing kernel memory to be solved at the user level. The problem still exists but it isn't considered the kernel's problem anymore. Consequently, this kernel design makes the creation of a scalable user land extremely challenging. For this reason, most use cases of seL4 remain solely static in nature, or combine static components with virtualization. The real potential of seL4 to scale towards dynamic systems remained untapped so far. Here is where Genode comes into play. Genode is designed as a dynamic user land for microkernels, which addresses the management of memory at the user-level via a unique resource-trading concept. It turns out that this concept is a suitable answer to the kernel-management problem posed by seL4. By completing the implementation of the framework's base mechanisms for this kernel, literally hundreds of existing Genode components become readily available to the seL4 community.

The Muen separation kernel is another take on the use of formal methods for assuring the absence of bugs in an OS kernel. In contrast to seL4, Muen applies different technologies (Ada/SPARK) and addresses static partitioned systems. A natural use case is the co-hosting of virtual machines. In a multi-level scenario, each virtual machine hosts a guest OS for editing documents at one security level. The separation kernel enforces the information-flow policy between the virtual machines. In such scenarios, the predominant guest OS is MS Windows. Consequently, Muen had to support the virtualization of such commodity OSes. Genode already solved this problem for another microkernel by making VirtualBox available on top of NOVA. So the idea was born to leverage Genode's version of VirtualBox on top of Muen - essentially using Genode as a runtime environment for VirtualBox. As crazy as it sounds - it works! The release documentation has a dedicated section that tells the full story. Speaking of VirtualBox, the ability to run VirtualBox directly on a microkernel is certainly a key feature of Genode. With Genode 16.08, a first version of VirtualBox 5 becomes available on the NOVA kernel.

The anecdotes above highlight the benefits of Genode's cross-kernel portability. The new version pushes this idea even further by attaining binary compatibility across all the supported kernels for a given CPU architecture. In fact, compiled once, an ELF binary of a regular component can be natively executed on kernels as different as seL4 and Linux as long as the component does not rely on a special feature of a particular kernel.

At a higher level, the current release extends the framework's library of ready-to-use building blocks in several areas. Most prominently, there are new network-related components for routing traffic, using TOR, and for distributing Genode over the network. Other added components are concerned with improving the use of Genode as a general-purpose OS, or to aid the optimization of components by the means of statistical profiling. Version 16.08 is further complemented with added board support for devices based on Xilinx Zynq, including drivers for GPIO, video DMA, SD cards, and I2C.

These and many more topics are covered in detail by the release documentation of version 16.08.

Thread beginning with comment 633807
To view parent comment, click here.
To read all comments associated with this story, please click here.
RE: Double Wow!
by nfeske on Fri 2nd Sep 2016 09:55 UTC in reply to "Double Wow!"
nfeske
Member since:
2009-05-27

Thanks for the nice feedback! No plan to slow down... :-)

Reply Parent Score: 1

RE[2]: Double Wow!
by tidux on Fri 2nd Sep 2016 15:59 in reply to "RE: Double Wow!"
tidux Member since:
2011-08-13

16.08 looks like a fantastic release! There are a few things I'm interested in that didn't make the release notes.

1. I know you guys were looking in to Nix as a package manager earlier rather than needing to compile-time bundle everything into OS components. Was that pushed off until after the cross-kernel ABI/API stabilization or is it still in the works?

2. Will noux ever get true threads or libpthread? (Either is fine, I just want the ability to use threaded software.) A GNU userland with full or nearly so POSIX compatibility and a package manager would be a HUGE boost to the usability of Genode and provide a bunch of "ready to run" software. As sort of a subquestion of this, are there plans for header files and C libraries to offer a compile time compatibility layer for noux audio applications that would normally talk to ALSA, OSS, or sndio?

3. How's the complete "Turmvilla scenario" of Genode as a day to day OS coming along in personal testing?

Reply Parent Score: 2

RE[3]: Double Wow!
by nfeske on Fri 2nd Sep 2016 17:30 in reply to "RE[2]: Double Wow!"
nfeske Member since:
2009-05-27

I consider package management as one of most important topics right now. The cross-kernel binary compatibility was very much motivated by it. We are exploring various ways forward and Nix is a big influence. The intermediate state is not release-notes-worthy yet. So we kept our lips tight.

Noux will certainly further improve but pthread support is not a priority right now. For applications that do not rely on fork, Noux is not needed. Such applications can just use our libc and pthread libraries.

As sort of a subquestion of this, are there plans for header files and C libraries to offer a compile time compatibility layer for noux audio applications that would normally talk to ALSA, OSS, or sndio?


No concrete plans. It would be intriguing to apply Genode's VFS plugin concept for this purpose. Maybe you'd like to start experimenting in this direction? ;-)

3. How's the complete "Turmvilla scenario" of Genode as a day to day OS coming along in personal testing?


I'm using Turmvilla exclusively since about one year. My actual work environment is (still) a Linux VM running on top of Turmvilla. To cultivate the use of Genode-native applications, proper package management is somehow a precondition. Right now, installing/updating/modifying Turmvilla is too labor-intensive to recommend it to broader user base.

Reply Parent Score: 1