AlphaZ Verifier, The

2011 Fall.Includes bibliographical references.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