Publications and Talks

Peer-reviewed Publications

  • Synthesizing Device Drivers with Ghost Writer.
    Bingyao Wang, Sepehr Noorafshan, Reto Achermann and Margo Seltzer.
    PLOS '23. [ .doi ] [ .pdf ] [ .bib ]
  • Sharding the State Machine: Automated Modular Reasoning for Complex Concurrent Systems.
    Travis Hance, Andrea Lattuada, Reto Achermann, Alex Conway, Ryan Stutsman, Gerd Zellweger, Chris Hawblitzel, Jon Howell and Bryan Parno.
    OSDI '23. [ .doi ] [ .pdf ] [ .bib ]
  • Why write address translation OS code yourself when you can synthesize it?.
    Reto Achermann, Ilias Karimalis and Margo Seltzer.
    HotOS '23. [ .doi ] [ .pdf ] [ .bib ]
  • Beyond isolation: OS verification as a foundation for correct applications.
    Matthias Brun, Reto Achermann, Tej Chajed, Jon Howell, Gerd Zellweger and Andrea Lattuada.
    HotOS '23. [ .doi ] [ .pdf ] [ .bib ]
  • Cache-Coherent Accelerators for Persistent Memory Crash Consistency.
    Ankit Bhardwaj, Todd Thornley, Vinita Pawar, Reto Achermann, Gerd Zellweger and Ryan Stutsman.
    HotStorage '22. [ .doi ] [ .pdf ] [ .bib ]
  • Enzian: An Open, General, CPU/FPGA Platform for Systems Software Research.
    David Cock, Abishek Ramdas, Daniel Schwyn, Michael Giardino, Adam Turowski, Zhenhao He, Nora Hossle, Dario Korolija, Melissa Licciardello, Kristina Martsenko, Reto Achermann, Gustavo Alonso and Timothy Roscoe.
    ASPLOS '22. [ .doi ] [ .pdf ] [ .bib ]
  • Fast Sparse Decision Tree Optimization via Reference Ensembles.
    Hayden McTavish, Chudi Zhong, Reto Achermann, Ilias Karimalis, Jacques Chen, Cynthia Rudin and Margo Seltzer.
    AAAI '22. [ .doi ] [ .pdf ] [ .bib ]
  • Generating Correct Initial Page Tables from Formal Hardware Descriptions.
    Reto Achermann, David Cock, Roni Haecki, Nora Hossle, Lukas Humbel, Timothy Roscoe and Daniel Schwyn.
    PLOS '21. [ .doi ] [ .pdf ] [ .bib ]
  • Declarative Power Sequencing.
    Jasmin Schult, Daniel Schwyn, Michael Giardino, David Cock, Reto Achermann and Timothy Roscoe.
    ACM TECS Vol 20-5s. [ .doi ] [ .pdf ] [ .bib ]
  • NrOS: Effective Replication and Sharing in an Operating System.
    Ankit Bhardwaj, Chinmay Kulkarni, Reto Achermann, Irina Calciu, Sanidhya Kashyap, Ryan Stutsman, Amy Tai and Gerd Zellweger.
    OSDI '21. [ .doi ] [ .pdf ] [ .bib ]
  • Mmapx: Uniform Memory Protection in a Heterogeneous World.
    Reto Achermann, David Cock, Roni Haecki, Nora Hossle, Lukas Humbel, Timothy Roscoe and Daniel Schwyn.
    HotOS '21. [ .doi ] [ .pdf ] [ .bib ]
  • 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 ]
  • 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 Vol 16-1. [ .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 ]
  • Towards Correct-by-Construction Interrupt Routing on Real Hardware.
    Lukas Humbel, Reto Achermann, David Cock and Timothy Roscoe.
    PLOS'17. [ .doi ] [ .pdf ] [ .bib ]
  • Separating Translation from Protection in Address Spaces with Dynamic Remapping.
    Reto Achermann, Chris Dalton, Paolo Faraboschi, Moritz Hoffmann, Dejan Milojicic, Geoffrey Ndu, Alexander Richardson, Timothy Roscoe, Adrian L. Shaw and Robert N. M. Watson.
    HotOS '17. [ .doi ] [ .pdf ] [ .bib ]
  • Machine-aware Atomic Broadcast Trees for Multicores.
    Stefan Kaestle, Reto Achermann, Roni Haecki, Moritz Hoffmann, Sabela Ramos and Timothy Roscoe.
    OSDI'16. [ .doi ] [ .pdf ] [ .bib ]
  • SpaceJMP: Programming with Multiple Virtual Address Spaces.
    Izzat El Hajj, Alexander Merritt, Gerd Zellweger, Dejan Milojicic, Reto Achermann, Paolo Faraboschi, Wen-mei Hwu, Timothy Roscoe and Karsten Schwan.
    ASPLOS '16. [ .doi ] [ .pdf ] [ .bib ]
  • Shoal: Smart Allocation and Replication of Memory for Parallel Programs.
    Stefan Kaestle, Reto Achermann, Timothy Roscoe and Tim Harris.
    USENIX ATC '15. [ .doi ] [ .pdf ] [ .bib ]
  • Not Your Parents' Physical Address Space.
    Simon Gerber, Gerd Zellweger, Reto Achermann, Kornilios Kourtis, Timothy Roscoe and Dejan Milojicic.
    HotOS'15. [ .doi ] [ .pdf ] [ .bib ]

