Verified Validation of Lazy Code Motion

Free registration required

Executive Summary

Translation validation establishes a posteriori the correctness of a run of a compilation pass or other program transformation. In this paper, the authors develop an efficient translation validation algorithm for the Lazy Code Motion (LCM) optimization. LCM is an interesting challenge for validation because it is a global optimization that moves code across loops. Consequently, care must be taken not to move computations that may fail before loops that may not terminate. Their validator includes a specific check for anticipability to rule out such incorrect moves. They present a mechanically-checked proof of correctness of the validation algorithm, using the Coq proof assistant.

  • Format: PDF
  • Size: 210.5 KB