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.
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 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.
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 groups studies the hardware/software interface and the OS abstractions best suited to make these complex systems programmable.