Optimisation Validation

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Optimisation Validation

Source

Electronic Notes in Theoretical Computer Science (ENTCS) archive
Volume 176 , Issue 3 (July 2007) table of contents

Pages 37-59

Year of Publication: 2007

ISSN:1571-0661

Authors

David Aspinall	LFCS, School of Informatics, University of Edinburgh, U.K.
Lennart Beringer	Institut für Informatik, Ludwig-Maximilians-Universität München, Germany
Alberto Momigliano	LFCS, School of Informatics, University of Edinburgh, U.K. and DSI, University of Milan, Italy

Publisher

Elsevier Science Publishers B. V. Amsterdam, The Netherlands, The Netherlands

Bibliometrics

Downloads (6 Weeks): n/a, Downloads (12 Months): n/a, Citation Count: 1

Additional Information:

abstract references cited by index terms collaborative colleagues

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

DOI Bookmark:	10.1016/j.entcs.2006.06.017

ABSTRACT

We introduce the idea of optimisation validation, which is to formally establish that an instance of an optimising transformation indeed improves with respect to some resource measure. This is related to, but in contrast with, translation validation, which aims to establish that a particular instance of a transformation undertaken by an optimising compiler is semantics preserving. Our main setting is a program logic for a subset of Java bytecode, which is sound and complete for a resource-annotated operational semantics. The latter employs resource algebras for measuring dynamic costs such as time, space and more elaborate examples. We describe examples of optimisation validation that we have formally verified in Isabelle/HOL using the logic. We also introduce a type and effect system for measuring static costs such as code size, which is proved consistent with the operational semantics.

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.

	[1]	Aspinall, D., Beringer, L., Hofmann, M., Loidl, H.-W. and Momigliano, A., A program logic for resource verification. In: Slind, K., Bunker, A., Gopalakrishnan, G. (Eds.), LNCS, 3223. pp. 34-49.
	[2]	Aspinall, D., L. Beringer, M. Hofmann, H.-W. Loidl and A. Momigliano, A program logic for resources (2005), to appear in Theoretical Computer Science
	[3]	Aspinall, D., Gilmore, S., Hofmann, M., Sannella, D. and Stark, I., Mobile resource guarantees for smart devices. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (Eds.), LNCS, 3362. pp. 1-26.
	[4]	Barrett, C.W., Fang, Y., Goldberg, B., Hu, Y., Pnueli, A. and Zuck, L.D., TVOC: A Translation Validator for Optimizing Compilers. In: Etessami, K., Rajamani, S.K. (Eds.), LNCS, 3576. pp. 291-295.
	[5]	Nick Benton, Simple relational correctness proofs for static analyses and program transformations, Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.14-25, January 14-16, 2004, Venice, Italy
	[6]	Beringer, L., Hofmann, M., Momigliano, A. and Shkaravska, O., Automatic certification of heap consumption. In: Franz Baader, A.V. (Ed.), LNCS, 3425. pp. 347-362.
	[7]	Beringer, L., MacKenzie, K. and Stark, I., Grail: a functional form for imperative mobile code. ENTCS. v85.1. 1-21.
	[8]	Jan Olaf Blech , Lars Gesellensetter , Sabine Glesner, Formal Verification of Dead Code Elimination in Isabelle/HOL, Proceedings of the Third IEEE International Conference on Software Engineering and Formal Methods, p.200-209, September 07-09, 2005 [doi>10.1109/SEFM.2005.20]
	[9]	Cachera, D., Jensen, T., Pichardie, D. and Schneider, G., Certified memory usage analysis. In: Fitzgerald, J., Hayes, I.J., Tarlecki, A. (Eds.), LNCS, 3582. pp. 91-106.
	[10]	Patrick Cousot , Radhia Cousot, Systematic design of program transformation frameworks by abstract interpretation, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.178-190, January 16-18, 2002, Portland, Oregon
	[11]	Maulik A. Dave, Compiler verification: a bibliography, ACM SIGSOFT Software Engineering Notes, v.28 n.6, November 2003 [doi>10.1145/966221.966235]
	[12]	Denney, E. and Fischer, B., Correctness of source-level safety policies. In: Araki, K., Gnesi, S., Mandrioli, D. (Eds.), LNCS, 2805. pp. 894-913.
	[13]	Genet, T., Jensen, T.P., Kodati, V. and Pichardie, D., A Java Card CAP converter in PVS. ENTCS. v82.
	[14]	Bernd Grobauer, Cost recurrences for DML programs, Proceedings of the sixth ACM SIGPLAN international conference on Functional programming, September 03-05, 2001, Florence, Italy
	[15]	Jörgen Gustavsson , David Sands, Possibilities and limitations of call-by-need space improvement, Proceedings of the sixth ACM SIGPLAN international conference on Functional programming, September 03-05, 2001, Florence, Italy
	[16]	Hankin, C. and D.L. Métayer, A type-based framework for program analysis, in: SAS, 1994, pp. 380--394
	[17]	Hoare, C.A.R., Procedures and parameters: An axiomatic approach. In: Engeler, E. (Ed.), Notes in Mathematics, 188. pp. 102-116.
	[18]	Atsushi Igarashi , Naoki Kobayashi, Resource usage analysis, ACM SIGPLAN Notices, v.37 n.1, p.331-342, Jan. 2002
	[19]	C. Barry Jay , Murray Cole , M. Sekanina , Paul Steckler, A Monadic Calculus for Parallel Costing of a Functional Language of Arrays, Proceedings of the Third International Euro-Par Conference on Parallel Processing, p.650-661, August 26-29, 1997
	[20].	Ken Kennedy , John R. Allen, Optimizing compilers for modern architectures: a dependence-based approach, Morgan Kaufmann Publishers Inc., San Francisco, CA, 2001
	[21]	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 [doi>10.1145/183432.183443]
	[22]	George C. Necula, Translation validation for an optimizing compiler, Proceedings of the ACM SIGPLAN 2000 conference on Programming language design and implementation, p.83-94, June 18-21, 2000, Vancouver, British Columbia, Canada
	[23]	Amir Pnueli , Michael Siegel , Eli Singerman, Translation Validation, Proceedings of the 4th International Conference on Tools and Algorithms for Construction and Analysis of Systems, p.151-166, March 28-April 04, 1998
	[24]	Rinard, M., Credible compilation, Technical Report MIT-LCS-TR-776, MIT Laboratory for Computer Science (1999)
	[25]	D. Sands, Improvement theory and its applications, Higher order operational techniques in semantics, Cambridge University Press, New York, NY, 1999
	[26]	Schmidt, H.W. and Zimmermann, W., A complexity calculus for object-oriented programs. Hournal of Object-Oriented Systems. v1. 117-147.
	[27]	Fred B. Schneider, Enforceable security policies, ACM Transactions on Information and System Security (TISSEC), v.3 n.1, p.30-50, Feb. 2000 [doi>10.1145/353323.353382]
	[28]	Schröder, L. and Mossakowski, T., Monad-independent Hoare logic in HasCASL. In: Pezze, M. (Ed.), LNCS, 2621. pp. 261-277.
	[29]	Skalka, C. and Smith, S.F., History effects and verification. In: Chin, W.-N. (Ed.), LNCS, 3302. pp. 107-128.
	[30]	Philip Wadler , Peter Thiemann, The marriage of effects and monads, ACM Transactions on Computational Logic (TOCL), v.4 n.1, p.1-32, January 2003 [doi>10.1145/601775.601776]
	[31]	Min Zhao , Bruce Childers , Mary Lou Soffa, Predicting the impact of optimizations for embedded systems, Proceedings of the 2003 ACM SIGPLAN conference on Language, compiler, and tool for embedded systems, June 11-13, 2003, San Diego, California, USA