Reto Achermann
Assistant Professor
Systopia Lab
Department of Computer Science
University of British Columbia
Projects
Note, the project pages is currently in overhaul. Please stay posted.Velosiraptor
Velosiraptor - Why program when you can automatically synthesize OS code?
Collaborators: Ryan Mehri, Em Chu, Ilias Karimalis and Margo Seltzer.
[ .www ]
Velosiraptor provides a specification language to express the behavior of translation hardware. Based on the specification, Velosiraptor automatically synthesizes the operating systems code that interfaces with the hardware and correctly configures the translation hardware.
IronSync
IronSync
Collaborators: Andrea Lattuada, Travis Hance, Chris Hawblitzel, Jon Howell, Bryan Parno, etal..
[ .git ]
CleanQ
CleanQ - Lightweight, uniform and formally specified Queues.
Collaborators: Roni Haecki, Lukas Humbel, Daniel Schwyn, Timothy Roscoe.
Queues or descriptor rings are used everywhere in an operating system from IPC mechanisms to interoperating with devices. Consequently, there exist many different queue implementations, each having a slightly different interface with non-uniform semantics. With CleanQ we clean up the queue mess by formally specifying the queue with its interfaces and semantics, providing a uniform and versatile framework to compose and use queues inside an operating system. We show that despite its formal rigor and well-defined interfaces, a resulting C implementation is not only correct but also fast.
Sockeye
Sockeye - Formally Specifying Hardware as Seen by Software
Collaborators: David Cock, Lukas Humbel, Daniel Schwyn, Nora Hossle, Timothy Roscoe.
The hardware/software boundary in modern heterogeneous multicore computers is increasingly complex and diverse across different platforms. A single memory access by a core or DMA engine traverses multiple hardware translation and caching steps, and the destination memory cell or register often appears at different physical addresses for different cores. Interrupts pass through a complex topology of interrupt controllers and remappers before delivery to one or more cores, each with specific constraints on their configurations. System software must not only correctly understand the specific hardware at hand, but also configure it appropriately at runtime.
Mitosis
Mitosis - Page-Table Replication for Big Memory Workloads
Collaborators: Ashish Panwar, Abhishek Bhattacharjee, Timothy Roscoe and Jayneel Gandhi.
[ .git ]
Multi-socket machines with 1-100 TBs of physical memory are becoming prevalent. Applications running on multi-socket machines suffer non-uniform bandwidth and latency when accessing physical memory. Decades of research have focused on data allocation and placement policies in NUMA settings, but there have been no studies on the question of how to place page tables among sockets. We make the case for explicit page-table allocation policies and show that page-table placement is becoming crucial to overall performance. We propose Mitosis to mitigate NUMA effects on page-table walks by transparently replicating and migrating page tables across sockets without application changes. This reduces the frequency of accesses to remote NUMA nodes when performing page-table walks. Mitosis uses two components: (i) a mechanism to enable efficient page-table replication and migration; and (ii) policies for processes to efficiently manage and control page-table replication and migration. We implement Mitosis in Linux and evaluate its benefits on real hardware. Mitosis improves performance for large-scale multi-socket workloads by up to 1.34x by replicating page-tables across sockets. Moreover, it improves performance by up to 3.24x in cases when the OS migrates a process across sockets by enabling cross-socket page-table migration.
Enzian
Enzian - A Research Computer
Collaborators: David Cock, Muhsen Owaida, Adam Turowski, Amit Kulkarni, Timothy Roscoe, Gustavo Alonso, and many more....
[ .www ]
As a research computer, Enzian is designed for computer systems software research, rather than any particular commercial workload. An Enzian node has a big server-class CPU closely coupled to a large FPGA, with ample main memory and network bandwidth on both sides.
Barrelfish
Barrelfish Operating System
Collaborators: The Barrelfish Team.
Barrelfish is a new research operating system being built from scratch and released by ETH Zurich in Switzerland, originally in collaboration with Microsoft Research and now partly supported by HP Enterprise Labs, Huawei, Cisco, Oracle, and VMware. We are exploring how to structure an OS for future multi- and many-core systems. We are motivated by two closely related trends in hardware design: first, the rapidly growing number of cores, which leads to a scalability challenge, and second, the increasing diversity in computer hardware, requiring the OS to manage and exploit heterogeneous hardware resources.
Smelt
Smelt - Machine Aware Message-Passing Primitives
Collaborators: Stefan Kaestle, Roni Haecki, Moritz Hoffmann, Sabela Ramos and Timothy Roscoe.
[ .git ]
The performance of tree-based group communication primitives such as broadcasts and reductions highly depend on the tree topology and and message send order. Furthermore, there is no single topology that works well across a wide variety of machines. In this project, we present Smelt a framework that constructs good trees for any machine.
Shoal
Shoal - Smart Memory Allocation for NUMA Machines
Collaborators: Stefan Kaestle, Timothy Roscoe and Tim Harris..
[ .git ]
Modern machines feature highly complex memory hierarchies and NUMA topologies which makes it hard for programmers to allocate and manipulate memory. We present Shoal, a runtime library for smart memory allocation based on data access patterns and hardware characteristics
