Abstrakt. Vi presenterar en effektiv teknik för korskontroll av ett C- eller C++-program mot en accelererad OpenCL-version, samt en teknik för att upptäcka dataraser i OpenCL-program. Våra tekniker implementeras i KLEE-CL, en symbolisk exekveringsmotor baserad på KLEE och KLEE-FP som stöder symboliskt resonemang om ekvivalensen mellan symboliska värden. Vårt tillvägagångssätt är att symboliskt modellera OpenCL-miljön med hjälp av ett OpenCL-runtime-bibliotek som är inriktat på symbolisk körning. Med hjälp av den här modellen kan vi köra OpenCL-program symboliskt, hålla reda på minnesåtkomster i syfte att upptäcka ras. Vi jämför sedan det symboliska resultatet mot den enkla C eller C++ implementationen för att upptäcka missmatchningar mellan de två versionerna. Vi tillämpade KLEE-CL på Parboil-riktmärkessviten, Bullet fysikbiblioteket och OP2-biblioteket, där vi kunde hitta totalt sju fel: två missmatchningar mellan OpenCL- och C-implementationer, tre minnesfel, en OpenCL-kompilator bugg och en race villkor.
Symbolisk exekveringsbaserad metod för att upptäcka dataraser i OpenCL-kod har undersökts i REF som registrerar varje minnesåtkomst och sedan använder denna information för att upptäcka datarasen.
Symbolic testing of OpenCL code
{'venue': 'in Haifa Verification Conference (HVC', 'journal': None, 'mag_field_of_study': ['Computer Science']}