Apresentando Matrizes de Limite de Diferença Estridada na Otimização de Compiladores

Um monte de problemas em matemática e ciência da computação podem ser representados usando formas chamadas poliedros. Grupos menores dessas formas, conhecidos como domínios sub-poliedrais, são úteis porque ocupam menos espaço e requerem menos tempo para lidar. Este artigo apresenta um novo tipo de domínio sub-poliedral chamado Matriz de Limites de Diferença Estridada (SDBM), que é especialmente útil para compiladores de otimização. A SDBM tem capacidades fortes e métodos eficientes que a tornam perfeita para compiladores de aprendizado de máquina. Este trabalho descreve métodos de decisão, operadores de domínio e provas relacionadas à complexidade das SDBMs. Um estudo empírico com o framework de compilador MLIR confirma a utilidade desse domínio em aplicações do mundo real. Também identificamos um tipo específico de SDBM que aparece com frequência na prática, mostrando algoritmos ainda mais rápidos para esse tipo.

#Introdução e Motivação

Ao analisar e verificar sistemas de computador, vários modelos são usados para representar como esses sistemas funcionam. Modelos numéricos focam nas características aritméticas das variáveis do sistema e suportam projetos matemáticos de diferentes sistemas, como sistemas de temporização e modelos híbridos, que combinam aspectos contínuos e discretos. Esses modelos ajudam a analisar loops e programas recursivos de forma eficaz.

Muitos desses modelos numéricos dependem de um tipo especial de matemática chamado aritmética de Presburger, onde problemas de decisão comuns são desafiadores e classificados como NP-difíceis. A versão mais simples desses problemas envolve casos não relacionais, como limites de intervalo onde uma variável tem um limite numérico específico. Versões mais complexas envolvem desigualdades que representam relações entre várias variáveis, como sistemas de desigualdades conhecidas como sistemas Unit Two Variable Per Inequality (UTVPI). Esses sistemas formam o que é chamado de domínio abstrato octogonal. Sistemas UTVPI são mais baratos de trabalhar do que formas complexas, mas ainda capturam muitos problemas de múltiplas variáveis.

Os algoritmos para sistemas UTVPI usam representações chamadas Matrizes de Limites de Diferença (DBMs), que podem expressar desigualdades entre variáveis. DBMs são amplamente usadas em verificação formal e análise estática de programas. Outros modelos numéricos, como Congruências, que focam em combinações lineares de variáveis inteiras, tendem a perder os aspectos importantes das desigualdades.

Um tipo específico de igualdades de congruência, onde certas variáveis estão fixadas a valores específicos, tem baixa complexidade. Esse cenário é útil ao melhorar outros modelos abstratos. No entanto, ainda não está claro se existem algoritmos eficientes para combinar UTVPI com restrições de congruência. Encontrar uma maneira de fundir esses dois teria muitas aplicações úteis na análise e otimização de modelos de aprendizado de máquina.

Compiladores modernos de aprendizado de máquina costumam usar formas de representação de Presburger para várias operações, como layouts de dados de memória e mudanças de formatação, como reestruturação. Expressões afins também aparecem durante mudanças de programas para otimizar hardware, incluindo vetorização e processamento paralelo. A maioria dessas expressões lida com formas hiperrretangulares, mas às vezes inclui formas mais complexas.

Certas operações, como convoluções e normalização, produzem valores relacionados a estridamentos e tamanhos que precisam de restrições de congruência. Embora otimizações avançadas de compiladores frequentemente dependam de bibliotecas completas de aritmética de Presburger, casos mais simples requerem um modelo que combina UTVPI e congruências que opera em polinômios de menor grau. Esse modelo também poderia beneficiar esforços de verificação que atualmente usam bibliotecas de aritmética de Presburger.

Este trabalho investiga a combinação de desigualdades representadas por DBMs com congruências de uma única variável, criando um novo domínio abstrato chamado Matrizes de Limites de Diferença Estridada (SDBM). Também analisamos uma versão especial conhecida como SDBM Harmônica (HSDBM), onde as condições de congruência formam um conjunto ordenado que frequentemente surge de mudanças de laços em código de alto desempenho.

Embora o problema de satisfabilidade da SDBM pareça complexo, fornecemos um algoritmo que roda em um intervalo de tempo gerenciável. Essa complexidade de tempo, que é prática para aplicações de análise de programas, nos permite desenvolver algoritmos para HSDBM também.

Para finalizar, estabelecemos uma forma padrão para sistemas de restrições SDBM que podem ser computados de forma eficiente. Também mostramos que dois sistemas em forma padrão podem ser processados rapidamente, levando a um conjunto de soluções que combina suas soluções, o que é comum em interpretação abstrata.

#DBMs, SDBMs e HSDBMs

Ao discutir conjuntos com elementos inteiros, focamos em subconjuntos de inteiros. Definimos alguns termos para clareza. Se um gráfico não tem ciclos negativos, a distância entre dois vértices pode ser calculada.

Descrevemos formalmente Matrizes de Limites de Diferença (DBM), que são sistemas de restrição envolvendo variáveis e desigualdades. Não é necessário que todos os limites superiores e inferiores para as variáveis estejam presentes em uma DBM. Quando não há limites de variável presentes, chamamos de livre de limites de variável (VBF); caso contrário, tem limites de variável. A satisfabilidade das restrições DBM pode ser determinada em um tempo razoável.

