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

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

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.