A Fast Implementation of the Octagon Abstract
Domain on Graphics Hardware
By: F. Banterle and R. Giacobazzi
Dipartimento di Informatica
Univ. di Verona
Strada Le Grazie a Ca' Vignal 2, 37134 Verona (Italy)
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.