Dissertação

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

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). ESBM...

ver descrição completa

Autor principal: Pereira, Phillipe Arantes
Outros Autores: http://lattes.cnpq.br/2234775460028893
Grau: Dissertação
Idioma: por
Publicado em: Universidade Federal do Amazonas 2019
Assuntos:
GPU
Programas CUDA
Verificação formal
Verificação de modelos
ENGENHARIAS: ENGENHARIA ELÉTRICA
Acesso em linha: https://tede.ufam.edu.br/handle/tede/7019
id oai:https:--tede.ufam.edu.br-handle-:tede-7019
recordtype dspace
spelling oai:https:--tede.ufam.edu.br-handle-:tede-70192019-03-15T05:03:51Z Verificação limitada de modelos baseada em SMT para programas CUDA Pereira, Phillipe Arantes Cordeiro, Lucas Carvalho http://lattes.cnpq.br/2234775460028893 http://lattes.cnpq.br/5005832876603012 Nacif, José Augusto Miranda http://lattes.cnpq.br/1946315322575953 Ferreira, Ricardo dos Santos http://lattes.cnpq.br/7078327363232474 GPU Programas CUDA Verificação formal Verificação de modelos ENGENHARIAS: ENGENHARIA ELÉTRICA 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. 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. 2019-03-14T14:07:39Z 2019-02-27 Dissertaçã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. https://tede.ufam.edu.br/handle/tede/7019 por Acesso Aberto application/pdf Universidade Federal do Amazonas Faculdade de Tecnologia Brasil UFAM Programa de Pós-graduação em Engenharia Elétrica
institution TEDE - Universidade Federal do Amazonas
collection TEDE-UFAM
language por
topic GPU
Programas CUDA
Verificação formal
Verificação de modelos
ENGENHARIAS: ENGENHARIA ELÉTRICA
spellingShingle GPU
Programas CUDA
Verificação formal
Verificação de modelos
ENGENHARIAS: ENGENHARIA ELÉTRICA
Pereira, Phillipe Arantes
Verificação limitada de modelos baseada em SMT para programas CUDA
topic_facet GPU
Programas CUDA
Verificação formal
Verificação de modelos
ENGENHARIAS: ENGENHARIA ELÉTRICA
description 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.
author_additional Cordeiro, Lucas Carvalho
author_additionalStr Cordeiro, Lucas Carvalho
format Dissertação
author Pereira, Phillipe Arantes
author2 http://lattes.cnpq.br/2234775460028893
author2Str http://lattes.cnpq.br/2234775460028893
title Verificação limitada de modelos baseada em SMT para programas CUDA
title_short Verificação limitada de modelos baseada em SMT para programas CUDA
title_full Verificação limitada de modelos baseada em SMT para programas CUDA
title_fullStr Verificação limitada de modelos baseada em SMT para programas CUDA
title_full_unstemmed Verificação limitada de modelos baseada em SMT para programas CUDA
title_sort verificação limitada de modelos baseada em smt para programas cuda
publisher Universidade Federal do Amazonas
publishDate 2019
url https://tede.ufam.edu.br/handle/tede/7019
_version_ 1831969732534730752
score 11.753735

Registros relacionados