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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Blythe, D.: The direct3d 10 system. In: SIGGRAPH 2006: ACM SIGGRAPH 2006 Papers, pp. 724–734. ACM Press, New York, USA (2006)
Bolz, J., Farmer, I., Grinspun, E., Schröoder, P.: Sparse matrix solvers on the gpu: conjugate gradients and multigrid. ACM Trans. Graph 22(3), 917–924 (2003)
Buck, I., Foley, T., Horn, D., Sugerman, J., Fatahalian, K., Houston, M., Hanrahan, P.: Brook for gpus: stream computing on graphics hardware. ACM Trans. Graph 23(3), 777–786 (2004)
Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Conference Record of the Fourth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Los Angeles, California, pp. 238–252. ACM Press, New York (1977)
Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: The ASTRÉE analyzer. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 21–30. Springer, Heidelberg (2005)
Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: POPL 1978. Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, pp. 84–96. ACM Press, New York, NY, USA (1978)
Da Graçca, G., Defour, D.: Implementation of float-float operators on graphics hardware. ArXiv Computer Science e-prints (March 2006)
Fan, Z., Qiu, F., Kaufman, A., Yoakum-Stover, S.: Gpu cluster for high performance computing. In: SC 2004. Proceedings of the 2004 ACM/IEEE conference on Supercomputing, Washington, DC, USA, p. 47. IEEE Computer Society Press, Los Alamitos (2004)
Galoppo, N., Govindaraju, N., Henson, M., Manocha, D.: Lu-gpu: Efficient algorithms for solving dense linear systems on graphics hardware. In: Gschwind, T., Aßmann, U., Nierstrasz, O. (eds.) SC 2005. LNCS, vol. 3628, p. 3. Springer, Heidelberg (2005)
Govindaraju, N., Gray, J., Kumar, R., Manocha, D.: Gputerasort: high performance graphics co-processor sorting for large database management. In: SIGMOD 2006. Proceedings of the 2006 ACM SIGMOD international conference on Management of data, pp. 325–336. ACM Press, New York, USA (2006)
Horn, D.R., Houston, M., Hanrahan, P.: Clawhmmer: A streaming hmmer-search implementation. In: Gschwind, T., Aßmann, U., Nierstrasz, O. (eds.) SC 2005. LNCS, vol. 3628, p. 11. Springer, Heidelberg (2005)
IEEE. IEEE 754: Standard for binary floating-point arithmetic
Kessenich, J., Baldwin, D., Rost, R.: The opengl shading language v.1.20 revision 8 (September 2006)
Kruger, J., Westermann, R.: Linear algebra operators for gpu implementation of numerical algorithms. In: SIGGRAPH 2003: ACM SIGGRAPH 2003 Papers, San Diego, California, pp. 908–916. ACM Press, New York, NY, USA (2003)
Lefohn, A., Sengupta, S., Kniss, J., Strzodka, R., Owens, J.: Glift: Generic, efficient, random-access gpu data structures. ACM Trans. Graph 25(1), 60–99 (2006)
Mark, W., Glanville, R., Akeley, K., Kilgard, M.: Cg: a system for programming graphics hardware in a c-like language. In: SIGGRAPH 2003: ACM SIGGRAPH 2003 Papers, pp. 896–907. ACM Press, New York, NY, USA (2003)
McCool, M., Du Toit, S., Popa, T., Chan, B., Moule, K.: Shader algebra. In: SIGGRAPH 2004: ACM SIGGRAPH 2004 Papers, pp. 787–795. ACM Press, New York, NY, USA (2004)
Miné, A.: The octagon abstract domain. In: AST 2001 in WCRE 2001, October 2001. IEEE, pp. 310–319. IEEE Computer Society Press, Los Alamitos (2001)
Miné, A.: Relational abstract domains for the detection of floating-point run-time errors. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol. 2986, pp. 3–17. Springer, Heidelberg (2004)
Neider, J., Davis, T.: OpenGL Programming Guide: The Official Guide to Learning OpenGL, Release 1. Addison-Wesley Longman Publishing Co., Inc., Boston, MA, USA (1993)
Owens, J., Luebke, D., Govindaraju, N., Harris, M., Kruger, J., Lefohn, A., Purcell, T.: A survey of general-purpose computation on graphics hardware. In: Eurographics 2005, State of the Art Reports, pp. 21–51 (August 2005)
Pharr, M., Fernando, R.: GPU Gems 2: Programming Techniques for High-Performance Graphics and General-Purpose Computation. Addison-Wesley Professional, Reading (2005)
Venkatasubramanian, S.: The graphics card as a stream computer. In: SIGMOD-DIMACS Workshop on Management and Processing of Data Streams (2003)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Banterle, F., Giacobazzi, R. (2007). A Fast Implementation of the Octagon Abstract Domain on Graphics Hardware. In: Nielson, H.R., Filé, G. (eds) Static Analysis. SAS 2007. Lecture Notes in Computer Science, vol 4634. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-74061-2_20
Download citation
DOI: https://doi.org/10.1007/978-3-540-74061-2_20
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-74060-5
Online ISBN: 978-3-540-74061-2
eBook Packages: Computer ScienceComputer Science (R0)