Home | Mentored Students

ETH Zurich

Multiple Address Spaces in a Distributed Capability System

Nora Hossle. Master's Thesis. ETH Zurich. September 2019. [ .pdf ]

Once upon a time each computing system had a single physical address space comprised of an ordered set of physical addresses. These addresses were unique over the whole system and every component of the system (core, MMU et cetera) agreed upon their meaning. This old and much loved model of computing systems is not only outdated and grossly oversimplifies current systems, indeed it may never have been appropriate at all. It is widely agreed upon that today’s systems are much more heterogeneous and complex than they used to be. System programmers are dealing with whole networks of cores, different memory blocks, interconnects and a diverse set of other devices. It is entirely possible that resources are rendered at different physical addresses for different cores. The purpose of this master thesis is to update the old model by introducing a network of address spaces with potentially more than one physical address space. It also aims to bring multiple address space support to the Barrelfish capability system. This is to be done by formally modelling the access rights of the different agents with respect to memory management. The new model gives rise to a Haskell model in the spirit of seL4’s executable specification.

Using NetBSD Kernel Components on Barrelfish Through Rump Kernels

Leo Horne. Bachelor's Thesis. ETH Zurich. August 2019. [ .pdf ]

A major task in the implementation of new operating systems is writing code for filesystems, the network stack, and various device drivers, which allow the operating system to run on a large range of hardware. Using the NetBSD rump kernel, a tool that allows running parts of the NetBSD kernel in userspace, we show how to reuse code from the NetBSD operating system in Barrelfish with the goal of avoiding having to manually port a large amount of code from other operating systems. We implement a basic hypervisor for the rump kernel which enables using OS components such as filesystems, the network stack, and PCI device drivers. We additionally show how to integrate portions of the NetBSD kernel into the Barrelfish ecosystem by wrapping them inside Barrelfish applications and using RPCs to communicate with them. Finally, we evaluate the performance of our implementation and show that overheads are typically kept within reasonable limits.

Formally modelling hardware standards

Giuseppe Arcuti. Bachelor's Thesis. ETH Zurich. August 2019. [ .pdf ]

When systems developers want to port an operating system to a new platform, they need a description of that platform. Those descriptions are usually written in prose. The problem is that the English language is not precise enough, thus leaving room for interpretation. In this thesis I analyze why current specifications are too vague and easily misinterpreted, with the examples being ARM’s TrustZone, ARM’s Server Base System Architecture and Cavium’s ThunderX CN88XX. I report the problems I found in these specifications. To remedy this situation I formalize TrustZone’s memory subsystem in Sockeye, a DSL to describe address decoding nets, write a Prolog query to check whether an address decoding net is TrustZone-compliant and model the SBSA’s memory subsystem in Isabelle as a predicate over address decoding nets. As an example of a concrete system I express ThunderX’ memory subsystem as an address decoding net in Isabelle. I make suggestions on how to improve the address decoding net model and Sockeye based on the experience in this thesis.

System Modeling Co-Design

Sven Knobloch. Bachelor's Thesis. ETH Zurich. September 2018. [ .pdf ]

In recent years, hardware systems and systems on a chip (SoCs) have become increasingly diverse. In order to build software for such a large variety of systems, better ways have to be found to target and test software for these platforms. One such solution is hardware simulation, which allows for quick, efficient and inexpensive experimentation of software with a large variety of systems. In addition, simulation allows software developers to better integrate their software with specific hardware platforms to increase performance, efficiency and overall interoperability. The Barrelfish group as operating system developers are extremely interested in increasing performance and compatibility with a large variety of systems. They have developed a domain specific specification language, Sockeye, to describe system models as a hardware decoding net to query for addresses and interrupt information at runtime. This project evaluates the viability of Sockeye as a language to generate system models from and successfully demonstrates how to generate valid hardware simulators from these models using ARM’s Fast Models framework and their modeling language LISA+[11]. ARM has also published their Server Base System Architecture[4], which defines a common standard for ARMv8 platforms. This project also analyzes and evaluates the Server Base System Architecture and determines its compatibility with the Barrelfish ecosystem, specifically how well it integrates with Sockeye for system modeling. The Server Base System Architecture is found to be a good starting point for a standard but is too loose in its restrictions to provide concrete information to developers.

