Прототип языка тензоров для высокопроизводительных компьютеров

Широко распространено мнение, что при проведении операций такого рода неизбежны компромиссы между скоростью и надежностью. Если скорость является главным приоритетом, согласно этой точке зрения, то надежность, скорее всего, пострадает, и наоборот.

Тем не менее, команда исследователей, базирующаяся в основном в Массачусетском технологическом институте, ставит это понятие под сомнение, утверждая, что на самом деле можно иметь все. С новым языком программирования, который они написали специально для высокопроизводительных вычислений, говорит Аманда Лю, аспирант второго курса Лаборатории компьютерных наук и искусственного интеллекта Массачусетского технологического института (CSAIL), «скорость и корректность не должны конкурировать. Вместо этого они могут идти вместе, рука об руку, в программах, которые мы пишем».

Лю вместе с постдоком Калифорнийского университета в Беркли Гилбертом Луисом Бернстайном, доцентом Массачусетского технологического института Адамом Члипалой и доцентом Массачусетского технологического института Джонатаном Раган-Келли описали потенциал своего недавно разработанного творения «Тензорный язык» (ATL) в прошлом месяце на конференции «Принципы языков программирования» в Филадельфии.

«Все в нашем языке, — говорит Лю, — направлено на получение либо одного числа, либо тензора». Тензоры, в свою очередь, являются обобщениями векторов и матриц. В то время как векторы являются одномерными объектами (часто представленными отдельными стрелками), а матрицы являются знакомыми двумерными массивами чисел, тензоры являются n-мерными массивами, которые могут принимать форму массива 3x3x3, например, или чего-то еще более высокого (или более низкого) измерения.

Весь смысл компьютерного алгоритма или программы заключается в том, чтобы инициировать конкретное вычисление. Но может быть много разных способов написания этой программы — «ошеломляющее разнообразие различных реализаций кода», как писали Лю и ее соавторы в своей скоро опубликованной работе на конференции— некоторые значительно быстрее, чем другие. Основное обоснование ATL заключается в следующем, объясняет она: «Учитывая, что высокопроизводительные вычисления настолько ресурсоемки, вы хотите иметь возможность модифицировать или переписывать программы в оптимальную форму, чтобы ускорить работу. Часто начинаешь с программы, которую проще всего писать, но это может быть не самым быстрым способом ее запуска, так что дальнейшие корректировки все еще необходимы».

В качестве примера предположим, что изображение представлено массивом чисел 100×100, каждое из которых соответствует пикселю, и вы хотите получить среднее значение для этих чисел. Это можно сделать в двухэтапном вычислении, сначала определив среднее значение каждой строки, а затем получив среднее значение каждого столбца. У ATL есть связанный инструментарий — то, что компьютерные ученые называют «фреймворком» — который может показать, как этот двухэтапный процесс может быть преобразован в более быстрый одноэтапный процесс.

«Мы можем гарантировать, что эта оптимизация верна, используя то, что называется помощником доказательства», — говорит Лю. С этой целью новый язык команды основывается на существующем языке, Coq, который содержит помощника по доказательствам. Помощник по доказательствам, в свою очередь, обладает врожденной способностью доказывать свои утверждения математически строгим образом.

У Coq была еще одна внутренняя особенность, которая делала его привлекательным для группы, основанной на MIT: программы, написанные в нем, или его адаптации, всегда заканчиваются и не могут работать вечно на бесконечных циклах (как это может произойти с программами, написанными на Java, например). «Мы запускаем программу, чтобы получить один ответ — число или тензор», — утверждает Лю. «Программа, которая никогда не прекращается, была бы бесполезна для нас, но терминация — это то, что мы получаем бесплатно, используя Coq».

Проект ATL объединяет два основных исследовательских интереса Ragan-Kelley и Chlipala. Раган-Келли давно занимается оптимизацией алгоритмов в контексте высокопроизводительных вычислений. Хлипала, тем временем, больше сосредоточился на формальной (как в математически обоснованной) верификации алгоритмических оптимизаций. Это их первое сотрудничество. Бернштейн и Лю были привлечены на предприятие в прошлом году, и результатом является ATL.

Теперь он стоит как первый, и до сих пор только тензорный язык с формально верифицированными оптимизациями. Лю предупреждает, однако, что ATL по-прежнему является лишь прототипом, хотя и многообещающим, который был протестирован на ряде небольших программ. «Одной из наших главных целей, заглядывая в будущее, является улучшение масштабируемости ATL, чтобы его можно было использовать для более крупных программ, которые мы видим в реальном мире», — говорит она.

В прошлом оптимизация этих программ обычно выполнялась вручную, на гораздо более специальной основе, что часто включает в себя метод проб и ошибок, а иногда и много ошибок. С ATL, добавляет Лю, «люди смогут следовать гораздо более принципиальному подходу к переписыванию этих программ — и делать это с большей легкостью и большей уверенностью в правильности».