Reto Achermann
Postdoctoral Resarch Fellow
Systopia Lab
Department of Computer Science
University of British Columbia
About Me
Introduction
I am a Postdoctoral Research Fellow working with Prof. Margo Seltzer at the Systopia Lab at the Department of Computer Science of the University of British Columbia in Vancouver Canada.
I did my PhD with Prof. Timothy Roscoe in the Systems Group at the Department of Computer Science, ETH Zurich. My PhD was about formally specifying the memory subsystem of a hardware platform as it is seen by software.
News
- Jan 04, 2020 - I will be co-teaching CS508 at UBC with Margo Seltzer.
- Nov 16, 2020 - Our work on 'Mirage: An Illusion of Fast Local Page-Tables for Virtualized NUMA Systems' got accepted at ASPLOS'21.
- Sept 7, 2020 - I'll be joining the University of British Columbia as a Postdoctoral Research Fellow.
Conference Papers
-
Fast Local Page-Tables for Virtualized NUMA Servers with vMitosis.
Ashish Panwar, Reto Achermann, Arkaprava Basu, Abhishek Bhattacharjee, K. Gopinath and Jayneel Gandhi. ASPLOS ’21. [ .doi ] [ .pdf ] [ .bib ] -
Mitosis: Transparently Self-Replicating Page-Tables for Large-Memory Machines.
Reto Achermann, Ashish Panwar, Abhishek Bhattacharjee, Timothy Roscoe and Jayneel Gandhi. ASPLOS ’20. [ .doi ] [ .pdf ] [ .bib ] -
Physical Addressing on Real Hardware in Isabelle/HOL.
Reto Achermann, Lukas Humbel, David Cock and Timothy Roscoe. ITP'18. [ .doi ] [ .pdf ] [ .bib ]
Journal Articles
PrePrint Papers
-
Secure Memory Management on Modern Hardware.
Reto Achermann, Nora Hossle, Lukas Humbel, Daniel Schwyn, David Cock and Timothy Roscoe.
arXiv:2009.02737. [ .doi ] [ .pdf ] [ .bib ] -
CleanQ: a lightweight, uniform, formally specified interface for intra-machine data transfer.
Roni Haecki, Lukas Humbel, Reto Achermann, David Cock, Daniel Schwyn and Timothy Roscoe.
arXiv:1911.08773. [ .doi ] [ .pdf ] [ .bib ] -
Cichlid: Explicit physical memory management for large machines.
Simon Gerber, Gerd Zellweger, Reto Achermann, Moritz Hoffmann, Kornilios Kourtis, Timothy Roscoe and Dejan Milojicic.
arXiv:1911.08367. [ .doi ] [ .pdf ] [ .bib ]
Patents
-
Transparent Self-Replicating Page Tables in Computing Systems.
Reto Achermann and Jayneel Gandhi. US20200117612A1. [ .www ] -
Interoperable capabilities.
Reto Achermann, Maurice Bailleu, Dejan S. Milojicic and Gabriel Parmer. US20170329526A1. [ .www ] -
Memory management with versioning of objects.
Izzat El Hajj, Alexander Merritt, Gerd Zellweger, Dejan S. Milojicic and Reto Achermann. WO2017131789A1. [ .www ]
Talks
-
Mitosis: Transparently Self-Replicating Page-Tables for Large-Memory Machines.
25th International Conference on Architectural Support for Programming Languages and Operating Systems. March 19, 2020. [ .pdf ] [ .video ] -
Memory Topology Models and Their Application in Operating Systems.
Trustworthy Systems, Data 61, CSIRO, Australia.. February 25, 2020. [ .pdf ] -
Faithful Hardware Representation and Least-Privilege Memory Management in Operating Systems.
Lab for Advanced Systems Research (LASR), University of Texas at Austin, USA. December 06, 2019. [ .pdf ]
Postdoctoral Reserach Fellow
University of British Columbia - Systopia Lab
December 2020 - present
Vancouver (BC), Canada
Research Assistant
ETH Zurich - Systems Group
November 2014 - November 2020
Zurich, Switzerland
Intern VMware Research Group
VMware, Inc. - VMware Research Group
June 2018 - September 2018
Palo Alto (CA), United States
Program Committees
- Usenix Annual Technical Conference 2021 (ATC '21): Program Committee
- ACM Sigops EuroSys 2021 (EuroSys '21): Shadow Program Committee
Master of Science (MSc) in Computer Science
ETH Zurich, Zurich, Switzerland
September 2013 - October 2014
Advisor: Prof. Timothy Roscoe
Specialization: Distributed Systems. Grade: 5.8 / 6.0 (with distinction)
Thesis: Message passing and bulk transport on heterogenous multiprocessors [ .www ] [ .pdf ]
Graduate Operating Systems (CPSC 508), University of British Columbia
Winter Term 2 2020Systems Programming and Computer Architecture (252-0061-00L), ETH Zurich
Autumn 2019, Autumn 2018, Autumn 2017, Autumn 2016, Autumn 2014, Autumn 2013Application-Oriented Programming (252-0840-02L), ETH Zurich
Spring 2019, Spring 2018CleanQ - Lightweight, uniform and formally specified Queues.
Collaborators: Roni Haecki, Lukas Humbel, Daniel Schwyn, Timothy Roscoe
CleanQ is a queue specification for intra-machine data-transfers. The specification defines the semantics of ownership transfers in Isabelle/HOL. We proof the correctness through a sequence of refinement steps down to the C implementation of a queue, and demonstrate the that the resulting implementation is lightweight and observes good performance.
[ .www ] [ .github ]Sockeye - Formally Specifying Hardware as Seen by Software
Collaborators: David Cock, Lukas Humbel, Daniel Schwyn, Nora Hossle, Timothy Roscoe
Sockeye is a framework for accurately representing hardware configurations. Faithful hardware abstractions used by operating systems to represent memory, interrupt, power and clock domain configurations of heterogeneous computer systems and formally define the semantics there of. With Sockeye, platform specific operating systems code can be generated (e.g.~correct-by-construction page-tables). Sockeye is integrated in the Barrelfish OS.
[ .www ] [ .github ]Mitosis - Page-Table Replication for Big Memory Workloads
Collaborators: Ashish Panwar, Abhishek Bhattacharjee, Timothy Roscoe and Jayneel Gandhi
Big-memory workloads spend a significant fraction of their runtime serving TLB misses. Walking page-tables require up to 24 memory accesses and experiences NUMA effects. Mitosis transparently replicates page-tables across sockets to eliminate cross-socket page-table walks. Implementation of Linux kernel extensions and application runtime.
[ .www ] [ .github ]Detailed Simulation of Enzian’s Cache Coherence Protocol
Joel Busch. Master's Thesis. ETH Zurich. October 2020.
Design and implementation of a detailed Enzian cache simulator
CleanQ for USB
Thore Goebel. Bachelor's Thesis. ETH Zurich. August 2020.
Exploring the use of CleanQ in the USB software stack.
A Unified Approach to Simulation of Hybrid CPU/FPGA systems
Patrick Ziegler. Bachelor's Thesis. ETH Zurich. April 2020.
Design and implementation of a simulation environment for cache coherency protocols.
