Please note: This seminar will take place in DC 1304.
Reto Achermann, Postdoctoral Research Fellow, Systopia Lab
Department of Computer Science, University of British Columbia
We use computer systems daily: texting with a friend, ordering something online, or letting a self-driving car help us navigate the roads. We trust these computer systems to behave correctly. Thus, building safe, secure, and performant systems is of paramount importance. Today’s systems are diverse and contain many layers of software abstractions, each with their own challenges and each relying on the layer below to operate correctly. Unfortunately, vulnerabilities or bugs occur frequently in any of these layers leading to bad user experiences or putting our data and even lives at risk.
My research focuses on the foundations of building performance-aware, resilient system software. I target problems at multiple levels of the software stack by developing innovative approaches or systems that make contributions in different research areas, including 1) accurately modeling hardware, 2) using verification to ensure correctness, 3) applying software synthesis techniques to automatically generate specialized and correct code, and 4) optimizing performance by adapting resource management to the hardware topology.
In this talk, I will focus on memory management which provides key abstractions and isolation features in today’s systems. At the lowest level, hardware platforms are becoming more specialized and diverse. Modern hardware platforms consist of a collection of heterogeneous cores, different memories, and smart devices — all connected through a network of high-speed interconnects and buses. On these platforms, correct and performant memory management is the cornerstone as it provides the necessary abstractions and isolation guarantees. Therefore, to ensure the integrity of the system, the operating system must correctly configure and manage the memory hardware of a platform while being aware of its memory architecture to ensure adequate performance of applications.
To solve this problem, I present Velosiraptor, a system that automatically generates low-level operating systems code that configures memory hardware from a behavioral specification. By using software synthesis, operating systems developers obtain guaranteed correct code and are freed from the burden of writing the program themselves. To make this tractable, Velosiraptor decomposes memory hardware as a selection of building blocks and composition rules. Moreover, it employs domain-specific optimizations to reduce the search space of candidate programs. As a result, Velosiraptor can generate correct implementations of configuration programs in less than a few seconds.
Bio: Reto Achermann is a Postdoctoral Research Fellow at the Systopia Lab of the Computer Science Department at the University of British Columbia working with Prof. Margo Seltzer.
His research interests are at the intersection of memory and storage systems, hardware platforms, formal specification and verification, device drivers, and software synthesis. The main goal of his research is to help developers build more reliable system software while reducing development efforts. He was part of the core Barrelfish operating system team, working on various subsystems such as memory management, capabilities, hardware abstractions, and device drivers.
Reto Achermann received a Doctor of Science from ETH Zurich where he was advised by Prof. Timothy Roscoe. His thesis “On Memory Addressing” presents a formal model of address decoding in computer systems and its implementation in a capability-based kernel. He also holds an MSc in Computer Science from ETH Zurich. He served on the program committees of ASPLOS, EuroSys and Usenix ATC. While at the University of British Columbia, he received the Faculty of Science Excellence in Service Award for his engagement in the education of undergraduate and graduate students.
200 University Avenue West
Waterloo, ON N2L 3G1
Canada
