Name
Abstract | ||
|---|---|---|
Existing pattern-based compiler technology is unable to effectively exploit the full potential of SIMD architectures. We present a new program synthesis based technique for auto-vectorizing performance critical innermost loops. Our synthesis technique is applicable to a wide range of loops, consistently produces performant SIMD code, and generates correctness proofs for the output code. The synthesis technique, which leverages existing work on relational verification methods, is a novel combination of deductive loop restructuring, synthesis condition generation and a new inductive synthesis algorithm for producing loop-free code fragments. The inductive synthesis algorithm wraps an optimized depth-first exploration of code sequences inside a CEGIS loop. Our technique is able to quickly produce SIMD implementations (up to 9 instructions in 0.12 seconds) for a wide range of fundamental looping structures. The resulting SIMD implementations outperform the original loops by 2.0x-3.7x. |
Year | DOI | Venue |
|---|---|---|
2013 | 10.1145/2442516.2442529 | PPOPP |
Keywords | Field | DocType |
simd architecture,new program synthesis,new inductive synthesis algorithm,relational verification,simd loop synthesis,loop-free code fragment,code sequence,inductive synthesis algorithm,wide range,simd implementation,synthesis condition generation,synthesis technique | Programming language,Correctness proofs,Program synthesis,Computer science,Parallel computing,SIMD,Exploit,Theoretical computer science,Compiler,Implementation | Conference |
Volume | Issue | ISSN |
48 | 8 | 0362-1340 |
Citations | PageRank | References |
16 | 0.66 | 25 |
Authors | ||
5 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Gilles Barthe | 1 | 2337 | 152.36 |
| Juan Manuel Crespo | 2 | 164 | 7.25 |
| Sumit Gulwani | 3 | 2263 | 110.91 |
| Cesar Kunz | 4 | 78 | 3.08 |
| Mark Marron | 5 | 77 | 3.56 |