Semantic reasoning about the sea of nodes
Semantic reasoning about the sea of nodes
复制标题
节点海的语义推理
DOI：
--
复制
发表时间：
2018
期刊：
影响因子：
--
通讯作者：
David Pichardie
中科院分区：
文献类型：
--
作者：
Delphine Demange;Yon Fernández de Retana;David Pichardie
Sea of Nodes 中间表示由 Cliff Click 在 90 年代中期引入，作为增强的静态单一分配 (SSA) 形式。它通过将基本块中指令的总顺序放松为显式数据和控制依赖性来改进初始 SSA 形式。这使得程序的优化更加灵活。这种基于图形的表示现在已用于许多工业级编译器，例如 HotSpot 或 Graal。虽然现在从语义角度很好地理解了 SSA 形式——甚至经过正式验证的优化编译器也在中端使用它——但关于节点海的语义研究却很少。本文提出了节点海形式的简单但严格的形式语义。它包括表示数据计算的指示组件和表示控制流的操作组件。然后，我们在 Sea of Nodes 程序上证明了一个基本的、基于支配性的语义属性，它决定了保存节点值的图区域。最后，我们应用我们的结果来证明冗余零检查消除优化的语义正确性。所有必要的语义属性都已在 Coq 证明助手中进行了机械验证。
The Sea of Nodes intermediate representation was introduced by Cliff Click in the mid 90s as an enhanced Static Single Assignment (SSA) form. It improves on the initial SSA form by relaxing the total order on instructions in basic blocks into explicit data and control dependencies. This makes programs more flexible to optimize. This graph-based representation is now used in many industrial-strength compilers, such as HotSpot or Graal. While the SSA form is now well understood from a semantic perspective -- even formally verified optimizing compilers use it in their middle-end -- very few semantic studies have been conducted about the Sea of Nodes. This paper presents a simple but rigorous formal semantics for a Sea of Nodes form. It comprises a denotational component to express data computation, and an operational component to express control flow. We then prove a fundamental, dominance-based semantic property on Sea of Nodes programs which determines the regions of the graph where the values of nodes are preserved. Finally, we apply our results to prove the semantic correctness of a redundant zero-check elimination optimization. All the necessary semantic properties have been mechanically verified in the Coq proof assistant.