Tree Borrows

 (plf.inf.ethz.ch)
1 điểm bởi GN⁺ 2025-07-10 | 1 bình luận | Chia sẻ qua WhatsApp
  • Tree Borrows, một mô hình bộ nhớ mới nhằm vượt qua giới hạn tối ưu hóa của mã unsafe trong ngôn ngữ Rust, được đề xuất
  • Mô hình Stacked Borrows trước đây không cho phép nhiều mẫu thường được dùng trong mã Rust thực tế, nhưng Tree Borrows giải quyết điều đó bằng cấu trúc cây, cung cấp các quy tắc thực tế và linh hoạt hơn
  • Tree Borrows vượt qua nhiều hơn 54% ca kiểm thử mã thực tế so với Stacked Borrows
  • Mô hình này vẫn giữ lại phần lớn khả năng tối ưu hóa và an toàn bộ nhớ quan trọng của Rust, đặc biệt là các tối ưu như read-read reordering, đồng thời phản ánh cả những tính năng nâng cao của borrow checker Rust hiện đại
  • Việc đưa vào mô hình máy trạng thái dựa trên cây đánh dấu một cột mốc quan trọng cho nghiên cứu về tối ưu hóa Rust và kiểm chứng an toàn

Hệ thống ownership của Rust và giới hạn của mã unsafe

  • Rust cung cấp các đảm bảo mạnh mẽ như an toàn bộ nhớ và ngăn chặn data race thông qua hệ thống kiểu dựa trên ownership
  • Tuy nhiên, Rust có unsafe escape hatch, trong đó trách nhiệm kiểm chứng an toàn được chuyển từ compiler sang cho lập trình viên
  • Compiler muốn tận dụng các quy tắc pointer alias để tối ưu hóa mạnh hơn, nhưng mã unsafe sai có thể làm vô hiệu các tối ưu đó

Stacked Borrows và các giới hạn của nó

  • Trước đây, mô hình Stacked Borrows được dùng để định nghĩa “hành vi sai” của mã unsafe và đưa ra tiêu chuẩn cho tối ưu hóa
  • Tuy nhiên, cách tiếp cận này không cho phép nhiều mẫu unsafe phổ biến trong mã Rust thực tế, đồng thời cũng không phản ánh được các tính năng borrow checker mới được đưa vào Rust gần đây

Sự xuất hiện của Tree Borrows

  • Tree Borrows là một mô hình mới theo dõi quyền truy cập bộ nhớ bằng cấu trúc cây thay vì cấu trúc stack
  • Nhờ đó, mô hình này cho phép an toàn nhiều mẫu mã Rust thực tế hơn, đồng thời nâng cao đáng kể tính linh hoạt và khả năng áp dụng thực tiễn của các quy tắc borrow
  • Trong đánh giá trên 30.000 crate Rust phổ biến, mô hình này vượt qua nhiều ca kiểm thử hơn 54% so với Stacked Borrows

Đặc điểm và ưu điểm của Tree Borrows

  • Mô hình vẫn giữ lại phần lớn các tối ưu hóa quan trọng của Stacked Borrows hiện có, chẳng hạn như read-read reorderings
  • Đồng thời, nó cũng có thể phản ánh các tính năng nâng cao của borrow checker Rust hiện đại, như các mẫu borrow không điển hình và thao tác con trỏ phức tạp
  • Bằng việc đưa vào mô hình máy trạng thái dựa trên cây, Tree Borrows cân bằng giữa an toàn và khả năng tối ưu hóa

Kết luận và ý nghĩa

  • Tree Borrows đặt ra một chuẩn mực mới cho việc xử lý mã unsafe và nghiên cứu tối ưu hóa trong compiler Rust
  • Đây được đánh giá là một mô hình bộ nhớ thực tế và vững chắc, bao quát cả mã Rust dùng trong thực tế lẫn các chính sách borrow checker hiện đại
  • Bài báo, artifact và mã nguồn liên quan đã được công khai, và được kỳ vọng sẽ tạo ảnh hưởng lớn tới cộng đồng nghiên cứu compiler Rust và kiểm chứng

Bài viết liên quan

