Michael Hohmuth's Projects and Publications

Please find on this page:


(roughly sorted by date---newest first)

VFiasco (2001--present)

The VFiasco project aims at building a formally verified microkernel.

Fiasco real-time microkernel (1998--present)

I am the main developer of the Fiasco microkernel, an L4-compatible real-time kernel that forms the base of DROPS system. I developed a pragmatic nonblocking synchronization methodology for real-time systems and verified my techniques in the development of Fiasco. This is my main PhD thesis work, and it also resulted in a USENIX'01 publication.

DROPS (1997--present)

DROPS is the Dresden real-time operating system. The DROPS group explored and continues to explore resource reservation techniques for real-time systems, and I have participated in that work. We presented our work at the 1998 SIGOPS European Workshop. Together with Jochen Liedtke and Hermann Härtig, I explored the effect of second-level cache partitioning as a resource-reservation technique in real-time systems. This work resulted in an RTAS'97 publication. I also coauthored the following papers about L4RTL, a reimplementation of the RTLinux API on top of L4. In these papers, we evaluated the effect of the introduction of address spaces on predictability, and we compared it to the similar effects introduced by dirty caches and blocked interrupts. This work resulted in an RTSS'02 publication.

Within the DROPS project, I also wrote a number of reports on various aspects of development with L4 microkernels.

The work on L4Linux is also relevant in the context of DROPS. L4Linux is the time-sharing component of DROPS.

L4Linux (1996--present)

L4Linux, a port of the Linux kernel to the L4 microkernel, was the subject of my diploma thesis.

For this project, I documented part of Linux's internal interface between its architecture-dependent and architecture-independent parts.

Together with Jochen Liedtke, Hermann Härtig and other researchers, I compared the performance of modern microkernel-based system, such as L4 with L4Linux, with the performance of monolithic systems (original, monolithic Linux) and the performance of systems based on older, first-generation microkernels (Mach with MkLinux). We proved that microkernel-based systems do not have to have bad performance. This work resulted in a SOSP'97 publication.

Together with Hermann Härtig, I modified L4Linux to work as a well-behaved citizen in an L4-based real-time system. We published a paper about this at PART'98.

Mach emulation for the L3 microkernel (1996)

In a pre-diploma term paper, I explored porting a Unix single server for Mach, Lites, to the L3 microkernel. This work was done in an effort to provide a modern development environment on top of L3. We later abandoned this work in favor of L4Linux. For this project, I documented some of the virtual-memory-management primitives of L3:


Michael Hohmuth <hohmuth@sax.de>
Last modified: Mon Jan 10 17:44:07 2005