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 项目的影响将是降低开发高性能应用程序的成本。首先，增量多模态规范从自然语言和非正式图表开始，并将其细化为用安全的可堆叠智能领域特定语言编写的精确组件规范，这些 DSL 构成了系统的第二层，可以生成独立于体系结构的分布式。下一层是通过构造正确的代码生成器生成，它为多个异构架构生成编译器后端，支持生成高度优化的汇编代码，并使用 Coq 证明的翻译验证来保证正确性。这些层中的每一层都使用学习来推断硬件平台的模型和有效优化这些平台的策略，以及形式化方法，以创建程序已正确优化的证据最后一层支持生命周期监控、学习、和适应来管理开发和发展异构软件系统的更“数据科学”方面，使用测量来驱动再生和扩展更高性能的代码。该奖项反映了 NSF 的法定使命，并被认为值得通过评估获得支持利用基金会的智力优势和更广泛的影响审查标准。