Có những ngày làm việc với DUY, nhìn toàn bộ thanh trạng thái test báo xanh liên tục khiến tôi nảy sinh cảm giác tự mãn rằng dự án của mình đã đi rất xa. Rồi tôi mở tài liệu nghiên cứu về CompCert hoặc seL4 ra đọc, và lập tức được đưa trở lại mặt đất một cách vô cùng lịch sự.
LLVM là ngọn núi đầu tiên, nhưng cũng là con đường thực tế nhất giúp các ngôn ngữ mới tồn tại. Nó bắt đầu như một dự án nghiên cứu học thuật về chiến lược biên dịch tối ưu dựa trên SSA (Static Single Assignment) tại đại học Illinois, sau đó lớn mạnh thành một tập hợp công nghệ compiler và toolchain có tính module hóa cao bậc nhất thế giới. Đối với một ngôn ngữ non trẻ như DUY, LLVM là một món quà vô giá: compiler của DUY chỉ cần tập trung làm tốt phần phân tích ngữ nghĩa, kiểm tra an toàn kiểu và sinh ra biểu diễn trung gian của mình, sau đó hạ cấp xuống LLVM IR để tận dụng bộ tối ưu hóa khổng lồ và sinh mã máy native cho hàng chục kiến trúc CPU khác nhau mà không cần tự tay viết từng backend máy từ con số không.
Nhưng việc sử dụng LLVM không tự động biến compiler của bạn trở nên đúng đắn. LLVM chỉ tối ưu hóa tốt những gì chúng ta diễn đạt chính xác trong biểu diễn trung gian và metadata gửi xuống. Nếu frontend compiler làm mất đi ngữ nghĩa an toàn bộ nhớ, tính toán sai lệch layout dữ liệu hoặc sinh control flow lỗi, backend LLVM mạnh mẽ đến đâu cũng chỉ giúp ta tạo ra mã máy thực thi sai một cách nhanh chóng và chuyên nghiệp hơn. LLVM cung cấp cho DUY đôi chân khỏe mạnh; nó không thể cung cấp cho DUY một bộ não đúng đắn.
CompCert đặt ra một câu hỏi triết học và kỹ thuật khó khăn hơn nhiều: "Làm sao chúng ta dám chắc chắn rằng trình biên dịch không biên dịch sai mã nguồn của con người?" Thay vì chỉ dựa vào hàng triệu ca kiểm thử để cầu may, CompCert sử dụng chứng minh toán học được hỗ trợ bởi máy (Coq proof assistant) để thiết lập một bảo đảm gọi là "semantic preservation" (bảo toàn ngữ nghĩa) cho phần lõi compiler, từ cây AST của ngôn ngữ C cho đến assembly mã máy. Mỗi ngôn ngữ trung gian trong compiler của họ đều có ngữ nghĩa toán học chặt chẽ; từng bước biến đổi (compilation pass) đều phải được chứng minh toán học rằng không làm thay đổi hành vi gốc của chương trình.
Tôi đọc tài liệu ấy không phải để hoang tưởng tuyên bố rằng DUY sẽ được formal-verify (chứng minh hình thức) hoàn toàn ở phiên bản 1.0. Nói câu đó thì dễ, bắt tay vào làm có thể tiêu tốn toàn bộ tuổi trẻ của một đội ngũ giáo sư toán học. Bài học thực tế hơn là thiết kế đường ống compiler sao cho mỗi tầng đều có hợp đồng dữ liệu rõ ràng: typed IR sạch sẽ, bộ xác minh verifier nghiêm ngặt, negative corpus dồi dào, so sánh snapshot liên tục và các pass biến đổi nhỏ gọn. Nếu hôm nay chúng ta không thể phát biểu các ràng buộc bất biến (invariants) của ngôn ngữ bằng lời nói mạch lạc, ngày mai chắc chắn chúng ta không cách nào chứng minh được nó bằng toán học.
seL4 là ngọn núi thứ ba. Công trình vĩ đại này chứng minh cho thế giới thấy một microkernel hệ điều hành thực tế, hiệu năng cao hoàn toàn có thể đạt được chứng minh toán học kiểm chứng bởi máy (machine-checked proof) ở mức mã nguồn C chống lại đặc tả thiết kế, một cột mốc lịch sử được công bố vào năm 2009. Điều đáng học hỏi từ seL4 không chỉ là các kỹ thuật chứng minh toán học phức tạp. Đó là kỷ luật thép trong việc giữ cho lõi hệ thống cực kỳ nhỏ gọn, phân định rạch ròi giữa cơ chế thực thi (mechanism) và chính sách quản lý (policy), và biết chính xác vùng an toàn nào đang được cam kết bảo vệ.
DUY có một phòng thí nghiệm hệ điều hành (OS lab), nhưng OS lab của DUY không phải là một Linux mới và càng chưa phải là một seL4 mới. Nó chỉ đơn thuần là phòng thử nghiệm áp suất thực tế để kiểm tra xem mã nguồn DUY có thể tự khởi động (boot), quản lý bộ nhớ vật lý trực tiếp, đi qua các ranh giới syscall và chạy độc lập freestanding tốt hay không. Gọi đúng tên thực tế của sản phẩm giúp ta có bằng chứng kỹ thuật mạnh mẽ hơn. Một proof-of-concept trung thực và hoạt động được luôn có giá trị gấp vạn lần một "hệ điều hành cách mạng" chỉ tồn tại trong các slide quảng cáo.
Ba ngọn núi dạy cho tôi ba loại khiêm tốn. LLVM nhắc nhở rằng ta không cần phải tự phát minh lại mọi bánh xe công nghệ. CompCert nhắc nhở rằng chính trình biên dịch cũng là một nguồn sinh bug khổng lồ cần được giám sát chặt chẽ. seL4 nhắc nhở rằng việc bảo đảm an toàn tuyệt đối đòi hỏi một phạm vi mục tiêu cực kỳ nhỏ gọn và một công sức lao động khổng lồ.
DUY không cần phải leo lên đỉnh của cả ba ngọn núi ấy ngay lập tức. Nhưng chúng tôi bắt buộc phải biết vị trí của chúng trên bản đồ thế giới. Không có bản đồ độ cao định vị, một gò đất nhỏ sau nhà rất dễ được chúng ta tự mãn viết thành đỉnh Everest trong các tài liệu công bố.
Bình luận (0)
Đang tải bình luận...