???item.export.label??? ???item.export.type.endnote??? ???item.export.type.bibtex???

Please use this identifier to cite or link to this item: https://tede.ufam.edu.br/handle/tede/7019
Tipo do documento: Dissertação
Título: Verificação limitada de modelos baseada em SMT para programas CUDA
Autor: Pereira, Phillipe Arantes 
Primeiro orientador: Cordeiro, Lucas Carvalho
Primeiro coorientador: Lima Filho, Eddie Batista de
Primeiro membro da banca: Nacif, José Augusto Miranda
Segundo membro da banca: Ferreira, Ricardo dos Santos
Resumo: 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.
Abstract: We present ESBMC-GPU tool, an extension to the Efficient SMT-Based Context-Bounded Model Checker (ESBMC), which is aimed at verifying Graphics Processing Unit (GPU) pro grams written for the Compute Unified Device Architecture (CUDA) platform. ESBMC-GPU uses an operational model, i.e., an abstract representation of the standard CUDA libraries, which conservatively approximates their semantics, in order to verify CUDA based programs. It then explicitly explores the possible interleavings (up to the given context bound), while treats each interleaving itself symbolically. Additionally, ESBMC-GPU employs the monotonic partial order reduction and the two-thread analysis to prune the state space exploration. Experimental results show that ESBMC-GPU can successfully verify 82% of all bench- marks, while keeping lower rates of false results. Going further than previous attempts, ESBMC-GPU is able to detect more properties violations than other existing GPU verifiers due to its ability to verify errors of the program execution flow and to detect array out-of-bounds and data race violations.
Palavras-chave: GPU
Programas CUDA
Verificação formal
Verificação de modelos
Área(s) do CNPq: ENGENHARIAS: ENGENHARIA ELÉTRICA
Idioma: por
País: Brasil
Instituição: Universidade Federal do Amazonas
Sigla da instituição: UFAM
Departamento: Faculdade de Tecnologia
Programa: Programa de Pós-graduação em Engenharia Elétrica
Citação: PEREIRA, Phillipe Arantes. Verificação limitada de modelos baseada em SMT para programas CUDA. 2019. 45 f. Dissertação (Mestrado em Engenharia Elétrica) - Universidade Federal do Amazonas, Manaus, 2019.
Tipo de acesso: Acesso Aberto
URI: https://tede.ufam.edu.br/handle/tede/7019
Data de defesa: 27-Feb-2019
Appears in Collections:Mestrado em Engenharia Elétrica

Files in This Item:
File Description SizeFormat 
Dissertação_PhillipePereira_PPGEE.pdf883,18 kBAdobe PDFThumbnail

Download/Open Preview


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.