Máy tính hiệu suất cao rất cần thiết để thực hiện các nhiệm vụ với số lượng tác vụ ngày càng tăng như xử lý hình ảnh, các ứng dụng học sâu khác nhau trên mạng nơron thần kinh, phải xử lý một khối lượng dữ liệu khổng lồ với tốc độ nhanh chóng hợp lý.
Một nhóm nhà nghiên cứu, chủ yếu thuộc MIT, tuyên bố rằng trên thực tế, đều có thể đáp ứng được cả tốc độ và độ chính xác. Amanda Liu, nghiên cứu sinh TS năm thứ 2 tại Phòng thí nghiệm Khoa học Máy tính và Trí tuệ Nhân tạo (CSAIL) cho biết, với ngôn ngữ lập trình mới, viết riêng cho máy tính hiệu suất cao, tốc độ và độ chính xác không cần phải cạnh tranh. Thay vào đó, cả hai yêu cầu này đều được đáp ứng trong các chương trình được viết.
Liu cùng với TS Gilbert Louis Bernstein thuộc Đại học California tại Berkeley, PGS Adam Chlipala và PGS Jonathan Ragan-Kelley của MIT giới thiệu tiềm năng của ngôn ngữ sáng tạo mới được phát triển “ A Tensor Language ” (ATL) vào tháng 1/2022 tại hội nghị Nguyên tắc của Ngôn ngữ Lập trình ở Philadelphia.
Mọi chương trình viết bằng ngôn ngữ mới nhằm tạo ra một số duy nhất hoặc một tensor. Tensor là tổng quát của vectơ và ma trận. Vector là các đối tượng một chiều (thường được biểu diễn bằng mũi tên) và ma trận là mảng số 2 chiều, tensor là mảng n chiều như có dạng mảng 3x3x3 hoặc có kích thước cao hơn hay thấp hơn.
Do máy tính hiệu suất cao tiêu tốn nhiều tài nguyên nên cần phải viết các chương trình thành một dạng tối ưu để tăng tốc độ. Giả sử 1 ảnh được đại diện bởi một mảng 100 × 100 số, mỗi số tương ứng với một pixel và cần lấy giá trị trung bình cho những con số này. Điều đó được thực hiện trong một phép tính hai giai đoạn bằng cách xác định giá trị trung bình của mỗi hàng và sau đó lấy giá trị trung bình của mỗi cột. ATL có một bộ công cụ liên quan, được gọi là “khuôn khổ” khiến quy trình hai bước này được chuyển đổi thành quy trình một bước nhanh hơn.
Phương pháp mới đảm bảo sự tối ưu hóa này chính xác bằng giải pháp sử dụng công cụ, được gọi là trợ lý chứng minh. Ngôn ngữ mới của nhóm được xây dựng trên cơ sở một ngôn ngữ hiện có, Coq chứa một trợ lý chứng minh. Trợ lý chứng minh có khả năng chứng minh các khẳng định theo phương thức toán học nghiêm ngặt.
Coq còn có một đặc điểm nội hàm khác, các chương trình được viết bằng Coq hoặc các bản chuyển thể luôn kết thúc và không thể chạy mãi trên các vòng lặp vô tận (điều đó có thể xảy ra với các chương trình được viết bằng Java). Chạy một chương trình để có một câu trả lời duy nhất, một số hoặc một tensor.
ATL hiện nay là ngôn ngữ tensor đầu tiên và duy nhất có những tính năng tối ưu đã được xác minh chính thức.
Với ATL, các kỹ sư phần mềm có thể tuân thủ phương pháp tiếp cận có nguyên tắc để viết lại các chương trình nhằm tối ưu hóa các máy tính hiệu suất cao dễ dàng hơn và đảm bảo tính chính xác.
