Resumo Técnico: PaSTTeL

Declaração do Problema

Provar a terminação ou não terminação de programas é um problema fundamental, porém indecidível, na ciência da computação. Uma abordagem prática envolve a busca por argumentos explícitos: um argumento de terminação (ex: uma função de ranking linear) implica terminação, enquanto um argumento de não terminação (ex: um conjunto de recorrência linear ou um argumento de não terminação geométrica) implica não terminação. Essas análises são frequentemente aplicadas a programas lasso — traços de execução consistindo em código de linha reta seguidos por um único laço while, representando caminhos infinitos candidatos frequentemente extraídos durante a síntese de terminação baseada em CEGAR.

Embora argumentos específicos de terminação ou não terminação sejam decidíveis, o problema geral permanece desafiador. As ferramentas de estado da arte existentes frequentemente empregam estratégias sequenciais, e há uma necessidade de um framework unificado que possa integrar diversos algoritmos de análise, executá-los concorrentemente e servir como um componente modular para ferramentas de verificação externas.

Metodologia: O Framework PaSTTeL

Os autores apresentam o PaSTTeL (Parallel analysiS framework for Termination and non-Termination of Lasso programs), um framework de portfólio modular, genérico e paralelo implementado em C++17. A arquitetura é projetada para unificar abordagens de terminação e não terminação dentro de um modelo de execução concorrente.

Arquitetura Central

O framework é estruturado em torno de três componentes primários, ilustrados em um design modular:

1. Mecanismo SMT (SMTSolverInterface): Uma camada de abstração que permite a troca de solvers SMT. A implementação atual suporta Z3 e CVC5. A instância do solver é passada para analisadores sequenciais para técnicas baseadas em restrições.
2. Analisador Sequencial (AnalysisInterface): Um adaptador que define a interface para estratégias individuais de terminação ou não terminação. Métodos chave incluem:
   • analyze(): Executa a análise e retorna um resultado (TERMINATING, NON_TERMINATING ou UNKNOWN).
   • getProof(): Retorna um certificado de prova em texto simples.
3. Camada de Paralelização (PortfolioAnalyzer): Gerencia a execução concorrente de múltiplas estratégias registradas no mesmo programa lasso de entrada. Ela lida com o deployment de threads, registro de estratégias e agregação de resultados.

Instanciação e Integração

O PaSTTeL é projetado como uma biblioteca autossuficiente. Para instanciar o framework, o usuário adapta uma função init-PaSTTeL (Algoritmo 1) que:

• Cria múltiplas instâncias de solvers SMT baseadas no tipo desejado (Z3 ou CVC5).
• Inicializa o PortfolioAnalyzer com o programa lasso e a contagem de threads.
• Registra técnicas de análise específicas (ex: síntese de terminação, argumentos de não terminação) no portfólio.
• Lança a busca concorrente via solve() e aguarda por um resultado conclusivo ou um limite de tempo via join().

Prova de Conceito: P-ULR

Para validar a genericidade do framework, os autores instanciaram o PaSTTeL para replicar as capacidades principais do Ultimate LassoRanker (ULR), uma ferramenta de estado da arte e vencedora do SV-COMP 2025. Esta instanciação, denominada P-ULR, implementa:

• Manipulação de Entrada: Um formato de entrada baseado em JSON seguindo padrões SMT-LIB com suporte a Single Static Assignment (SSA). Ele lineariza programas lasso onde necessário.
• Estratégias de Terminação: Síntese baseada em restrições usando templates de ranking linear, especificamente templates de ranking afim e aninhado.
• Estratégias de Não Terminação: Síntese baseada em restrições incluindo verificação de ponto fixo e Argumentos de Não Terminação Geométrica (GNTA).

Nota sobre Limitações: A implementação atual do P-ULR possui restrições específicas: ela não cobre totalmente casos não lineares (ex: operações complexas de arrays), depende de fórmulas lineares para a maioria das estratégias e atualmente suporta apenas QF_LRA para terminação e QF_LIA para GNTA.

Resultados Experimentais

O framework foi avaliado em 4.619 programas lasso derivados dos repositórios SV-COMP 2025, TermCOMP 2025 e Ultimate. Os experimentos foram conduzidos em uma máquina com 16 processadores Intel Core i5-14400T e 30 GB de memória, com um timeout de 600 segundos por instância.

Comparação de Desempenho

O estudo comparou três configurações:

1. ULR-Baseline: A ferramenta ULR original executando estratégias sequencialmente.
2. P-ULR-Seq: PaSTTeL executando as mesmas estratégias sequencialmente (para garantir uma comparação justa).
3. P-ULR-Par4: PaSTTeL executando com 4 threads concorrentes (Fixpoint, GNTA, Affine, Nested).

Principais Descobertas:

• Eficiência Sequencial: O P-ULR-Seq superou o ULR-Baseline, alcançando uma economia de tempo total de 862 segundos (~14 minutos). Notavelmente, o tempo acumulado para síntese de não terminação caiu de 47,13s para 1,78s (uma redução de 26x).
• Análise de Terminação: O P-ULR-Seq reduziu significativamente o tempo para encontrar funções de ranking. No entanto, o ULR-Baseline ocasionalmente produziu funções de ranking mais simples devido a um passo de particionamento interno que o P-ULR atualmente não possui.
• Análise de Não Terminação: O P-ULR-Seq demonstrou uma vantagem clara ao lidar com provas de não terminação complexas (GNTA) comparado ao baseline.
• Execução Paralela: O P-ULR-Par4 reduziu o tempo total de execução por um fator de 2,8 em relação ao ULR-Baseline. No entanto, o ganho de velocidade sobre o P-ULR-Seq foi marginal. Os autores atribuem isso à composição do benchmark: 98% dos programas lasso admitiam uma função de ranking afim, que o P-ULR-Seq resolve imediatamente em sua ordem sequencial, deixando pouco espaço para estratégias paralelas melhorarem o desempenho neste dataset específico.

Significância e Contribuições

O artigo afirma que o PaSTTeL demonstra com sucesso que um framework modular e genérico pode unificar técnicas de ponta de terminação e não terminação sem comprometer o desempenho. As principais contribuições são:

1. Modularidade: Um design que facilita a integração de novos algoritmos de análise em um portfólio unificado.
2. Concorrência: A capacidade de executar estratégias registradas concorrentemente para acelerar a análise.
3. Reusabilidade: Um componente de biblioteca C++ autossuficiente que permite que projetos externos incorporem capacidades de análise de (não) terminação sem precisar entender o design interno.
4. Desempenho Competitivo: A instanciação (P-ULR) performa competitivamente contra a ferramenta original ULR, com acelerações significativas na síntese de não terminação e no tempo de execução geral, validando a eficiência do framework.

Os autores concluem que, embora a implementação atual tenha limitações em relação à aritmética não linear e passos de otimização específicos, o framework fornece uma base robusta para futuras extensões, como a integração de síntese de conjuntos de recorrência e o suporte para aritmética não linear (QF_NRA/QF_NIA).