The AlphaZ Verifier
Date
2011
Authors
Basupalli, Vamshi, author
Rajopadhye, Sanjay, advisor
Strout, Michelle, committee member
Pasricha, Sudeep, committee member
Journal Title
Journal ISSN
Volume Title
Abstract
In the context of a compiler research framework, it is useful to have a tool that can certify that a proposed transformation is legal according to the semantics of the source language and a model of the target architecture (sequential, SIMD, shared memory, etc.) This thesis describes such a tool, the AlphaZ Verifier developed for a system for parallelizing and transforming programs in Alphabets, a high level polyhedral equational language. Our Verifier takes an alphabets program and a proposed target mapping as input. The mapping is very general and includes a proposed space-time mapping, a memory mapping, and a tiling specification (specifically which of the dimensions after the space-time mapping are to be tiled). The Verifier first checks whether the space-time mapping is legal, i.e., no dependences are violated. Next it validates the memory mapping by ensuring that no live values are overwritten before their final use. Finally, it checks tiling legality by ensuring that the proposed tiling dimensions are fully permutable. We show how all the necessary checks are reduced to polyhedron emptiness checking so that a single back-end engine can be used for each of these steps.