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

职业：一种用于开发在不可靠的硬件上可靠执行的软件的编程语言

• 批准号: 1751011
• 负责人: Michael Carbin
• 金额: $ 52.5万
• 依托单位: Massachusetts Institute of Technology
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2018
• 资助国家: 美国
• 起止时间: 2018-07-01 至 2024-06-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1751011&HistoricalAwards=false
• 关键词: CAREER; Programming; Language; Developing; Software

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.

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

项目成果

DiffTune: Optimizing CPU Simulator Parameters with Learned Differentiable Surrogates

DiffTune：使用学习的可微代理优化 CPU 模拟器参数

• DOI: 10.1109/micro50266.2020.00045
• 发表时间: 2020
• 期刊: Annual IEEE/ACM International Symposium on Microarchitecture (MICRO
• 作者: Renda, Alex;Chen, Yishen;Mendis, Charith;Carbin, Michael
• 通讯作者: Carbin, Michael

Programming with neural surrogates of programs

• DOI: 10.1145/3486607.3486748
• 发表时间: 2021-10
• 期刊: Proceedings of the 2021 ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software
• 作者: Alex Renda;Yi Ding;Michael Carbin

Ithemal: Accurate, Portable and Fast Basic Block Throughput Estimation using Deep Neural Networks

• 发表时间: 2018-08
• 期刊: ArXiv
• 作者: Charith Mendis;Saman P. Amarasinghe;Michael Carbin

VeGen: a vectorizer generator for SIMD and beyond

• DOI: 10.1145/3445814.3446692
• 发表时间: 2021-04
• 期刊: Proceedings of the 26th ACM International Conference on Architectural Support for Programming Languages and Operating Systems
• 作者: Yishen Chen;Charith Mendis;Michael Carbin;Saman P. Amarasinghe

Leto: verifying application-specific hardware fault tolerance with programmable execution models

Leto：使用可编程执行模型验证特定于应用程序的硬件容错能力

• DOI: 10.1145/3276533
• 发表时间: 2018
• 期刊: Proceedings of the ACM on Programming Languages
• 作者: Boston, Brett;Gong, Zoe;Carbin, Michael
• 通讯作者: Carbin, Michael