Tree Borrows: Mô hình quy tắc aliasing cho mã unsafe của Rust
(plf.inf.ethz.ch)- Để trình biên dịch Rust tận dụng bảo đảm aliasing của con trỏ cho tối ưu hóa, cần phải định nghĩa rõ unsafe code vi phạm quy tắc ở đâu
- Mô hình Stacked Borrows trước đây đã đưa ra tiêu chuẩn đó, nhưng chưa đủ chấp nhận các mẫu phổ biến trong mã unsafe Rust thực tế và các tính năng mới của borrow checker
- Tree Borrows thay cấu trúc cốt lõi của Stacked Borrows từ stack sang tree, nhờ đó có thể biểu diễn nhiều mẫu hợp lệ hơn
- Khi đánh giá trên 30.000 crate Rust được dùng nhiều nhất, số test case bị từ chối ít hơn 54% so với Stacked Borrows
- Chứng minh bằng Rocq xác nhận có thể giữ lại phần lớn các tối ưu hóa hiện có, đồng thời cho phép cả tối ưu hóa mới như read-read reordering
Quy tắc aliasing cần thiết trong unsafe Rust
- Rust cung cấp các bảo đảm mạnh như an toàn bộ nhớ và ngăn chặn data race nhờ hệ thống kiểu dựa trên quyền sở hữu
- Tuy vậy, trong vùng unsafe code, tính an toàn không còn được bảo đảm tự động, và cần có các quy tắc riêng mà lập trình viên phải tuân thủ
- Trình biên dịch muốn tận dụng các bảo đảm của hệ thống kiểu, đặc biệt là thông tin liên quan đến aliasing của con trỏ, để tăng cường tối ưu hóa bên trong hàm
- Mã unsafe viết sai có thể phá vỡ các tối ưu hóa này, nên việc có tiêu chuẩn rõ ràng để xem mã nào là “badly behaved” là rất quan trọng
- Nghiên cứu trước đây Stacked Borrows đã định nghĩa tiêu chuẩn này, nhưng vẫn có giới hạn
- Từ chối nhiều mẫu vốn phổ biến trong mã unsafe Rust thực tế
- Chưa phản ánh được các tính năng nâng cao mới được đưa vào borrow checker của Rust
Cách tiếp cận của Tree Borrows và kết quả đánh giá
- Tree Borrows được định nghĩa bằng cách thay stack, cấu trúc trung tâm của Stacked Borrows, bằng tree
- Thay đổi cấu trúc này giúp nới lỏng các hạn chế của mô hình cũ
- Khi đánh giá trên 30.000 crate Rust được dùng nhiều nhất, số test case bị từ chối giảm 54% so với Stacked Borrows
- Chứng minh bằng Rocq cũng xác nhận các tính chất liên quan đến tối ưu hóa
- Giữ lại phần lớn các tối ưu hóa mà Stacked Borrows cho phép
- Đồng thời cho phép tối ưu hóa mới quan trọng là read-read reorderings
- Tree Borrows đã nhận PLDI'25 Distinguished Paper Award
- Tài liệu liên quan
1 bình luận
Ý kiến trên Hacker News
Bonus: cũng có bài thuyết trình gần đây của nhóm Ralf Jung về việc đặc tả chính xác, dưới dạng có thể thực thi, ngữ nghĩa thực thi của Rust bằng một phương ngữ Rust: https://youtube.com/watch?v=yoeuW_dSe0o
Torvalds từ lâu đã lập luận rằng strict aliasing rule của C hại nhiều hơn lợi, và nghe khá thuyết phục. Ví dụ ở đây: https://lore.kernel.org/all/CAHk-=wgq1DvgNVoodk7JKc6BuU1m9Un... Nếu quan tâm chủ đề này thì toàn bộ thread cũng đáng đọc
Dựa trên trải nghiệm hạn chế của tôi, Rust về cơ bản có khác không thì có vẻ là không. Ít nhất là càng không khi có unsafe tham gia
Tôi cho rằng chúng hữu ích hơn cho compiler và ít gây gánh nặng hơn cho programmer. Ngoài ra, trong ngôn ngữ cũng thực sự có cách thoát: dùng raw pointer. Và cũng có công cụ để kiểm tra code
Sau cùng, cũng như mọi thứ trong thiết kế ngôn ngữ, đây là một sự đánh đổi; tôi nghĩ có thể Rust đã tìm được một sweet spot mới cho kiểu tối ưu hóa này. Đúng hay không thì thời gian sẽ trả lời
Trong C có một thứ như “vũ khí hạt nhân” là
restrict, nhưng theo kinh nghiệm của tôi với clang và gcc thì nó chỉ có tác dụng gì đó khi gắn vào tham số hàm. Phân tích aliasing dựa trên kiểu nói chung khó dùng, và bạn cũng không thể, cũng như có lẽ không muốn, tạo vô hạn bản sao của kiểuint64_t. Việc bị buộc phải dùngmemcpyđể diễn giải lại thành kiểu khác cũng phiềnTrong khi đó, reference của Rust được ranh giới hóa rất chi tiết theo lifetime, scope và mutability, và không quá bận tâm đến chính kiểu “vật lý”. Vì vậy có thể diễn giải lại và chuyển đổi cùng một vùng nhớ giữa
&mut i32/&i32và&mut i64/&i64. Miễn là abstraction unsafe không đưa ra các reference&mutchồng lấn đồng thời, hoặc chia một&mutthành nhiều&mutkhông chồng lấn, thì bằng các thao tác đọc/ghi Rust safe bình thường vẫn có thể đọc và ghi nửa giá trị hoặc nhiều giá trịPhân tích aliasing rất quan trọng để đạt hiệu năng tốt ngày nay. Tuy nhiên cũng cần nhớ rằng lợi ích lớn nhất đến từ các heuristic đơn giản nhất. Ví dụ, hai lần load dùng cùng một giá trị SSA làm pointer thì chắc chắn alias với nhau
Từ góc nhìn LLVM, BasicAA đảm nhiệm vai trò đó. Nó là một tập hợp heuristic đơn giản gần như “nếu có thể truy vết điểm cấp phát của object thì giải dứt khoát truy vấn alias, nếu không thì không biết”
Câu hỏi thật sự là giá trị của phân tích aliasing vượt ra ngoài các kiểm tra cơ bản và hiển nhiên. Khi truy vấn alias không còn được giải một cách tầm thường nữa, những việc có thể làm từ kết quả đó nhìn chung cũng giảm mạnh, gần như chỉ còn tìm rủi ro khi di chuyển code. Lợi ích của nó nhỏ hơn nhiều
Một thí nghiệm tôi muốn làm là đo tổng mức tăng tốc mà một phân tích aliasing hoàn hảo về mặt lý thuyết sẽ mang lại. Tôi đoán ngay cả với code không phải HPC như kernel Linux thì cũng vào khoảng 20%
[1] Điều này không bao gồm các tối ưu hóa “anh hùng” như chuyển đổi bố cục dữ liệu mà ta sẽ không thử nếu không có phân tích aliasing chất lượng cao. Vì thực tế ta đã biết không có phân tích aliasing như vậy, nên cũng sẽ không thử các tối ưu hóa đó, và tôi cho rằng không đáng đưa chúng vào mức tăng tốc dự kiến
Aliasing của C chỉ dựa trên kiểu, vì vậy tên gọi khác của nó cũng là phân tích aliasing dựa trên kiểu hay TBAA
Tôi tìm thấy tuyên bố rằng
noaliasđóng góp khoảng 5% cải thiện hiệu năng tính theo thời gian chạy, nhưng rõ ràng tài liệu đó đã rất cũhttps://github.com/rust-lang/rust/issues/54878#issuecomment-...
https://news.ycombinator.com/item?id=22281205
https://news.ycombinator.com/item?id=17715399
Nhìn theo phần giải thích, nếu tạo
*mut i32từ&mut, rồi dùng*x = 10thay vìwrite(x), thì vì không dùng implicit two-phase borrow nên compiler phải từ chối, nhưng thực tế lại pass*x = 10;sẽ báo lỗi còn bảnwrite(x);thì khôngLỗi có dạng “Undefined Behavior: attempting a write access using [...] but that tag does not exist in the borrow stack for this location”
Bản thân rustc không có lý do gì để từ chối bất kỳ trường hợp nào trong hai trường hợp đó. Vì
ylà*mut, và từ góc nhìn của hệ thống kiểu tại thời điểm biên dịch thì nó không có quan hệ mượn hay vòng đời với&mutlàx.Borrow checker hiện tại dùng một phân tích hạn chế hơn nên không phát hiện được xung đột cụ thể này giữa con trỏ thô và tham chiếu khả biến
Theo kinh nghiệm thực tế [1] [2], nó cũng cho phép những đoạn mã hợp lý nhưng bị coi là bất hợp pháp trong Stacked Borrows
[1] https://github.com/Voultapher/sort-research-rs/blob/main/wri... cột Miri
[2] https://github.com/rust-lang/rust/blob/6b3ae3f6e45a33c2d95fa...
Nó đã chuyển từ borrow checker dựa trên phạm vi sang borrow checker với vòng đời phi từ vựng, và triển khai thử nghiệm Polonius tiếp theo cũng có thể được bật như một tùy chọn. Tuy nhiên khi triển khai mới sẵn sàng cho production thì triển khai cũ sẽ bị bỏ, vì không có lý do gì để chọn nó nữa
Kiểm tra mượn rất nhanh, và triển khai mới chấp nhận một cách nghiêm ngặt nhiều chương trình đúng hơn
Ngoài ra còn có các kiểu
RcvàRefCell, cho phép linh hoạt hơn với cái giá là kiểm tra ở runtimeTất cả đều có chi phí và năng lực khác nhau về mặt triển khai, hiệu năng và trải nghiệm lập trình viên
Và điều mà phần lớn các ngôn ngữ ngoài Rust thực sự hướng tới là năng suất của quản lý tài nguyên tự động. Tức là dùng quản lý tài nguyên tự động, bất kể bằng cách nào, rồi chỉ kết hợp một trong các hệ thống kiểu trên cho các đường dẫn quan trọng về hiệu năng
Trong bối cảnh này, có thể xem “Rust” chẳng qua là “những bất biến mà mọi người thường muốn” và “một tập hợp các tối ưu hóa giả định đúng các bất biến thông thường đó, không hơn không kém”
Phần lớn thời gian biên dịch được dành cho diễn giải trait, đơn hình hóa, các pass tối ưu hóa LLVM và liên kết
Có thể đây là một câu hỏi ngớ ngẩn, nhưng tôi tự hỏi liệu có thể chạy nhiều triển khai trên các luồng song song và để bên nào đưa ra kết quả chấp nhận trước thì thắng hay không
Việc dùng con trỏ để khiến nhiều tham chiếu khả biến tới cùng một biến tồn tại đồng thời là hành vi không xác định. Nếu tôi không hiểu sai ý của bài báo thì có vẻ là như vậy
Đoạn mã trên được trình biên dịch Rust chấp nhận nhưng phá vỡ các quy tắc. Vấn đề là nó phá vỡ quy tắc nào
Về cơ bản, những gì borrow checker chấp nhận là hợp pháp; unsafe có thể biểu diễn cả những thứ bất hợp pháp hoặc hành vi không xác định; và tồn tại một tập quy tắc rộng hơn những gì borrow checker có thể kiểm tra, nhưng vẫn hợp pháp và là hành vi được định nghĩa
Mục tiêu của nghiên cứu này là đặc tả chính xác tập quy tắc đó. Phác thảo lớn thì gần với “con trỏ có thể ghi không được alias”, nhưng các chi tiết như con trỏ nội bộ, vô hiệu hóa iterator, hay việc tạo ra con trỏ xấu mới là vấn đề hay sử dụng nó mới là vấn đề, đều rất khó
Bài báo Stacked Borrows trước đó đơn giản hơn nhưng hạn chế hơn, nên unsafe code trong thực tế thường không vượt qua được các quy tắc. Tree Borrows rộng hơn, cho phép nhiều mã hơn mà vẫn có thể chứng minh là an toàn
Tree Borrows chính là đề xuất một định nghĩa như vậy
Ở đây, “code có thể làm việc này” nghĩa là “có thể viết, biên dịch và chạy đoạn code này, và nếu không có thứ như Tree Borrows thì không có cơ sở để khẳng định đoạn code này có vấn đề”
Như vậy là đã chấp nhận rằng cần phải nói những đoạn code như thế này là hành vi không xác định, tức là cần một thứ như Tree Borrows. Phần này của bài báo là đoạn lập luận vì sao cần thứ như vậy
https://play.rust-lang.org/?version=stable&mode=debug&editio...
Nội dung là vì các nhà phát triển trình biên dịch Rust rõ ràng muốn hỗ trợ tối ưu hóa dựa trên aliasing, nên họ cần một cách để “loại trừ” các phản ví dụ như trên khỏi phạm vi xét
unsafedành cho những trường hợp khó chứng minh tính hợp lệ của mã bằng phân tích vòng đời của Rust, nhưng nó có thể bị lạm dụng để làm nhiều việc hơn thế rất nhiều