Resumo Técnico: Eliminação Rápida de Quantificadores de Ramsey em LIRA

Declaração do Problema

A verificação de programas, particularmente para sistemas de estado infinito, frequentemente requer o raciocínio sobre propriedades que não são expressáveis na lógica de primeira ordem padrão. Embora os resolvedores de Satisfatibilidade Modulo Theories (SMT) lidem efetivamente com propriedades de segurança usando teorias de primeira ordem (por exemplo, Aritmética Inteira Linear - LIA, Aritmética Real Linear - LRA), provar vivacidade (como a terminação) normalmente requer o raciocínio sobre o bem-fundamento. Esta propriedade não é definível em primeira ordem, mesmo com predicados recursivos.

Trabalhos recentes propuseram quantificadores de Ramsey como um framework unificado para lidar com tais propriedades. Um quantificador de Ramsey, denotado por $\exists^{\text{ram}} x, y: \phi(x, y, z)$, afirma a existência de um clique direcionado infinito no grafo definido por $\phi$. Especificamente, é verdadeiro se existir uma sequência infinita de vetores distintos entre si $a_1, a_2, \dots$ tal que $\phi(a_i, a_j, z)$ seja verdadeiro para todo $1 \le i < j$. Este formalismo permite a codificação de vivacidade e decomponibilidade monádica.

No entanto, apesar das provas teóricas de que os quantificadores de Ramsey podem ser eliminados em tempo polinomial para os fragmentos existenciais de LIA, LRA e o caso misto (LIRA), a implementação prática tem sido escassa. As implementações anteriores foram:

1. Prototípicas e limitadas: As ferramentas existentes eram primariamente protótipos para LIA e LRA, sem uma implementação completa para o caso misto LIRA.
2. Problemas de escalabilidade: Os testes foram restritos a micro-benchmarks pequenos.
3. Barreiras de usabilidade: As implementações dependiam fortemente de APIs específicas (ex: Z3 Python), impedindo que os usuários especificassem restrições em formatos SMT-LIB padrão ou se integrassem com outros solvers.

Metodologia

O artigo apresenta o REAL (Ramsey Elimination for Arithmetic Logic), uma ferramenta agnóstica a solver projetada para eliminar quantificadores de Ramsey de fórmulas existenciais em LIA, LRA e LIRA. A metodologia envolve um pipeline de três estágios:

1. Especificação de Entrada (Extensão SMT-LIB):
   O REAL estende o padrão SMT-LIB para suportar quantificadores de Ramsey. Ele introduz novas regras de sintaxe para termos, permitindo que os usuários especifiquem restrições usando construtos (ramsey ...). Isso permite que a ferramenta aceite entradas em um formato padronizado em vez de depender de chamadas de API proprietárias.

2. Algoritmo de Eliminação:
   Baseando-se no framework teórico estabelecido em trabalhos anteriores [5], o REAL computa uma fórmula equivalente contendo apenas quantificadores existenciais padrão. O algoritmo:

   • Substitui variáveis quantificadas existencialmente na fórmula original por variáveis adicionais quantificadas por Ramsey.
   • Identifica condições suficientes e necessárias para a existência de um clique infinito, formulando-as como fórmulas LIRA existenciais.
   • Por exemplo, uma condição que exige uma sequência infinita $a, a+b, a+2b, \dots$ é traduzida em restrições sobre o vetor base $a$ e o vetor de passo $b$.

3. Otimizações de Implementação (REAL vs. Protótipo):
   Os autores melhoraram significativamente o protótipo original através de três categorias principais de otimização:

   • Estruturas de Dados: Implementação de cache e compartilhamento para (sub)fórmulas, normalização de forma de átomo mais eficiente e combinação de caminhadas de árvore duplicadas para reduzir o overhead computacional.
   • Estrutura da Fórmula: Manipulação direta de igualdades inteiras e desigualdades reais não estritas, compartilhamento de subexpressões comuns em abstrações Booleanas e substituição de variáveis de teoria desnecessárias por variáveis Booleanas para produzir fórmulas mais compactas.
   • Interoperabilidade: A ferramenta gera a fórmula resultante livre de quantificadores como um arquivo SMT-LIB padrão, que pode ser processado por qualquer solver SMT que suporte LIA, LRA ou LIRA (ex: Z3).

