Bộ kiểm tra borrow theo chiều ngược: Ý tưởng lạ nhưng đầy hứa hẹn của ngôn ngữ Valen

Khi nhắc đến borrow checker — cơ chế đảm bảo an toàn bộ nhớ nổi tiếng của Rust — hầu hết lập trình viên đều hình dung đến một quá trình phân tích tuần tự từ đầu hàm xuống cuối hàm. Nhưng đội ngũ phát triển ngôn ngữ Valen lại đang thử nghiệm một hướng đi hoàn toàn khác: duyệt hàm theo chiều ngược, từ câu lệnh cuối cùng lên đến đầu hàm. Nghe có vẻ kỳ quặc, nhưng tác giả khẳng định nó hoạt động — và hoạt động rất tốt.

Một ý tưởng "điên rồ" nhưng hiệu quả

Tác giả bài viết thừa nhận cảm giác của mình khi ý tưởng này thành công: "Đã bao giờ bạn có một ý tưởng kỳ lạ, rồi nó hoạt động, nhưng bạn vẫn không thể tin nổi chưa?" Đó chính là cảm giác hiện tại của anh với bộ kiểm tra borrow của Valen.

Điểm khác biệt cốt lõi: đây không phải là bộ kiểm tra borrow kiểu shared-xor-mutable thông thường. Valen cho phép mutable aliasing an toàn về bộ nhớ — một đặc điểm mà Rust không hỗ trợ — và có thể gọi vào các hàm Rust vẫn đảm bảo an toàn bộ nhớ xuyên biên giới.

Quy trình biên dịch bốn giai đoạn

Valen biên dịch một hàm qua bốn giai đoạn, trong đó giai đoạn thứ tư — và cũng là giai đoạn kỳ lạ nhất — diễn ra theo chiều ngược:

• Giai đoạn 1: Đánh dấu các lệnh gọi hàm, phân rã cú pháp và các bước tiền xử lý khác
• Giai đoạn 2: Gán kiểu tĩnh (static typing) — duyệt xuôi như thông thường
• Giai đoạn 3: Phân nhóm tĩnh (static grouping) — xác định mỗi tham chiếu trỏ đến đâu
• Giai đoạn 4: Kiểm tra use-after-free — duyệt ngược từ cuối hàm lên đầu

"Theo hiểu biết của tôi, đây là bộ kiểm tra borrow duy nhất thực hiện việc kiểm tra an toàn theo chiều ngược," tác giả viết.

Cách hoạt động của bước quét ngược

Thuật toán duyệt từ cuối hàm về đầu, tìm kiếm ba loại sự kiện:

• DECLARE — điểm mà một biến được khai báo hoặc gán
• USE — điểm mà biến được sử dụng
• MUTATE — điểm mà dữ liệu bị thay đổi (ví dụ: add_buff())

Cơ chế cốt lõi dựa trên một danh sách gọi là pending, chứa những thứ đã được USE ở phía dưới mà ta hy vọng sẽ thấy DECLARE ở phía trên. Mục tiêu là không bao giờ gặp một MUTATE làm vô hiệu hóa bất kỳ phần tử nào trong pending.

Hãy xem ví dụ đơn giản hóa:

e.add_buff();
buff = &e.buffs[0];
observe(buff);

Khi quét ngược:

1. Gặp observe(buff) → thêm buff vào pending
2. Gặp buff = &e.buffs[0] → thêm thông tin buff trỏ vào e.buffs[] vào pending
3. Gặp e.add_buff() → đây là MUTATE trên e, và buff đang trỏ vào e.buffs[] → lỗi use-after-free!

Nếu ta di chuyển e.add_buff() lên đầu hàm, quá trình quét ngược sẽ gặp DECLARE của buff trước khi thấy MUTATE, xóa nó khỏi pending và kết luận chương trình an toàn.

Ba lý do để đi ngược: Tiện lợi, vòng lặp và tốc độ

1. Tiện lợi

Khi quét xuôi, để biết một biến được dùng lần cuối ở đâu, ta phải thực hiện thêm một bước truy vấn/điều hướng phức tạp. Quét ngược thì không: khi gặp lần dùng đầu tiên (tính từ cuối lên), đó chính là lần dùng cuối cùng. Điều này đặc biệt hữu ích cho việc chèn destructor hoặc giảm reference count.

2. Vòng lặp

Vòng lặp là bài toán hóc búa với mọi bộ kiểm tra borrow. Ví dụ:

arr.push(123);
e = &arr[0];
while foo() {
    observe(e);
}

Biến e có thể đến từ hai nguồn: bên ngoài vòng lặp, hoặc từ một vòng lặp trước đó. Quét xuôi sẽ cần "nhìn trước" để xác định điều này, còn quét ngược thì thu thập thông tin một cách tự nhiên. Thuật toán bổ sung thêm hai cấu trúc dữ liệu — revived_after_this và mutations_after_this — cùng một bước kiểm tra LOOP START để xử lý chính xác.

3. Tốc độ

Mỗi nút chỉ cần xử lý một lần duy nhất ở giai đoạn 3 (xuôi) và một lần duy nhất ở giai đoạn 4 (ngược). Tác giả tin rằng cách tiếp cận này nhanh hơn so với các phương án phức tạp khác mà anh đã cân nhắc.

Vẫn còn nhiều việc phía trước

Bộ kiểm tra borrow của Valen hiện chỉ khoảng 3.600 dòng mã — khá non trẻ và còn thiếu nhiều tính năng:

• Luồng điều khiển ngắt quãng (break, continue)
• Các nhóm liên kết (associated groups)
• Closure
• Và nhiều thứ thú vị khác

Kế hoạch trước mắt là tái cấu trúc để bộ kiểm tra làm việc với đồ thị luồng điều khiển (control-flow graph) thay vì AST có kiểu, giúp xử lý luồng ngắt quãng dễ dàng hơn nhiều.

Góc nhìn cho lập trình viên Việt Nam

Với cộng đồng lập trình viên Việt Nam — những người ngày càng quan tâm đến Rust và các ngôn ngữ hệ thống an toàn bộ nhớ — dự án Valen là một cái tên đáng theo dõi. Nếu thành công, nó có thể mở ra hướng đi mới cho việc cân bằng giữa hiệu năng, an toàn bộ nhớ và sự linh hoạt trong phát triển phần mềm cấp thấp, đồng thời cho phép tương tác liền mạch với hệ sinh thái Rust vốn đã rất mạnh.

Tác giả hứa hẹn sẽ giải thích thêm về cách Valen kết hợp reference counting và generational references trong các bài viết tiếp theo, cũng như điểm qua các ngôn ngữ khác đang khám phá những cách tiếp cận an toàn bộ nhớ mới như Ante, Carbon, Zeta, Fang và exclusion typing.