Tree Borrows | Hacker News

LinkTree Borrows – Programming Language Foundations Lab | ETH Zurich
https://plf.inf.ethz.ch/research/pldi25-tree-borrows.html#

📌 Summary:
本篇介紹了由蘇黎世聯邦理工學院（ETH Zurich）Programming Language Foundations Lab 發表的「Tree Borrows」機制，旨在更精確定義 Rust 程式語言中「unsafe」代碼的行為邊界，以保障記憶體安全與資料競爭防止。Rust 採用以所有權（ownership）為基礎的型別系統，能有效避免記憶體錯誤，但對於 unsafe 代碼，編譯器無法自動保證安全，需程式設計師自行維持。過去的 Stacked Borrows 規則雖達到此目的，但過於嚴格，排除了不少真實世界常見的 unsafe 程式碼模式，且未能涵蓋新版 Rust 借用檢查器的多項先進特性。Tree Borrows 則以樹狀結構取代原本的堆疊模型，不僅降低不合法拒絕率達 54%，也保留並擴展過去 Stack Borrows 的優化能力，如允許「讀讀重排序」(read-read reorderings)。該方法配合形式化證明（使用 Rocq 工具），同時提供實務測試與理論基礎，提升 Rust 編譯器及其社羣在處理 unsafe 代碼時的正確性與效率，並於 PLDI 2025 獲頒優秀論文獎。

🎯 Key Points:
★ Rust 的所有權型別系統與 unsafe：
→ Rust 以所有權與借用檢查器確保記憶體安全，但 unsafe 區塊允許逃避此檢查。
→ unsafe 代碼需明確界定「行為合法性」，以支持編譯器優化且避免未定義行為（UB）。

★ Stacked Borrows 的限制與 Tree Borrows 的創新：
→ Stacked Borrows 模型以堆疊方式追蹤指標借用，導致真實 unsafe 代碼中常見模式無法通過檢查。
→ Tree Borrows 改以樹狀結構呈現借用狀態，允許多分支借用及更靈活的指標追蹤，降低錯誤拒絕率。
→ 實證於近 30,000 個熱門 Rust 套件，Tree Borrows 拒絕的錯誤測試案例較 Stacked Borrows 下降 54%。

★ 性能及形式化驗證成果：
→ Tree Borrows 不僅保持 Stacked Borrows 的多數編譯器優化適用性，亦引入了像是讀讀重排序等新優化方式。
→ 使用 Rocq 工具進行形式化證明，確保模型對 unsafe 行為的正確界定與屬性保障。
→ 本研究結果有助 Rust 編譯器及其工具鏈更準確地處理 unsafe 代碼，提升安全性與效能。

🔖 Keywords:
#Rust_程式語言 #所有權系統 #unsafe_code #借用檢查器 #Tree_Borrows