Lazy code motion

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Lazy code motion

Full text

Pdf (994 KB)

Source

Conference on Programming Language Design and Implementation archive
Proceedings of the ACM SIGPLAN 1992 conference on Programming language design and implementation table of contents

San Francisco, California, United States

Pages: 224 - 234

Year of Publication: 1992

ISBN:0-89791-475-9

Also published in ...

Authors

Jens Knoop
Oliver Rüthing
Bernhard Steffen

Sponsor

SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 17, Downloads (12 Months): 109, Citation Count: 72

Additional Information:

abstract references cited by index terms collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/143095.143136 What is a DOI?

ABSTRACT

We present a bit-vector algorithm for the optimal and economical placement of computations within flow graphs, which is as efficient as standard uni-directional analyses. The point of our algorithm is the decomposition of the bi-directional structure of the known placement algorithms into a sequence of a backward and a forward analysis, which directly implies the efficiency result. Moreover, the new compositional structure opens the algorithm for modification: two further uni-directional analysis components exclude any unnecessary code motion. This laziness of our algorithm minimizes the register pressure, which has drastic effects on the run-time behaviour of the optimized programs in practice, where an economical use of registers is essential.

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	AU	A. V. Aho , J. D. Ullman, Node listings for reducible flow graphs, Proceedings of seventh annual ACM symposium on Theory of computing, p.177-185, May 05-07, 1975, Albuquerque, New Mexico, United States [doi>10.1145/800116.803767]
	Ch	Frederick Chi-Tak Chow, A portable machine-independent global optimizer--design and measurements, 1984
	Dh1	Dhamdhere, D.M. Characterization of program loops in code optimization. Comp. Lang. 8, 2 (1983), 69- 76.
	Dh2	D. M. Dhamdhere, A fast algorithm for code movement optimisation, ACM SIGPLAN Notices, v.23 n.10, p.172-180, Oct. 1988 [doi>10.1145/51607.51621]
	Dh3	D. M. Dhamdhere, Practical adaption of the global optimization algorithm of Morel and Renvoise, ACM Transactions on Programming Languages and Systems (TOPLAS), v.13 n.2, p.291-294, April 1991 [doi>10.1145/103135.214520]
	DS	Karl-Heinz Drechsler , Manfred P. Stadel, A solution to a problem with Morel and Renvoise's “Global optimization by suppression of partial redundancies”, ACM Transactions on Programming Languages and Systems (TOPLAS), v.10 n.4, p.635-640, Oct. 1988 [doi>10.1145/48022.214509]
	GW	Susan L. Graham , Mark Wegman, A Fast and Usually Linear Algorithm for Global Flow Analysis, Journal of the ACM (JACM), v.23 n.1, p.172-202, Jan. 1976 [doi>10.1145/321921.321939]
	He	Matthew S. Hecht, Flow Analysis of Computer Programs, Elsevier Science Inc., New York, NY, 1977
	HU1	Matthew S. Hecht , Jeffrey D. Ullman, Analysis of a simple algorithm global data flow problems, Proceedings of the 1st annual ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.207-217, October 01-03, 1973, Boston, Massachusetts [doi>10.1145/512927.512946]
	HU2	Hecht, M. S., and Ullman, J.D. A simple algorithm for global data flow analysis problems. In SIAM J. Comput. d, 4 (1977), 519- 532.
	JD1	Joshi, S. M., and Dhamdhere, D.M. A composite hoisting-strength reduction transformation for global program optimization- part I. Internat. J. Computer Maih. 11, (1982), 21 - 41.
	JD2	Joshi, S. M., and Dhamdhere, D.M. A composite hoisting-strength reduction transformation for global program optimization- part II. Internat. J. Computer Math. 11, (1982), 111- 126.
	Ke	K. W. Kennedy, Node listings applied to data flow analysis, Proceedings of the 2nd ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.10-21, January 20-22, 1975, Palo Alto, California [doi>10.1145/512976.512978]
	KRS	Knoop, J., Riithing, O., and Steffen, B. Lazy strength reduction. To appear.
	KS1	Knoop, J., and Steffen, B. The interprocedurM coincidence theorem. Aachener Informafik- Berichte Nr. 9127, Rheinisch-Westfiilische Technische Hochschule Aachen, Aachen, 1991.
	KS2	Knoop, J., and Steffen, B. Efficient and optimal interprocedural bit-vector data flow analyses: A uniform interprocedural framework. To appear.
	KU1	John B. Kam , Jeffrey D. Ullman, Global Data Flow Analysis and Iterative Algorithms, Journal of the ACM (JACM), v.23 n.1, p.158-171, Jan. 1976 [doi>10.1145/321921.321938]
	KU2	Kam, J. B., and Ullman, j.D. Monotone data flow analysis frameworks. Acta Informatica 7, (1977), 309- 317.
	Mo	E Morel, Data flow analysis and global optimization, Methods and tools for compiler construction, Cambridge University Press, New York, NY, 1984
	MR1	E. Morel , C. Renvoise, Global optimization by suppression of partial redundancies, Communications of the ACM, v.22 n.2, p.96-103, Feb. 1979 [doi>10.1145/359060.359069]
	MR2	Morel, E., and Renvoise, C. Interprocedural elimination of partial redundancies. In: Muchnick, St. S., and Jones, N. D. (Eds.). Program flow analysis: Theory and applications. Prentice Hall, Englewood Cliffs, NJ, 1981.
	RWZ	B. K. Rosen , M. N. Wegman , F. K. Zadeck, Global value numbers and redundant computations, Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.12-27, January 10-13, 1988, San Diego, California, United States [doi>10.1145/73560.73562]
	So	Arthur Sorkin, Some comments on “A solution to a problem with Morel and Renvoise's 'Global optimization by suppression of partial redundancies'”, ACM Transactions on Programming Languages and Systems (TOPLAS), v.11 n.4, p.666-668, Oct. 1989 [doi>10.1145/69558.214513]
	St	Bernhard Steffen, Data Flow Analysis as Model Checking, Proceedings of the International Conference on Theoretical Aspects of Computer Software, p.346-365, September 24-27, 1991
	SKR1	B. Steffen , J. Knoop , O. Rüthing, The value flow graph: a program representation for optimal program transformations, Proceedings of the third European symposium on programming on ESOP '90, p.389-405, May 1990, Copenhagen, Denmark
	SKR2	Bernhard Steffen , Jens Knoop , Oliver Rüthing, Efficient code motion and an adaption to strength reduction, Proceedings of the international joint conference on theory and practice of software development on Advances in distributed computing (ADC) and colloquium on combining paradigms for software development (CCPSD): Vol. 2, p.394-415, April 1991, Brighton, United Kingdom
	Ta1	Robert Endre Tarjan, Applications of Path Compression on Balanced Trees, Journal of the ACM (JACM), v.26 n.4, p.690-715, Oct. 1979 [doi>10.1145/322154.322161]
	Ta2	Robert Endre Tarjan, A Unified Approach to Path Problems, Journal of the ACM (JACM), v.28 n.3, p.577-593, July 1981 [doi>10.1145/322261.322272]
	Ta3	Robert Endre Tarjan, Fast Algorithms for Solving Path Problems, Journal of the ACM (JACM), v.28 n.3, p.594-614, July 1981 [doi>10.1145/322261.322273]
	Ull	Ullman, J.D. Fast algorithms for the elimination of common subexpressions. Acia Informaiica 2, 3 (1973), 191- 213.

