Thesis
Formal verification of spiral generated code
Master of Science (M.S.), Drexel University
Oct 2020
DOI:
https://doi.org/10.17918/00000310
Abstract
This thesis formally verifies a subset of SPIRAL, an efficient code generation system for digital signal processing algorithms and related computations. The thesis focuses on algorithms for fast signal transforms. SPIRAL represents algorithms for linear transforms as sparse matrix factorizations using a domain specific language called the Signal Processing Language (SPL). An SPL expression representing a signal transform algorithm is obtained by repeated application of factorization and matrix identities. Such an SPL expression can then be compiled to some target language. The rules used for generating these algorithms as well as an SPL compiler targeting a simple imperative language with arrays and values from a commutative ring, IMP+V, are verified. The Coq proof assistant is used to create a deep embedding of SPL expressions and a formal definition of the algorithm generation rules. Each SPL expression can be evaluated to a matrix, and applying any algorithm generation rules to an SPL expression should produce a new SPL expression that evaluates to the same matrix. A theory of matrices in developed in Coq in order to formally express this matrix equivalence and prove that the algorithm generation process is correct. Finally, the syntax and semantics of IMP+V are defined in Coq. Hoare logic is used to verify parameterized IMP+V code fragments that are used to build an SPL to IMP+V compiler. This compiler is verified by showing that any IMP+V program compiled from a given SPL expression must apply that SPL expression's matrix to its input vector. Using this machinery, a formal proof of correctness of the fast Fourier transform (FFT) and related transforms is obtained.
Metrics
48 File views/ downloads
36 Record Views
Details
- Title
- Formal verification of spiral generated code
- Creators
- Patrick J. Brinich
- Contributors
- Jeremy Russell Johnson (Advisor)
- Awarding Institution
- Drexel University
- Degree Awarded
- Master of Science (M.S.)
- Publisher
- Drexel University; Philadelphia, Pennsylvania
- Number of pages
- iv, 134 pages
- Resource Type
- Thesis
- Language
- English
- Academic Unit
- Computer Science (Computing) (2013-2026); College of Computing and Informatics (2013-2026); Drexel University
- Other Identifier
- 991014695546704721