SOSP 2019: Tutorials

Popcorn Linux | Serval | Derecho

Workshop and Tutorial Program (PDF)

All three of the half-day tutorials will take place on Sunday October 27, 2019.

Programming Heterogeneous-ISA Platforms with Popcorn Linux OS and Compiler Framework
Logistics
  • Date: Sunday October 27, 2019
  • Time: 9:00 am - 12:30 pm
  • Building: Pavilion Meeting Space
  • Room: Waterhouse Ballroom 3

Tutorial Presenters
Details
Abstract

Computer systems are increasingly heterogeneous. Beside classic heterogeneity, CPUs of different instruction set architectures (ISAs) are more and more being integrated on the same platform, including SoC, single machine, data-center, and at the edge.

A programmer facing such platforms is challenged by the fact that each ISA-different processor runs its own software stack (i.e., OS, compiler, libraries). Although being part of the same system, each ISAdifferent processor ends up acting like an independent system. A fundamental limitation of current software is that applications started on one software stack cannot be migrated to another due to the ISA difference, limiting resource management, which negatively affects system-level properties such as performance and energy consumption.

The Popcorn Linux family of projects attacks this problem by enabling users to exploit platforms of heterogeneous-ISA CPUs. Popcorn Linux provides the familiar abstraction of a shared memory multiprocessor, enabling thread-level, process-level, and VM-level migration across ISA-different processors. This is achieved by a new compiler toolchain, runtime, OS, and VMM, which taken together, enable applications to execute on heterogeneous-ISA hardware with minimal modifications.

This tutorial introduces Popcorn Linux OS and Compiler Framework, shows how to compile and run an application, and discusses execution migration in a heterogeneous-ISA environment. Multiple demos will be run through the event – thus, any participant is welcome, even if not keen to try-it out, or without a laptop/tablet/phablet! Note that we will do our best to provide spare laptops as well as remote access to our systems.

Automated verification of systems software with Serval
Logistics
  • Date: Sunday October 27, 2019
  • Time: 2:00 pm - 5:30 pm
  • Building: Pavilion Meeting Space
  • Room: A.J. Casson Room

Tutorial Presenters
Details
Abstract

Formal verification has become an increasingly hot topic in systems research over recent years due to its promise to guarantee the absence of classes of bugs. However, formal verification poses a steep learning curve for systems researchers and practitioners and often requires a background in formal methods, which hinders a wider use of verification in our community.

This tutorial will introduce Serval (SOSP 2019), a framework for automated verification of lowlevel systems code that leverages recent advances to lower the proof burden and minimize developer effort. For example, using Servalwe have found more than 20 bugs in systems such as security monitors and the Linux kernel's BPF subsystem, all confirmed and fixed. This tutorial will give a brief overview of systems verification in general, a hands-on guide of how to formally specify and verify a system using Serval, and an in-depth discussion of formal verification techniques that power Serval.

Derecho: Blindingly Fast RDMA Replication for Cloud and Edge Services
Logistics
  • Date: Sunday October 27, 2019
  • Time: 2:00 pm - 6:00 pm
  • Building: Pavilion Meeting Space
  • Room: Waterhouse Ballroom 3

Tutorial Presenters
Details
Abstract

Cloud computing services often replicate data, and consistency can matter too (particularly for IoT applications, where rapidly-changing data is used to coordinate distributed actions). This tutorial centers on Derecho, a library to assist with solving these problems [1, 2]. Derecho is far faster than prior solutions, including the weakly-consistent mechanisms that dominate today’s cloud computing infrastructures.

Derecho’s asynchronous design is key to its performance: the system achieves lock-free data streaming for critical paths (queries and updates occur concurrently but independently), and data movement is out-of-band from the control plane. The biggest payoff is with RDMA, but Derecho outperforms even on TCP.

Part of our goal in the tutorial is to understand the “design pattern” that enables this big performance boost; it involves separating the control and data planes, performing updates on a code path distinct from that used for queries, and transforming the system to use an asynchronous streaming communication model, in which participants often can independently deduce safety properties and perform batches of actions on received data. On 100Gbps RDMA, Derecho can send millions of events per second in each subgroup or shard, and throughput peaks at almost 16GB/s (125Gbps).

We anticipate a few use cases for the technology. The big one is the Edge IoT: Derecho was motivated by the desire to move machine learning tools closer to the IoT edge (the first tier of the cloud, which interacts directly with IoT devices). Existing edge platforms lack support for building complex, structured applications that maintain state and offer coordinated, consistent behavior; Derecho respond to this need. This said, we also see important opportunities in the operating system itself (existing systems have many services that could be improved using Derecho. Some low-hanging fruit includes Zookeeper, pub/sub and DDS technologies, file systems like HDFS or Ceph, and the network infrastructure layer.

The tutorial is structured into two parts. In the first half, based primarily on our TOCS paper [1], situates Derecho relative to prior work, explains how it obtains such high speeds, and reviews experiments that clarify why it outperforms prior solutions. We also learn about features aimed at Edge IoT applications that work with real-time sensor data yet still need strong consistency. The second part teaches attendees to use Derecho: we walk through the process of downloading the library, building services that use it, running them locally, and installing them on a cloud. At the end of the second part, participants modify the Derecho demo (a simple AI Sys application), rebuild it and rerun it.

SOSP participants who only want to hear about the work but not to really learn the system are welcome to drop in just at the beginning, and then can duck out when we get to the hands-on stage.