检索结果-内蒙古大学图书馆

42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI)

作者： Koenig, Jeremie Shao, Zhong Yale Univ New Haven CT 06520 USA

ISBN: (纸本)9781450383912

Since the introduction of CompCert, researchers have been refining its language semantics and correctness theorem, and used them as components in software verification efforts. Meanwhile, artifacts ranging from CPU designs to network protocols have been successfully verified, and there is interest in making them interoperable to tackle end-to-end verification at an even larger scale. Recent work shows that a synthesis of game semantics, refinement-based methods, and abstraction layers has the potential to serve as a common theory of certified components. Integrating certified compilers to such a theory is a critical goal. However, none of the existing variants of CompCert meets the requirements we have identified for this task. CompCertO extends the correctness theorem of CompCert to characterize compiled program components directly in terms of their interaction with each other. Through a careful and compositional treatment of calling conventions, this is achieved with minimal effort.

关键词： compositional compiler correctness Game Semantics Simulation Convention Language Interface

来源：评论

学校读者我要写书评

暂无评论

compositional Optimizations for CertiCoq

引用

PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL 2021年第ICFP期5卷 1–30页

作者： Paraskevopoulou, Zoe Li, John M. Appel, Andrew W. Northeastern Univ Boston MA 02115 USA Princeton Univ Princeton NJ 08544 USA

compositional compiler verification is a difficult problem that focuses on separate compilation of program components with possibly different verified compilers. Logical relations are widely used in proving correctness of program transformations in higher-order languages;however, they do not scale to compositional verification of multi-pass compilers due to their lack of transitivity. The only known technique to apply to compositional verification of multi-pass compilers for higher-order languages is parametric inter-language simulations (PILS), which is however significantly more complicated than traditional proof techniques for compiler correctness. In this paper, we present a novel verification framework for lightweight compositional compiler correctness. We demonstrate that by imposing the additional restriction that program components are compiled by pipelines that go through the same sequence of intermediate representations, logical relation proofs can be transitively composed in order to derive an end-to-end compositional specification for multi-pass compiler pipelines. Unlike traditional logical-relation frameworks, our framework supports divergence preservationDeven when transformations reduce the number of program steps. We achieve this by parameterizing our logical relations with a pair of relational invariants. We apply this technique to verify a multi-pass, optimizing middle-end pipeline for CertiCoq, a compiler from Gallina (Coq's specification language) to C. The pipeline optimizes and closure-converts an untyped functional intermediate language (ANF or CPS) to a subset of that language without nested functions, which can be easily code-generated to low-level languages. Notably, our pipeline performs more complex closure-allocation optimizations than the state of the art in verified compilation. Using our novel verification framework, we prove an end-to-end theorem for our pipeline that covers both termination and divergence and applies to whole-progr

关键词： compositional compiler correctness logical relations separate compilation compilation by transformation A-normal form closure conversion lambda lifting

来源：评论

学校读者我要写书评

暂无评论

Verified Optimizations for Functional Languages

Verified Optimizations for Functional Languages

引用

作者： Paraskevopoulou, Zoe Princeton University

学位级别：Ph.D.

Coq is one of the most widely adopted proof development systems. It allows programmers to write purely functional programs and verify them against specifications with machine-checked proofs. After verification, one can use Coq’s extraction plugin to obtain a program (in OCaml, Haskell, or Scheme) that can be compiled and executed. However, bugs in either the extraction function or the compiler of the extraction language may cause the executable to exhibit unexpected behaviors, rendering source-level verification futile. A verified compiler is a compiler whose output provably preserves the semantics of the source language. CertiCoq is a verified compiler, currently under development, for Coq’s specification language, Gallina. CertiCoq targets Clight, a subset of the C language, that can be compiled with the CompCert verified compiler to obtain a certified executable, bridging the gap between the formally verified source program and the compiled target program. For proving CertiCoq correct, I develop a framework based on the technique of logical relations, making novel technical contributions. I extend logical relations with notions of relational preconditions and postconditions that facilitate reasoning about the resource consumption of programs simultaneously with functional correctness. I demonstrate how this enables reasoning about preservation of non-terminating behaviors, which is not supported by traditional logical relations. Moreover, I develop a novel, lightweight technique that allows logical-relation proofs to be composed in order to obtain a top-level compositional compiler correctness theorem. This technique is used to obtain a separate compilation theorem that guarantees that programs compiled separately through CertiCoq, perhaps using different sets of optimizations, can be safely linked at the target level. Lastly, I use the framework to prove that CertiCoq’s closure conversion is not only functionally correct but also safe for time and space, meaning

关键词： compiler correctness compositional compiler correctness Coq functional programming languagegs logical relations

来源：评论

学校读者我要写书评

暂无评论

A Kripke Logical Relation Between ML and Assembly 11

A Kripke Logical Relation Between ML and Assembly

引用

38th Symposium on Principles of Programming Languages

作者： Hur, Chung-Kil Dreyer, Derek Max Planck Institute for Software Systems Saarbruecken Germany

ISBN: (纸本)9781450304900

There has recently been great progress in proving the correctness of compilers for increasingly realistic languages with increasingly realistic runtime systems Most work on this problem has focused on proving the correctness of a particular compiler, leaving open the question of how to verify the correctness of assembly code that is hand-optimized or linked together from the output of multiple compilers. 'This has led Benton and other researchers to propose more abstract, compositional notions of when a low-level program correctly realizes a high-level one. However, the state of the art in so-called "compositional compiler correctness" has only considered relatively simple high-level and low-level languages. In this paper, we propose a novel, extensional, compiler-independent notion of equivalence between high-level programs in an expressive, impure ML-like lambda-calculus and low-level programs in an (only slightly) idealized assembly language. We define this equivalence by mean 3 of a biorthogonal, step-indexed, Kripke logical relation, which enables us to reason quite flexibly about assembly code that uses ocal state in a different manner than the high-level code it implements (e.g., self-modifying code). In contrast to prior work, we factor our relation in a symmetric, language-generic fashion, which helps to simplify and clarify the formal presentation, and vie also show how to account for the presence of a garbage collector. Our approach relies on recent developments in Kripke logical relations for ML-like languages, in particular the idea of possible worlds as state transition systems.

关键词： Step-indexed Kripke logical relations biorthogonality compositional compiler correctness garbage collection self-modifying code

来源：评论

学校读者我要写书评

暂无评论

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：