From relational verification to SIMD loop synthesis

Gilles Barthe, Juan Manuel Crespo, Sumit Gulwani, César Kunz, Mark Marron

Research output: Contribution to journalArticlepeer-review

10 Scopus citations


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.0×-3.7×.

Original languageEnglish
Pages (from-to)123-133
Number of pages11
JournalACM SIGPLAN Notices
Issue number8
StatePublished - Aug 2013


  • Deductive Synthesis
  • Inductive Synthesis
  • Program Synthesis
  • Program Vectorization
  • Relational Program Verification

ASJC Scopus subject areas

  • General Computer Science


Dive into the research topics of 'From relational verification to SIMD loop synthesis'. Together they form a unique fingerprint.

Cite this