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

随着计算平台进入摩尔时代的末期，软件开发的前景已经发生了变化。年代法律。具体来说，大幅缩小计算机处理器以提高计算机性能的策略已经暂停，因为现代处理器在制造和操作中变得更容易出错。因此，在许多新兴系统上执行的应用程序需要专门设计为通过底层执行平台中的错误执行。该项目提供了一种带有支持编译器和验证系统的新编程语言，使开发人员能够使用执行平台的模型来交付可证明的可靠计算，即使在底层执行平台中存在错误。该项目的智力优点是开发了最先进的技术，用于对程序行为进行推理，这些技术捕获了越来越多的软计算结构的可用性，例如不可靠的计算机处理器、能量收集系统和网络物理系统。此外，在一个越来越依赖计算机系统的社会中，项目？更广泛的意义是为软件开发人员、工程师和科学家提供新的工具，以构建高效、强大的系统，充分利用新硬件平台的优势，同时提供社会所需的可靠、有弹性的执行。这个项目背后的一个关键思想是扩展语言、编译器和验证系统，以支持可编程的、一流的执行模型，这些模型捕获执行平台的语义，为给定的操作提供可选的结果。这样的执行模型是一流的，因为开发人员可以与验证系统通信，以验证与执行模型本身的显式状态相关的计算的正确性属性。该方法可行性背后的一个关键驱动因素是项目利用关系验证。具体来说，系统可以对程序的两种单独执行进行推理：1)程序的理想可靠执行和2)执行模型指定的实际错误执行。这样的推理1)使用户能够指定属性，如准确性，将两次执行之间的值联系起来；2)使用户和系统能够一起有效地验证程序，例如，通过证明一个期望的属性在错误的执行中保持不变，因为错误不会干扰属性的有效性。在这些关键方向的基础上，本项目还研究了新的机制，以构建可感知可靠性的优化编译器，即使在存在替代执行模型的情况下，这些编译器仍然可以很好地转换程序。总之，这个项目的结果将使开发人员能够利用各种各样的新计算平台，这些平台的执行模型是非标准的、高度可配置的和近似的——但仍然产生具有强大保证的应用程序。此外，我们的建议是通过将结果整合到编程语言设计和实现的新课程中来验证这种方法。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

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.