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

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

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.