About Me

Reto Achermann

PhD Student, 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.

Publications and Talks

  >> Complete List
  >> DBLP Profile
  >> Google Scholar Profile

Conference Papers

  • 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 ]
  • Towards Correct-by-Construction Interrupt Routing on Real Hardware.
    Lukas Humbel, Reto Achermann, David Cock and Timothy Roscoe.
    PLOS'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

  • 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 ]
  • Mitosis: Transparently Self-Replicating Page-Tables for Large-Memory Machines.
    Reto Achermann, Ashish Panwar, Abhishek Bhattacharjee, Timothy Roscoe and Jayneel Gandhi.
    arXiv:1910.05398. [ .doi ] [ .pdf ] [ .bib ]
  • Mitosis: Transparently Self-Replicating Page-Tables for Large-Memory Machines (Poster).
    Reto Achermann, Ashish Panwar, Abhishek Bhattacharjee, Timothy Roscoe and Jayneel Gandhi.
    OSDI'18:Poster Sessions. [ .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 ]


  • Realistic Hardware Abstractions and Least-Privilege Memory Management in Operating Systems.
    Networks, Systems, and Security (NSS) Lab, University of British Columbia, Canada. November 01, 2019. [ .pdf ]
  • Model based system configuration and tasteful hardware.
    Systems Research Group, University of Cambridge, Cambridge, UK. July 06, 2017. [ .pdf ]
  • Provable Correct Memory Management.
    11th EuroSys Doctoral Workshop. April 23, 2017. [ .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 - PRESENT, 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