Racer verifica che le riscritture dei kernel GPU preservino la funzione

Quando gli sviluppatori riscrivono kernel GPU per aumentarne la velocità, come possono verificare che il nuovo codice calcoli ancora la stessa funzione?

I test su input campionati confrontano gli output solo per alcuni valori scelti e possono non rilevare casi rari, dati nascosti in memoria, scritture aggiuntive o errori logici abbastanza piccoli da rientrare nella tolleranza.

Racer confronta simbolicamente i kernel GPU con i rispettivi riferimenti per verificare se calcolano la stessa funzione per tutti gli input possibili.

Per verificare che una riscrittura di un kernel GPU ne preservi la funzione, gli autori presentano Racer, un motore che confronta simbolicamente un kernel con un riferimento.

Confronta le espressioni degli output per tutti gli input possibili e tiene traccia delle scritture in memoria, affrontando i punti ciechi dei test che provano input campionati e confrontano gli output dichiarati entro una tolleranza.

In uno studio su 2.408 kernel di produzione, gli autori hanno trovato 82 bug distinti.

Racer ne ha rilevati automaticamente 76 tramite diagnostica o confutazioni basate sugli output: un’evidenza che l’approccio può individuare difetti reali in questa raccolta, compresi quelli sfuggiti ai test convenzionali.

Lo studio riguarda i kernel raccolti e le configurazioni di avvio esaminate. Racer ha rifiutato l’esecuzione per 499 dei 2.408 kernel; una dimostrazione vale solo per gli output e le assegnazioni di indici verificati con quella configurazione.