Verificação limitada de modelos baseada em SMT para programas CUDA

• Ano de defesa: 2019
• Autor(a) principal: Pereira, Phillipe Arantes
• Outros Autores: http://lattes.cnpq.br/2234775460028893
• Tipo de documento: Dissertação
• Tipo de acesso: Acesso aberto
• Idioma: por
• Instituição de defesa: Universidade Federal do Amazonas; Faculdade de Tecnologia; Brasil; UFAM; Programa de Pós-graduação em Engenharia Elétrica
• Palavras-chave em Português: GPU; Programas CUDA; Verificação formal; Verificação de modelos; ENGENHARIAS: ENGENHARIA ELÉTRICA
• Link de acesso: https://tede.ufam.edu.br/handle/tede/7019

A ferramenta de verificação ESBMC-GPU é uma extensão do Verificador de Modelos de Contexto Limitado baseado em SMT (ESBMC), que tem como propósito verificar programas de Unidades de Processamento Gráfico (GPU) escritos na plataforma de Computação Unificada da Arquitetura de Dispositivos (CUDA). ESBMC-GPU usa um modelo operacional, i.e., uma abstração das bibliotecas do CUDA, que conservativamente aproxima suas semânticas para verificar os programas. Assim, são exploradas as possíveis intercalações (sob um dado limite de contexto), enquanto trata cada uma simbolicamente. Além disso, a ferramenta implementa um algoritmo de redução monotônica de ordem parcial para realizar uma análise sobre duas threads a fim de reduzir a exploração do espaço de estados. Resultados experimentais mostram que o ESBMC-GPU pode, com sucesso, verificar 82% dos benchmarks enquanto mantém baixas taxas de falsos resultados. A ferramenta também é capaz de detectar mais violações de propriedades quando comparada a outras ferramentas de verificação existentes. Isso é devido a sua capacidade de verificar erros no fluxo de execução do programa e detectar violações de condições de corrida e acessos fora dos limites de vetores.