Presburger Arithmetic in Memory Access Optimization for Data-Parallel Languages - Archive ouverte HAL Access content directly
Conference Papers Year : 2013

Presburger Arithmetic in Memory Access Optimization for Data-Parallel Languages

(1) , (2, 3) , (2, 4)
1
2
3
4

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.

Dates and versions

hal-00931954 , version 1 (16-01-2014)

Identifiers

Cite

Ralf Karrenberg, Marek Kosta, Thomas Sturm. Presburger Arithmetic in Memory Access Optimization for Data-Parallel Languages. 9th International Conference Frontiers of Combining Systems (FroCos 2013), Sep 2013, Nancy, France. pp.56-70, ⟨10.1007/978-3-642-40885-4_5⟩. ⟨hal-00931954⟩
109 View
0 Download

Altmetric

Share

Gmail Facebook Twitter LinkedIn More