On Complexity Bounds and Confluence of Parallel Term Rewriting

Resumo Técnico: Limites de Complexidade e Confluência em Reescrita de Termos Paralela

1. Problema e Motivação

O artigo aborda uma lacuna na literatura sobre análise de complexidade computacional: a falta de técnicas automáticas para inferir limites de complexidade (superiores e inferiores) para estratégias de reescrita de termos paralelos, especificamente a reescrita innermost (interna) paralela.

• Contexto: Muitos programas funcionais modernos (OCaml, Scala, Rust) utilizam estratégias de avaliação call-by-value, que correspondem à reescrita innermost. Com o advento de hardware massivamente paralelo (como GPUs), é crucial entender não apenas o tempo de execução sequencial (trabalho), mas também o tempo de execução paralelo (profundidade ou span).
• O Desafio: Técnicas existentes para complexidade sequencial não se aplicam diretamente ao caso paralelo. No caso paralelo, chamadas de funções independentes são avaliadas simultaneamente, o que pode reduzir drasticamente o número de passos de reescrita necessários. Além disso, para inferir limites inferiores precisos, a relação de reescrita deve ser conflua (determinística), garantindo que o resultado não dependa da ordem de avaliação.

2. Metodologia

Os autores propõem uma abordagem transformacional que reutiliza o arcabouço existente de Pares de Dependência (Dependency Pairs) e Tuplas de Dependência (Dependency Tuples - DTs), originalmente desenvolvidos para complexidade sequencial.

A metodologia divide-se em três pilares principais:

A. Tuplas de Dependência Paralelas (Parallel Dependency Tuples - PDTs)

• Em vez de agrupar todas as chamadas de função de uma regra em uma única tupla (como na análise sequencial), os autores introduzem as PDTs.
• Para uma regra $\ell \to r$, identificam as Cadeias de Dependência Estrutural Máxima (MSDC). Uma cadeia de dependência estrutural representa uma sequência de posições de símbolos definidos onde a avaliação de um depende da conclusão da avaliação do anterior (devido à estratégia innermost).
• Mecanismo: Para cada cadeia de dependência máxima, gera-se uma PDT distinta. Isso modela o fato de que, em execução paralela, o custo total de uma regra é determinado pelo "fio" (thread) mais lento entre as cadeias de dependência independentes.
• Resultado: Isso permite reutilizar processadores de complexidade existentes (como interpretações polinomiais) para calcular limites superiores para a complexidade paralela ($pirc$).

B. Transformação para Reescrita Relativa (Lower Bounds)

• Para inferir limites inferiores, os autores propõem uma transformação que converte o problema de DTs paralelas de volta para um Sistema de Reescrita de Termos (TRS) Relativo.
• Utilizam a reescrita relativa ($S / ((D \setminus S) \cup R)$), onde as regras de DTs ($S$) contribuem para a complexidade, enquanto as regras originais ($R$) e outras DTs são tratadas como "gratuitas" (custo zero) em certos contextos.
• Isso permite que ferramentas existentes de análise de complexidade (como APROVE e TCT) sejam aplicadas diretamente ao problema transformado para obter limites inferiores.

C. Critérios de Confluência para Reescrita Paralela-Interna

• A inferência de limites inferiores via a transformação acima requer que a relação de reescrita paralela ($\xrightarrow{i}_{R}$) seja conflua.
• Os autores demonstram que a confluência da reescrita sequencial não implica necessariamente a confluência paralela.
• Novos Critérios:
  1. Regras Não-Sobrepostas: Se um TRS não possui pares críticos, a reescrita paralela é determinística e, portanto, conflua.
  2. Critério de Overlays Críticos Triviais (Teorema 6.18): Um critério mais forte que exige apenas que todos os overlays críticos internos (critical overlays) sejam triviais (ambos os lados do par crítico são idênticos). Isso cobre casos onde a sobreposição de regras não gera não-determinismo real no resultado.

3. Contribuições Principais

1. Definição Formal: Formalização da complexidade de tempo de execução innermost paralela ($pirc$) para TRSs.
2. Tuplas de Dependência Paralelas (PDTs): Introdução de uma nova estrutura de dados que captura dependências estruturais para modelar a execução paralela, permitindo o uso de técnicas de análise sequencial para obter limites superiores.
3. Transformação para Limites Inferiores: Um método para transformar problemas de complexidade paralela em problemas de reescrita relativa, habilitando o uso de ferramentas de limites inferiores existentes.
4. Critérios de Confluência: Desenvolvimento de critérios sintáticos verificáveis automaticamente para garantir a confluência da reescrita paralela, essenciais para a precisão dos limites inferiores.
5. Implementação: Integração de todas as técnicas na ferramenta APROVE, tornando-a a primeira ferramenta totalmente automática para inferência de limites de complexidade para reescrita paralela.

4. Resultados Experimentais

Os autores realizaram experimentos extensivos no conjunto de benchmarks TPDB (Termination Problem Data Base) e COPS (Confluence Competition).

• Limites Superiores: A abordagem melhorou significativamente a precisão dos limites superiores. Em muitos casos, a complexidade paralela foi identificada como estritamente menor que a sequencial (ex: de $O(n^2)$ para $O(n)$). A ferramenta conseguiu inferir limites lineares para 70 TRSs onde a análise sequencial previa limites quadráticos.
• Limites Inferiores e Confluência:
  • O critério de confluência proposto (Teorema 6.18) provou ser superior ao critério de "não-sobreposição" (Corolário 6.10), provando confluência para 64,6% do conjunto de benchmarks de complexidade, contra 56,1% do critério anterior.
  • Combinando a transformação de limites inferiores com a prova de confluência, foi possível obter limites precisos ($\Theta$) para 49 TRSs.
• Desempenho: A análise de confluência é extremamente rápida (milissegundos), pois baseada em verificações sintáticas. A análise de complexidade consome mais tempo (média de ~200s por exemplo), mas é comparável ao tempo gasto por ferramentas de complexidade sequencial.

5. Significado e Impacto

• Avanço Teórico: Preenche a lacuna entre a teoria de reescrita de termos e a análise de complexidade de computação paralela, fornecendo fundamentos matemáticos para a análise de "span" (profundidade) em sistemas de reescrita.
• Aplicabilidade Prática: A implementação no APROVE demonstra que é possível analisar automaticamente o potencial de paralelização de programas funcionais representados como TRSs.
• Otimização de Compiladores: As técnicas podem auxiliar compiladores paralelos a decidir quais funções devem ser paralelizadas. Se a complexidade paralela for assintoticamente igual à sequencial, a paralelização pode ser evitada para economizar recursos.
• Hardware Específico: A análise é relevante para o uso de GPUs, onde o custo de inicialização de threads é alto e o "span" é o fator limitante.

Em suma, o artigo estabelece um framework robusto e automatizado para analisar quão rápido um programa pode rodar em um ambiente de paralelismo ilimitado, utilizando técnicas de reescrita de termos e garantindo a correção através de critérios de confluência.