Tập 35: `owned` và `move` — Bộ nhớ bắt đầu có chủ

Ảo tưởng lớn nhất của các lập trình viên hệ thống mới là họ nghĩ họ có thể quản lý vòng đời của từng vùng nhớ bằng trí nhớ. Họ tin rằng mình sẽ nhớ để free đúng một lần, không đọc lại sau khi đã giải phóng, và không chia sẻ con trỏ bừa bãi. Lịch sử của hàng triệu lỗ hổng bảo mật bảo chúng ta điều ngược lại.

Sprint 14 của DUY bắt đầu xây dựng cột trụ đầu tiên của mô hình bộ nhớ phi GC: owned[T].

let a: owned[Buffer] = make_buffer()
let b = move a

Quy tắc của owned là độc quyền sở hữu. Tại một thời điểm, chỉ có một tên biến được làm chủ vùng nhớ đó. Khi anh gán b = move a, quyền sở hữu đã chuyển dịch. Biến a lập tức trở thành một cái vỏ rỗng. Nếu anh cố gắng đọc a ở dòng tiếp theo, compiler sẽ chặn đứng:

Use of moved value 'a'

Để làm được điều này, context kiểm tra kiểu (Γ) của compiler phải mang thêm một trạng thái cho mỗi binding: moved ∈ {false, true}. Mỗi khi đi qua một biểu thức move, compiler đánh dấu trạng thái đó thành true. Mọi lượt truy cập tiếp theo vào biến đó đều bị coi là bất hợp pháp.

Thách thức của V0 là sự đơn giản của phân tích dòng điều khiển. Chúng tôi chưa có một Control Flow Graph (CFG) hoàn chỉnh. Điều này dẫn đến việc checker xử lý các nhánh rẽ rất bảo thủ (conservatively): nếu biến a bị move ở một trong hai nhánh if / else, compiler sẽ coi như nó đã bị move ở cuối khối lệnh, bất kể nhánh nào chạy thật ở runtime.

Tôi đã mất cả buổi chiều để tranh luận với AI về việc sửa một lỗi false positive của move checker. Một biến được khởi tạo lại trong vòng lặp nhưng compiler vẫn báo lỗi là đã bị move từ vòng lặp trước. Đó là lúc tôi nhận ra sự phức tạp khủng khiếp của dòng dữ liệu tĩnh. Chúng tôi quyết định giữ lại sự cứng nhắc đó ở V0: thà từ chối một chương trình đúng còn hơn cho qua một chương trình sai. owned và move biến bộ nhớ từ một vấn đề runtime thành một bài toán tĩnh ở compile-time, giúp giải phóng lập trình viên khỏi nỗi ám ảnh mang tên memory leaks.

---