Presburger Arithmetic in Memory Access Optimization for Data-parallel Languages

Karrenberg, Ralf; Košta, Marek; Sturm, Thomas

doi:10.1007/978-3-642-40885-4_5

Item

ITEM ACTIONSEXPORT

Add to Basket

Local TagsRelease HistoryDetailsSummary

Released

Conference Paper

Presburger Arithmetic in Memory Access Optimization for Data-parallel Languages

MPS-Authors

/persons/resource/persons127668

Košta, Marek
Automation of Logic, MPI for Informatics, Max Planck Society;

/persons/resource/persons73108

Sturm, Thomas
Automation of Logic, MPI for Informatics, Max Planck Society;

External Resource

No external resources are shared

Fulltext (restricted access)

There are currently no full texts shared for your IP range.

Fulltext (public)

There are no public fulltexts stored in PuRe

Supplementary Material (public)

There is no public supplementary material available

Citation

Karrenberg, R., Košta, M., & Sturm, T. (2013). Presburger Arithmetic in Memory Access Optimization for Data-parallel Languages. In P. Fontaine, C. Ringeissen, & R. A. Schmidt (Eds.), Frontiers of Combining Systems (pp. 56-70). Berlin: Springer. doi:10.1007/978-3-642-40885-4_5.

Cite as: https://hdl.handle.net/11858/00-001M-0000-0015-7A11-C

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.