Jump to content

Compiler correctness

Edit links
From Wikipedia, the free encyclopedia
This is an old revision of this page, as edited by 200.19.106.219 (talk) at 20:00, 20 March 2017. The present address (URL) is a permanent link to this revision, which may differ significantly from the current revision.

In computing, compiler correctness is the branch of computer science that deals with trying to show that a compiler behaves according to its language specification.[citation needed] Techniques include developing the compiler using formal methods and using rigorous testing (often called compiler validation) on an existing compiler.

Formal methods

Compiler validation with formal methods involves a long chain of formal, deductive logic.[1] However, since the tool to find the proof (theorem prover) is implemented in software and is complex, there is a high probability it will contain errors. One approach has been to use a tool that verifies the proof (a proof checker) which because it is much simpler than a proof-finder is less likely to contain errors.

A language described as a subset of C has been formally verified (although no proof was given of its connection to the C Standard), and the proof has been machine checked.[2]

Methods include model checking, formal verification, and provably correct semantics-directed compiler generation.[3]

Testing

Testing represents a significant portion of the effort in shipping a compiler, but receives comparatively little coverage in the standard literature. The 1986 edition of Aho, Sethi, & Ullman has a single-page section on compiler testing, with no named examples.[4] The 2006 edition omits the section on testing, but does emphasize its importance: “Optimizing compilers are so difficult to get right that we dare say that no optimizing compiler is completely error-free! Thus, the most important objective in writing a compiler is that it is correct.”[5] Fraser & Hanson 1995 has a brief section on regression testing; source code is available.[6] Bailey & Davidson 2003 cover testing of procedure calls[7] A number of articles confirm that many released compilers have significant code-correctness bugs.[8] Sheridan 2007 is probably the most recent journal article on general compiler testing.[9] Commercial compiler compliance validation suites are available from ACE,[10] Perennial,[11] and Plum-Hall.[12] For most purposes, the largest body of information available on compiler testing are the Fortran[13] and Cobol[14] validation suites.

See also

References

  1. ^ De Millo, R. A.; Lipton, R. J.; Perlis, A. J. (1979). "Social processes and proofs of theorems and programs". Communications of the ACM. 22 (5): 271–280. doi:10.1145/359104.359106.
  2. ^ Leroy, X. (2006). "Formal Certification of a Compiler Back-End or: Programming a Compiler with a Proof Assistant". ACM SIGPLAN Notices. 41: 42–54. doi:10.1145/1111320.1111042.
  3. ^ Stephan Diehl, Natural Semantics Directed Generation of Compilers and Abstract Machines,Formal Aspects of Computing, Vol. 12 (2), Springer Verlag, 2000. doi:10.1007/PL00003929
  4. ^ Compilers: Principles, Techniques and Tools, infra 1986, p. 731.
  5. ^ ibid, 2006, p. 16.
  6. ^ Christopher Fraser; David Hanson (1995). A Retargetable C compiler: Design and Implementation. Benjamin/Cummings Publishing. ISBN 0-8053-1670-1., pp. 531–3.
  7. ^ Mark W. Bailey; Jack W. Davidson (2003). "Automatic Detection and Diagnosis of Faults in Generated Code for Procedure Calls" (PDF). IEEE Transactions on Software Engineering. 29 (11): 1031–1042. doi:10.1109/tse.2003.1245304. Retrieved 2009-03-24., p. 1040.
  8. ^ E.g., Christian Lindig (2005). "Random testing of C calling conventions" (PDF). Proceedings of the Sixth International Workshop on Automated Debugging. ACM. ISBN 1-59593-050-7. Retrieved 2009-03-24. {{cite conference}}: Unknown parameter |booktitle= ignored (|book-title= suggested) (help), and Eric Eide; John Regehr (2008). "Volatiles are miscompiled, and what to do about it" (PDF). Proceedings of the 7th ACM international conference on Embedded software. ACM. ISBN 978-1-60558-468-3. Retrieved 2009-03-24. {{cite conference}}: Unknown parameter |booktitle= ignored (|book-title= suggested) (help)
  9. ^ Flash Sheridan (2007). "Practical Testing of a C99 Compiler Using Output Comparison" (PDF). Software: Practice and Experience. 37 (14): 1475–1488. doi:10.1002/spe.812. Retrieved 2009-03-24. Bibliography at "http://pobox.com/~flash/compiler_testing_bibliography.html". Retrieved 2009-03-13. {{cite web}}: External link in |title= (help).
  10. ^ "http://www.ace.nl/compiler/supertest.html". Retrieved 2011-01-15. {{cite web}}: External link in |title= (help)
  11. ^ "http://peren.com/pages/products_set.htm". Retrieved 2009-03-13. {{cite web}}: External link in |title= (help)
  12. ^ "http://plumhall.com/suites.html". Retrieved 2009-03-13. {{cite web}}: External link in |title= (help)
  13. ^ "Source of Fortran validation suite". Retrieved 2011-09-01.
  14. ^ "Source of Cobol validation suite". Retrieved 2011-09-01.


Stub icon

This programming-language-related article is a stub. You can help Wikipedia by expanding it.

Retrieved from "https://en.wikipedia.org/w/index.php?title=Compiler_correctness&oldid=771305944"