CAREER: A Programming Language for Developing Software to Execute Reliably on Unreliable Hardware

Massachusetts Institute Of Technology, Cambridge MA

Investigators

Abstract

The landscape of software development has changed as computing platforms have reached the end of Moore?s Law. Specifically, the tactic of aggressively shrinking computer processors to yield increased computer performance has been paused as modern processors have -- as a result -- become more vulnerable to errors in their manufacture and operation. As a result, applications executed on many emerging systems need to be specifically designed to execute through faults in the underlying execution platform. This project provides a new programming language with a supporting compiler and verification system that enables developers to work with a model of the execution platform to deliver provably reliable computations even in the presence of faults in the underlying execution platform. The project's intellectual merit is the development of state-of-the-art techniques for reasoning about program behavior that capture the growing availability of soft-computing fabrics, such as unreliable computer processors, energy-harvesting systems, and cyber-physical systems. Moreover, in a society that is increasingly dependent on computing systems, the project?s broader significance is to provide software developers, engineers, and scientists with new tools to build efficient and powerful systems that fully exploit the benefits of new hardware platforms while simultaneously delivering the reliable, resilient execution that society needs. A key idea behind this project is to extend a language, compiler, and verification system to support programmatic, first-class execution models that capture the semantics of execution platforms that deliver alternative results for a given operation. Such execution models are first-class in that the developer can communicate with the verification system to verify correctness properties of the computation that are related to the explicit state of the execution model itself. A key driver behind the feasibility of this approach is that the project leverages relational verification. Specifically, the system can reason about two separate executions of the program: 1) the idealized reliable execution of the program and 2) the actual, faulty execution as specified by the execution model. Such reasoning 1) enables a user to specify properties, such as accuracy, that relate values between the two executions and 2) enables the system and user together efficiently verify programs by, for example, demonstrating that a desired property holds of the faulty execution because faults do not interfere with the property's validity. Building upon these key directions, this project also investigates new mechanisms to build reliability-aware optimizing compilers that still soundly transform the program even in the presence of alternative execution models. Together, the results of this project will enable developers to leverage the wide variety of new computing platforms for which execution models are non-standard, highly configurable, and approximate -- yet still produce an application that has strong guarantees. Moreover, the proposal is to validate the approach by integrating the results into new coursework on programming language design and implementation. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.