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

SHF：小型：协作研究：资源引导程序综合

• 批准号: 1812876
• 负责人: Jan Hoffmann
• 金额: $ 25万
• 依托单位: Carnegie-Mellon University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2018
• 资助国家: 美国
• 起止时间: 2018-06-01 至 2021-05-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1812876&HistoricalAwards=false
• 关键词: SHF; Small; Collaborative; Research; Resource

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.

RESYN项目的目标是通过推进计划合成的最新技术来自动化有效计划的开发。程序合成是一种新兴技术，用于自动从其必须执行的任务的高级描述中生成程序。但是，对于任何给定的任务，通常有许多程序可以执行相同的功能，但在使用计算资源（例如时间，内存或能量）方面有所不同。大多数最先进的合成工具不会建模或分析资源使用情况。通过在合成过程中考虑对候选程序的资源消耗，Resyn能够合成可证明的有效程序，以及针对具有特定资源需求的平台的定制程序。该项目涉及这项研究的研究生和本科生。为了利用合成过程中的资源使用信息，研究人员结合了两种最新技术：类型驱动的程序合成和自动化的摊销资源分析。首先，他们开发了一种新颖的资源感知精炼类型系统，该系统将两种技术的核心统一性类型系统统一。接下来，基于此类型系统，研究人员构建了一种新的类型驱动的合成引擎，能够根据其资源消耗进行修剪和优先搜索程序。最后，他们评估了三个相关应用程序域中的合成引擎：无服务器计算，智能合约和侧通道攻击的预防。该项目中开发的课程材料和研究产品将被免费获得。该奖项反映了NSF的法定任务，并被认为是值得通过基金会的知识分子和更广泛影响的评论标准来评估值得支持的。

项目成果

Type-guided worst-case input generation

• DOI: 10.1145/3290326
• 发表时间: 2019-01
• 期刊: Proceedings of the ACM on Programming Languages
• 作者: Di Wang;Jan Hoffmann

Automatic amortized resource analysis with the Quantum physicist’s method

• DOI: 10.1145/3473581
• 发表时间: 2021-06
• 期刊: Proceedings of the ACM on Programming Languages
• 作者: David M. Kahn;Jan Hoffmann

Automatic Space Bound Analysis for Functional Programs with Garbage Collection

具有垃圾收集的功能程序的自动空间限制分析

• DOI: 10.29007/xkwx
• 发表时间: 2018
• 期刊: EPiC Series in Computing
• 作者: Niu, Yue;Hoffmann, Jan
• 通讯作者: Hoffmann, Jan

Liquid Resource Types

液体资源类型

• 发表时间: 2020
• 期刊: Proceedings of the ACM on programming languages
• 作者: Knoth, Tristan;Reynolds, Adam;Wang, Di;Hoffmann, Jan;Polikarpova, Nadia
• 通讯作者: Polikarpova, Nadia

A unifying type-theory for higher-order (amortized) cost analysis

高阶（摊销）成本分析的统一类型理论

• DOI: 10.1145/3434308
• 发表时间: 2021
• 期刊: Proceedings of the ACM on Programming Languages
• 作者: Rajani, Vineet;Gaboardi, Marco;Garg, Deepak;Hoffmann, Jan
• 通讯作者: Hoffmann, Jan