Synthesis and Analysis of Heap Data Structures

堆数据结构的综合与分析

• 批准号: 1160904
• 负责人: Alexander Aiken
• 金额: $ 84.84万
• 依托单位: Stanford University
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2012
• 资助国家: 美国
• 起止时间: 2012-05-01 至 2019-04-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1160904&HistoricalAwards=false
• 关键词: Synthesis; Analysis; Heap; Data; Structures

Almost all software today is developed in two stages. First, a human writes a program and subsequently various automated tools process that program to produce the actual computer code that is the software application. Over time, researchers have found ways to shift more of the burden of developing software from the programmer to the automated tools, which has gradually made software development more and more productive. One area of software development that has not changed for a couple of decades is the way in which the structure of data is programmed. The organization of data is still described in relatively low-level terms as links between individual objects in memory, which is too low-level for the tools to reason successfully about. As a result, programmers must spend significant time hand-coding and tuning their data structures, and there are significant missed opportunities for improvements to program performance, correctness, and security.We propose to try a new approach to this problem, consisting of two parts: we will synthesize data structures from high-level relational specifications. We will also use inference techniques to automatically analyze the program?s use of the relations. In a relational style of programming explicit pointers are eliminated, removing one of the biggest impediments to automatic reasoning. We believe recent advances in the analysis of control flow, destructive updates, and low-level indexing operations make it feasible to capture most other aspects of programs.If successful, programs, including concurrent programs, will be written at a higher level and be more easily retargeted to new situations because the data representations are not fixed in advance, and tools will be able to do a more reliable, efficient, and scalable job of optimizing resources and verifying properties of programs. As part of the project, we will seek to demonstrate these benefits by conducting studies of our techniques applied to realistic challenge applications.

当今几乎所有软件都是分两个阶段开发的。首先，人类编写程序，随后各种自动化工具处理该程序以生成实际的计算机代码，即软件应用程序。随着时间的推移，研究人员找到了将更多软件开发负担从程序员转移到自动化工具的方法，这逐渐使软件开发变得越来越高效。软件开发的一个领域几十年来一直没有改变，那就是数据结构的编程方式。数据的组织仍然以相对低级的术语描述为内存中各个对象之间的链接，这对于工具来说太低级了，无法成功推理。因此，程序员必须花费大量时间手动编码和调整数据结构，并且错失了改进程序性能、正确性和安全性的机会。我们建议尝试一种新方法来解决这个问题，该方法由两部分组成：我们将从高级关系规范中综合数据结构。 我们还将使用推理技术来自动分析程序对关系的使用。在关系风格的编程中，显式指针被消除，从而消除了自动推理的最大障碍之一。我们相信，控制流、破坏性更新和低级索引操作分析方面的最新进展使得捕获程序的大多数其他方面变得可行。如果成功，程序（包括并发程序）将在更高的级别上编写，并且更加高效。由于数据表示没有提前固定，因此很容易重新定位到新的情况，并且工具将能够更加可靠、高效和可扩展地优化资源和验证程序的属性。作为该项目的一部分，我们将通过研究应用于现实挑战应用的技术来寻求证明这些好处。