Vx: Ngôn ngữ lập trình hệ thống cho mọi loại chip

Vx là một ngôn ngữ lập trình hệ thống dành cho điện toán không đồng nhất (heterogeneous computing), trong đó bộ nhớ của CPU, GPU, NPU và các bộ tăng tốc là một phần của hệ thống kiểu. Điều này có nghĩa là việc một luồng máy chủ truy cập con trỏ thiết bị sẽ trở thành lỗi biên dịch, chứ không phải lỗi segmentation fault vào lúc ba giờ sáng.

Ngôn ngữ này hướng tới các kỹ sư cần viết mã chính xác và nhanh trên nhiều loại silicon khác nhau, thay vì phụ thuộc vào runtime khổng lồ để quyết định cách phân phối tính toán.

Định vị dữ liệu nằm trong hệ thống kiểu

Hầu hết các ngôn ngữ coi bộ tăng tốc là hạ tầng: bạn viết phép toán, và một runtime lớn không minh bạch sẽ quyết định cách gửi nó đi. Vx coi đó là ngữ nghĩa. Một tensor được ghim vào bộ nhớ băng thông cao của NPU có kiểu khác với tensor nằm trong DRAM của máy chủ, và việc chuyển đổi giữa chúng đòi hỏi một lệnh transfer() tường minh — ngay cả khi ranh giới phần cứng là miễn phí.

Trên bộ nhớ hợp nhất của Apple, lệnh chuyển đổi đó biên dịch thành gần như không có gì. Nhưng nó vẫn được viết ra, bởi vì tính cục bộ của dữ liệu nên có thể chứng minh được bằng cách đọc mã nguồn thay vì phải profiling file nhị phân.

// Hai ma trận đã nằm sẵn trong bộ nhớ NPU.
fn custom_matmul(
    a: Pinned, Topology::NPU[0]>,
    b: Pinned, Topology::NPU[0]>)
    -> Verified> {
    let mut result =
        Tensor::uninit();

    // Gửi tính toán tới bộ tăng tốc.
    spawn on(Topology::NPU[0]) {
        for i in 0..4 {
            for j in 0..4 {
                result[i][j] = 0.0;
                for k in 0..4 {
                    result[i][j] += a[i][k] * b[k][j];
                }
            }
        }
    }
    return Verified(result);
}

Những gì trình biên dịch loại trừ

Vx đưa một loạt lỗi thường xuất hiện dưới dạng crash runtime, hỏng dữ liệu âm thầm hoặc hết bộ nhớ ở bước huấn luyện thứ 1200 vào giai đoạn kiểm tra kiểu.

• Định kiểu không gian địa chỉ: Truy cập con trỏ thiết bị từ máy chủ, hoặc một Pinned thoát vào biểu thức máy chủ.
• Kiểm tra dung lượng: Một vị trí đặt có tập làm việc không vừa với không gian bộ nhớ mục tiêu — được kiểm tra dựa trên máy đã khai báo, trước khi file nhị phân tồn tại.
• Hợp đồng đường nối: Đọc một buffer mà quá trình chuyển đổi bất đồng bộ chưa được hiển thị. Được giải quyết bằng bộ chứng minh SMT.
• Kiểu tuyến tính: Sử dụng sau khi di chuyển của một buffer đã bị tiêu thụ, cùng với bộ kiểm tra mượn có variance và theo dõi vùng.
• Khả năng tiếp cận topology: Chuyển đổi giữa hai không gian bộ nhớ không có đường dẫn nào được khai báo giữa chúng.
• Vi phân tự động: Vi phân qua một vùng mà adjoint của nó không được định nghĩa.

Máy được khai báo, không phải giả định

Hầu hết các trình biên dịch hard-code một mô hình chi phí. Vx đọc một mô hình. Một file máy mô tả hệ thống phân cấp bộ nhớ và kết nối của một linh kiện thực, và trình biên dịch chấp nhận hoặc từ chối các vị trí đặt dựa trên đó.

