HPC: MIT phát triển ngôn ngữ lập trình mới cho điện toán hiệu suất cao

Với nguyên mẫu ngôn ngữ tensor, “tốc độ và độ chính xác không phải cạnh tranh lẫn nhau… chúng có thể song hành cùng nhau!”

Điện toán hiệu suất cao (HPC) là cần thiết cho số lượng tác vụ ngày càng tăng – chẳng hạn như xử lý hình ảnh hoặc các ứng dụng học sâu khác nhau trên mạng nơ-ron – nơi người ta phải làm việc với hàng núi dữ liệu khổng lồ và tiến hành một cách tối ưu và nhanh chóng nhất, nếu không, điều đó có thể chiếm lượng thời gian vô tận. Nhiều người tin rằng, khi thực hiện các hoạt động kiểu này, không thể tránh khỏi sự đánh đổi giữa tốc độ và độ tin cậy. Từ quan điểm này, nếu tốc độ là ưu tiên hàng đầu, thì độ tin cậy có thể sẽ bị ảnh hưởng, và ngược lại.

Tuy nhiên, một nhóm các nhà nghiên cứu, chủ yếu có trụ sở tại MIT, đang đặt vấn đề về khái niệm đó, tuyên bố rằng trên thực tế, ai cũng có thể có tất cả. Amanda Liu, một nghiên cứu sinh năm thứ hai 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 mà họ đã viết riêng cho điện toán hiệu suất cao, “tốc độ và độ chính xác không nhất thiết phải cạnh tranh lẫn nhau. Thay vào đó, chúng có thể song hành, chung tay trong các chương trình mà chúng tôi viết ra”.

Giải pháp hạ tầng Deep Learning, Trí tuệ Nhân tạo - AI

Liu – cùng với Đại học California tại Berkeley postdoc Gilbert Louis Bernstein, Phó Giáo sư Adam Chlipala của MIT và Trợ lý Giáo sư Jonathan Ragan-Kelley của MIT – đã mô tả về tiềm năng của sáng kiến được phát triển gần đây của họ, “ A Tensor Language” (ATL), vào tháng trước tại hội nghị Principles of Programming Languages ở Philadelphia.

“Mọi thứ nằm trong ngôn ngữ của chúng tôi”, Liu nói, “nhằm tạo ra một con số duy nhất hoặc một Tensor.” Đến lượt mình, các Tensor là sự tổng quát hóa của vectơ và ma trận. Trong khi vectơ là các đối tượng một chiều (thường được biểu diễn bằng các mũi tên đơn) và ma trận là mảng số hai chiều quen thuộc, thì Tensor là mảng n chiều, ví dụ: có thể có dạng mảng 3x3x3 hoặc một thứ gì đó có kích thước cao hơn (hoặc thấp hơn).

Toàn bộ mấu chốt của một thuật toán hoặc chương trình máy tính là sự khởi tạo một phép tính cụ thể. Nhưng có thể có nhiều cách khác nhau để viết chương trình đó – “một loạt các cách thực hiện với mã thực thi khác nhau sẽ gây hoang mang”, Liu và các đồng tác giả của cô đã viết trong bài báo sắp được xuất bản của họ – một số sẽ nhanh hơn đáng kể so với những cách khác. Cô giải thích lý do chính đằng sau ATL là: “Do HPC tiêu tốn nhiều tài nguyên nên bạn có thể muốn sửa đổi hoặc viết lại các chương trình thành một dạng tối ưu để tăng tốc độ. Người ta thường bắt đầu với một chương trình dễ viết nhất, nhưng đó có thể không phải là cách nhanh nhất để chạy nó, do đó vẫn cần phải điều chỉnh thêm”.

Ví dụ: giả sử một hình ảnh được đại diện bởi một mảng số có kích thước 100 × 100, mỗi số tương ứng với một pixel và bạn muốn lấy giá trị trung bình cho những con số này. Điều đó có thể đượ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ái mà các nhà khoa học máy tính gọi là “framework” – cho thấy quy trình hai bước này có thể được chuyển đổi thành quy trình một bước nhanh hơn như thế nào.

Liu nói: “Chúng tôi có thể đảm bảo rằng sự tối ưu hóa này là chính xác bằng cách sử dụng một thứ gọi là trợ lý xác thực (proof assistant). Hướng tới mục tiêu này, ngôn ngữ mới của nhóm được xây dựng dựa trên một ngôn ngữ hiện có, Coq, có chứa một proof assistant. Đến lượt, proof assistant lại có khả năng để chứng minh các khẳng định của mình theo phương thức toán học nghiêm ngặt.

Coq có một đặc điểm nội tại khác khiến nó trở nên hấp dẫn đối với nhóm dựa trên MIT: các chương trình được viết trong đó, hoặc các bản chuyển thể của nó, luôn kết thúc và không thể chạy mãi mãi trên các vòng lặp vô tận (chẳng hạn như có thể xảy ra với các chương trình được viết bằng Java). “Chúng tôi 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,” Liu nói. “Một chương trình không bao giờ kết thúc sẽ vô dụng đối với chúng tôi, nhưng sự kết thúc là thứ mà chúng tôi nhận được miễn phí bằng cách sử dụng Coq”.

Dự án ATL kết hợp hai trong số các mối quan tâm nghiên cứu chính của Ragan-Kelley và Chlipala. Ragan-Kelley từ lâu đã quan tâm đến việc tối ưu hóa các thuật toán trong bối cảnh của điện toán hiệu suất cao. Trong khi đó, Chlipala đã tập trung nhiều hơn vào việc xác minh cho việc tối ưu hóa thuật toán (như trong việc xác minh dựa trên toán học). Điều này thể hiện sự hợp tác đầu tiên của họ. Bernstein và Liu đã được thành lập vào năm ngoái, và kết quả là sự ra đời của ATL.

Hiện tại, nó là ngôn ngữ tensor đầu tiên và cho đến nay là ngôn ngữ tensor duy nhất có các tính năng tối ưu đã được xác minh chính thức. Tuy nhiên, Liu cảnh báo rằng ATL vẫn chỉ là một prototype – mặc dù là một prototype đầy hứa hẹn – đã được thử nghiệm trên một số chương trình nhỏ. “Một trong những mục tiêu chính của chúng tôi, nhìn về phía trước, là cải thiện khả năng mở rộng của ATL, để nó có thể được sử dụng cho các chương trình lớn hơn mà chúng tôi thấy trong thế giới thực,” cô nói.

Trước đây, việc tối ưu hóa các chương trình này thường được thực hiện bằng tay, trên cơ sở ngẫu nhiên (ad-hoc) hơn nhiều, thường liên quan đến việc thử và sai, và đôi khi có rất nhiều lỗi. Với ATL, Liu nói thêm, “mọi người sẽ có thể tuân theo một cách tiếp cận có nguyên tắc hơn nhiều để viết lại các chương trình này – và làm như vậy một cách dễ dàng hơn và đảm bảo tính đúng đắn hơn.”

Theo SciTechDaily

____
Bài viết liên quan