@inproceedings{gillesbartheand2013from,
author = {, Gilles Barthe and , Juan Manuel Crespo and Gulwani, Sumit and , Cesar Kunz and Marron, Mark},
title = {From Relational Verification to SIMD Loop Synthesis},
booktitle = {PPoPP '13 Proceedings of the 18th ACM SIGPLAN symposium on Principles and practice of parallel programming},
year = {2013},
month = {February},
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 2x-3x.},
publisher = {Association for Computing Machinery},
url = {http://approjects.co.za/?big=en-us/research/publication/relational-verification-simd-loop-synthesis/},
pages = {123-134},
}