Lecture Notes in Computer Science, 1999, Volume 1710/1999, 288-315, DOI: 10.1007/3-540-48092-7_13

Optimization Under the Perspective of Soundness, Completeness, and Reusability

Jens Knoop and Oliver Rüthing

View Related Documents

Abstract

While soundness and completeness are unchallengedly the surveyor‘s rod for evaluating the worthiness of proof calculi in program verification, it is not common to refer to these terms for rating the worthiness of performance improving transformations in program optimization. In this article we reconsider optimization under the perspective of soundness, completeness, and, additionally, reusability. Soundness can here be interpreted as semantics preservation, completeness as optimality in a specific, well-defined sense, and reusability as paradigm-transcending robustness of the rationale guaranteeing soundness and completeness of an optimization for a specific setting. Using partial redundancy elimination (PRE) for illustration, we demonstrate that these rationales are usually quite sensitive to paradigm changes. Neither completeness nor soundness are generally preserved. Hence, the reuse of optimization strategies in new paradigms requires usually paradigm-specific adaptations in order to accommodate their specifics. We exemplify this for PRE, and demonstrate that it is generally worth the effort, and an effective means for mastering the complexity of compiler construction in the specific field of code optimization.

Keywords  Programming paradigms - imperative - explicitly parallel - object-oriented - program optimization - data-flow analysis - safety - coincidence theorems - optimizer generators - code motion - soundness - completeness - reusability - admissibility - optimality

Acknowledgements  We dedicate this article to Hans Langmaack. It presents a profile of our work on optimizing compilation under the perspective of soundness and completeness, a focal point of his research interests. We appreciate his constant encouragement and support, and gratefully acknowledge the inspiring and stimulating impact of his advice and attitude towards computer science on our research.

Fulltext Preview

Image of the first page of the fulltext document