Device Queues for USB

Joel Busch. Bachelor's Thesis. ETH Zurich. May 2018. [ .pdf ]

The motivation behind this thesis is that we want to provide the research operating system Barrelfish with a useful feature and in the course of implementing it we want to prove that some of Barrelfish’s newer systems work well. Therefore the goal we chose was to develop a USB mass storage service. The implementation of the service provides an opportunity to use the newly introduced Device Queues for inter-process bulk communication. Demonstrating their functionality and efficiency is part of our aim. Furthermore, in the course of developing the USB mass storage driver we can show how well the system knowledge base and the device manager cooperate to enable event based driver startup. Our approach was to first reorganize the existing USB subsystem to conform to the new driver model for Barrelfish and to change its initialization to be based around events dispatched by the system knowledge base. Next we added a USB mass storage driver to the subsystem and used Device Queues for providing clients with access to the service over a zero-copy channel. Finally Barrelfish’s FAT implementation was extended to include write support and its back-end was modified to use the aforementioned communication channel. The resulting mass storage service achieves better performance than Linux when both are run virtualized on the same host with the same USB hardware being passed through. Some stability issues, particularly based around FAT, still need to be addressed and performance can still be improved, but the core functionality has been demonstrated. We further provide evidence that the Device Queues do not add any measurable communication overhead. Finally we show that the device manager and the system knowledge base robustly solve the problem of device initialization on a discoverable bus.

Hardware Configuration With Dynamically-Queried Formal Models

Daniel Schwyn. Master's Thesis. ETH Zurich. October 2017. [ .pdf ]

Hardware is getting increasingly complex and heterogeneous. With different components having different views of the system, the traditional assumption of unique physical addresses has become an illusion. To adapt to such hardware, an operating system (OS) needs to understand the complex address translation chains and be able to handle the presence of multiple address spaces. This thesis takes a recently proposed model that formally captures these aspects and applies it to hardware configuration in the Barrelfish OS. To this end, I present Sockeye, a domain specific language that uses the model to describe hardware. I then show, that code relying on knowledge about the address spaces in a system can be statically generated from these specifications. Furthermore, the model is successfully applied to device management, showing that it can also be used to configure hardware at runtime. The implementation presented here does not rely on any platform specific code and it reduced the amount of such code in Barrelfish’s device manager by over 30%. Applying the model to further hardware configuration tasks is expected to have similar effects.

Explicit OS support for hardware threads

Andrei Poenaru. Master's Thesis. ETH Zurich. March 2017. [ .pdf ]

Current mainstream processors provide multiple SMT (i.e., simultaneous multithreading) lanes on top of each physical core. These hardware threads share more resources (e.g., execution units and caches) when compared to CPU cores, but are managed by operating systems in the same way as if they were separate physical cores. This Thesis explores the interaction between hardware threads and proposes an extension to the Barrelfish OS, meant to improve the performance of a system by adequately handling SMT lanes. On an Intel Haswell CPU, with 2-way SMT via Hyper-Threading Technology, each SMT lane had 2/3 of the processing power that was yielded by the physical core with a single active hardware thread. The multi-HT CPU Driver (i.e., Barrelfish’s microkernel) is able to modify the set of active hardware threads with an overhead in the order of thousands of processor cycles, which means that it can quickly adapt to the parallelism exhibited by the workload.

Dynamic Linking and Loading in Barrelfish

David Keller. Bachelor's Thesis. ETH Zurich. August 2015. [ .pdf ]

Dynamic linking and loading capabilities are an integral part of most modern operating systems. They make the system more modular, enable independent updates of system resources and client applications and save space. This work describes the design and implementation of dynamic linking and loading in Barrelfish – a multikernel research operating system – using its native APIs and build toolchain. The evaluation shows that space can be saved for executables compared to a static linked binary if more than 37 applications share the same set of libraries. A threshold easily met if mandatory system libraries are shared.


Reto Achermann

acreto [at] inf.ethz.ch

+41 44 633 70 15

Dept. of Computer Science
CAB E 69, ETH Zürich
Universitätstrasse 6
8092 Zürich