Reto Achermann
Research Assistant
Systems Group
Department of Computer Science
ETH Zurich
About Me
Reto Achermann
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.
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 ]
Journal Articles
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 ]
Patents
-
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 ]
Talks
-
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 ]
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
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)
Thesis:
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 2013Application-Oriented Programming (252-0840-02L), ETH Zurich
Spring 2019, Spring 2018Advanced Operating Systems (263-3800-00L), ETH Zurich
Spring 2019, Autumn 2017Sockeye - 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 ]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.
acreto [at] inf.ethz.ch
+41 44 633 70 15
https://orcid.org/0000-0003-3263-7236Dept. of Computer Science
CAB E 69, ETH Zürich
Universitätstrasse 6
8092 Zürich
Switzerland
