Scalable Deductive Verification of Data-Level Parallel Programs

Resumo Técnico: Verificação Dedutiva Escalável de Programas com Paralelismo ao Nível de Dados

Declaração do Problema
A verificação dedutiva de programas com paralelismo ao nível de dados (por exemplo, kernels GPU utilizando CUDA, OpenCL ou SYCL) enfrenta desafios significativos de escalabilidade. Estes programas manipulam tipicamente grandes arrays e matrizes, levando a contratos formais ricos em quantificadores aninhados. Os principais gargalos identificados são:

1. Instanciação de Quantificadores: Solucionadores SMT têm dificuldade com quantificadores aninhados que contêm expressões aritméticas em índices de array (por exemplo, A[i * stride + offset]). A correspondência E padrão (instanciação baseada em gatilhos) exige que os gatilhos sejam padrões simples; operações aritméticas dentro dos gatilhos frequentemente impedem o solucionador de encontrar instanciações adequadas, levando à falha de verificação ou a tempos excessivos.
2. Raciocínio sobre Alias: Programas que utilizam múltiplos arrays ou matrizes frequentemente exigem raciocínio sobre se essas estruturas se sobrepõem (aliasing). Na lógica de separação, verificar permissões de não sobreposição para arrays potencialmente sobrepostos gera um número quadrático de obrigações de prova, aumentando drasticamente o tempo de verificação.

Metodologia
Os autores propõem três técnicas integradas implementadas no VerCors, um verificador dedutivo de programas baseado em lógica de separação com permissões e na linguagem de verificação intermediária Viper.

1. Reescrita de Quantificadores para Geração de Gatilhos:
   O artigo introduz um procedimento para reescrever expressões com quantificadores aninhados ou complexos em formas equivalentes com quantificadores únicos e gatilhos livres de aritmética.

   • Mecanismo: O método identifica padrões de indexação aritmética linear da forma $f(x_1, \dots, x_k) = \sum a_i x_i + b$. Define-se uma bijeção (função inversa $f^{-1}$) do índice linear de volta às variáveis quantificadas originais.
   • Transformação: O quantificador original $\forall x_1, \dots, x_k; \dots; R(A[f(x_1, \dots, x_k)], \dots)$ é reescrito para $\forall x; Y(x); R(A[x], f^{-1}(x))$. Isso permite que $A[x]$ sirva como um gatilho válido para o solucionador SMT.
   • Corretude: A corretude do procedimento é formalmente provada usando o provador de teoremas Lean (aproximadamente 2500 linhas de código), garantindo que o quantificador reescrito seja logicamente equivalente ao original sob condições específicas relativas a limites e coeficientes.

2. Qualificadores de Tipo Únicos e Imutáveis:
   Para abordar o aliasing e a sobrecarga de permissões, os autores introduzem dois qualificadores de tipo:

   • Imutável: Indica que os dados apontados por um ponteiro não mudam durante a execução. Isso permite que o verificador modele os dados como sequências matemáticas em vez de blocos de heap mutáveis, eliminando a necessidade de rastreamento de permissões e reduzindo a complexidade dos instantâneos do heap.
   • Único: Atribui um número de unicidade aos ponteiros. Ponteiros com números de unicidade diferentes são garantidos como não sobrepostos. Isso permite que o verificador codifique arrays não sobrepostos em campos distintos no backend Viper, prevenindo a explosão quadrática de comparações de instantâneos necessárias para verificar aliasing.
   • Integração: Esses qualificadores são compatíveis com bibliotecas existentes e permitem verificação de tipos flexível, garantindo que funções que esperam arrays não únicos ainda possam aceitar únicos se as restrições de unicidade forem respeitadas.

3. Extração do Corpo do Kernel:
   Os autores observam que verificar kernels GPU monolíticos é frequentemente mais lento devido ao volume enorme de informações apresentado ao solucionador SMT. Eles propõem uma estratégia de extração automatizada onde o corpo do kernel é movido para uma função separada com seu próprio contrato. Essa modularização reduz o tamanho do contexto para o solucionador, melhorando o desempenho.

Contribuições Principais

• Procedimento Formal de Reescrita: Um método matematicamente provado para achatar quantificadores aninhados com índices aritméticos em formas de quantificador único adequadas para correspondência E, implementado no VerCors.
• Redução de Alias Baseada em Tipo: A introdução dos qualificadores unique e immutable para guiar explicitamente o verificador sobre o layout de memória e mutabilidade, reduzindo significativamente o espaço de busca para verificações de aliasing.
• Avaliação Abrangente: Uma avaliação experimental em grande escala cobrindo:
  • Biblioteca CLBlast: Um conjunto de kernels OpenCL que implementam Subprogramas de Álgebra Linear Básica (BLAS).
  • Pipeline de Rádio Telescópio: Um estudo de caso envolvendo o algoritmo Padre e outros programas paralelos otimizados em CPU gerados a partir da DSL Halide.
• Disponibilidade do Artefato: Todos os dados experimentais, a prova em Lean e a versão específica do VerCors utilizada são fornecidos em um artefato acompanhante.

Resultados
Os experimentos demonstram melhorias substanciais na escalabilidade e nas taxas de sucesso:

• Kernels CLBlast: A aplicação das técnicas combinadas (reescrita, tipos únicos/imutáveis e extração) resultou em uma redução média do tempo de verificação por um fator de 9. Em casos específicos atípicos (por exemplo, o kernel xger), a verificação foi 150 vezes mais rápida. Crucialmente, a combinação de técnicas permitiu a verificação de kernels (como xger e xher2) que anteriormente eram inverificáveis ou altamente frágeis (falhando em muitas execuções).
• Pipeline de Rádio Telescópio: As técnicas permitiram a verificação do algoritmo perform_iteration (Padre), que anteriormente era inatingível em estudos anteriores. Os tempos de verificação para casos bem-sucedidos foram reduzidos por fatores variando de 1,2 a 3,4, dependendo do algoritmo e configuração específicos.
• Dependência da Reescrita: Os autores observam que, sem o procedimento de reescrita de quantificadores, nenhum dos experimentos relatados poderia ser verificado de forma alguma, destacando seu papel fundamental.

Significado
O artigo afirma que essas técnicas abordam gargalos fundamentais na verificação dedutiva de programas com paralelismo de dados. Ao automatizar a geração de gatilhos adequados para acessos complexos a arrays e reduzir a sobrecarga do raciocínio sobre alias através de qualificadores de tipo, os autores permitem a verificação de kernels complexos de GPU e CPU paralelos do mundo real que anteriormente eram inviáveis. O trabalho preenche a lacuna entre a lógica de separação teórica e a verificação prática e escalável de código de computação de alto desempenho, demonstrando especificamente sucesso no algoritmo Padre usado no processamento de dados de rádio telescópios. Os autores enfatizam que, embora a reescrita manual seja possível, a detecção e aplicação automáticas desses padrões são essenciais para a verificação estruturada e automatizada de kernels GPU.