Advertisement

Verifying Compilers and ASMs or ASMs for Uniform Description of Multistep Transformations

  • Gerhard Goos
  • Wolf Zimmermann
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1912)

Abstract

A verifying compiler ensures that the compiled code is always correct but the compiler may also terminate with an error mesage and then fails to generate code. We argue that with respect to compiler correctness this is the best possible result which can be achieved in practice. Such a compiler may even include unverified code provided the results of such code can be proven correct independently from how they are generated.We then show how abstract state machines (ASMs) can be used to uniformly describe the dynamic semantics of the programs being compiled across the various intermediate transformation steps occurring within a compiler. Besides being a convenient tool for describing dynamic semantics the fact that we do not have to switch between difaerent descriptional methods is found to be extremely useful.

Keywords

Observable State Operational Semantic Transition Rule Source Program Syntax Tree 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    M. Blum and S. Kannan. Program correctness checking::: and the design of programs that check their work. In Proceedings 21st Symposium on Theory of Computing, 1989.Google Scholar
  2. 2.
    M. Blum, M. Luby, and R. Rubinfeld. Self-testing/correcting with applications to numerical problems. In Proceedings 22nd Symposium on Theory of Computing, 1990.Google Scholar
  3. 3.
    Manuel Blum and Sampath Kannan. Designing programs that check their work. Journal of the Association for Computing Machinery, 42(1):269–291, January 1995.CrossRefzbMATHGoogle Scholar
  4. 4.
    Egon Boerger, Igor Durdanovic, and Dean Rosenzweig. Occam: Specification and Compiler Correctness.Part I: The Primary Model. In U. Montanari and E.-R. Olderog, editors, Proc. Procomet’94 (IFIP TC2 Working Conference on Programming Concepts, Methods and Calculi). North-Holland, 1994.Google Scholar
  5. 5.
    E. Börger, G. Del Castillo, P. Glavan, and D. Rosenzweig. Towards a Mathematical Specification of the APE100 Architecture: the APESE Model. In B. Pehrson and I. Simon, editors, IFIP 13th World Computer Congress, volume I: Technology/Foundations, pages 396–401, Elsevier, Amsterdam, the Netherlands, 1994.Google Scholar
  6. 6.
    E. Börger and I. Durdanovic. Correctness of compiling occam to transputer. The Computer Journal, 39(1):52–92, 1996.CrossRefGoogle Scholar
  7. 7.
    E. Börger and S. Mazzanti. A Practical Method for Rigorously Controllable Hardware Design. In J.P. Bowen, M.B. Hinchey, and D. Till, editors, ZUM’97: The Z Formal Specification Notation, volume 1212 of LNCS, pages 151–187. Springer, 1997.Google Scholar
  8. 8.
    E. Börger and D. Rosenzweig. The WAM-definition and Compiler Correctness. Technical Report TR-14/92, Dip. di informatica, Univ. Pisa, Italy, 1992.zbMATHGoogle Scholar
  9. 9.
    E. Börger and W. Schulte. A Modular Design for the Java VM architecture. In E. Börger, editor, Architecture Design and Validation Methods. Springer, 1998.Google Scholar
  10. 10.
    E. Börger and W. Schulte. Defining the Java Virtual Machine as Platform for Provably Correct Java Compilation. In 23rd International Symposium on Mathematical Foundations of Computer Science, LNCS. Springer, 1998. To appear.Google Scholar
  11. 11.
    E. Börger and W. Schulte. Programmer Friendly Modular Defiunition of the Semantics of Java. In J. Alves-Foss, editor, Formal Syntax and Semantics of Java, LNCS. Springer, 1998.Google Scholar
  12. 15.
    D. F. Brown, H. Moura, and D. A. Watt. Actress: an action semantics directed compiler generator. In Compiler Compilers 92, volume 641 of Lecture Notes in Computer Science, 1992.Google Scholar
  13. 16.
    B. Buth, K.-H. Buth, M. Fränzle, B. v. Karger, Y. Lakhneche, H. Langmaack, and M. Müller-Olm. Provably correct compiler development and implementation. In U. Kastens and P. Pfahler, editors, Compiler Construction, volume 641 of LNCS. Springer-Verlag, 1992.CrossRefGoogle Scholar
  14. 17.
    Bettina Buth and Markus Müller-Olm. Provably Correct Compiler Implementation. In Tutorial Material-Formal Methods Europe’ 93, pages 451–465, Denmark, April 1993. IFAD Odense Teknikum.Google Scholar
  15. 18.-Stephan Diehl. Semantics-Directed Generation of Compilers and Abstract Machines. PhD thesis, University of the Saarland, Germany, 1996.Google Scholar
  16. 19.
    A. Dold, T. Gaul, W. Goerigk, G. Goos, A. Heberle, F. von Henke, U. Hoffmann, H. Langmaack, H. Pfeifer, H. Ruess, and W. Zimmermann. Deffinition of the Language IS. VerifixWorking Paper [Verifix/UKA/1], University of Karlsruhe/Kiel/Ulm, 1995.Google Scholar
  17. 20.
    A. Dold, T. Gaul, and W. Zimmermann. Mechanized verification of compiler back-ends. In B. Steffen and T. Margaria, editors, Proceedings of the International Workshop on Software Tools for Technology Transfer STTT’ 98, pages 13–24, Aalborg, Denmark, 1998.Google Scholar
  18. 21.
    H. Emmelmann. Code selection by regularly controlled term rewriting. In R. Giegerich and S.L. Graham, editors, Code Generation-Concepts, Tools, Techniques,Workshops in Computing. Springer-Verlag, 1992.Google Scholar
  19. 22.
    H. Emmelmann, F.-W. Schröer, and R. Landwehr. Beg-a generator for efficientback ends. In ACM Proceedings of the Sigplan Conference on Programming Language Design and Implementation, June 1989.Google Scholar
  20. 23.
    Albert Endres. An analysis of errors and their causes in system programs. SIG-PLAN Notices, 10(6):327–336, 1975.CrossRefGoogle Scholar
  21. 24.
    David A. Espinosa. Semantic Lego. PhD thesis, Columbia University, 1995.Google Scholar
  22. 25.
    T.S. Gaul. An Abstract State Machine Specification of the DEC-Alpha Processor Family. Verifix Working Paper [Verifix/UKA/4], Universität Karlsruhe, 1995.Google Scholar
  23. 26.
    W. Goerigk, T.S. Gaul, and W. Zimmermann. Correct Programs without Proof? On Checker-Based Program Verification. In “Proceedings ATOOLS’98 Workshop onℴol Support for System Specification, Development, and Verification”, Advances in Computing Science, Malente, 1998. Springer VerlGoogle Scholar
  24. 27.
    Wolfgang Goerigk. Towards Rigorous Compiler Implementation Verification. In Proc. of the 1997 Workshop on Programming Languages and Fundamentals of Programming, Avendorf, Germany, November 1997.Google Scholar
  25. 28.
    Gerhard Goos. Sather-K-The Language. Software-Concepts and Tools, 18:91–109, 1997.Google Scholar
  26. 29.
    Y. Gurevich. Evolving Algebras: Lipari Guide. In E. Börger, editor, Specification and Validation Methods. Oxford University Press, 1995.Google Scholar
  27. 30.
    Y. Gurevich and J. Huggins. The Semantics of the C Programming Language. In CSL’ 92, volume 702 of LNCS, pages 274–308. Springer-Verlag, 1993.Google Scholar
  28. 31.
    A. Heberle, T. Gaul, W. Goerigk, G. Goos, and W. Zimmermann. Construction of Verified Compiler Front-Ends with Program-Checking. In Proceedings of PSI’ 99: Andrei Ershov Third International Conference on Perspectives Of System Informatics, volume 1755 of Lecture Notes in Computer Science, Novosibirsk, Russia, 1999. Springer Verlag.zbMATHGoogle Scholar
  29. 32.
    Andreas Heberle and Dirk Heuzeroth. The formal specification of IS. Technical Report [Verifix/UKA/2 revised], IPD, Universität Karlsruhe, January 1998.Google Scholar
  30. 33.
    C.A.R. Hoare, He Jifeng, and A. Sampaio. Normal Form Approach to Compiler Design. Acta Informatica, 30:701–739, 1993.MathSciNetCrossRefzbMATHGoogle Scholar
  31. 34.
    J. Huggins and D. Van Campenhout. Specification and Verification of Pipelining in the ARM2 RISC Microprocessor. ACM Transactions on Design Automation of Electronic Systems, 3(4):563–580, October 1998.Google Scholar
  32. 35.
    P. W. Kutter and A. Pierantonio. Montages specifications of realistic programming languages. Journal of Universal Computer Science, 3(5):416–442, 1997.MathSciNetzbMATHGoogle Scholar
  33. 36.
    John McCarthy and J. Painter. Correctness of a compiler for arithmetic expressions. In Schwartz [51], pages 33–41.Google Scholar
  34. 37.
    Sun Microsystems. Sun official java compiler bug database. http://java.sun.com/products/jdk/1.2/bugs.html, mar 2000.
  35. 38.
    J S. Moore. Piton, A Mechanically Verified Assembly-Level Language. Kluwer Academic Publishers, 1996.Google Scholar
  36. 39.
    C. Robert Morgan. Building an Optimizing Compiler. Digital Press, Februar 1998. ISBN 155558179X.Google Scholar
  37. 40.
    P. D. Mosses. Abstract semantic algebras. In D. Bjørner, editor, Formal description of programming concepts II, pages 63–88. IFIP IC-2 Working Conference, North Holland, 1982.Google Scholar
  38. 41.
    P. D. Mosses. Action Semantics. Cambridge University Press, 1992.Google Scholar
  39. 42.
    Markus Müller-Olm. An Exercise in Compiler Verification. Internal report, CS Department, University of Kiel, 1995.Google Scholar
  40. 43.
    Markus Müller-Olm. Modular Compiler Verification. PhD thesis, Techn. Fakultät der Christian-Albrechts-Universität, Kiel, June 1996.zbMATHGoogle Scholar
  41. 44.
    Jens Palsberg. Provably Correct Compiler Generation. PhD thesis, Department of Computer Science, University of Aarhus, 1992. xii+224 pages.Google Scholar
  42. 45.
    L. Paulson. A compiler generator for semantic grammars. PhD thesis, Stanford University, 1981.Google Scholar
  43. 46.
    A. Pnueli, M. Siegel, and E. Singermann. Translation validation. In Tools and Algorithms for the Construction and Analysis of Systems, volume 1384 of Lecture Notes in Computer Science, pages 151–166. Springer-Verlag, 1998.CrossRefGoogle Scholar
  44. 47.
    Amir Pnueli, O. Shtrichman, and M. Siegel. The code validation tool (cvt). Int. J. on Software Tools for Technology Transfer, 2(2):192–201, 1998.CrossRefzbMATHGoogle Scholar
  45. 48.
    W. Polak. Compiler specification and verification. In Lecture Notes in Computer Science, number 124 in LNCS. Springer-Verlag, 1981.Google Scholar
  46. 49.
    Robert M. Poston. Preventing software requirements specification errors with ieee 830. IEEE Software, 2(1):83–86, January 1985.Google Scholar
  47. 50.
    T. Rus. Algebraic processing of programming languages. Theoretical Computer Science, 199:105–143, 1998.MathSciNetCrossRefzbMATHGoogle Scholar
  48. 51.
    J. T. Schwartz, editor. Mathematical Aspects of Computer Science, Proc. Symp. in Appl. Math., RI, 1967. Am. Math. Soc.Google Scholar
  49. 52.
    Reinier Sterkenburg. Borland pascal compiler bug list. http://www.dataweb.nl/r.p.sterkenburg/bugsall.htm, feb 2000.
  50. 53.
    M. Tofte. Compiler Generators. Springer-Verlag, 1990.Google Scholar
  51. 54.
    William M. Waite and Gerhard Goos. Compiler Construction. Springer-Verlag, 1984.Google Scholar
  52. 55.
    C. Wallace. The Semantics of the C++ogramming Language. In E. Börger, editor, Specification and Validation Methods. Oxford University PressGoogle Scholar
  53. 56.
    M. Wand. A semantic prototyping system. SIGPLAN Notices, 19(6):213–221, June 1984. SIGPLAN 84 Symp. On Compiler Construction.Google Scholar
  54. 57.
    Hal Wasserman and Manuel Blum. Software reliability via run-time result-checking. Journal of the ACM, 44(6):826–849, November 1997.Google Scholar
  55. 58.
    W. Zimmermann and T. Gaul. An Abstract State Machine for Java Byte Code. Verifix Working Paper [Verifix/UKA/12], University of Karlsruhe, 1997.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2000

Authors and Affiliations

  • Gerhard Goos
    • 1
  • Wolf Zimmermann
    • 1
  1. 1.Universitäat Karlsruhe Fakultät für InformatikKarlsruheGermany

Personalised recommendations