Formalization of the OSMosis Isolation Model

Phillip Dumitru. Honours's Thesis. University of British Columbia. September 2023 - April 2024.

TBD

Profiling Stack Traces in Non-Linux Virtual Machines

Brice Michael Wilson. Honours's Thesis. University of British Columbia. September 2022 - April 2023.

Carefully developed operating systems provide the computing world with the complexity necessary to allow any application to run easily on a diverse set of machines. However, this general-purpose ability comes with a cost; it introduces overhead. Unikernels address this problem by linking just the parts of the operating system needed by a specific application directly with that application. This means that resources are not wasted on components or features that will not be used.Unikraft is a unikernel operating system reputed to be uniquely suited to obtaining high performance to support general-purpose applications, however, there is the potential for improvement. Finding out where slowdowns occur can be obtained by using a technique called profiling. Profiling can locate where time is spent within an operating system and determine where it is being spent unnecessarily. A couple of profilers for Unikraft exist such as QProfiler, however, none of them work with QEMU or sample stack traces. My goal is to optimize Unikraft and eliminate even more overhead. I developed a custom profiler, based on QProfiler, that exposes hidden overheads in Unikraft. I developed BeeProf as a tool that enables detailed profiling of unmodified Unikraft applications. BeeProf leverages the virtual machine monitor interface to sample stack traces and not just the current instruction

Encoding memory models for address translation in an SMT solver.

Ryan Mehri. Directed Studies's Thesis. University of British Columbia. June 2023 - August 2023.

Generating translation hardware components for the Arm FastModels simulator.

Emily Chu. Intern's Thesis. University of British Columbia. June 2023 - August 2023.

Formally specifying optimal sparse decision trees (OSDT) in Dafny.

David Bromley. Intern's Thesis. University of British Columbia. June 2022 - August 2022.

Revisiting device driver synthesis with behavior trees.

Sepehr Noorafshan. Intern's Thesis. University of British Columbia. June 2022 - August 2022.

Design and implementation of a DSL to specify translation hardware.

Ilias Karimalis. Intern's Thesis. University of British Columbia. June 2022 - August 2022.

Detailed Simulation of Enzian's Cache Coherence Protocol

Joel Busch. Master's Thesis. ETH Zurich. April 2020 - 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 equal 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 the 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 analyzing 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. February 2020 - 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 classes of 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. October 2019 - April 2020.

Implementing a cache coherence protocol in hardware requires thorough testing of each aspect of the protocol. Testing on real hardware as part of the normal development workflow is often infeasible due to large synthesis times and using simulated test benches does not provide the necessary abstractions for testing such a protocol, signals need to be set appropriately every cycle without being able to directly specify coherency messages that should be processed. I present a simulation environment providing a layer of abstraction, allowing users to interact with the coherence protocol through coherency messages instead of at the signal level. I demonstrate that the hardware simulation runs at an adequate speed, being able to process 10'000 messages in less than one second. I further show that thanks to the common message format used for coherency messages, the simulator can connect to a protocol analyzer to automatically check the protocol implementation's behavior.

Tools for Cache Coherence Protocol Interoperability

Jakob Meier. Master's Thesis. ETH Zurich. September 2018 - March 2019.

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

Multiple Address Spaces in a Distributed Capability System

Nora Hossle. Master's Thesis. ETH Zurich. March 2018 - 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. Resources may be 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 modeling the access rights of the different agents concerning 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. February 2019 - August 2019.

A major task in the implementation of new operating systems is writing code for file systems, 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 to avoid having to manually port a large amount of code from other operating systems. We implement a basic hypervisor for the rump kernel which enables the use of OS components such as file systems, 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. February 2019 - 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 the 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. March 2018 - 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 its 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. December 2017 - 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 on events dispatched by the system knowledge base. Next, we added a USB mass storage driver to the subsystem and used Device Queues to provide 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. April 2017 - 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. September 2016 - 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) can 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. February 2015 - 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 multi-kernel research operating system – using its native APIs and build toolchain. The evaluation shows that space can be saved for executables compared to a statically linked binary if more than 37 applications share the same set of libraries. A threshold easily met if mandatory system libraries are shared.