Preprints

  • OSmosis: No more Déjà vu in OS isolation.
    Sidhartha Agrawal, Reto Achermann and Margo Seltzer.
    arXiv:2309.09291. [ .doi ] [ .pdf ] [ .bib ]
  • 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 ]
  • 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 ]

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 ]

Thesis

  • On Memory Addressing.
    Reto Achermann.
    2020. Doctoral Thesis. Department of Computer Science, ETH Zurich. Switzerland.
    [ .doi ] [ .pdf ] [ .bib ]
  • Message Passing and Bulk Transport on Heterogenous Multiprocessors.
    Reto Achermann.
    2014. Master's Thesis. Department of Computer Science, ETH Zurich. Switzerland.
    [ .doi ] [ .pdf ] [ .bib ]
  • Barrelfish USB Subsystem.
    Reto Achermann.
    2013. Bachelor's Thesis. Department of Computer Science, ETH Zurich. Switzerland.
    [ .doi ] [ .pdf ] [ .bib ]

Talks

  • Why write code when you can synthesize address translations?.
    19th Workshop on Hot Topics in Operating Systems. June 22, 2023.
    [ .slides ]
  • Fast Local Page Tables for NUMA Servers with Mitosis.
    ICSA Colloquium – University of Edinburgh. June 08, 2021.
    [ .slides ]
  • 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.
    [ .slides ] [ .video ]
  • Memory Topology Models and Their Application in Operating Systems.
    Trustworthy Systems, Data 61, CSIRO, Australia.. February 25, 2020.
    [ .slides ]
  • 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.
    [ .slides ]
  • 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.
    [ .slides ]
  • Mitosis: Transparently Self-Replicating Page-Tables for Large-Memory Machines.
    Systems Group, ETH Zurich, Switzerland.. November 30, 2018.
    [ .slides ]
  • Model based system configuration and tasteful hardware.
    Systems Research Group, University of Cambridge, Cambridge, UK. July 06, 2017.
    [ .slides ]
  • Provable Correct Memory Management.
    11th EuroSys Doctoral Workshop. April 23, 2017.
    [ .slides ]
  • Smelt: ​Machine-aware Atomic Broadcast Trees for Multicores​.
    12th USENIX Symposium on Operating Systems Design and Implementation. November 2, 2016.
    [ .slides ]

Posters

  • Sidhartha Agrawal and Shaurya Patel and Reto Achermann and Margo Seltzer. OSmosis: Modeling and Building Flexible OS Isolation Mechanisms (Poster). 2023. .
    [ .doi ] [ .pdf ] [ .bib ]
  • Reto Achermann and Ashish Panwar and Abhishek Bhattacharjee and Timothy Roscoe and Jayneel Gandhi. Mitosis: Transparently Self-Replicating Page-Tables for Large-Memory Machines (Poster). 2018. .
    [ .doi ] [ .pdf ] [ .bib ]
  • Reto Achermann and Lukas Humbel and Roni Haecki and David Cock and Timothy Roscoe. Sockeye: Formally Describing Hardware as Seen by Software (Poster). 2018. .
    [ .doi ] [ .pdf ] [ .bib ]
  • David Cock and David Sidler and Muhsen Owaida and Reto Achermann and Tobias Grosser and Zeke Wang and Amit Kulkarni and Alain Denzler and Adam Turowski and Abishek Ramdas and Anastasiia Ruzhanskaia and Timothy Roscoe and Gustavo Alonso. Enzian: a research computer for datacenter and rackscale computing (Poster). 2018. .
    [ .doi ] [ .pdf ] [ .bib ]
  • Reto Achermann and Timothy Roscoe. Formalizing Address Space Interactions (Poster). 2016. .
    [ .doi ] [ .pdf ] [ .bib ]

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