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

调制解调器应用程序将极端可伸缩性的需求与巨大的复杂性结合起来，为数百万同时存在的用户提供丰富的功能。在这种情况下，程序员的生产力是通过构建预先存在的组件和系统软件的深层堆栈来实现的，从而允许程序员专注于核心应用程序逻辑。然而，对于具有最高性能需求的应用程序，标准方法是不够的；相反，代码需要进行艰苦的性能工程工作，以利用所有可用的加速器并利用所有优化机会。这种工作的成本可能使应用程序难以适应需求的变化或新的可用硬件。ScaMP项目正在开发一种新颖的编程系统，它为构建具有强大性能和可伸缩性需求的现代应用程序提供了一种新方法。ScaMP代表可扩展机器编程，该项目的新颖之处在于它利用先进的机器学习和编程语言技术在高层次上捕获用户的意图，将该意图转化为工作实现，使生成的代码在各种平台上有效地执行，并支持其维护和发展。ScaMP提供了一个迭代开发模型，它结合了非常高级的规范、对低级实现决策的精细控制和高度的性能可移植性。ScaMP项目的影响将是降低开发高性能应用程序的成本。ScaMP分解为四个主要层。首先，增量式多模态规范从自然语言和非正式图开始，并将它们细化为用安全可堆叠的智能领域特定语言编写的精确组件规范。这些dsl构成了系统的第二层，可以通过coq证明的代数重写规则生成与体系结构无关的分布式代码。下一层是按结构正确生成代码生成器，它为多个异构体系结构生成编译器后端，支持生成高度优化的汇编代码，并使用coq证明的翻译验证保证正确性。这两层都使用学习来推断硬件平台的模型和有效优化这些平台的策略；以及形式化的方法，来证明程序是正确优化的。最后，最后一层支持生命周期监控、学习和适应，以管理开发和发展异构软件系统的更“数据科学”的方面，使用度量来驱动更新和扩展更高性能的代码。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

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.