CITED BY 72

	Motohiro Kawahito , Hideaki Komatsu , Toshio Nakatani, Effective null pointer check elimination utilizing hardware trap, ACM SIGPLAN Notices, v.35 n.11, p.139-149, Nov. 2000
	Lawrence Feigen , David Klappholz , Robert Casazza , Xing Xue, The revival transformation, Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.421-434, January 16-19, 1994, Portland, Oregon, United States
	Rastislav Bodík , Rajiv Gupta , Mary Lou Soffa, Interprocedural conditional branch elimination, ACM SIGPLAN Notices, v.32 n.5, p.146-158, May 1997
	Jens Knoop , Bernhard Steffen , Jürgen Vollmer, Parallelism for free: efficient and optimal bitvector analyses for parallel programs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.18 n.3, p.268-299, May 1996
	Jens Knoop , Bernhard Steffen, Code motion for explicitly parallel programs, ACM SIGPLAN Notices, v.34 n.8, p.13-24, Aug. 1999
	Ali-Reza Adl-Tabatabai , Michał Cierniak , Guei-Yuan Lueh , Vishesh M. Parikh , James M. Stichnoth, Fast, effective code generation in a just-in-time Java compiler, ACM SIGPLAN Notices, v.33 n.5, p.280-290, May 1998
	Oliver Rüthing , Jens Knoop , Bernhard Steffen, Sparse code motion, Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.170-183, January 19-21, 2000, Boston, MA, USA
	Priyadarshan Kolte , Michael Wolfe, Elimination of redundant array subscript range checks, ACM SIGPLAN Notices, v.30 n.6, p.270-278, June 1995
	Preston Briggs , Keith D. Cooper, Effective partial redundancy elimination, ACM SIGPLAN Notices, v.29 n.6, p.159-170, June 1994
	Robert Kennedy , Sun Chan , Shin-Ming Liu , Raymond Lo , Peng Tu , Fred Chow, Partial redundancy elimination in SSA form, ACM Transactions on Programming Languages and Systems (TOPLAS), v.21 n.3, p.627-676, May 1999
	Kazuaki Ishizaki , Motohiro Kawahito , Toshiaki Yasue , Hideaki Komatsu , Toshio Nakatani, A study of devirtualization techniques for a Java Just-In-Time compiler, ACM SIGPLAN Notices, v.35 n.10, p.294-310, Oct. 2000
	Gagan Agrawal , Joel Saltz , Raja Das, Interprocedural partial redundancy elimination and its application to distributed memory compilation, ACM SIGPLAN Notices, v.30 n.6, p.258-269, June 1995
	Jens Knoop , Oliver Rüthing , Bernhard Steffen, The power of assignment motion, ACM SIGPLAN Notices, v.30 n.6, p.233-245, June 1995
	Motohiro Kawahito , Hideaki Komatsu , Toshio Nakatani, Effective sign extension elimination, ACM SIGPLAN Notices, v.37 n.5, May 2002
	Rastisalv Bodík , Sadun Anik, Path-sensitive value-flow analysis, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.237-251, January 19-21, 1998, San Diego, California, United States
	Richard Johnson , Keshav Pingali, Dependence-based program analysis, ACM SIGPLAN Notices, v.28 n.6, p.78-89, June 1993
	Fred Chow , Sun Chan , Robert Kennedy , Shin-Ming Liu , Raymond Lo , Peng Tu, A new algorithm for partial redundancy elimination based on SSA form, ACM SIGPLAN Notices, v.32 n.5, p.273-286, May 1997
	Jens Knoop , Oliver Rüthing , Bernhard Steffen, Optimal code motion: theory and practice, ACM Transactions on Programming Languages and Systems (TOPLAS), v.16 n.4, p.1117-1155, July 1994
	Rastislav Bodík , Rajiv Gupta , Vivek Sarkar, ABCD: eliminating array bounds checks on demand, ACM SIGPLAN Notices, v.35 n.5, p.321-333, May 2000
	Rajiv Gupta , David A. Berson , Jesse Z. Fang, Resource-sensitive profile-directed data flow analysis for code optimization, Proceedings of the 30th annual ACM/IEEE international symposium on Microarchitecture, p.358-368, December 01-03, 1997, Research Triangle Park, North Carolina, United States
	Reinhard von Hanxleden , Ken Kennedy, GIVE-N-TAKE—a balanced code placement framework, ACM SIGPLAN Notices, v.29 n.6, p.107-120, June 1994
	Dhananjay M. Dhamdhere , Uday P. Khedker, Complexity of bi-directional data flow analysis, Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.397-408, March 1993, Charleston, South Carolina, United States
	Keith D. Cooper , L. Taylor Simpson , Christopher A. Vick, Operator strength reduction, ACM Transactions on Programming Languages and Systems (TOPLAS), v.23 n.5, p.603-625, September 2001
	Raymond Lo , Fred Chow , Robert Kennedy , Shin-Ming Liu , Peng Tu, Register promotion by sparse partial redundancy elimination of loads and stores, ACM SIGPLAN Notices, v.33 n.5, p.26-37, May 1998
	Uday P. Khedker , Dhananjay M. Dhamdhere, A generalized theory of bit vector data flow analysis, ACM Transactions on Programming Languages and Systems (TOPLAS), v.16 n.5, p.1472-1511, Sept. 1994
	L. Almagor , Keith D. Cooper , Alexander Grosul , Timothy J. Harvey , Steven W. Reeves , Devika Subramanian , Linda Torczon , Todd Waterman, Finding effective compilation sequences, ACM SIGPLAN Notices, v.39 n.7, July 2004
	Kazuaki Ishizaki , Motohiro Kawahito , Toshiaki Yasue , Mikio Takeuchi , Takeshi Ogasawara , Toshio Suganuma , Tamiya Onodera , Hideaki Komatsu , Toshio Nakatani, Design, implementation, and evaluation of optimizations in a just-in-time compiler, Proceedings of the ACM 1999 conference on Java Grande, p.119-128, June 12-14, 1999, San Francisco, California, United States
	Jin Lin , Tong Chen , Wei-Chung Hsu , Pen-Chung Yew , Roy Dz-Ching Ju , Tin-Fook Ngai , Sun Chan, A compiler framework for speculative analysis and optimizations, ACM SIGPLAN Notices, v.38 n.5, May 2003
	Michael Wolfe, Partial redundancy elimination is not bidirectional, ACM SIGPLAN Notices, v.34 n.6, June 1999
	R. Veldema , R. F. H. Hofman , R. A. F. Bhoedjang , C. J. H. Jacobs , H. E. Bal, Source-level global optimizations for fine-grain distributed shared memory systems, ACM SIGPLAN Notices, v.36 n.7, p.83-92, July 2001
	Motohiro Kawahito , Hideaki Komatsu , Toshio Nakatani, Effective null pointer check elimination utilizing hardware trap, ACM SIGOPS Operating Systems Review, v.34 n.5, p.139-149, Dec. 2000
	Bassam Tabbara , Abdallah Tabbara , Alberto Sangiovanni-Vincentelli, Task response time optimization using cost-based operation motion, Proceedings of the eighth international workshop on Hardware/software codesign, p.110-114, May 2000, San Diego, California, United States
	Ali-Reza Adl-Tabatabai , Thomas Gross , Guei-Yuan Lueh, Code reuse in an optimizing compiler, ACM SIGPLAN Notices, v.31 n.10, p.51-68, Oct. 1996
	Daniel Weise , Roger F. Crew , Michael Ernst , Bjarne Steensgaard, Value dependence graphs: representation without taxation, Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.297-310, January 16-19, 1994, Portland, Oregon, United States
	Dhananjay M. Dhamdhere, E-path_PRE: partial redundancy elimination made easy, ACM SIGPLAN Notices, v.37 n.8, August 2002
	Uday P. Khedker , Dhananjay M. Dhamdhere, Bidirectional data flow analysis: myths and reality, ACM SIGPLAN Notices, v.34 n.6, June 1999
	Keith D. Cooper , Li Xu, An efficient static analysis algorithm to detect redundant memory operations, ACM SIGPLAN Notices, v.38 n.2 supplement, p.97-107, February 2003
	Jin Lin , Tong Chen , Wei-Chung Hsu , Pen-Chung Yew, Speculative register promotion using Advanced Load Address Table (ALAT), Proceedings of the international symposium on Code generation and optimization: feedback-directed and runtime optimization, March 23-26, 2003, San Francisco, California
	V. K. Paleri , Y. N. Srikant , P. Shankar, Partial redundancy elimination: a simple, pragmatic, and provably correct algorithm, Science of Computer Programming, v.48 n.1, p.1-20, July 2003
	Gagan Agrawal, Interprocedural Partial Redundancy Elimination With Application to Distributed Memory Compilation, IEEE Transactions on Parallel and Distributed Systems, v.9 n.7, p.609-625, July 1998
	Soumen Chakrabarti , Manish Gupta , Jong-Deok Choi, Global communication analysis and optimization, ACM SIGPLAN Notices, v.31 n.5, p.68-78, May 1996
	Guei-Yuan Lueh , Thomas Gross , Ali-Reza Adl-Tabatabai, Fusion-based register allocation, ACM Transactions on Programming Languages and Systems (TOPLAS), v.22 n.3, p.431-470, May 2000
	Jens Knoop , Oliver Rüthing , Bernhard Steffen, Partial dead code elimination, ACM SIGPLAN Notices, v.29 n.6, p.147-158, June 1994
	Motohiro Kawahito , Hideaki Komatsu , Toshio Nakatani, Effective sign extension elimination for java, ACM Transactions on Programming Languages and Systems (TOPLAS), v.28 n.1, p.106-133, January 2006
	Antonia Zhai , Christopher B. Colohan , J. Gregory Steffan , Todd C. Mowry, Compiler optimization of scalar value communication between speculative threads, ACM SIGPLAN Notices, v.37 n.10, October 2002
	T. Suganuma , T. Ogasawara , M. Takeuchi , T. Yasue , M. Kawahito , K. Ishizaki , H. Komatsu , T. Nakatani, Overview of the IBM Java just-in-time compiler, IBM Systems Journal, v.39 n.1, p.175-193, January 2000
	Jin Lin , Tong Chen , Wei-Chung Hsu , Pen-Chung Yew , Roy Dz-Ching Ju , Tin-Fook Ngai , Sun Chan, A compiler framework for speculative optimizations, ACM Transactions on Architecture and Code Optimization (TACO), v.1 n.3, p.247-271, September 2004
	Jens Knoop , Eduard Mehofer, Distribution Assignment Placement: Effective Optimization of Redistribution Costs, IEEE Transactions on Parallel and Distributed Systems, v.13 n.6, p.628-647, June 2002
	Manish Gupta , Edith Schonberg , Harini Srinivasan, A Unified Framework for Optimizing Communication in Data-Parallel Programs, IEEE Transactions on Parallel and Distributed Systems, v.7 n.7, p.689-704, July 1996
	Keith D. Cooper , Alexander Grosul , Timothy J. Harvey , Steven Reeves , Devika Subramanian , Linda Torczon , Todd Waterman, ACME: adaptive compilation made efficient, ACM SIGPLAN Notices, v.40 n.7, July 2005
	J. Gregory Steffan , Christopher Colohan , Antonia Zhai , Todd C. Mowry, The STAMPede approach to thread-level speculation, ACM Transactions on Computer Systems (TOCS), v.23 n.3, p.253-300, August 2005
	Vijay S. Menon , Neal Glew , Brian R. Murphy , Andrew McCreight , Tatiana Shpeisman , Ali-Reza Adl-Tabatabai , Leaf Petersen, A verifiable SSA program representation for aggressive compiler optimization, ACM SIGPLAN Notices, v.41 n.1, p.397-408, January 2006
	Sebastian Unger , Frank Mueller, Handling irreducible loops: optimized node splitting versus DJ-graphs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.24 n.4, p.299-333, July 2002
	Jin Lin , Wei-Chung Hsu , Pen-Chung Yew , Roy Dz-Ching Ju , Tin-Fook Ngai, Recovery code generation for general speculative optimizations, ACM Transactions on Architecture and Code Optimization (TACO), v.3 n.1, p.67-89, March 2006
	Keith D. Cooper , Alexander Grosul , Timothy J. Harvey , Steve Reeves , Devika Subramanian , Linda Torczon , Todd Waterman, Exploring the structure of the space of compilation sequences using randomized search algorithms, The Journal of Supercomputing, v.36 n.2, p.135-151, May 2006
	Jin Lin , Wei-Chung Hsu , Pen-Chung Yew , Roy Dz-Ching Ju , Tin-Fook Ngai, A Compiler Framework for Recovery Code Generation in General Speculative Optimizations, Proceedings of the 13th International Conference on Parallel Architectures and Compilation Techniques, p.17-28, September 29-October 03, 2004
	Jingling Xue , Qiong Cai, A lifetime optimal algorithm for speculative PRE, ACM Transactions on Architecture and Code Optimization (TACO), v.3 n.2, p.115-155, June 2006
	Xiaotong Zhuang , Santosh Pande, Parallelizing load/stores on dual-bank memory embedded processors, ACM Transactions on Embedded Computing Systems (TECS), v.5 n.3, p.613-657, August 2006
	Yutaka Matsuno , Atsushi Ohori, A type system equivalent to static single assignment, Proceedings of the 8th ACM SIGPLAN symposium on Principles and practice of declarative programming, July 10-12, 2006, Venice, Italy
	Min Zhao , Bruce R. Childers , Mary Lou Soffa, An approach toward profit-driven optimization, ACM Transactions on Architecture and Code Optimization (TACO), v.3 n.3, p.231-262, September 2006
	Antonia Zhai , J. Gregory Steffan , Christopher B. Colohan , Todd C. Mowry, Compiler and hardware support for reducing the synchronization of speculative threads, ACM Transactions on Architecture and Code Optimization (TACO), v.5 n.1, p.1-33, May 2008
	Stefan Schäfer , Bernhard Scholz, Optimal chain rule placement for instruction selection based on SSA graphs, Proceedingsof the 10th international workshop on Software & compilers for embedded systems, April 20-20, 2007, Nice, France
	Ando Saabas , Tarmo Uustalu, Proof optimization for partial redundancy elimination, Proceedings of the 2008 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation, January 07-08, 2008, San Francisco, California, USA
	Rei Odaira , Kei Hiraki, Sentinel PRE: Hoisting beyond Exception Dependency with Dynamic Deoptimization, Proceedings of the international symposium on Code generation and optimization, p.328-338, March 20-23, 2005
	Rajiv A. Ravindran , Pracheeti D. Nagarkar , Ganesh S. Dasika , Eric D. Marsman , Robert M. Senger , Scott A. Mahlke , Richard B. Brown, Compiler Managed Dynamic Instruction Placement in a Low-Power Code Cache, Proceedings of the international symposium on Code generation and optimization, p.179-190, March 20-23, 2005
	Karl-Heinz Drechsler , Manfred P. Stadel, A variation of Knoop, Rüthing, and Steffen's Lazy Code Motion, ACM SIGPLAN Notices, v.28 n.5, p.29-38, May 1993
	Brian R. Murphy , Vijay Menon , Florian T. Schneider , Tatiana Shpeisman , Ali-Reza Adl-Tabatabai, Fault-safe code motion for type-safe languages, Proceedings of the sixth annual IEEE/ACM international symposium on Code generation and optimization, April 05-09, 2008, Boston, MA, USA
	Guilherme Ottoni , David I. August, Communication optimizations for global multi-threaded instruction scheduling, ACM SIGOPS Operating Systems Review, v.42 n.2, March 2008
	Vijay Sundaresan , Mark Stoodley , Pramod Ramarao, Removing redundancy via exception check motion, Proceedings of the sixth annual IEEE/ACM international symposium on Code generation and optimization, April 05-09, 2008, Boston, MA, USA
	R. Daniel Resler , Victor Winter, A higher-order strategy for eliminating common subexpressions, Computer Languages, Systems and Structures, v.35 n.4, p.341-364, December, 2009
	Sara Kalvala , Richard Warburton , David Lacey, Program transformations using temporal logic side conditions, ACM Transactions on Programming Languages and Systems (TOPLAS), v.31 n.4, p.1-48, May 2009
	Jean-Baptiste Tristan , Xavier Leroy, Verified validation of lazy code motion, ACM SIGPLAN Notices, v.44 n.6, June 2009