TopoOpt is a novel DNN training system that co-optimizes the distributed training process across computation, communication, and network topology.

FSCQ is the first file system with machine-checkable proof that its implementation meets its specification and whose specification includes crashes.

A Protected Dataplane Operating System for High Throughput and Low Latency

Shinjuku is a single-address space operating system that uses hardware support for virtualization to make preemption practical at the microsecond scale.

Shenango is a system that enables servers in datacenters to simultaneously provide low tail latency and high CPU efficiency, by rapidly reallocating cores across applications, at timescales as small as every 5 microseconds.

Ward is a Spectre and Meltdown resistant research operating system based on sv6 which was in turn based on xv6.

AIFM stands for Application-Integrated Far Memory. It provides a simple, general, and high-performance mechanism for users to adapt ordinary memory-intensive applications to far memory. Different from existing paging-based systems, AIFM exposes far memory as far-memory pointers and containers in the language level.