Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Search
The essence of compiling with traces
Guo S., Palsberg J.  ACM SIGPLAN Notices 46 (1): 563-574, 2011. Type: Article
Date Reviewed: Feb 24 2011

A widely quoted rule of thumb says that a program spends 90 percent of its time in ten percent of its code. Can we record sequences of instructions (traces) that the program executes very frequently, optimize them in isolation, and make the program run a lot faster? Guo and Palsberg provide us with the theory to safely do just that.

Using notation developed in the late 1980s to describe concurrent processes, they characterize the process of recording traces, and prove that some optimizations are sound and others are not. Their goal is to provide a framework for reasoning about the soundness of trace optimizations, not to validate any particular optimization strategy.

The treatment is formal, although it includes good examples to develop the reader’s intuition. Since I had no experience with the proof techniques used, I found the paper heavy going. The authors provide an excellent reference list, with pointers to sources that are necessary for understanding the notation and terminology. After some concentrated study, I could follow their development, but I’m not convinced that I would be able to reason about a different optimization without more background.

Reviewer:  W. M. Waite Review #: CR138831 (1108-0838)
Bookmark and Share
 
Correctness Proofs (D.2.4 ... )
 
 
Compilers (D.3.4 ... )
 
 
Formal Methods (D.2.4 ... )
 
 
Operational Semantics (F.3.2 ... )
 
 
Processors (D.3.4 )
 
 
Software/ Program Verification (D.2.4 )
 
Would you recommend this review?
yes
no
Other reviews under "Correctness Proofs": Date
Proof-directed parallelization synthesis by separation logic
Botinan M., Dodds M., Jagannathan S.  ACM Transactions on Programming Languages and Systems 35(2): 1-60, 2013. Type: Article
Sep 27 2013
Functional pearl: streams and unique fixed points
Hinze R.  ACM SIGPLAN Notices 43(9): 189-200, 2008. Type: Article
Jun 11 2009
Model checking the Java metalocking algorithm
Basu S., Smolka S.  ACM Transactions on Software Engineering and Methodology 16(3): 12-es, 2007. Type: Article
Jan 10 2008
more...

E-Mail This Printer-Friendly
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright © 2000-2014 ThinkLoud, Inc.
Terms of Use
| Privacy Policy