CAREER: The Next 700 Solver-Aided Languages

软件是现代基础设施的重要组成部分，而编程是从物理到生物再到社会科学等许多领域知识工作的重要组成部分。然而，将算法和想法转化为代码并不是一件容易的事情，而且错误可能代价高昂。脚本中的错误可能会使科学结果无效，文件系统中的错误可能会导致灾难性的数据丢失。该项目通过一种新的编程方法使系统程序员和科学家的编程变得更容易，该方法使用用于程序验证和综合的求解器辅助工具自动化特定于域的语言(DSL)。智力上的优点是提高了编程方面的知识，支持特定领域的验证和综合，共同设计语言和工具，并将求解器辅助编程应用到新的领域。该项目的更广泛的意义和重要性是将求解器辅助编程的范围扩展到数量级和数千名程序员，促进具有社会、教育和工业影响的新应用程序。该项目的关键思想是使验证和综合工具像由广泛的程序员开发的DSL一样简单，这些工具通常由计算机科学博士手工制作。PI之前在求解器辅助语言方面的工作证明了这是可能的，使从专业开发人员到高中生的广泛程序员能够快速构建用于各种领域的合成和验证工具，从放射治疗软件到低功率计算到K-12教育。由此产生的工具基于对可满足性模理论(SMT)的简化求解，因此依赖于(1)从根本上难以解决的技术，(2)需要多年的经验和培训才能有效地使用。因此，该提案的目标是解决求解器辅助编程的核心挑战：使非专家能够诊断和优化求解器辅助工具的性能。为了实现这一目标，该项目开发了以下自动化技术：(1)符号分析，以提供关于整个解算器辅助堆栈中可伸缩性瓶颈的原因的诊断信息；(2)符号优化，以通过代码重构、(元)草图挖掘和求解引擎的组合来缓解已识别的可伸缩性瓶颈；以及(3)应用程序，作为评估符号分析和优化的新挑战问题，以及作为吸引从计算机架构师到教育专家的不同用户群的演示。

Software is a critical part of modern infrastructure, and programming is an essential part of knowledge work in many fields, from physics to biology to social science. Yet translating algorithms and ideas into code is no easy task, and mistakes can be costly. A bug in a script can invalidate scientific results, and a bug in a file system can cause catastrophic loss of data. This project makes programming easier for systems programmers and scientists alike, through a novel approach to programming that automates domain-specific languages (DSLs) with solver-aided tools for program verification and synthesis. The intellectual merits are to advance knowledge in programming support for domain-specific verification and synthesis, in co-design of languages and tools, and in applying solver-aided programming to new domains. The project's broader significance and importance are to extend the reach of solver-aided programming by orders of magnitude and to thousands of programmers, facilitating new applications with societal, educational, and industrial impact.The project's key idea is to make verification and synthesis tools, which are usually hand-crafted by computer science PhDs, as simple to build as DSLs, which are developed by a broad spectrum of programmers. The PI's prior work on solver-aided languages has demonstrated that this is possible, enabling a wide range of programmers, from professional developers to high-school students, to rapidly construct synthesis and verification tools for a variety of domains, from radiation therapy software to low-power computing to K-12 education. The resulting tools are based on reduction to Satisfiability Modulo Theories (SMT) solving, and as such, rely on technology that is (1) fundamentally intractable and (2) requires years of experience and training to use effectively. The goal of this proposal is thus to address the central challenge of solver-aided programming: enabling non-experts to diagnose and optimize the performance of solver-aided tools. To achieve this goal, the project develops automatic techniques for (1) symbolic profiling to provide diagnostic information about the causes of scalability bottlenecks across the solver-aided stack; (2) symbolic optimization to mitigate the identified scalability bottlenecks via code refactoring, (meta)sketch mining, and combination of solving engines; and (3) applications to serve as new challenge problems for evaluating symbolic profiling and optimization, and as demos for attracting a diverse population of users, from computer architects to education experts.