DOOM chạy bằng kiểu TypeScript [Video]

• Đây là một thử nghiệm khởi động trò chơi DOOM năm 1993 và xuất ra khung hình đầu tiên chỉ bằng hệ thống kiểu TypeScript, chứ không phải mã runtime
• Để đến được khung hình đầu tiên, trình kiểm tra kiểu TypeScript đã xử lý 3,5 nghìn tỷ dòng, tổng cộng 177TB trong suốt 12 ngày; ước tính ban đầu là 1,25PB và hơn 3 tháng
• Cốt lõi của phần triển khai là một máy ảo WebAssembly được tạo bằng kiểu, hiện thực 116 lệnh cần cho DOOM bằng logic ở cấp kiểu và đánh giá 18 triệu lệnh
• Trong quá trình phát triển, tác giả đã gỡ bỏ các giới hạn của trình biên dịch về đệ quy, union, tuple và khởi tạo kiểu sâu, nhưng thành phẩm cuối cùng vẫn là TypeScript thuần mà người dùng có thể tự chạy
• Vì đây là khối lượng kiểm tra kiểu vượt xa ứng dụng thông thường, các công cụ phát triển hiện có gần như vô dụng, và tác giả phải tự tạo 12.364 bài kiểm thử cùng các công cụ tùy biến

---

Một chiếc máy tính được dựng bên trong hệ thống kiểu TypeScript

• DOOM không chạy bằng JavaScript thông thường mà chỉ hoạt động bên trong hệ thống kiểu TypeScript
• Mục tiêu là tạo ra một máy ảo WebAssembly có thể chạy các chương trình khác chỉ bằng kiểu, không dùng mánh khóe hay ngôn ngữ thực thi nào khác
• Máy tính ở cấp kiểu có các thành phần cơ bản cần cho việc thực thi, được biểu diễn bằng kiểu
  • RAM
  • không gian đĩa
  • ngăn xếp lời gọi
  • chương trình con
  • con trỏ bộ nhớ
  • ngữ cảnh thực thi
  • công cụ phát triển tùy biến
• 116 lệnh WebAssembly cần để chạy DOOM được hiện thực bằng logic kiểu TypeScript
• Chỉ riêng logic này đã tạo ra 18 triệu lệnh mà trình kiểm tra kiểu phải đánh giá từng cái một, và mỗi lệnh biểu thị một trạng thái máy riêng của hệ thống

Quy mô để đi tới khung hình đầu tiên

• Để tạo ra khung hình DOOM đầu tiên cần tới 3,5 nghìn tỷ dòng kiểu, với tổng kích thước 177TB
• Trình biên dịch TypeScript TSC được chạy liên tục trong 12 ngày để khởi động trò chơi và lấy ra khung hình đầu tiên
• Theo tính toán ban đầu, máy tính sẽ phải xử lý 1,25PB kiểu TypeScript và thời gian chạy dự kiến là hơn 3 tháng
• Sau những tối ưu hóa cực đoan, khối lượng này được giảm xuống còn 177TB và 12 ngày
• Trong khi kiểm tra kiểu TSC của một ứng dụng thông thường thường ở mức 200.000–500.000 lần khởi tạo kiểu, công việc này duy trì 20 triệu lần khởi tạo mỗi giây suốt 12 ngày
• Đầu ra cuối cùng là một đối tượng TypeScript, trong đó mỗi giá trị biểu thị một dòng pixel
  • Khung hình đầu ra là 320×200
  • Đây là một khung ASCII gồm tổng cộng 128.000 pixel
• Cũng có cách điều khiển trò chơi bằng đầu vào từ bàn phím

Những cơ chế bảo vệ TypeScript đã bị gỡ trong quá trình phát triển

