MIT створює нову мову програмування для високопродуктивних комп’ютерів
Високопродуктивні обчислення необхідні для таких завдань, як обробка зображень або глибоке навчання в нейронних мережах. Тут потрібно обробляти великі обсяги даних, причому робити це швидко. Однак при виконанні таких операцій неминучий компроміс між швидкістю і надійністю: якщо швидкість є головним пріоритетом, то, швидше за все, постраждає надійність, і навпаки.
У Массачусетському технологічному інституті впевнені, що швидкість і правильність не повинні конкурувати один з одним. Натомість вони можуть йти «пліч-о-пліч».
Ось як описують там нову, недавно розроблену «Тензорну мову» A Tensor Language (ATL), яка призначена для високопродуктивних обчислень. У цій мові все спрямовано на створення чи числа, чи тензора. У той час як вектори – це одномірні об’єкти (часто представлені окремими стрілками), а матриці – двомірні масиви чисел, то тензори – це n-мірні масиви, які можуть набувати форми масиву 3x3x3, наприклад.
Весь сенс комп’ютерного алгоритму чи програми у тому, щоб ініціювати конкретне обчислення. Але може бути багато різних способів написання цієї програми. Основна причина використання ATL полягає в наступному: «високопродуктивні обчислення настільки ресурсомісткі, що ви захочете мати можливість модифікувати їх для приведення до оптимальної форми, щоб прискорити процес. Часто починають із програми, яку найлегше написати, але це може бути не найшвидший спосіб її запуску, тому все ще необхідні подальші коригування».
Як приклад припустимо, що зображення представлене масивом чисел 100×100, кожне з яких відповідає пікселю, і ви хочете отримати середнє для цих чисел. Результат можна отримати у двоетапному обчисленні, спочатку визначивши середнє значення кожного рядка, а потім отримавши середнє значення кожного стовпця. ATL має відповідний інструментарій — те, що програмісти називають «структурою», — який може показати, як цей двоетапний процес можна перетворити на швидший одноетапний процес.
Повідомляється, що нова мова ґрунтується на існуючій мові Coq, яка містить помічника з перевірки. Помічник за доказом, у свою чергу, має здатність доводити свої твердження математично суворим чином.
У Coq є ще одна невід’ємна особливість, яка зробила його привабливим для групи з Массачусетського технологічного інституту: програми, написані на ньому, або його адаптації завжди завершуються і не можуть працювати в нескінченних циклах (як це може статися, наприклад, з програмами, написаними на ньому на Java). «Ми запускаємо програму, щоб отримати єдину відповідь – число чи тензор. Програма, яка ніколи не завершується, була б для нас марною, але завершення це те, що ми отримуємо безкоштовно, використовуючи Coq», кажуть у MIT.
Тепер це перша і поки що єдина тензорна мова з формально перевіреними оптимізаціями. Однак ATL все ще є прототипом, хоч і перспективним, який був протестований на ряді невеликих програм. Розробники заявляють, що однією з головних цілей є покращення масштабованості ATL, щоб його можна було використовувати для більших програм, які є у реальному світі.
У минулому оптимізація цих програм, як правило, виконувалася вручну, що часто змушувало робити багато підходів і призводило до багатьох помилок. За допомогою ATL розробники зможуть оптимізувати програми набагато швидше та з мінімальною кількістю помилок.
