Run-time validation of speculative optimizations using CVC

Clark Barrett, Benjamin Goldberg, Lenore Zuck

Research output: Contribution to journalArticle

Abstract

Translation validation is an approach for validating the output of optimizing compilers. Rather than verifying the compiler itself, translation validation mandates that every run of the compiler generate a formal proof that the produced target code is a correct implementation of the source code. Speculative loop optimizations are aggressive optimizations which are only correct under certain conditions which cannot be validated at compile time. We propose using an automatic theorem prover together with the translation validation framework to automatically generate run-time tests for such speculative optimizations. This run-time validation approach must not only detect the conditions under which an optimization generates incorrect code, but also provide a way to recover from the optimization without aborting the program or producing an incorrect result. In this paper, we apply the run-time validation technique to a class of speculative reordering transformations and give some initial results of run-time tests generated by the theorem prover CVC.

Original languageEnglish (US)
Pages (from-to)89-107
Number of pages19
JournalElectronic Notes in Theoretical Computer Science
Volume89
Issue number2
DOIs
StatePublished - Oct 2003

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Run-time validation of speculative optimizations using CVC'. Together they form a unique fingerprint.

  • Cite this