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.
- Project website:
[WWW]
- VFiasco - Towards a Provably Correct
Microkernel. H. Tews, H. Härtig, M. Hohmuth (TU Dresden
technical report, 2001)
[PDF]
- Applying source-code verification to a microkernel - The
VFiasco project. M. Hohmuth, H. Tews, S. Stephens (TU
Dresden technical report, 2002)
[PDF]
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.
- Project website:
[WWW]
- Pragmatic nonblocking synchronization for real-time
systems. M. Hohmuth (Ph.D. thesis, 2002):
[PDF]
- Pragmatic nonblocking synchronization for real-time
systems. M. Hohmuth, H. Härtig (in the proceedings of
USENIX Annual Technical 2001, June 2001, Boston, MA, USA):
[PDF]
[WWW]
- Helping in a multiprocessor environment. M. Hohmuth,
M. Peter (in the proceedings of the
Second Workshop on Common Microkernel System Platforms, 2001):
[PDF]
- The Fiasco Kernel: Requirements Definition. M. Hohmuth
(TU Dresden technical report. This report includes most
of Jochen Liedtke's L4 Reference Manual, version 2.2.):
[PS]
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.
- Project website: [WWW]
- DROPS - OS Support for Distributed Multimedia
Applications. H. Härtig, R. Baumgartl, M. Borriss,
Cl.-J. Hamann, M. Hohmuth, F. Mehnert, L. Reuther,
S. Schönberg, J. Wolter (in the proceedings of the Eigth ACM
SIGOPS European Workshop, September 7-10, 1998, Sintra,
Portugal):
[PS]
- Dresden Realtime Operating System. R. Baumgartl,
M. Borriss, H. Härtig, Cl.-J. Hamann, M. Hohmuth, L. Reuther,
S. Schönberg, J. Wolter (in the proceedings of the Workshop of
System-Designed Automation (SDA'98), March 1998, Dresden,
Germany): [PS]
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.
- OS-Controlled Cache Predictability for Real-Time
Systems. J. Liedtke, H. Härtig, M. Hohmuth (in the proceedings
of the Third IEEE Real-time Technology and Applications Symposium
(RTAS'97), June 9-11, 1997 in Montreal, Canada):
[PS]
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.
- Cost and benefit of separate address spaces in real-time
operating systems. F. Mehnert, M. Hohmuth, H. Härtig (in
the proceedings of the 23rd IEEE International Real-Time
Systems Symposium, December 2002, Austin, TX, USA):
[PDF]
- RTLinux with Address Spaces. F. Mehnert, M. Hohmuth,
S. Schönberg, H. Härtig (in the proceedings of the 3rd Real-Time
Linux Workshop, November 2001, Milano, Italy):
[PDF]
Within the DROPS project, I also wrote a number of reports on various
aspects of development with L4 microkernels.
- Using the OSKit as a base for L4 applications. M. Hohmuth (in the
proceedings of the First Workshop on Common Microkernel System
Platforms, 1999): [PS]
- Omega0 -- a portable interface to interrupt hardware for L4
systems. J. Löser, M. Hohmuth (in the proceedings of the
First Workshop on Common Microkernel System Platforms, 1999):
[PS]
- DRAFT: Platform-independent L4 version 2 system-call
bindings. M. Hohmuth (appeared at the First Workshop on Common
Microkernel System Platforms, 1999):
[PS]
The work on L4Linux
is also relevant in the context of DROPS.
L4Linux is the time-sharing component of
DROPS.
L4Linux, a port of the Linux kernel to the
L4 microkernel, was the subject of my diploma thesis.
- Project website: [WWW]
- Diploma-thesis website:
[WWW]
- Linux-Emulation auf einem Mikrokern. M. Hohmuth (TU Dresden
technical report, diploma thesis, 1996):
[PS]
[WWW]
- Prinzessin auf der Erbse - Linux-Portierung auf den
Mikrokern L4. M. Hohmuth, J. Wolter (in iX 1/1997):
[WWW]
- Portierung von Linux auf den µ-Kern L4. M. Borriss,
M. Hohmuth, J. Wolter, H. Härtig (appeared at the
``Int. wiss. Kolloquium Ilmenau'', Sept. 1997):
[PS]
For this project, I documented part of Linux's internal interface
between its architecture-dependent and architecture-independent parts.
- Linux Architecture-Specific Kernel
Interfaces. M. Hohmuth (TU Dresden
technical report, 1996):
[PS]
[WWW]
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.
- The Performance of µ-Kernel-based Systems. H. Härtig, M.
Hohmuth, J. Liedtke, S. Schönberg, J. Wolter (in the
proceedings of the 16th ACM Symposium on Operating Systems
Principles (SOSP'97), October 5-8, 1997 in St. Malo, France):
[PS]
[WWW]
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.
- Taming Linux. H. Härtig, Michael Hohmuth (in the
proceedings of PART '98):
[PS]
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.
- Project website: [WWW]
- Steps Towards Porting a Unix
Single Server to the L3 Microkernel. M. Hohmuth, S. Rudolph
(TU Dresden technical report, ``Großer Beleg'', 1996)
[PS]
[WWW]
For this project, I documented some of the virtual-memory-management
primitives of L3:
- DRAFT: Preliminary L3 Documentation. Marion Schalm,
Jean Wolter, Michael Hohmuth, Martin Borriss [PS]
[WWW]
Michael Hohmuth <hohmuth@sax.de>
Last modified: Mon Jan 10 17:44:07 2005