Stacked borrows, an aliasing model for Rust

栏目: IT技术 · 发布时间: 4年前

Type systems are useful not just for the safety guarantees they provide, but also for helping compilers generate more efficient code by simplifying important program analyses. In Rust, the type system imposes a strict discipline on pointer aliasing, and it is an express goal of the Rust compiler developers to make use of that alias information for the purpose of program optimizations that reorder memory accesses. The problem is that Rust also supports unsafe code, and programmers can write unsafe code that bypasses the usual compiler checks to violate the aliasing discipline. To strike a balance between optimizations and unsafe code, the language needs to provide a set of rules such that unsafe code authors can be sure, if they are following these rules, that the compiler will preserve the semantics of their code despite all the optimizations it is doing.

In this work, we propose Stacked Borrows , an operational semantics for memory accesses in Rust. Stacked Borrows defines an aliasing discipline and declares programs violating it to have undefined behavior , meaning the compiler does not have to consider such programs when performing optimizations. We give formal proofs (mechanized in Coq) showing that this rules out enough programs to enable optimizations that reorder memory accesses around unknown code and function calls, based solely on intraprocedural reasoning. We also implemented this operational model in an interpreter for Rust and ran large parts of the Rust standard library test suite in the interpreter to validate that the model permits enough real-world unsafe Rust code.


以上就是本文的全部内容,希望对大家的学习有所帮助,也希望大家多多支持 码农网

查看所有标签

猜你喜欢:

本站部分资源来源于网络,本站转载出于传递更多信息之目的,版权归原作者或者来源机构所有,如转载稿涉及版权问题,请联系我们

千夫所指

千夫所指

乔恩·罗森 / 王岑卉 / 九州出版社 / 2016-10-1 / CNY 42.80

编辑推荐: 《乌合之众》是为了跪舔权贵?《普通心理学》实验存在重大漏洞?《引爆点》的理论都是瞎掰的?社交网络时代《1984》预言的“老大哥”是否已经变成事实? 《纽约时报》年度十佳书 《GQ》杂志年度十佳书 《卫报》年度十佳书 《泰晤士报》年度十佳书 《经济学人》年度重推! 黑天鹅年度重点图书! 《乌合之众》是为了迎合权贵?《普通心理学》实验存在重大......一起来看看 《千夫所指》 这本书的介绍吧!

JS 压缩/解压工具
JS 压缩/解压工具

在线压缩/解压 JS 代码

SHA 加密
SHA 加密

SHA 加密工具

正则表达式在线测试
正则表达式在线测试

正则表达式在线测试