Workshop Program

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

The complete workshop proceedings are available in the ACM DL for download.

The schedule of all SOSP worksops is published at the SOSP website.

9:00 AM — Welcome, Best Paper Award
Stefan Lankes (RWTH Aachen University), Program Chair
[slides]

9:05 AM — Keynote
Session Chair: Stefan Lankes (RWTH Aachen University)

• Premature Popularity is the Root of all Evil
  Amit Levy (Princeton University)
  

  Abstract: For decades, systems builders have been playing fast-and-loose with program correctness. For decades, systems software has been plagued with bugs. For decades, we've known of better ways to build more correct systems. The sudden rise in popularity and credibility over the past decade of safe systems languages, Rust most significantly, suggests we might be witness to a dramatic improvement systems safety and security. I'll make the argument that Rust is uniquely well positioned to replace C/C++ in the vast majority of important systems, that it can do so while significantly improving how well computers work, and it can help lead to more advances in the future. But I'll also argue that Rust's popularity might end up being a curse to itself and type-safe languages in systems more generally. Which future awaits is, in part at least, up to us.

  About the speaker: Amit Levy is a senior research and the executive director of Better Bytes where he leads research and development of the Tock operating system, and before that was an Assistant Professor of Computer Science at Princeton University. His research is focused on achieving systems that are extensible, secure, and performant all at the same time, particularly combining tools from programming languages, cryptography, and system design. He is the recipient of an NSF CAREER Award, Google Faculty Award, OSDI and USENIX Security best paper awards, he was the runner-up for best eyes in his high-school year book, and was the co-founder and CEO of MemCachier.

9:45 AM — Session 1: A Resource Manager’s Journey
Session Chair: Hugo Lefeuvre (University of British Columbia)

• Comparing Isolation Mechanisms with OSmosis
  Sidhartha Agrawal (University of British Columbia), Shaurya Patel (University of British Columbia, Google), Linh Pham (Hammerspace), Arya Stevinson (Oracle Labs), Ilias Karimalis (University of British Columbia), Hugo Lefeuvre (University of British Columbia), Aastha Mehta (University of British Columbia), Reto Achermann (University of British Columbia), Margo Seltzer (University of British Columbia)
  [slides]


• Monolift: Automating Distribution With the Tools You Have at Home
  Tim Goodwin, Esteban Ramos, Andi Quinn, Lindsey Kuper (University of California, Santa Cruz)
  [slides]


• Static Analysis of Reference-Counted Objects for the C Programming Language
  Ole Wiedemann, Volkmar Sieh (Friedrich-Alexander-Universität Erlangen-Nürnberg)
  [slides]

10:45 AM — Coffee break

11:15 AM — Session 2: The Power of Verification
Session Chair: Olaf Spinczyk (Universität Osnabrück)

• Modal Verification Patterns for Systems Software
  Ismail Kuru, Colin S. Gordon (Drexel University)
  [slides]


• Towards Hybrid Cooperative-Preemptive Scheduling
  Yizheng Xie, Di Jin, Nikos Vasilakis (Brown University)
  [slides]


• Applying Modern Verification Techniques to a Root-of-Trust Bootloader
  Nicholas Gordon, Carsten Weinhold (Barkhausen Institut)
  [slides]


• Compositional Model-Driven Verification of Weakly Consistent Distributed Systems
  Bryant J. Curto (Northeastern University), Jeonghyeon Kim (KAIST), Alan Wang (Northeastern University), Gijung Im (Yonsei University), Jieung Kim (Yonsei University), Jeehoon Kang (FuriosaAI), Ji-Yong Shin (Northeastern University)
  


• Debug, Execute, Verify! - Development-Verification Co-Design Made Practical
  František Farka, Carmine Abate, Shuanglong Kan, Sebastian Ertel (Barkhausen Institute)
  [slides]


• High-Fidelity Specification of Real-World Devices
  Liam Murphy (UNSW Sydney), Albert Rizaldi (PlanV GmbH), Lesley Rossouw (UNSW Sydney), Chen George (University of Wisconsin), James Treloar (UNSW Sydney), Hammond Pearce (UNSW Sydney), Miki Tanaka (UNSW Sydney), Gernot Heiser (UNSW Sydney)
  

1:00 PM — Lunch

2:00 PM — Session 3: To Wait Or Not To Wait?
Session Chair: Stefan Lankes (RWTH Aachen University)

• High-Fidelity Specification of Real-World Devices
  Liam Murphy (UNSW Sydney), Albert Rizaldi (PlanV GmbH), Lesley Rossouw (UNSW Sydney), Chen George (University of Wisconsin), James Treloar (UNSW Sydney), Hammond Pearce (UNSW Sydney), Miki Tanaka (UNSW Sydney), Gernot Heiser (UNSW Sydney)
  [slides]


• Towards Hybrid Cooperative-Preemptive Scheduling
  Yizheng Xie, Di Jin, Nikos Vasilakis (Brown University)
  


• Path Expressions Revisited – Towards Compiler-enforced Reusable Synchronization Patterns
  Thomas Alexander Hövelmann (TU Dortmund University), Olaf Spinczyk (Universität Osnabrück), Alexander Krause (TU Dortmund University), Horst Schirmeier TU Dresden, Peter Ulbrich (TU Dortmund University)
  [slides]


• Are Your GPU Atomics Secretly Contending?
  Peter Maucher, Nick Djerfi, Lennard Kittner, Lukas Werling, Frank Bellosa (Karlsruhe Institute of Technology)
  [slides]


• Tapestry: Revealing Wait-For Dependencies Between Application Threads
  Tomáš Faltín (Charles University), Himadri Chhaya-Shailesh (Inria), Julia Lawall (Inria), Jean-Pierre Lozi (Inria)
  [slides]

3:25 PM — Session 4a: Crossing Boundaries

• Propagating C++ Exceptions across the User/Kernel Boundary
  Dmitry Voronetskiy, Tom Spink (University of St Andrews)
  [slides]

3:45 PM — Coffee break

4:15 PM — Session 4b: Crossing Boundaries
Session Chair: Carsten Weinhold (Barkhausen Institut)

• From Rust Till Run: Extending Memory Safety From Rust to Cryptographic Assembly 
  Shai Caspin, Nikhil Pimpalkhare, Amit Levy (Princeton University)
  [slides (pdf)]


• KLean: Extending Operating System Kernels with Lean
  Di Jin (Brown University), Ethan Lavi (Brown University), Jinghao Jia (University of Illinois Urbana-Champaign), Robert Y. Lewis (Brown University), Nikos Vasilakis (Brown University)
  [slides]


• From Browser to Kernel: Exploring a Lightweight Sandboxed Approach for Unikernel Extensions
  Martin Kröning, Stefan Lankes, Jonathan Klimt, Antonello Monti (RWTH Aachen University)
  [slides]

5:15 PM — Closing remarks