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