Conference proceeding
Verification of Vectorization of Signal Transforms
LANGUAGES AND COMPILERS FOR PARALLEL COMPUTING, LCPC 2020, v 13149, pp 215-231
01 Jan 2022
Abstract
This paper proves properties of the vectorized code generated by the SPIRAL system for implementing, optimizing, and tuning fast signal transforms. In particular, it is shown that the generated code is correct and fully vectorized. The SPIRAL system uses multiple rewrite systems with varying levels of abstraction to generate, optimize, parallelize and implement code. The proofs proceed by showing that the rules preserve semantics and lead to code with guaranteed performance and correctness properties. Unlike more general approaches, much of the work is done at a higher level incorporating the underlying mathematics. This shifts much of the verification from proving equivalence of programs to proving equivalence of mathematical expressions. Furthermore, the proofs incorporate domain specific knowledge leading to stronger guarantees than could be obtained for a more general vectorizing compiler.
Metrics
Details
- Title
- Verification of Vectorization of Signal Transforms
- Creators
- Patrick Brinich - Drexel UniversityJeremy Johnson - Drexel University
- Contributors
- B Chapman (Editor)J Moreira (Editor)
- Publication Details
- LANGUAGES AND COMPILERS FOR PARALLEL COMPUTING, LCPC 2020, v 13149, pp 215-231
- Series
- Lecture Notes in Computer Science
- Publisher
- Springer Nature
- Number of pages
- 17
- Resource Type
- Conference proceeding
- Language
- English
- Academic Unit
- Computer Science
- Web of Science ID
- WOS:000771729000015
- Scopus ID
- 2-s2.0-85125299554
- Other Identifier
- 991019169786704721
InCites Highlights
Data related to this publication, from InCites Benchmarking & Analytics tool:
- Web of Science research areas
- Computer Science, Software Engineering
- Computer Science, Theory & Methods