A computação de alto desempenho é necessária para um número cada vez maior de tarefas – como processamento de imagens ou vários aplicativos de aprendizado profundo em redes neurais – em que é preciso percorrer imensas pilhas de dados e fazê-lo com rapidez razoável, ou então pode ser ridículo quantidades de tempo. Acredita-se amplamente que, na realização de operações desse tipo, há trocas inevitáveis entre velocidade e confiabilidade. Se a velocidade for a principal prioridade, de acordo com essa visão, a confiabilidade provavelmente será prejudicada e vice-versa.
No entanto, uma equipe de pesquisadores, baseada principalmente no MIT, está questionando essa noção, alegando que se pode, de fato, ter tudo. Com a nova linguagem de programação, que eles escreveram especificamente para computação de alto desempenho, diz Amanda Liu, Ph.D. do segundo ano. estudante do Laboratório de Ciência da Computação e Inteligência Artificial do MIT (CSAIL), “velocidade e correção não precisam competir. Em vez disso, elas podem andar juntas, de mãos dadas, nos programas que escrevemos”.
Liu – junto com o pós-doutorando da Universidade da Califórnia em Berkeley Gilbert Louis Bernstein, o professor associado do MIT Adam Chlipala e o professor assistente do MIT Jonathan Ragan-Kelley – descreveram o potencial de sua criação recentemente desenvolvida, “A Tensor Language” (ATL), no mês passado em a conferência de Princípios de Linguagens de Programação na Filadélfia.
“Tudo em nossa linguagem”, diz Liu, “é destinado a produzir um único número ou um tensor”. Os tensores, por sua vez, são generalizações de vetores e matrizes. Enquanto os vetores são objetos unidimensionais (geralmente representados por setas individuais) e as matrizes são matrizes de números bidimensionais familiares, os tensores são matrizes n-dimensionais, que podem assumir a forma de uma matriz 3x3x3, por exemplo, ou algo ainda maior (ou menores) dimensões.
O objetivo de um algoritmo ou programa de computador é iniciar uma computação específica. Mas pode haver muitas maneiras diferentes de escrever esse programa – “uma variedade desconcertante de diferentes realizações de código”, como Liu e seus coautores escreveram em seu documento de conferência que será publicado em breve – algumas consideravelmente mais rápidas do que outras. A principal razão por trás da ATL é esta, ela explica: “Dado que a computação de alto desempenho é tão intensiva em recursos, você deseja modificar ou reescrever programas em uma forma ideal para acelerar as coisas. com um programa que é mais fácil de escrever, mas que pode não ser a maneira mais rápida de executá-lo, de modo que ainda são necessários ajustes adicionais.”
Como exemplo, suponha que uma imagem seja representada por uma matriz de números de 100 x 100, cada um correspondendo a um pixel, e você deseja obter um valor médio para esses números. Isso pode ser feito em um cálculo de dois estágios, primeiro determinando a média de cada linha e, em seguida, obtendo a média de cada coluna. A ATL tem um kit de ferramentas associado – o que os cientistas da computação chamam de “framework” – que pode mostrar como esse processo de duas etapas pode ser convertido em um processo de uma etapa mais rápido.
“Podemos garantir que essa otimização esteja correta usando algo chamado assistente de prova”, diz Liu. Para isso, a nova linguagem da equipe se baseia em uma linguagem existente, Coq, que contém um assistente de prova. O assistente de prova, por sua vez, tem a capacidade inerente de provar suas asserções de forma matematicamente rigorosa.
O Coq tinha outra característica intrínseca que o tornava atraente para o grupo baseado no MIT: programas escritos nele, ou adaptações dele, sempre terminam e não podem ser executados para sempre em loops infinitos (como pode acontecer com programas escritos em Java, por exemplo). “Executamos um programa para obter uma única resposta – um número ou um tensor”, afirma Liu. “Um programa que nunca termina seria inútil para nós, mas a terminação é algo que obtemos de graça usando o Coq.”
O projeto ATL combina dois dos principais interesses de pesquisa de Ragan-Kelley e Chlipala. Ragan-Kelley há muito se preocupa com a otimização de algoritmos no contexto da computação de alto desempenho. Chlipala, por sua vez, concentrou-se mais na verificação formal (como na matemática) de otimizações algorítmicas. Isso representa sua primeira colaboração. Bernstein e Liu foram trazidos para a empresa no ano passado, e a ATL é o resultado.
Ela agora é a primeira e até agora a única linguagem tensorial com otimizações formalmente verificadas. Liu adverte, no entanto, que o ATL ainda é apenas um protótipo – embora promissor – que foi testado em vários pequenos programas. “Um dos nossos principais objetivos, olhando para o futuro, é melhorar a escalabilidade do ATL, para que possa ser usado para os programas maiores que vemos no mundo real”, diz ela.
No passado, as otimizações desses programas geralmente eram feitas à mão, em uma base muito mais ad hoc, o que geralmente envolve tentativa e erro e, às vezes, bastante erro. Com a ATL, acrescenta Liu, “as pessoas poderão seguir uma abordagem muito mais baseada em princípios para reescrever esses programas – e fazê-lo com maior facilidade e maior garantia de correção”.
Publicado em 17/02/2022 05h22
Artigo original:
Estudo original: