Workshop Program

Location: All of the workshop's sessions will take place in the room Virgo.

The complete workshop proceedings are available in the ACM Digital Library for download. The schedule of all SOSP worksops is published at the SOSP website.

8:30 AM — Welcome, Best Paper Award
Carsten Weinhold (Barkhausen Institute), Program Chair

8:35 AM — Keynote
Session Chair: Carsten Weinhold (Barkhausen Institute)

• The Case for Operating System Models
  Timothy Roscoe (ETH Zurich)
  [slides]

  Abstract: Despite their fundamental role in computing infrastructure, Operating Systems design is mostly ad-hoc in nature, even when algorithmically informed by theory or formally verified. Knowledge of how to build a "good" OS is mostly tacit, and learned by doing. The stream of new hardware features seem to require new OS structures, which ironically often resemble existing ones.
  Related areas like networking, databases, and distributed systems have long relied on "reference models" to make sense of the complexity they inhabit, facilitate discussion and sharing of ideas, summarize and codify knowledge, and enable rapid adaptation to new technologies.
  Operating Systems were also like this decades ago, but the sheer complexity and rapid evolution of hardware has caused them to lose any clear sense of an architectural model, and also render the original models obsolete.
  It's time to rethink this. There is real value in reference models for OS design and implementation which are clean, general, faithful to real hardware and application requirements, and which facilitate reasoning about the safety of a computer system. We should create them.
  Borrowing from ideas in distributed systems, I'll propose how to use such models to put OS design on a somewhat more sound footing than it is now, and what advantages and opportunities this approach opens up in building real OSes today.

  About the speaker: Timothy Roscoe is a Full Professor in the Systems Group of the Computer Science Department at ETH Zurich, where he works on operating systems, networks, and distributed systems.
  Mothy received a PhD in 1995 from the Computer Laboratory of the University of Cambridge, where he was a principal designer and builder of the Nemesis OS. After three years working on web-based collaboration systems at a startup in North Carolina, he joined Sprint's Advanced Technology Lab in Burlingame, California in 1998, working on cloud computing and network monitoring. He joined Intel Research at Berkeley in April 2002 as a principal architect of PlanetLab, an open, shared platform for developing and deploying planetary-scale services. Mothy joined the Computer Science Department at ETH Zurich in January 2007, and was named Fellow of the ACM in 2013 for contributions to operating systems and networking research. He was head of department from 2021 to 2023.
  His work at ETH has included the Barrelfish multikernel research OS, as well as work on distributed stream processors, and using formal specifications to describe the hardware/software interfaces of modern computer systems. Mothy's current research centers on foundational methodologies for OS design and implementation, and Enzian, a powerful hybrid CPU/FPGA machine designed for research into systems software.

9:20 AM — Session 1: Know your Hardware
Session Chair: Reto Achermann (Technical University of Munich)

• Towards Tractable Hardware Model Validation Against Real Hardware
  Rishika Varma Kalidindi (University of Texas at Austin); Reto Achermann (Technical University of Munich)
  🗎 [paper] [slides]


• Making Weird Machines Untypeable: A Type-and-Effect View of Microarchitectural Attacks
  Anitha Gollamudi (University of Massachusetts Lowell)
  🗎 [paper]

10:00 AM — Coffee break

10:30 AM — Session 2: Measurements and Optimizations
Session Chair: Olaf Spinczyk (Universität Osnabrück)

• Topology-aware TLB Shootdown Protocols: It's more complicated than you think.
  Ning Ding, Margo Seltzer (University of British Columbia); Reto Achermann (Technical University of Munich)
  🗎 [paper] [slides]


• Dissecting the Performance Impact of System Calls
  Martin Kröning, Vincent Feinendegen, Stefan Lankes, Sarah Simon, Jonathan Klimt, Antonello Monti (RWTH Aachen University)
  🗎 [paper] [slides]


• Lost Bytes At The Crossroads Between User- And Kernel-Level Memory Allocation
  Pasha Fistanto, Sören Tempel, Christian Dietrich (Technische Universität Braunschweig)
  🗎 [paper]


• Blink and you miss it - VMM-OS Co-Design for Millisecond Boot of Isolated Serverless Applications
  Jonathan Klimt, Sarah Simon, Martin Kröning, Ellen Emilia Anna Zscheile, Panagiotis Vasilopoulos, Stefan Lankes, Antonello Monti (RWTH Aachen University)
  🗎 [paper] [slides]

12:00 PM — Lunch

1:30 PM — Session 3: Security and Safety
Session Chair: Horst Schirmeier (Technische Universität Dresden)

• We Need to Talk About the Actual Guarantees of Rust-based Systems
  Corinn Tiffany, Artem Agvanian, Ziyun Song, Isabella Szabo (Brown University); Kinan Dak Albab (Boston University); Will Crichton (Brown University); Philip Levis (Stanford University and Google); Akshay Narayan, Deepti Raghavan, Malte Schwarzkopf (Brown University)
  🗎 [paper] [slides]


• Beyond Zero-Cost: Understanding Rust Safety Overheads in Systems Code
  Soham Bagchi, Manvik Nanda, Anton Burtsev (University of Utah)
  🗎 [paper] [slides]


• zBulk: Towards Automatic Compartmentalization in Rust with Zero Manual Retrofitting
  Maxim Ritter von Onciul, Phillip Raffeck, Peter Wägemann, Rüdiger Kapitza (Friedrich-Alexander-Universität Erlangen-Nürnberg)
  🗎 [paper] [slides]


• Exploring the Design Space of Isolation Mechanisms
  Sidhartha Agrawal, Shaurya Patel (University of British Columbia); Linh Pham (Hammerspace); Arya Stevinson (Oracle); Ilias Karimalis, Hugo Lefeuvre, Aastha Mehta (University of British Columbia); Reto Achermann (Technical University of Munich); Margo Seltzer (University of British Columbia)
  🗎 [paper] [slides]

3:00 PM — Coffee break

3:30 PM — Session 4: Code Generation and Debugging
Session Chair: Carsten Weinhold (Barkhausen Institute)

• Code Generation from Regression Trees for Microsecond-Scale Decisions in Operating Systems
  Birte Friesel, Marcel Lütke Dreimann, Olaf Spinczyk (Universität Osnabrück)
  🗎 [paper] [slides]


• ACF: Infrastructure for Debugging Long-Running Systems with Tracing and Unit Test Execution
  Roman Vašut, Pavel Parízek (Charles University)
  🗎 [paper] [slides]

4:10 PM — Session 5: Built for Verification
Session Chair: Carsten Weinhold (Barkhausen Institute)

• SMT-based Deductive Verification of Device Drivers using the Pancake-to-Viper Transpiler
  Samuel Tyler (UNSW Sydney); Alessandro Legnani (ETH Zurich); Junming Zhao, Zhewen Shen, Rihui Wu, Miki Tanaka, Gernot Heiser (UNSW Sydney)
  🗎 [paper] [slides]


• All Your Assembly Belongs to Rust
  Charly Castes, Gurvan Debaussart, Thomas Bourgeat (EPFL)
  🗎 [paper] [slides]


• DeterV: Verifying Deterministic Parallel Execution
  Zhengqing Liu, Marios Kogias (Imperial College London)
  🗎 [paper] [slides]

5:10 PM — Closing remarks