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.