Abstract
This paper outlines a formal model of the Intel IA-64 architecture, and explains how this model can be used to verify the correctness of assembly-level code optimizations. The formalization and proofs were carried out using the HOL Light theorem prover.
All names and brands are the property of their respective owners.
Research supported by the Intel Corporation and the Australian Research Council.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Jerry R. Burch and David L. Dill. Automatic verification of pipelined microprocessor control. In David L. Dill, editor, Computer Aided Verification: Proceedings of the 6th International Conference (CAV’94), volume 818 of Lecture Notes in Computer Science, pages 68–80, Stanford, California, June 1994. Springer-Verlag.
Michael Butler, Jim Grundy, Thomas Långbacka, Rimvydas Rukšenas, and Joakim von Wright. The refinement calculator: proof support for program refinement. In Lindsay Groves and Steve Reeves, editors, Formal Methods Pacific’97: Proceedings of FMP’97, Discrete Mathematics and Theoretical Computer Science, pages 40–61, Victoria University of Wellington, New Zealand, March 1997. Springer-Verlag.
Carole Dulong. The IA-64 architecture at work. Computer, 31(7):24–32, July 1998.
Mike Gordon. A formalization of a simplified subset of the Alpha shared memory model. http://www.cl.cam.ac.uk/Research/HVG/FTP/FTP.html#papers.
John Harrison. The HOL Light Manual. University of Cambridge, Computer Laboratory, New Museums Site, Pembroke Street, Cambridge CB2 3QG, England, edition 1.0, May 1998.
Intel. IA-64 application developer’s architecture guide. Order number 245188, Intel Corporation, Santa Clara CA, USA, May 1999.
Robert Brent Jones. Applications of Symbolic Simulation to the Verification of Microprocessors. PhD thesis, Stanford University, Department of Electrical Engineering, 161 Packard, 350 Serra Mall, Stanford CA 94305, USA, August 1999.
Michael Norrish and Konrad Slind. The HOL System Description. University of Cambridge, Computer Laboratory, New Museums Site, Pembroke Street, Cambridge CB2 3QG, England, hol98 Taupo-2 edition, February 2000.
SPARC International. The SPARC Architecture Manual. Prentice-Hall, New Jersey, 8th edition, 1992.
Joakim von Wright and Kaisa Sere. Program transformations and refinements in HOL. In Myla Archer, Jeffrey J. Joyce, Karl N. Levitt, and Phillip J. Windley, editors, The HOL Theorem Proving and its Applications: International Workshop, pages 231–239, University of California at Davis, August 1991. ACM-SIGDA, IEEE Computer Society Press.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Grundy, J. (2000). Verified Optimizations for the Intel IA-64 Architecture. In: Aagaard, M., Harrison, J. (eds) Theorem Proving in Higher Order Logics. TPHOLs 2000. Lecture Notes in Computer Science, vol 1869. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44659-1_14
Download citation
DOI: https://doi.org/10.1007/3-540-44659-1_14
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67863-2
Online ISBN: 978-3-540-44659-0
eBook Packages: Springer Book Archive