http://os.inf.tu-dresden.de/~hohmuth/dir/pub/

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]

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.
  • 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 (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.
  • 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 (1996--present)

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]

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.
  • 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 <[email protected]>
Last modified: Mon Jan 10 17:44:07 2005

Reply via email to