1 bình luận

 
GN⁺ 2025-07-10
Ý kiến trên Hacker News

  • Bài viết blog gần đây của Ralf Jung cung cấp thêm nhiều bối cảnh liên kết
    Thêm nữa: cũng khuyên xem bài trình bày gần đây của nhóm nghiên cứu đang cố gắng đặc tả rõ ràng ngữ nghĩa thực thi của Rust bằng một phương ngữ của Rust YouTube

  • Có ý kiến cho rằng từ góc nhìn của trình biên dịch, có thể tận dụng những bảo đảm mạnh mẽ của hệ thống kiểu liên quan đến pointer aliasing để thực hiện các tối ưu hóa mạnh; nhưng tôi tò mò không biết trên thực tế điều đó hiệu quả đến mức nào
    Linus Torvalds từ lâu đã cho rằng quy tắc strict aliasing của C ít có ích mà còn dễ gây ra vấn đề
    Bài viết ví dụ của ông ấy cũng khá thú vị
    Tôi cũng tò mò liệu Rust có thực sự khác C một cách căn bản hay không, vì theo kinh nghiệm cá nhân thì, nhất là khi có unsafe, cảm giác cũng chẳng khác mấy

    • Tôi thực sự nghĩ quy tắc strict aliasing của C rất tệ
      Các quy tắc được đề xuất trong Rust khác hơn nhiều, hữu ích hơn với trình biên dịch, và cũng bớt gánh nặng hơn cho lập trình viên
      Có thể opt-out ngay trong ngôn ngữ bằng cách dùng raw pointer, và cũng có công cụ để kiểm tra mã
      Rốt cuộc cũng là một sự đánh đổi, như mọi thiết kế ngôn ngữ khác
      Có vẻ Rust đã tìm ra một điểm cân bằng mới trong vùng tối ưu hóa này, và thời gian sẽ trả lời kết quả của lựa chọn đó

    • Quy tắc aliasing của Rust rất khác C
      Trong C, từ khóa restrict hầu như chỉ có ý nghĩa với tham số hàm, còn type-based aliasing thì trên thực tế ít được dùng hoặc dùng rất bất tiện
      Trong Rust, lifetime, mutability được biểu đạt tinh vi hơn, và có thể xử lý bộ nhớ an toàn theo nhiều cách mà không phụ thuộc vào chính kiểu dữ liệu
      Điểm lớn là chỉ cần không tạo ra các tham chiếu &mut chồng lấn, và vẫn có thể tận dụng bằng cách tách thành nhiều &mut không chồng lấn

    • Tôi muốn thấy một phân tích rộng hơn về việc điều này thực sự ảnh hưởng đến hiệu năng đến mức nào
      Chỉ cần bỏ toàn bộ phần compiler truyền thông tin aliasing cho LLVM rồi so sánh hiệu năng là biết ngay
      Cũng có ý kiến cho rằng annotation noalias cải thiện khoảng 5% hiệu năng runtime, có bình luận liên quan (dù dữ liệu đã khá cũ)

    • Nên cân nhắc khi nghe Linus nói về trình biên dịch
      Kernel hệ điều hành và trình biên dịch là hai lĩnh vực hoàn toàn khác nhau
      Ngày nay, phân tích alias thực sự là chìa khóa cho những cải thiện hiệu năng rất mạnh
      Tác động lớn nhất đến từ các heuristic đơn giản, còn các truy vấn alias phức tạp tự thân lại không hữu dụng lắm
      Về mặt lý thuyết, tôi muốn thử nghiệm xem phân tích alias hoàn hảo có thể cải thiện hiệu năng bao nhiêu, nhưng có lẽ với mã thông thường thì khoảng 20% đã là giới hạn
      Tất nhiên, một số tối ưu hóa rất cao cấp (ví dụ: biến đổi data layout) sẽ thậm chí không được thử nếu thiếu phân tích alias

    • strict aliasing của C và aliasing của Rust là hai khái niệm khác nhau
      C lấy type-based analysis (TBAA) làm trọng tâm, còn Rust thì cố ý không áp dụng điều đó

  • Đã có các thread cũ về Stacked Borrows vào năm 2020 và 2018
    Thread 2020
    Thread 2018

  • Tôi đã đọc đặc tả Tree Borrows trên website của Nevin vài năm trước, và rất ấn tượng vì nó giải quyết những vấn đề phức tạp một cách thanh nhã
    Theo kinh nghiệm thực tế của tôi, Tree Borrows cho phép những đoạn mã hợp lý mà Stacked Borrows không thể chấp nhận
    Đoạn mã ví dụ trong thư viện chuẩn Rust cũng đáng tham khảo

  • Tôi tự hỏi liệu Rust hoặc các ngôn ngữ PL thế hệ tiếp theo có thể phát triển đến mức cho phép chọn giữa nhiều triển khai borrow checker khác nhau, với đặc tính và mục tiêu khác nhau (tốc độ biên dịch, tốc độ runtime, độ linh hoạt của thuật toán, v.v.) hay không

    • Rust đã hỗ trợ chuyển đổi triển khai borrow checker rồi
      Nó đã chuyển từ kiểu dựa trên scope sang non-lexical, và cũng có một triển khai thử nghiệm tên là Polonius dưới dạng tùy chọn
      Khi triển khai mới sẵn sàng, bản cũ thường không cần giữ lại
      Ngoài ra cũng có thể dùng linh hoạt hơn với Rc, RefCell và các cơ chế cần kiểm tra runtime

    • Nhiều cách tiếp cận như affine type (Rust dùng), linear type, effect system, dependent type, formal proof... đã tồn tại từ lâu
      Mỗi cách có đặc tính khác nhau về chi phí triển khai, hiệu năng, trải nghiệm phát triển, v.v.
      Ngoài Rust, cũng có xu hướng theo đuổi sự kết hợp giữa quản lý tài nguyên tự động có năng suất cao và hệ thống kiểu

    • Điều thực sự cần là separation logic có thể mô tả chính xác precondition của hàm và thậm chí chứng minh cả các điều kiện trung gian
      Cách tiếp cận của Rust là hệ thống hóa những bất biến thông thường mà mọi người thực sự muốn, để bảo đảm các tối ưu hóa mạnh

    • Tôi thắc mắc liệu kết quả của borrow checker có đúng là chỉ có false negative chứ không có false positive hay không
      Nếu đúng vậy, thì liệu có thể chạy song song nhiều triển khai trên các thread khác nhau và dùng kết quả của bên thắng nhanh nhất hay không

    • Cho phép đồng thời nhiều triển khai borrow checker dễ dẫn đến sự phân mảnh của hệ sinh thái, nên không phải điều đáng mong muốn

  • Tôi đã thử kiểm tra đoạn mã Rust trong bài báo và xác nhận rằng trình biên dịch stable mới nhất không từ chối nó
    Mã ví dụ:

    fn write(x: &mut i32) {*x = 10}