Em seguida, apresentamos a SDBM. Uma DBM Estridada mantém a estrutura de uma DBM, mas adiciona restrições de congruência específicas. Uma SDBM Harmônica (HSDBM) refere-se a uma SDBM onde as condições de congruência são organizadas de modo que cada uma divide a próxima.

Para simplificar o problema de satisfabilidade da SDBM, demonstramos que pode ser reduzido a checar sistemas mais simples de SDBMs, onde todas as restrições de congruência têm um resto de zero. Essa abordagem reduz a complexidade de encontrar soluções.

Fornecemos métodos para converter SDBMs para uma forma mais simples. Quando uma solução existe, a SDBM pode ser manipulada sem mudar suas propriedades. O processo de conversão de SDBMs para SDBMs simples é eficiente e garante que as soluções permaneçam válidas.

No caso de HSDBMs, mostramos que operações de fechamento de caminhos e aperto de MDC são suficientes para confirmar a satisfabilidade. Podemos realizar projeções dos conjuntos de soluções, levando a soluções que se conformam tanto com as desigualdades quanto com as condições de congruência.

#Satisfabilidade para HSDBMs em Tempo

Para HSDBMs, assumimos que o sistema é simples e realiza operações para garantir que todos os componentes sejam apertados e válidos. As projeções dos conjuntos de soluções permitem uma análise adicional de limites e congruências. Usando descobertas anteriores, podemos determinar soluções baseadas em variáveis projetadas.

Ao verificar se uma HSDBM é válida, o fechamento de caminhos e o aperto de MDC são suficientes para estabelecer se uma solução existe. Por meio de métodos como SolveHSDBM, que une passos de fechamento de caminhos e aperto, confirmamos se nossos sistemas são satisfáveis.

#Satisfabilidade para SDBMs em Tempo

O problema de determinar a satisfabilidade de SDBMs é desafiador e atualmente é considerado NP-difícil, significando que não se conhecem algoritmos em tempo polinomial. No entanto, propomos uma abordagem que funciona de forma eficiente dentro do tamanho das restrições. O algoritmo SDBM foca nos valores das restrições de congruência, que tendem a ser menores em comparação aos limites estabelecidos pelas desigualdades.

Transformando o problema SDBM em uma forma mais gerenciável, podemos encontrar soluções efetivamente. O método proposto envolve identificar soluções inteiras para as restrições de desigualdade e ajustar cuidadosamente os limites das variáveis.

Para otimizar nossa abordagem, discutimos como apertar limites para evitar soluções indesejadas. A técnica de aperto de MDC garante que os valores permaneçam alinhados com as propriedades necessárias, enquanto o fechamento de caminhos mantém a integridade do sistema de restrição.

Por fim, realizamos normalização nos sistemas HSDBM, garantindo que as desigualdades sejam tão apertadas quanto possível. Essa etapa garante que quaisquer limites estejam realmente refletindo as soluções disponíveis dentro do sistema, melhorando assim a análise geral.

#Aplicações à Validação de Traduções

Também exploramos a aplicação de nossos métodos na validação de traduções, especialmente com modelos de aprendizado de máquina. Os frameworks para processar esses modelos são configurados para usar nossa proposta de SDBM durante todo o processo de compilação.

Analisamos vários modelos de aprendizado de máquina, convertendo-os em representações adequadas para processamento adicional. Durante esse processo, verificamos como as representações SDBM se sustentam em cenários práticos, garantindo que as operações e transformações suportem consistentemente os requisitos do modelo.

Os resultados demonstram que a SDBM pode representar com precisão muitas das expressões e estruturas comumente encontradas em ambientes de aprendizado de máquina. Os estudos mostram forte compatibilidade da SDBM com vários modelos, enfatizando seu potencial em diferentes estágios de processamento de modelos.

#Estudo Empírico

Uma parte significativa da investigação envolve analisar a eficácia da SDBM em aplicações do mundo real. Instrumentamos vários compiladores estabelecidos usando SDBM para avaliar sua prevalência e adequação em ambientes práticos.

Esses compiladores cobrem uma ampla gama de usos, desde aprendizado de máquina até design de hardware. Focamos em quantas expressões e conjuntos podem ser representados dentro da estrutura SDBM e quantificamos isso em termos de taxas de sucesso durante a compilação.

Nossas descobertas revelam que a maioria das expressões afins nesses testes pode, de fato, ser representada usando SDBM. Isso sugere que a SDBM está equipada para lidar com uma vasta gama de construtos encontrados nas infraestruturas de compilador. Apesar de algumas limitações em casos extremos, os resultados indicam alta adequação para uso de ponta a ponta em muitos cenários computacionais.

No geral, a SDBM e a HSDBM demonstram um potencial significativo para aumentar a eficiência e a precisão dos processos de interpretação abstrata, particularmente no reino das otimizações de compiladores e aprendizado de máquina. A pesquisa estabelece as bases para futuras explorações em tornar os compiladores mais eficazes usando essas novas representações.