Operating Systems

The role of operating systems has evolved over time, from sharing one device’s resources among many users in the mainframe era, to providing convenient user interface, storage, and networking abstractions in the personal computer era. As we transition to the ubiquitous computing era, operating systems must now manage a user’s information and computation across many computers and devices. Yale is developing new operating system architectures, application environments, and security frameworks to meet today’s challenges across the computing spectrum, including IoT devices, cyber-physical systems (such as self-driving cars and quadcopters), cloud computers, and blockchain ecosystems.

Faculty working in this area:

Highlights in this area:

Abhishek Bhattacharjee and his students are buildinging next-generation operating systems for emerging heterogeneous computer systems. The waning of Moore’s Law and Dennard scaling as well as the widespread success of AI have prompted systems designers to embrace heterogeneity in hardware. Today’s systems integrate tightly- and loosely-coupled accelerators, ranging from GPUs, TPUs, neural network hardware, DSPs, etc., a swath of heterogeneous memory devices, ranging from high-bandwidth to non-volatile memories, with a complex amalgam of operating systems, drivers, firmware, runtimes, and languages. Abhishek’s group studies the hardware/software interface and the OS abstractions best suited to make these complex systems programmable.

Anurag Khandelwal and his team are exploring the design for an Operating System stack for emerging serverless and disaggregated architectures. Over the last few years, significant improvements in inter-server network performance, coupled with stagnating intra-server interconnect performance, have driven advances in data center resource disaggregation — where server compute, memory and storage resources are physically separated into network attached resource “blades”. However, actualizing the benefits of resource disaggregation while ensuring application performance requires operating system (OS) support. Unfortunately, existing approaches expose a hard tradeoff between application performance on one hand and resource elasticity on the other. Anurag’s group is exploring a fundamentally new network-centric design for the disaggregated OS — one that places resource management and access functionality in the data center network fabric to break the above tradeoff.

Zhong Shao and his FLINT team at Yale are working to develop a new class of formally verified operating systems for modern heterogeneous platforms. In the last few years, they have made multiple breakthroughs showing that building a hacker-resistant concurrent OS kernel is not only feasible but also practical. They developed a novel language-based account of certified concurrent abstraction layers, advocated abstraction over a particularly rich class of specification (called deep specification), and then constructed new methodologies and tools for formally specifying, programming, verifying, and composing abstraction layers.  They have successfully developed the CertiKOS operating system and verified its contextual functional correctness in Coq. CertiKOS is written in 6500 lines of C and x86 assembly and runs on stock x86 multicore machines. This is the world’s first proof of functional correctness of a complete, general-purpose concurrent OS kernel with fine-grained locking. Shao and his team are now working on expanding the CertiKOS infrastructure so it can be applied to support more advanced system software for modern heterogeneous platforms and distributed enclaves. 

Lin Zhong and his team are examining some foundational assumptions made by modern OSes in the context of mobile and edge computing. First, modern OSes assume permissive and weak languages such as C; as a result, they feature complex, error-prone mechanisms to ensure correctness at runtime, leading to poor efficiency and availability. Using the Rust language, Lin’s team has constructed an experimental OS called Theseus to explore the power of language and compiler-based mechanisms. Theseus enforces many correctness invariants and even realize traditional OS-based functions at compile-time. Second, modern OSes assume complete trust from the user and their applications and as a result, they have unfettered access to application data by design. Lin’s team is exploring both incremental changes to existing OSes, e.g., Linux, and clean-slate designs to decouple virtualization, the essential role of OS, from data access.