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 Notices46 (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
Using symbolic execution for verification of Ada tasking programs
Dillon L. (ed) ACM Transactions on Programming Languages and Systems 22(6): 643-669, 2000. Type: Article
Jul 1 1991
Reasoning about programs (videotape)
Dijkstra E. (ed), University Video Communications, Stanford, CA, 1990. Type: Book
Dec 1 1992
Error-free software
Baber R., John Wiley & Sons, Inc., New York, NY, 1991. Type: Book (9780471930167)
May 1 1994
more...

E-Mail This Printer-Friendly
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright 1999-2024 ThinkLoud®
Terms of Use
| Privacy Policy