SHF: Small: Collaborative Research: Resource-Guided Program Synthesis

RESYN项目的目标是通过提高程序合成技术的水平来实现高效程序的自动化开发。程序合成是一种新兴技术，用于根据程序必须执行的任务的高级描述自动生成程序。然而，对于任何给定的任务，通常有许多程序执行相同的功能，但它们对计算资源（如时间、内存或能量）的使用不同。大多数最先进的合成工具不建模也不分析资源使用情况。RESYN在合成过程中考虑候选程序的资源消耗，既可以合成可证明高效的程序，也可以针对具有特定资源需求的平台定制程序。该项目涉及研究生和本科生。为了在合成过程中利用资源使用信息，研究人员结合了两种最新技术：类型驱动程序合成和自动平摊资源分析。首先，他们开发了一种新的资源感知的细化类型系统，该系统将两种技术的核心表达型类型系统统一起来。接下来，在这个类型系统的基础上，研究人员建立了一个新的类型驱动的合成引擎，能够根据程序的资源消耗来修剪和优先搜索程序。最后，他们在三个相关的应用领域评估了合成引擎：无服务器计算、智能合约和防止侧信道攻击。在这个项目中开发的课程材料和研究成果将免费提供。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

The goal of the RESYN project is to automate the development of efficient programs by advancing the state of the art in program synthesis. Program synthesis is an emerging technology for automatically generating programs from high-level descriptions of the task they must perform. For any given task, however, there are generally many programs that perform the same function, but differ in their use of computing resources, such as time, memory, or energy. Most state-of-the-art synthesis tools do not model nor analyze resource usage. By taking resource consumption of candidate programs into account during synthesis, RESYN is able to synthesize provably efficient programs, as well as customized programs for platforms with specific resource requirements. The project involves graduate and undergraduate students in this research.To leverage resource usage information during synthesis, the investigators combine two recent techniques: type-driven program synthesis and automated amortized resource analysis. First, they develop a novel resource-aware refinement type system, which unifies the expressive type systems at the core of the two techniques. Next, based on this type system, the investigators build a new type-driven synthesis engine, capable of pruning and prioritizing the search for programs based on their resource consumption. Finally, they evaluate the synthesis engine in three relevant application domains: server-less computing, smart contracts, and prevention of side-channel attacks. The course materials and research products developed in this project will be made freely available.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.