Các đơn vị là chuyển đổi số nguyên chính xác, không bao giờ dùng số thực: tiền tố SI là thập phân (GB = 10⁹), IEC là nhị phân (GiB = 2³⁰). Một con số sao chép từ bảng thông số nhà cung cấp có nghĩa đúng như bảng đó muốn nói.

Kho lưu trữ cung cấp sẵn các file máy cho H100, H200, B200, A100, MI300X, Apple M4 và các node đa GPU — mỗi file đều trích dẫn nguồn, và đánh dấu rõ những số liệu chưa được xác minh.

Memory HBM  { capacity: 80 GiB, bandwidth: 3.35 TB/s,
              managed: explicit, scope: device }
Memory L2   { within: Memory::HBM, capacity: 50 MiB,
              bandwidth: 12 TB/s, managed: cached }
Memory SMEM { within: Memory::L2, capacity: 228 KiB,
              bandwidth: 128 B/cyc, clock: 1.98 GHz,
              replicas: 132, granule: 1 KiB, scope: sm }

Topology Device {
  arch: nvptx64,
  memory: Memory::HBM,
  transfer Memory::CPU_DRAM -> Memory::HBM : 63 GB/s,
}

Cách thức biên dịch

Frontend song song hướng dữ liệu

Mỗi ký hiệu, kiểu danh nghĩa và biến thể monomorphized là một định danh phẳng 256-bit. Hệ thống kiểu danh nghĩa cộng với việc đóng hộp bắt buộc cho các kiểu đệ quy giúp tách rời các module, cho phép pipeline chạy song song trên nhiều lõi mà không cần query engine và không có tranh chấp khóa. Quá trình biên dịch duyệt qua các mảng phẳng thay vì các cây bám con trỏ.

Cùng một mã nguồn biên dịch thành MLIR giống hệt từng byte dù được xây dựng tuần tự hay song song. Điều này được khẳng định trong bộ kiểm thử chứ không phải chỉ hy vọng — ở quy mô benchmark, tại một luồng, bốn luồng, và với thread pool bị loại khỏi đường dẫn hoàn toàn.

Backend

• CPU (x86-64, arm64): MLIR → LLVM IR → native, AOT hoặc JIT
• GPU NVIDIA: MLIR → NVVM → PTX → SASS
• Apple AMX / ANE: Điều phối primitive CoreML qua plugin
• Phân tán: Các vùng từ xa điều khiển bởi manifest qua giao thức truyền dẫn

Các nhà cung cấp mở rộng trình biên dịch thông qua plugin pass MLIR thay vì vá trực tiếp vào nó.

Khi nào Vx là công cụ sai

Người dùng PyTorch thay đổi kiến trúc giữa vòng lặp, in hình dạng tensor, rẽ nhánh dựa trên nó, rồi tiếp tục. Trong Vx — với tính chất ahead-of-time, hướng dữ liệu, vùng tĩnh — sự năng động đó đòi hỏi công sức thực sự.

Vx là ngôn ngữ đúng cho thứ cần chính xác và nhanh trên mười loại silicon. Nó không phải là ngôn ngữ đúng cho thứ bạn vẫn đang tìm hiểu.

Với lập trình viên Việt Nam đang làm việc trong lĩnh vực AI, tính toán hiệu năng cao hoặc phát triển trên các nền tảng đa phần cứng, Vx đáng để theo dõi như một hướng tiếp cận mới cho bài toán mà hiện tại vẫn thường được giải quyết bằng CUDA, ROCm hay các framework runtime nặng nề.

Bắt đầu từ đâu

• Hướng dẫn nhập môn: Cài đặt toolchain và chạy chương trình đầu tiên.
• Tham quan Vx: Toàn bộ ngôn ngữ trong một lần đọc: kiểu, generic, quyền sở hữu.
• Topology và bộ nhớ: Vị trí đặt, chuyển đổi, và những gì trình kiểm tra thực thi.
• File máy: Mô tả một linh kiện thực; biên dịch dựa trên giới hạn của nó.

Mã nguồn có sẵn trên GitHub. Cài đặt nhanh trên macOS Apple Silicon và Linux x86_64 bằng lệnh:

curl -fsSL https://vxlang.org/install.sh | sh