Towards "Mouldable Code" as a Better Approach to Synthesis of Efficient and Correct Software

将“可塑代码”作为合成高效、正确软件的更好方法

• 批准号: RGPIN-2017-05684
• 负责人: Kahl, Wolfram
• 金额: $ 1.46万
• 依托单位: McMaster University
• 依托单位国家: 加拿大
• 项目类别: Discovery Grants Program - Individual
• 财政年份: 2020
• 资助国家: 加拿大
• 起止时间: 2020-01-01 至 2021-12-31
• 项目状态: 已结题
• 来源: https://www.nserc-crsng.gc.ca/ase-oro/Details-Detailles_eng.asp?id=711763
• 关键词: Towards; Mouldable; Code; Better; Approach

Important parts of the supporting infrastructure for optimising code generators, in particular in compilers, consist of analyses of graphs, especially control-flow graphs and data-flow graphs. In addition, many of the optimisations enabled by these analyses are usefully understood as graph transformations. Interestingly, the program transformation literature almost exclusively concentrates on transformation of (higher-order) abstract syntax trees. This corresponds to the usual approach in a compiler context to first parse the given programs into abstract syntax trees, and then extract from these the necessary information to construct the graphs to be used for data-flow and control-flow analyses, while still considering the abstract syntax trees as the internal representation of the program. However, many of the transformations that are used for code optimisation, in particular in the back-ends of compilers, act on patterns that can usefully be thought of as graph patterns, and the resulting transformations are frequently explained in the literature as graph transformations applied to control-flow graphs and data-flow graphs. In this research programme, I aim to create the theoretical justifications for control-flow graph transformation and data-flow graph transformations by linking the theories of control-flow and data-flow semantics with appropriate theories of graph transformation and build on these foundations a mechanised framework for nested code graph transformation. The goal of this framework is to be the first representative of a new class of mechanised environments in which experts can design special-purpose optimisation passes in a graph-based formalism that captures the intuitive graph-based descriptions of optimisation passes as they are customary in the compiler literature. However, while the graph-based descriptions in the literature are technically completely informal, the envisaged mechanised system will support not only capturing the design itself, but also proving the correctness of these optimisations at a level that is conceptually close to the design, and will finally also automatically generate correct-by-construction implementations of these optimisation passes.

优化代码生成器的支持基础设施的重要部分，特别是在编译器中，包括对图形的分析，特别是控制流图和数据流图。此外，这些分析实现的许多优化都被有用地理解为图形转换。 有趣的是，程序转换文献几乎完全集中在(高阶)抽象语法树的转换上。这对应于编译器上下文中的常见方法，即首先将给定程序解析成抽象语法树，然后从这些抽象语法树中提取必要的信息，以构建用于数据流和控制流分析的图，同时仍将抽象语法树视为程序的内部表示。 然而，用于代码优化的许多转换，特别是在编译器的后端中，作用于可以有用地认为是图形模式的模式，并且所产生的转换在文献中经常被解释为应用于控制流图和数据流图的图形转换。 在这个研究计划中，我的目标是通过将控制流和数据流语义的理论与适当的图转换理论联系起来，创建控制流图转换和数据流图转换的理论理由，并在这些基础上建立嵌套代码图转换的机械化框架。 这个框架的目标是成为一类新的机械化环境的第一个代表，在这种环境中，专家可以用基于图形的形式来设计特殊目的的优化通道，该图形基于图形的形式捕获了对优化通道的直观的基于图形的描述，因为它们在编译器文献中是惯例的。然而，尽管文献中基于图形的描述在技术上是完全非正式的，所设想的机械化系统将不仅支持捕获设计本身，而且将在概念上接近设计的水平上证明这些优化的正确性，并且最终还将自动生成这些优化通道的按构造正确的实现。