fn main() {
  let x = &mut 0;
  let y = x as *mut i32;
  //write(x); 
  *x = 10; 
  unsafe {*y = 15 };
}
    • Stacked Borrows là mô hình runtime của miri
      miri sẽ báo lỗi ở *x = 10; nếu chạy đoạn mã trên, nhưng write(x); thì không gây lỗi
      Từ góc nhìn hệ thống kiểu, rustc không có lý do gì để từ chối cả hai phiên bản vì y là *mut

  • Bài báo nêu ví dụ dưới đây như một vấn đề của mã unsafe:

    fn main() {
  let mut x = 42;
  let ptr = &mut x as *mut i32;
  let val = unsafe { write_both(&mut *ptr, &mut *ptr) };
  println!("{val}");
}

    Tôi băn khoăn liệu chuyện này có thực sự khả thi hay không
    Dùng pointer để tạo nhiều tham chiếu mutable tới cùng một biến rõ ràng là UB, nên tôi tự hỏi liệu mình có đang hiểu sai điều gì không

    • Trọng tâm của nghiên cứu này là xác định chính xác ranh giới của UB (hành vi không xác định)
      Đoạn mã trên, dù được trình biên dịch Rust chấp nhận, vẫn vi phạm quy tắc
      Là quy tắc nào?

  • Mã vượt qua borrow checker là hợp lệ

  • unsafe có thể biểu đạt cả điều không hợp lệ/UB

  • Có một tập quy tắc rộng hơn phạm vi của borrow checker nhưng vẫn hợp lệ
    Nghiên cứu này nhằm đặc tả chặt chẽ ranh giới đó
    Bài báo Stacked Borrows đơn giản hơn nhưng có giới hạn với mã unsafe thực tế, còn Tree Borrows thừa nhận một phạm vi an toàn rộng hơn

    • Điểm “không thể đồng thời tồn tại nhiều pointer tới mutable reference” là rõ ràng, nhưng lại không có chỗ nào nêu rõ chính xác nó vi phạm quy tắc nào
      Tree Borrows chính là đề xuất một định nghĩa như vậy
      Câu “mã có thể làm chuyện như thế này” có nghĩa là: thực sự có thể tạo và chạy đoạn mã đó, nhưng nếu không có một định nghĩa như Tree Borrows thì sẽ khó có cơ sở để giải thích vì sao nó sai
      Có vẻ chính bạn cũng đã phần nào chấp nhận sự cần thiết của những quy tắc rõ ràng như Tree Borrows

    • Mã unsafe kiểu đó thực sự khả thi, và đó chính là lý do nó là UB
      Ví dụ: liên kết playground

    • Nếu muốn hiểu thêm bối cảnh liên quan, phần mở đầu của đoạn ngay sau đó trong bài báo thể hiện khá rõ dụng ý

Nếu các nhà phát triển trình biên dịch Rust muốn có các tối ưu hóa aliasing, họ cần một cách để loại trừ các đoạn mã phản ví dụ như trên

  • Đúng, đó chính là vấn đề cốt lõi
    Rất khó duy trì quy tắc cấm nhiều mutable reference, và unsafe phản ánh việc Rust có thể cho phép nhiều thứ hơn đáng kể so với những gì hệ thống lifetime của nó bảo đảm

  • Một trong các tác giả, Neven Villani, là con trai của Cédric Villani, người đoạt Fields Medal 2010
    Tôi chợt nghĩ đến câu ví “quả táo không rơi xa gốc cây”

    • Và tôi cũng muốn đùa rằng “có thể nói là cậu ấy cũng đã mượn phẩm chất từ cái cây”

    • Tôi từng có văn phòng gần cha của cậu ấy (người đoạt Fields Medal)
      Đó là trước khi ông bước vào chính trường

  • Mô hình này thực sự rất xuất sắc
    Tôi dự định sẽ triển khai nó trong ngôn ngữ mình đang làm

  • Không thể là déjà vu được
    Tôi có cảm giác cứ 2–3 tháng lại thấy bài này một lần

    • Bài báo đã được chuẩn bị trong nhiều năm, và giờ cuối cùng cũng được xuất bản chính thức