• Thành phẩm cuối cùng là TypeScript thuần mà người dùng có thể tự chạy
• Để biến thử nghiệm này thành hiện thực, tác giả đã chỉnh sửa trình biên dịch TypeScript và gỡ nhiều giới hạn
  • Gỡ giới hạn độ sâu ngăn xếp quá mức khi so sánh kiểu
  • Gỡ giới hạn khởi tạo kiểu quá sâu hoặc có thể vô hạn
  • Đặt kích thước tối đa của union và tuple thành Infinity
  • Gỡ giới hạn cắt bớt đầu ra
  • Gỡ bỏ giới hạn đệ quy nổi tiếng của TypeScript
• Giới hạn ngăn xếp của chính máy tính cũng được nâng lên
• Khi bỏ các cơ chế bảo vệ này, trình kiểm tra kiểu có thể dễ dàng dùng tới 100GB bộ nhớ
• Cái giá của việc gỡ giới hạn cũng rất lớn
  • Một lỗi nhỏ như gõ sai import cũng có thể tạo ra vòng lặp vô hạn
  • Cấp phát heap có thể dùng hết bộ nhớ và làm toàn bộ hệ thống sập
  • Stack trace trở nên cực kỳ khổng lồ, và phần lớn lỗi chỉ thất bại theo kiểu treo hẳn

Những thứ còn phải xây thêm để chạy DOOM

• Sau 6 tháng làm việc, tác giả đã có thể chạy các chương trình C nhỏ, nhưng để chạy DOOM thì cần nhiều phần triển khai hơn rất nhiều
• Mọi thành phần của DOOM đều phải được mã hóa thành kiểu
  • bản đồ trò chơi
  • texture
  • sprite
  • âm thanh
  • AI của kẻ địch
  • vũ khí
  • vật phẩm
  • động cơ vật lý
  • hệ thống con âm thanh
  • văn bản trong trò chơi
• Ở cấp kiểu, tác giả còn hiện thực cả các tính năng gần với runtime
  • bộ gom rác
  • bộ nhớ đệm CPU L1
  • loại bỏ mã chết lúc runtime
  • bộ nén bộ nhớ thời gian thực
  • ngăn xếp giá trị toàn cục kèm đếm độ sâu để bảo vệ khỏi stack underflow
  • bảng phân phối động
  • biến toàn cục ở cấp mô-đun
  • labeled goto
  • xử lý ngoại lệ ở cấp kiểu
  • theo dấu stack lúc runtime
  • core dump đầy đủ
• RAM tuyến tính được biểu diễn thành một đối tượng khổng lồ không thể sắp xếp, với khóa địa chỉ 32-bit và giá trị byte
• Tác giả đã tìm ra cách tạm dừng việc đánh giá kiểu trong không gian người dùng của hệ kiểu, từ đó mới có thể làm được core dump, xử lý ngoại lệ và theo dấu stack

Giới hạn công cụ và các ràng buộc trong triển khai

• Kích thước tệp cần thiết có thể lên tới 1GB, vượt quá phạm vi Prettier có thể xử lý
• Tích hợp language server hay linter đều sập ngay lập tức, trên thực tế gần như chỉ còn tô sáng cú pháp là hoạt động nổi
• Bên trong engine được hiện thực bằng các số nhị phân bù hai lưu trong literal chuỗi
• TypeScript chỉ có thể duyệt chuỗi từ trái sang phải, nên mọi thuật toán nhị phân đều phải được hiện thực theo chiều ngược lại
• Bên trong engine không có mảng, đối tượng, chuỗi hay boolean, mà chỉ dùng số nhị phân
• DOOM chỉ dùng số nguyên 64-bit và 32-bit, và các số nguyên đó không phải signed cũng không phải unsigned, điều mà tác giả mất cả một ngày mới hiểu ra
• Khi bắt đầu, tác giả còn chưa biết tới 10% số kiến thức cần thiết, và đã phải tự làm công cụ, tự tay viết 12.364 bài kiểm thử, đồng thời học mới nhiều ngôn ngữ lập trình