A Fast Implementation of the Octagon Abstract Domain on Graphics Hardware

By: F. Banterle and R. Giacobazzi

Roberto Giacobazzi
Dipartimento di Informatica
Univ. di Verona
Strada Le Grazie a Ca' Vignal 2, 37134 Verona (Italy)
roberto.giacobazzi@univr.it

Abstract:

We propose an efficient implementation of the Octagon Abstract Domain (OAD) on Graphics Processing Unit (GPU) by exploiting stream processing to speed-up OAD computations. OAD is a relational numerical abstract domain which approximates invariants as conjunctions of constraints of the form +/-x +/- y <= c, where x and y are program variables and c is a constant which can be an integer, rational or real. Since OAD computations are based on matrices, and basic matrix operators, they can be mapped easily on Graphics Hardware using texture and pixel shader in the form of a kernel that implements matrix operators. The main advantage of our implementation is that we can achieve sensible speed up by using a single GPU, for each OAD operation. This can be the basis for an efficient abstract program analyzer based on a mixed CPU-GPU architecture.

Available: PDF, BibTeX Entry.

roberto.giacobazzi@univr.it