Verificação de Kernels em Programas CUDA usando Bounded Model Checking
Resumo
Este artigo apresenta uma extensão da ferramenta Efficient SMTBased Context-Bounded Model Checker (ESBMC) para verificar programas que executam em unidades de processamento gráfico (GPU), chamado de ESBMCGPU. Em especial, ESBMC-GPU é um verificador de modelos limitado baseado nas teorias do módulo da satisfatibilidade para programas desenvolvidos na arquitetura de dispositivo unificado de computação (CUDA). O ESBMC-GPU é baseado em um modelo operacional, uma representação abstrata das bibliotecas padrões do CUDA que conservadoramente aproxima suas semânticas. Com ESBMC-GPU, é possível verificar mais programas CUDA reais do que outras abordagens existentes.
Referências
Baier, C. and Katoen, J.-P. (2008). Principles of Model Checking. The MIT Press. Barrett, C. W., Sebastiani, R., Seshia, S. A., and Tinelli, C. (2009). Satisability Modulo Theories. In Handbook of Satisability, pages 825–885.
Betts, A., Chong, N., Donaldson, A. F., Qadeer, S., and Thomson, P. (2012). GPUVerify: a verier for GPU kernels. In OOPSLA, pages 113–132.
Biere, A., Cimatti, A., Clarke, E. M., Fujita, M., and Zhu, Y. (1999). Symbolic Model Checking Using SAT Procedures instead of BDDs. volume 1579 of LNCS, pages 317– 320.
Bradley, A. R. and Manna, Z. (2007). The Calculus of Computation: Decision Procedures with Applications to Verication. Springer.
Cheng, J., Grossman, M., and McKercher, T. (2014). Professional CUDA C Programming. John Wiley and Sons, Inc.
Cordeiro, L. C. and Fischer, B. (2011). Verifying Multi-threaded Software using SMTbased Context-Bounded Model Checking. In ICSE, pages 331–340.
Cordeiro, L. C., Fischer, B., and Marques-Silva, J. (2012). SMT-Based Bounded Model Checking for Embedded ANSI-C Software. IEEE Trans. Software Eng., 38(4):957– 974.
De Moura, L. and Bjørner, N. (2008). Z3: An Efcient SMT Solver. In TACAS, volume 4963 of LNCS, pages 337–340.
Kahlon, V., Wang, C., and Gupta, A. (2009). Monotonic Partial Order Reduction: An Optimal Symbolic Partial Order Reduction Technique. In CAV, volume 5643 of LNCS, pages 398–413.
Kirk, D. B. and Hwu, W.-m. W. (2010). Programming Massively Parallel Processors. Elsevier Inc., 1st edition.
Le Goues, C., Leino, K. R. M., and Moskal, M. (2011). The Boogie Verication Debugger (Tool Paper). In SEFM, volume 7041 of LNCS, pages 407–414.
Li, G. and Gopalakrishnan, G. (2010). Scalable SMT-based Verication of GPU Kernel Functions. In FSE, pages 187–196.
Li, G., Li, P., Sawaya, G., Gopalakrishnan, G., Ghosh, I., and Rajan, S. P. (2012). Gklee: Concolic verication and test generation for gpus. In PPoPP, pages 215–224. ACM.
Li, P., Li, G., and Gopalakrishnan, G. (2014). Practical Symbolic Race Checking of GPU Programs. In SC, pages 179–190.
Morse, J. (2015). Expressive and Efcient Bounded Model Checking of Concurrent Software. University of Southampton, PhD Thesis.
Morse, J., Cordeiro, L. C., Nicole, D., and Fischer, B. (2013). Handling Unbounded Loops with ESBMC 1.20 (Competition Contribution). In TACAS, volume 7795 of LNCS, pages 619–622.
Morse, J., Ramalho, M., Cordeiro, L. C., Nicole, D., and Fischer, B. (2014). ESBMC 1.22 (Competition Contribution). In TACAS, volume 8413 of LNCS, pages 405–407.
NVIDIA (2015). CUDA C Programming Guide. NVIDIA Corporation, v7.0 edition.
Ramalho, M., Freitas, M., Sousa, F., Marques, H., Cordeiro, L., and Fischer, B. (2013). SMT-Based Bounded Model Checking of C++ Programs. In ECBS, pages 147–156.
Rocha, H., Ismail, H., Cordeiro, L. C., and Barreto, R. S. (2015). Model Checking C Programs with Loops via k-Induction and Invariants. CoRR, abs/1502.02327.
Betts, A., Chong, N., Donaldson, A. F., Qadeer, S., and Thomson, P. (2012). GPUVerify: a verier for GPU kernels. In OOPSLA, pages 113–132.
Biere, A., Cimatti, A., Clarke, E. M., Fujita, M., and Zhu, Y. (1999). Symbolic Model Checking Using SAT Procedures instead of BDDs. volume 1579 of LNCS, pages 317– 320.
Bradley, A. R. and Manna, Z. (2007). The Calculus of Computation: Decision Procedures with Applications to Verication. Springer.
Cheng, J., Grossman, M., and McKercher, T. (2014). Professional CUDA C Programming. John Wiley and Sons, Inc.
Cordeiro, L. C. and Fischer, B. (2011). Verifying Multi-threaded Software using SMTbased Context-Bounded Model Checking. In ICSE, pages 331–340.
Cordeiro, L. C., Fischer, B., and Marques-Silva, J. (2012). SMT-Based Bounded Model Checking for Embedded ANSI-C Software. IEEE Trans. Software Eng., 38(4):957– 974.
De Moura, L. and Bjørner, N. (2008). Z3: An Efcient SMT Solver. In TACAS, volume 4963 of LNCS, pages 337–340.
Kahlon, V., Wang, C., and Gupta, A. (2009). Monotonic Partial Order Reduction: An Optimal Symbolic Partial Order Reduction Technique. In CAV, volume 5643 of LNCS, pages 398–413.
Kirk, D. B. and Hwu, W.-m. W. (2010). Programming Massively Parallel Processors. Elsevier Inc., 1st edition.
Le Goues, C., Leino, K. R. M., and Moskal, M. (2011). The Boogie Verication Debugger (Tool Paper). In SEFM, volume 7041 of LNCS, pages 407–414.
Li, G. and Gopalakrishnan, G. (2010). Scalable SMT-based Verication of GPU Kernel Functions. In FSE, pages 187–196.
Li, G., Li, P., Sawaya, G., Gopalakrishnan, G., Ghosh, I., and Rajan, S. P. (2012). Gklee: Concolic verication and test generation for gpus. In PPoPP, pages 215–224. ACM.
Li, P., Li, G., and Gopalakrishnan, G. (2014). Practical Symbolic Race Checking of GPU Programs. In SC, pages 179–190.
Morse, J. (2015). Expressive and Efcient Bounded Model Checking of Concurrent Software. University of Southampton, PhD Thesis.
Morse, J., Cordeiro, L. C., Nicole, D., and Fischer, B. (2013). Handling Unbounded Loops with ESBMC 1.20 (Competition Contribution). In TACAS, volume 7795 of LNCS, pages 619–622.
Morse, J., Ramalho, M., Cordeiro, L. C., Nicole, D., and Fischer, B. (2014). ESBMC 1.22 (Competition Contribution). In TACAS, volume 8413 of LNCS, pages 405–407.
NVIDIA (2015). CUDA C Programming Guide. NVIDIA Corporation, v7.0 edition.
Ramalho, M., Freitas, M., Sousa, F., Marques, H., Cordeiro, L., and Fischer, B. (2013). SMT-Based Bounded Model Checking of C++ Programs. In ECBS, pages 147–156.
Rocha, H., Ismail, H., Cordeiro, L. C., and Barreto, R. S. (2015). Model Checking C Programs with Loops via k-Induction and Invariants. CoRR, abs/1502.02327.
Publicado
18/10/2015
Como Citar
PEREIRA, Phillipe; ALBUQUERQUE, Higo; MARQUES, Hendrio; SILVA, Isabela; SANTOS, Vanessa; FERREIRA, Ricardo; CARVALHO, Celso; CORDEIRO, Lucas.
Verificação de Kernels em Programas CUDA usando Bounded Model Checking. In: SIMPÓSIO EM SISTEMAS COMPUTACIONAIS DE ALTO DESEMPENHO (SSCAD), 16. , 2015, Florianópolis.
Anais [...].
Porto Alegre: Sociedade Brasileira de Computação,
2015
.
p. 24-35.
DOI: https://doi.org/10.5753/wscad.2015.14269.
