About Me


Research Assistant, Systems Group, Department of Computer Science, ETH Zurich

I graduated from ETH Zurich in 2014 with a MSc in Computer Science with specialization in Distributed Systems. Currently, I doing my PhD in the Systems Group, Department of Computer Sience, ETH Zurich. My advisor is Prof. Timothy Roscoe.

I am part of the Barrelfish team. Barrelfish is a research operating system with a distinct architecture called the multikernel. Barrelfish treats a single machine as a distributed system. My work involves several device drivers such as USB, DMA engines and the Xeon Phi co-processor. My key interest is how to program modern, heterogeneous multiprocessors. A multi-core is inherently complex showing many similarities to distributed systems. Therefore we need to treat multi-core machines as such and hence rethink the way we write software for a multi-core machine to account for interconnect networks, NUMA regions and even failures.


Reto Achermann holds a MSc in computer science from ETH Zurich and is doing his PhD in computer science at ETH Zurich where he is advised by Prof. Timothy Roscoe. He is part of the Barrelfish research operating system team, working on various subsystems such as memory management, capabilities, hardware abstractions, device drivers. Besides Barrelfish, he is also working on Sockeye which is a framework to formally specify hardware as seen by software and the Enzian platform, a research computer combining a Cavium ThunderX processor and a large FGPA connected by the native coherence interconnect. During his PhD he also did internships at VMware Research and Hewlett-Packard Labs.

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

  • 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 ]
  • A Least-Privilege Memory Protection Model for Modern Hardware.
    Reto Achermann, Nora Hossle, Lukas Humbel, Daniel Schwyn, David Cock and Timothy Roscoe.
    arXiv:1908.08707. [ .doi ] [ .pdf ] [ .bib ]
>> more preprints


  • Transparent Self-Replicating Page Tables in Computing Systems.
    Reto Achermann and Jayneel Gandhi. Pending. [ .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 ]


  • 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

ETH Zurich, Zurich Switzerland

November 2014 - present, Research Assistant

Prof. Timothy Roscoe. Operating Systems Research

  • Dissertation: On Memory Addressing - a more faithful hardware abstractions for modern operating systems.
  • Barrelfish: Member of the core OS team working on device drivers, memory management, networking.
  • Sockeye: Describing hardware as seen by software using a formal model specified in Isabelle/HOL
  • Shoal: memory allocation strategies in a NUMA machine with knowledge of the access patterns.
  • Smelt: automatically tuning message passing primitives to the machine hardware topology using measurements.
  • Enzian: understanding the coherency protocol for the Enzian research computer.

VMware Research, Palo Alto (CA), United States

June 2018 - September 2018, Intern VMware Research Group

Jayneel Gandhi. Project: Mitosis - Page-table Replication for Big Memory Machines.

  • Project: Mitosis: Transparently Self-Replicating Page-Tables for Large-Memory Machines.

Hewlett-Packard Labs, Palo Alto (CA), United States

September 2015 - December 2015, Intern Systems Software

Dejan S. Milojicic Consensus and Capabilties for The Machine

  • Project: Consensus protocols and capabilities for the Machine.


Doctor of Science (PhD) in Computer Science, ETH Zurich

November 2014 - February 2020, Advisor: Prof. Timothy Roscoe

On Memory Addressing [ .www ] [ .pdf ]

Master of Science (MSc) in Computer Science, ETH Zurich

September 2013 - October 2014, Advisor: Prof. Timothy Roscoe

Specialization: Distributed Systems. Grade: 5.8 / 6.0 (with distinction)

Message passing and bulk transport on heterogenous multiprocessors [ .www ] [ .pdf ]


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


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.

[ .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 ]

Enzian - A Research Computer

Collaborators: David Cock, Muhsen Owaida, Adam Turowski, Amit Kulkarni, Timothy Roscoe, Gustavo Alonso, and many more...

Enzian is a research computer combining a big server-class ARM CPU with a large FPGA connected through the Enzian Coherency Interface (ECI). My work targeted the understanding of the processor's native coherence protocol driving the development of ECI.

[ .www ]

Mentored Students

Multiple Address Spaces in a Distributed Capability System

Nora Hossle. Master's Thesis. ETH Zurich. September 2019. [ .pdf ]

Semantic model and execuatable specification of multiple address spaces in Barrelfish.

Using NetBSD Kernel Components on Barrelfish Through Rump Kernels

Leo Horne. Bachelor's Thesis. ETH Zurich. August 2019. [ .pdf ]

Support for NetBSD Rump Kernels on Barrelfish.

Formally modelling hardware standards

Giuseppe Arcuti. Bachelor's Thesis. ETH Zurich. August 2019. [ .pdf ]

Analsysis of hardware descriptions and standards in manuals.


Reto Achermann

acreto [at] inf.ethz.ch

+41 44 633 70 15

Dept. of Computer Science
CAB E 69, ETH Zürich
Universitätstrasse 6
8092 Zürich