PPoSS: LARGE: Intel: Combining Learning and Formal Verification for Scalable Machine Programming (ScaMP)

PPoSS：大：英特尔：结合学习和形式验证实现可扩展机器编程 (ScaMP)

• 批准号: 2217064
• 负责人: Saman Amarasinghe
• 金额: $ 250万
• 依托单位: Massachusetts Institute of Technology
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2022
• 资助国家: 美国
• 起止时间: 2022-10-01 至 2027-09-30
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2217064&HistoricalAwards=false
• 关键词: PPoSS; LARGE; Intel; Combining; Learning

Modem applications combine the need for extreme scalability with enormous complexity to provide rich functionality to millions of simultaneous users. In this context, programmer productivity is achieved by building on deep stacks of pre-existing components and systems software, allowing programmers to focus on core application logic. However, for the applications with the highest performance needs, the standard approach is not enough; instead, painstaking performance engineering effort is needed for the code to take advantage of all available accelerators and exploit all the opportunities for optimization. The cost of this effort can make applications difficult to adapt to changes in requirements or to the newly available hardware. The ScaMP project is developing a novel programming system that offers a new approach for building modern applications with strong performance and scalability requirements. ScaMP stands for Scalable Machine Programming, and the project’s novelty is the way in which it leverages advances in machine learning and programming-language technology to capture users’ intent at the high level, translate that intent into a working implementation, make the generated code perform efficiently on a variety of platforms, and support its maintenance and evolution. ScaMP provides an iterative development model that combines extremely high-level specification with fine control over low-level implementation decisions and a high degree of performance portability. The impact of the ScaMP project will be to lower the cost of developing high-performance applications. ScaMP decomposes into four main layers. First, incremental multimodal specification starts from natural language and informal diagrams and refines them into precise component specifications written in safe stackable smart domain-specific languages. These DSLs make up the second layer of the system and can generate architecture-independent distributed code through Coq-proved algebraic rewrite rules. The next layer is correct-by-construction code-generator generation, which produces compiler backends for multiple heterogeneous architectures, supporting generation of highly optimized assembly code, guaranteeing correctness using Coq-proved translation validation. Both of these layers use learning, to infer both models of hardware platforms and strategies for optimizing for those platforms effectively; as well as formal methods, to create proof that programs were optimized correctly. Finally, the last layer supports lifetime monitoring, learning, and adaptation to manage the more "data-science" side of developing and evolving a heterogeneous software system, using measurement to drive regeneration and scaling out of higher-performance code.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.

调制解调器应用程序将极端可扩展性的需求与增强的复杂性相结合，为数百万个简单用户提供丰富的功能。在这种情况下，通过在预先存在的组件和系统软件的深层堆栈上构建程序员生产是实现的，从而使程序员可以专注于核心应用程序逻辑。但是，对于具有最高性能需求的应用程序，标准方法还不够。取而代之的是，代码需要艰苦的性能工程工作，以利用所有可用的加速器并利用所有优化机会。这项工作的成本可能使应用程序难以适应需求的变化或新可用的硬件。 SCAMP项目正在开发一种新颖的编程系统，该系统为建立具有强大性能和可伸缩要求的现代应用程序提供了新的方法。 SCAMP代表可扩展的机器编程，该项目的新颖性是它利用机器学习和编程语言技术的进步方式，可以在高级捕获用户的意图，将其转化为工作实现，使生成的代码在各种平台上有效地执行，并支持其维护和进化。 SCAMP提供了一个迭代开发模型，该模型将极高的高级规范与对低级实施决策和高度性能可移植性的良好控制结合在一起。 SCAMP项目的影响是降低开发高性能应用程序的成本。 Scamp分解为四个主要层。首先，增量多模式规范从自然语言和非正式图表开始，并将其完善成精确的组件规格，以安全堆叠的智能域特异性语言编写。这些DSL构成了系统的第二层，可以通过COQ-pred代数重写规则生成独立于架构的分布式代码。下一层是正确的构造代码生成器，它为多个异质体系结构生成编译器的后端，支持生成高度优化的装配代码，并使用COQ-pred-pread的翻译验证确保正确性。这两种层都使用学习，推断硬件平台的两个模型和为这些平台有效优化的策略；以及正式方法，以创建证明程序已正确优化。最后，最后一层支持终身监控，学习和适应，以管理开发和发展的“数据科学”方面，使用衡量方法来推动再生和扩大更高表现的代码。这项奖项反映了NSF的法定任务，并通过评估基础的Merit和Broadial和广泛的评估，以表现出珍贵的支持。