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

Latest News and Upcoming Travel

  • 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

  • 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 ]
  • Formalizing Memory Accesses and Interrupts.
    Reto Achermann, Lukas Humbel, David Cock and Timothy Roscoe.
    MARS'17. [ .doi ] [ .pdf ] [ .bib ]
>> more papers

Journal Articles

  • Memory-Side Protection With a Capability Enforcement Co-Processor.
    Leonid Azriel, Lukas Humbel, Reto Achermann, Alex Richardson, Moritz Hoffmann, Avi Mendelson, Timothy Roscoe, Robert N. M. Watson, Paolo Faraboschi and Dejan Milojicic.
    ACM TACO. 16-1 [ .doi ] [ .pdf ] [ .bib ]

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 ]
>> more preprints

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 ]
>> more talks

Professional Experience

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

Service

Program Committees

Education

Doctor of Science (PhD) in Computer Science

ETH Zurich, Zurich, Switzerland

November 2014 - February 2020

Advisor: Prof. Timothy Roscoe

Thesis: On Memory Addressing [ .www ] [ .pdf ]

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 ]

Teaching

Systems Programming and Computer Architecture (252-0061-00L), ETH Zurich

Autumn 2019, Autumn 2018, Autumn 2017, Autumn 2016, Autumn 2014, Autumn 2013

Application-Oriented Programming (252-0840-02L), ETH Zurich

Spring 2019, Spring 2018

Advanced Operating Systems (263-3800-00L), ETH Zurich

Spring 2019, Autumn 2017

Projects

CleanQ - 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 ]

Mentored Students

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.

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