Reasoning about program transformations. Imperative programming and flow of data

Publication date 9 March 2003

This book focuses on one key characteristic of programs: the flow of data, which imperative programming hides through its use and reuse of memory. The author details some program transformations that conserve this data flow, introduces a family of analyses, called reaching definition analyses, but also sometimes array data-flow analysis or value-based dependencies, to do this task. It is shown that correctness of program transformations (assuming that functions and operations are preserved by the transformation) is guaranteed by the conservation of data flow. It is studied how to make data flow explicit, using single-assignment forms, and how to better use memory, using expansion and contraction, while improving performance using parallelization. In fact, it is discussed dependence tests, showing that such tests are in fact conservative but easy-to-implement ways to guarantee that the flow of data is preserved. One key feature of this book is a detailed description of state-of-the-art symbolic analyses that handle array elements and statement instances individually. The benefit of these analyses is that they achieve much better precision than their classical counterparts. This book also features many examples and exercises, nearly all with solutions, to make this book easy to read and use and a good bookshelf reference. Symbolic-solver examples utilize real code, which can be copied verbatim to reproduce the examples, thereby enabling readers to quickly start doing their own experiments. The author presents cutting-edge results, including those in symbolic reaching definition analysis, array data-flow analysis, and array expansion, describes how to formally prove program properties and prototype compiler optimizations. These techniques have never before been presented in a single volume, using a single framework and consistent notation -- only dispersed technical publications were available. Ch. 1, Introduction, presents the key concepts and issues this book addresses. The author intentionally prefers to give an intuitive flavor to the text, ``hand-waving rather than formally defining. Since this book deals with reasoning about program transformations, Ch. 2, Describing Program Executions, analyzes and manipulates program texts to enhance certain properties of their execution: leaving more freedom to the computing devices in ordering the individual operations, reducing the number of auxiliary memory locations needed during execution, and so on. Ch. 3, Labels, is devoted to loop nests. In Ch. 4, Revisiting Some Classical Compiler Concepts, most compiler techniques and many imperative programming concepts are described with respect to control-flow graphs. In contrast, this book defines programming language concepts using a handful of basic properties and first-order logic on these properties. Alias analysis is considered, which has a tremendous impact in parallelizing compilers. A real alias analysis has to address all the features of a real programming language, like storage location and procedure call convention. However, the key issues of possible executions and conservative approximation are presented in a concise way. Reaching definition analysis is defined. Actually, this analysis is so important that two chapters, 5 and 6, are devoted to it. In Ch. 5, Reaching Definition Analysis, the details of this type of program analysis are given. Reaching definitions provide a description of the successive definitions and uses of variables, but they do not say what the values of these variables are. However, data flow and value flow are tightly related, and this relation is leveraged in Ch. 6, Applications of Reaching Definition Analysis. The author first examines when values are provably equal. Then it is shown that this piece of information can be useful to program verification or even to a second iteration of reaching definition analysis. Ch. 7, Some Classical Compiler Concepts, revisits two analysis nonpresent earlier. The first, dependence analysis, is often presented in textbooks before reaching definition analysis because it is usually simpler. However, the author prefers to discuss reaching definitions first because it shows what the root of the issue is: A program transformation must preserve the data flow. The goal of the second analysis is to find cases where values can be reused or ``copy-propagated in a program. Reusing a value instead of loading it from memory is possible if the memory location is not written since it was last accessed. Sounds familiar. Indeed, it boils down to looking for def-use or use-use chains, which makes it an extension of def-use chains captured by reaching definitions. Ch. 8, Single-Assignment Forms, discusses single-assignment forms: plain single-assignment, and what is known in the literature as static single assignment. Less aggressive expansions are also discussed. Ch. 9, Maximal Static Expansion, details a restricted form of single assignment called maximal static expansion. Ch. 10, Parallel Languages, shows how reaching definitions and single-assignment forms can be derived for parallel programs. Finally, Ch. 11, Conclusion: Toward Algorithm Recognition, gives a conclusion to the presentation. This new book provides a detailed, current, and pragmatic presentation of the program analyses and transformations that extract the flow of data in computer memory systems. Professionals, practitioners, and researchers in software engineering, computer engineering, program design analysis, and compiler design will benefit from its presentation of data-flow and memory optimization techniques and tools.

Recommendations

Cited in

(6)

This page was built for publication: Reasoning about program transformations. Imperative programming and flow of data

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4797829)