Workshop Program

---

Note:To access the video presentations (mp4) and to download the papers (PDF) you will need a username and a password. Registered participants will receive this information by email and it has also been posted in the workshop's slack channel. If you still don't have access, contact any of the organizers.

---

3:00 PM CEST — Welcome
Pierre-Evariste Dagand (Université de Paris), Program Chair

3:10 PM CEST — Keynote

• Formal Verification of Systems Software: The Good, The Bad, The Ugly
  Haibo Chen (Shanghai Jiao Tong University)

  Abstract: Formal methods have recently gained a resurgent interest in industry due to the the increasing demand of high-assurance systems software . This can be evidenced by the increasing investment on formal methods in industry like Microsoft, Amazon and Huawei. In this talk, I will share our experiences in applying formal methods in verifying systems software. Specifically, I will describe the efforts in applying formal methods in the design and implementation operating systems, synchronization primitives, file systems and distributed system protocols. Based on these, I will further describe the experiences and lessons learned in applying formal methods at a large scale setting, and discuss possible challenges and opportunities in fostering better synergy between academia and industry.

  About the speaker: Haibo Chen is a Distinguished Professor of Shanghai Jiao Tong University, who founds and directs the Institute for Parallel and Distributed Systems (IPADS). His main research areas are operating systems and distributed systems and its interaction with formal methods. He has won the First Prize of Technical Invention by the Ministry of Education, China Youth Science and Technology Award, President's Award of Shanghai Jiao Tong University, CCF Young Scientist Award, National Excellent Doctoral Dissertation Award of China, etc. He is currently the Chair of ACM SIGOPS ChinaSys, the Vice Chair of the Special Committee on System Software of the China Computer Federation, seves on the editorial board member and co-chair of Special Sections of Communications of the ACM, and the editorial board member of ACM Transactions on Storage. He has also received Best Paper Awards from ASPLOS, EuroSys, VEE, ICPP and APSys, etc. Meanwhile, he founds and leads the OS Kernel Lab, and currently serves as the Chief Scientist for Operating Systems and the Vice President of Central Software Institute at Huawei.

4:00 PM CEST — Session 1.1: The System is Calling
Session Chair: Hui Lu (State University of New York at Binghamton)

• AnyCall: Fast and Flexible System-Call Aggregation [PDF] [video]
  Luis Gerhorst (Friedrich-Alexander-Universität Erlangen-Nürnberg), Benedict Herzog (Ruhr-Universität Bochum), Stefan Reif (Friedrich-Alexander-Universität Erlangen-Nürnberg), Wolfgang Schröder-Preikschat (Friedrich-Alexander-Universität Erlangen-Nürnberg) and Timo Hönig (Ruhr-Universität Bochum)


• Asterope: A Cross-Platform Optimization Method for Fast Memory Copy [PDF] [video]
  Giorgos Kappes and Stergios V. Anastasiadis (University of Ioannina)


• Files-as-Filesystems for POSIX Shell Data Processing [PDF] [video]
  Michael Greenberg (Stevens Institute of Technology)

4:30 PM CEST — Session 1.2: The Virtue of Persistence
Session Chair: Hui Lu (State University of New York at Binghamton)

• Decoupling Application Logic from Persistent Memory Frameworks with AspectC++ [PDF] [video]
  Marcel Köppen, Daniel Friesel, Christoph Borchert and Olaf Spinczyk (Universität Osnabrück)


• PyMM: Heterogeneous Memory Programming for Python Data Science [PDF] [video]
  Daniel Waddington, Moshik Hershcovitch and Clem Dickey (IBM Research)

4:50 PM CEST — Break

5:00 PM CEST — Session 2.1: Do not go wrong
Session Chair: Jeehoon Kang (KAIST)

• CppSig: Extracting Type Information for C-Preprocessor Macro Expansions [PDF] [video]
  Christian Dietrich (Technische Universität Hamburg)


• Generating correct initial page tables from formal hardware descriptions [PDF] [video]
  Reto Achermann (University of British Columbia), David Cock, Roni Haecki, Nora Hossle, Lukas Humbel, Timothy Roscoe and Daniel Schwyn (ETH Zürich)

5:20 PM CEST — Session 2.2: Isolated but not alone
Session Chair: Jeehoon Kang (KAIST)

• FlashCube: Fast Provisioning of Serverless Functions with Streamlined Container Runtimes [PDF] [video]
  Zhen Lin, Kao-Feng Hsieh, Yu Sun, Seunghee Shin and Hui Lu (State University of New York at Binghamton)


• Using Coroutines for Multi-core Preemptive Scheduling [PDF] [video]
  Ole Lehrmann Madsen (Aarhus University)


• Understanding the Overheads of Hardware and Language-Based IPC Mechanisms [PDF] [video]
  Zhaofeng Li, Tianjiao Huang, Vikram Narayanan and Anton Burtsev (University of California, Irvine)

5:50 PM CEST— Session 2.3: Something borrowed, something amiss
Session Chair: Jeehoon Kang (KAIST)

• Isolation in Rust: What is Missing? [PDF] [video]
  Anton Burtsev, Dan Appel, David Detweiler, Tianjiao Huang, Zhaofeng Li, Vikram Narayanan (University of California, Irvine) and Gerd Zellweger (VMware Research)


• How ISO C Became Unusable for Operating System Development [PDF] [video]
  Victor Yodaiken (E27812)

6:10 PM CEST — Wrap-Up