Thumbnail
Access Restriction
Subscribed

Author Sekar, R. ♦ Ramakrishnan, I. V. ♦ Mishra, P.
Source ACM Digital Library
Content type Text
Publisher Association for Computing Machinery (ACM)
File Format PDF
Copyright Year ©1997
Language English
Subject Domain (in DDC) Computer science, information & general works ♦ Data processing & computer science
Subject Keyword Abstract interpretation ♦ Completeness ♦ Program analysis ♦ Strictness analysis
Abstract Strictness analysis is an important technique for optimization of lazy functional languages. It is well known that all strictness analysis methods are $\textit{incomplete},$ i.e., fail to report some strictness properties. In this paper, we provide a precise and formal characterization of the loss of information that leads to this incompletenss. Specifically, we establish the following characterization theorem for Mycroft's strictness analysis method and a generalization of this method, called $\textit{ee-analysis},$ that reasons about exhaustive evaluation in nonflat domains: Mycroft's method will deduce a strictness property for program P iff the property is independent of any constant appearing in any evaluation of P. To prove this, we specify a small set of equations, called $\textit{E-axioms},$ that capture the information loss in Mycroft's method and develop a new proof technique called $\textit{E-rewriting}.$ $\textit{E}-rewriting$ extends the standard notion of rewriting to permit the use of reductions using $\textit{E}-axioms$ interspersed with standard reduction steps. $\textit{E}-axioms$ are a syntactic characterization of information loss and $\textit{E}-rewriting$ provides and $\textit{algorithm-independent}$ proof technique for characterizing the power of analysis methods. It can be used to answer questions on completeness and incompleteness of Mycroft's method on certain natural classes of programs. Finally, the techniques developed in this paper provide a general principle for establishing similar results for other analysis methods such as those based on abstract interpretation. As a demonstration of the generality of our technique, we give a characterization theorem for another variation of Mycroft's method called $\textit{dd}-analysis.$
ISSN 00045411
Age Range 18 to 22 years ♦ above 22 year
Educational Use Research
Education Level UG and PG
Learning Resource Type Article
Publisher Date 1997-05-01
Publisher Place New York
e-ISSN 1557735X
Journal Journal of the ACM (JACM)
Volume Number 44
Issue Number 3
Page Count 21
Starting Page 505
Ending Page 525


Open content in new tab

   Open content in new tab
Source: ACM Digital Library