苏黎世联邦理工学院的编程语言基础实验室专注于编程语言的研究，包括树借用（Tree Borrows）等主题。该实验室提供教育课程和学生项目，致力于推动编程语言理论的发展。

主要内容总结

文章介绍了Tree Borrows，这是由ETH Zurich的编程语言基础实验室（Programming Language Foundations Lab）提出的一种新的内存管理模型，旨在解决Rust编程语言中unsafe代码的优化问题。

背景

Rust以其基于所有权的类型系统著称，能够提供内存安全和数据竞争自由等强保证。然而，Rust也提供了unsafe代码的“逃生舱”，这些代码的安全性无法自动保证，需要程序员手动维护。这导致了一个矛盾：编译器希望利用类型系统的强保证（特别是关于指针别名的规则）来进行强大的过程内优化，但这些优化容易被“行为不良”的unsafe代码破坏。因此，必须明确定义什么是“行为不良”的unsafe代码。

现有问题

在之前的工作中，Stacked Borrows模型定义了一组规则来解决这个问题，但它排除了实际Rust代码中常见的几种模式，并且没有考虑到Rust借用检查器引入的先进特性。

Tree Borrows的提出

Tree Borrows通过将Stacked Borrows中的栈结构替换为树结构，克服了上述限制。通过对30,000个最广泛使用的Rust crate进行评估，Tree Borrows比Stacked Borrows少拒绝了54%的测试用例。此外，研究团队在Rocq中证明了Tree Borrows保留了Stacked Borrows的大部分优化，并启用了重要的新优化，特别是读-读重排序。

主要贡献

• Tree Borrows模型通过树结构改进了Rust的unsafe代码优化。
• 评估表明，Tree Borrows在实际代码中的表现优于Stacked Borrows。
• 研究团队在Rocq中证明了Tree Borrows的优化能力。

相关资源

• 论文 (PDF)
• 实验数据
• 源代码

荣誉

该研究在PLDI'25会议上获得了Distinguished Paper Award（杰出论文奖）。

图片

其他信息

文章还提供了ETH Zurich的相关导航链接、服务信息以及关于Cookie使用的说明。

1. 关于Stacked Borrows的历史讨论

   • 评论1提到Stacked Borrows在2020年和2018年已有相关讨论，并提供了相关链接。
     • "The Stacked Borrows mentioned had threads in 2020 and 2018"
     • 链接：2020年讨论、2018年讨论

2. Ralf Jung的最新博客和演讲

   • 评论2提到Ralf Jung最近的博客文章和演讲，提供了关于Rust操作语义的额外背景信息。
     • "Recent blog post from Ralf Jung providing some extra context"
     • "Bonus: recent talk from Ralf Jung on his group's efforts to precisely specify Rust's operational semantics"

3. 关于unsafe代码的讨论

   • 评论3对论文中关于unsafe代码的示例提出质疑，认为使用指针创建多个可变引用是未定义行为。
     • "No it can't? Using pointers to coexist multiple mutable references to the same variable is undefined behavior."
     • "Unless I'm just misunderstanding the point they're trying to make here."

4. 作者背景的发现

   • 评论4指出论文作者之一Neven Villani是2010年菲尔兹奖得主Cédric Villani的儿子，感叹其学术背景的传承。
     • "Just realised that one of the author, Neven Villani, is Cédric Villani's (Fields Medal 2010) son."
     • "Apples don't fall far from the tree, indeed."

5. 关于Rust未来发展的设想

   • 评论5提出疑问，Rust或未来的编程语言是否会允许选择不同的借用检查器实现，以平衡编译速度、运行速度等特性。
     • "I wonder if Rust or future PL would evolve into allowing multiple borrow checker implementations with varying characteristics"
     • "that projects can choose from."