Presburger Arithmetic in Memory Access Optimization for Data-Parallel Languages

Ralf Karrenberg 1 Marek Kosta 2, 3 Thomas Sturm 2, 4
1 Compiler Design Lab [Saarbrücken]
2 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
3 Automation of Logic
MPII - Max-Planck-Institut für Informatik
4 Computational Logic
MPII - Max-Planck-Institut für Informatik
Abstract : Data-parallel languages like OpenCL and CUDA are an important means to exploit the computational power of today's computing devices. We consider the compilation of such languages for CPUs with SIMD instruction sets. To generate efficient code, one wants to statically decide whether or not certain memory operations access consecutive addresses. We formalize the notion of consecutivity and algorithmically reduce the static decision to satisfiability problems in Presburger Arithmetic. We introduce a preprocessing technique on these SMT problems, which makes it feasible to apply an off-the-shelf SMT solver. We show that a prototypical OpenCL CPU driver based on our approach generates more efficient code than any other state-of-the-art driver.
Type de document :
Communication dans un congrès
Pascal Fontaine and Christophe Ringeissen and Renate A. Schmidt. 9th International Conference Frontiers of Combining Systems (FroCos 2013), Sep 2013, Nancy, France. Springer, 8152, pp.56-70, 2013, Frontiers of Combining Systems. 〈10.1007/978-3-642-40885-4_5〉
Liste complète des métadonnées
https://hal.inria.fr/hal-00931954
Contributeur : Stephan Merz <>
Soumis le : jeudi 16 janvier 2014 - 10:19:06
Dernière modification le : jeudi 20 septembre 2018 - 07:54:02

Identifiants

Collections

INRIA | UNIV-LORRAINE | LORIA-FM | LORIA

Citation

Ralf Karrenberg, Marek Kosta, Thomas Sturm. Presburger Arithmetic in Memory Access Optimization for Data-Parallel Languages. Pascal Fontaine and Christophe Ringeissen and Renate A. Schmidt. 9th International Conference Frontiers of Combining Systems (FroCos 2013), Sep 2013, Nancy, France. Springer, 8152, pp.56-70, 2013, Frontiers of Combining Systems. 〈10.1007/978-3-642-40885-4_5〉. 〈hal-00931954〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

174

Contact


archive-ouverte@inria.fr