4. Pipeline de Aplicação (Alchemist):
   Para demonstrar utilidade na verificação de vivacidade, os autores desenvolveram o Alchemist, um transpiler que converte relações de alcançabilidade geradas pelo FAST(er) (uma ferramenta para verificar alcançabilidade em sistemas de contadores inteiros usando a linguagem Armoise) para o formato SMT-LIB exigido pelo REAL. Isso cria um toolchain completo: Armoise $\to$ FAST(er) $\to$ Alchemist $\to$ REAL $\to$ SMT Solver.

Principais Contribuições

• A Ferramenta REAL: Um procedimento de eliminação agnóstico a solver para quantificadores de Ramsey que suporta LIA, LRA e LIRA.
• Entrada/Saída Padronizada: A primeira implementação permitindo que restrições sejam especificadas via um formato SMT-LIB estendido, removendo dependências estritas de APIs de solvers específicos.
• Melhorias de Desempenho: Um aumento substancial de velocidade sobre o protótipo original, alcançado através de estruturas de dados otimizadas e técnicas de geração de fórmulas.
• Framework de Verificação de Vivacidade: Um pipeline demonstrado (Fig. 1) que traduz relações de alcançabilidade de sistemas de contadores inteiros em fórmulas de quantificador de Ramsey, permitindo a verificação automática de propriedades de vivacidade para protocolos distribuídos parametrizados.

Resultados Experimentais

Experimentos foram conduzidos em uma máquina Arch Linux usando Z3 v4.15.1 para verificação de satisfatibilidade.

• Estudos de Caso: A ferramenta verificou com sucesso a vivacidade para vários benchmarks, incluindo a função McCarthy 91, Sliding Window Protocol, Algoritmo de Bakery de Lamport e vários protocolos de Coerência de Cache (Berkeley, Dragon, MOESI, SYNAPSE, futurbus).
  • Para a função McCarthy 91, o REAL verificou com sucesso a ausência de cliques infinitos, provando a terminação.
  • Para o algoritmo de Bakery de Lamport, a ferramenta identificou corretamente que a verificação da ausência de um clique infinito causando inanição (starvation) a um processo falha sem suposições de justiça (fairness).
• Métricas de Desempenho:
  • Escalabilidade: O tempo de eliminação escala quase linearmente com a dimensão do problema através de várias famílias de benchmarks (Sorted Chain, Average, Cyclic Dependency, Bounding Box). Fórmulas com milhares de átomos e variáveis foram processadas em intervalos de sub-segundo a poucos segundos.
  • Comparação com o Protótipo: O REAL supera o protótipo original por várias ordens de magnitude tanto em tempos de eliminação quanto de resolução (Fig. 5). Em alguns casos de inteiros, a saída gerada é tão simples que o tempo do solver excede o tempo de eliminação.
  • Tamanho da Fórmula: O REAL produz fórmulas significativamente mais compactas comparadas ao protótipo, reduzindo o número de nós de árvore nas fórmulas SMT de saída (Fig. 3).

Significância e Alegações

O artigo alega que o REAL fornece um pipeline de verificação modular e eficiente para sistemas de estado infinito. Ao preencher a lacuna entre algoritmos de eliminação teóricos e a verificação prática baseada em SMT, ele permite a checagem automática de propriedades de vivacidade que anteriormente eram difíceis de expressar ou resolver.

Os autores observam que, embora a abordagem seja eficaz, o caso de aritmética mista de inteiros e reais lineares (LIRA) ainda incorre em um overhead substancial em comparação com LIA ou LRA puros devido à atual separação de variáveis inteiras e reais. Eles sugerem que trabalhos futuros poderiam envolver a substituição do FASTer por ferramentas que visem diretamente relações de alcançabilidade ou o refinamento do pipeline para reduzir a redundância de codificação SMT. O artigo conclui que a implementação atual expande com sucesso as capacidades de ferramentas existentes como o FASTer para lidar com a verificação de vivacidade para protocolos distribuídos parametrizados.