Mentored Students

ETH Zurich

Detailed Simulation of Enzian’s Cache Coherence Protocol

Joel Busch. Master's Thesis. ETH Zurich. October 2020.

Enzian is a research computer developed by the Systems Group at ETH Zurich. It contains a 48 core processor and a large field programmable gate array (FPGA), which are treated as equals partners who can share their respective memory over the Enzian Coherent Interconnect (ECI) that connects them. This work develops a software simulation of the cache coherence hardware found in the Enzian processor to create an environment for development and testing of software intended to run on Enzian and for the benefit of researchers working to develop a coherent FPGA implementation for the other socket. The simulator is based on an earlier simplified implementation and uses the Arm Fast Models simulation environment. This thesis uses the formal specification of the ECI Cache Coherence Protocol Specification and also proposes some corrections to it. I compare the implementation to the specification using a combination of running software tests within it and analysing the instrumented log output to check if the specified finite state machines are properly exercised.

CleanQ for USB

Thore Goebel. Bachelor's Thesis. ETH Zurich. August 2020.

Today, USB is the de-facto standard for connecting peripherals to a computing system. However, its structure is inherently complex, and no real-world software can or ever will be bug-free. CleanQ has been introduced as an approach to unify one part of system software: descriptor queues. By formally specifying a queue’s semantics, it eliminates ambiguities in terms of how the queue must be used and what guarantees it provides, thus erasing some classesof bugs. While CleanQ is already used in the network stack of the Barrelfish research operating system, USB transfers are still managed in a complex and intertwined manner. In this thesis, we will explore how USB transfers can be migrated to use the CleanQ framework and take advantage of the benefits it provides.

A Unified Approach to Simulation of Hybrid CPU/FPGA systems

Patrick Ziegler. Bachelor's Thesis. ETH Zurich. April 2020.

Implementing a cache coherence protocol in hardware requires thoroughtesting of each aspect of the protocol. Testing on real hardware as part of thenormal development workflow is often infeasible due to large synthesis timesand using simulated testbenches does not provide the necessary abstractionsfor testing such a protocol, signals need to be set appropriately every cyclewithout being able to directly specify coherency messages that should beprocessed. I present a simulation environment providing a layer of abstraction, allowingusers to interact with the coherence protocol through coherency messagesinstead of at the signal level. I demonstrate that the hardware simulationruns at an adequate speed, being able to process 10’000 messages in less thanone second. I further show that, thanks to the common message format usedfor coherency messages, the simulator can connect to a protocol analyzer toautomatically check the protocol implementation’s behavior.

Tools for Cache Coherence Protocol Interoperability

Jakob Meier. Master's Thesis. ETH Zurich. March 2019.

The Enzian Coherent Interconnect (ECI) connects a server-class CPU and alarge FPGA on an Enzian board. Within the scope of this thesis, I developed aseries of software tools to ease the analysis of ECI. The tools enable automaticcomparison of traces from actual hardware to a formal specification of the ECIprotocols, which I have written down. I further demonstrate an approach to simulate my model using its machine-readable specification and I test it againstboth real and emulated hardware.

Multiple Address Spaces in a Distributed Capability System

Nora Hossle. Master's Thesis. ETH Zurich. September 2019.

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.

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.

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.

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.

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.

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.

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.

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.

Contact

Reto Achermann

achreto [at] cs.ubc.ca

The University of British Columbia
Dept. of Computer Science
201-2366 Main Mall
Vancouver, BC V6T 1Z4
Canada