Improved Invariant Generation for Tvoc

Yi Fang, Lenore D. Zuck

Research output: Contribution to journalArticle

Abstract

The NYU Tvoc project applies the method of translation validation to verify that optimized code is semantically equivalent to the unoptimized code, by establishing, for each run of the optimizing compiler, a set of verification conditions (VCs) whose validity implies the correctness of the optimized run. The core of Tvoc is Tvoc-sp, that handles structure preserving optimizations, i.e., optimizations that do not alter the inner loop structures. The underlying proof rule, Val, on whose soundness Tvoc-sp is based, requires, among other things, to generating invariants at each "cutpoint" of the control graph of both source and target codes. The current implementation of Tvoc-sp employs somewhat naïve fix-point computations to obtain the invariants. In this paper, we propose an alternative method to compute invartiants which is based on simple data-flow analysis techniques.

Original languageEnglish (US)
Pages (from-to)21-35
Number of pages15
JournalElectronic Notes in Theoretical Computer Science
Volume176
Issue number3 SPEC. ISS.
DOIs
StatePublished - Jul 19 2007

Fingerprint

Data flow analysis
Invariant
Optimizing Compilers
Optimization
Fixpoint
Soundness
Data Flow
Thing
Correctness
Verify
Imply
Target
Alternatives
Graph in graph theory

Keywords

  • data abstraction
  • data-flow analysis
  • invariant generation
  • Translation validation

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Improved Invariant Generation for Tvoc. / Fang, Yi; Zuck, Lenore D.

In: Electronic Notes in Theoretical Computer Science, Vol. 176, No. 3 SPEC. ISS., 19.07.2007, p. 21-35.

Research output: Contribution to journalArticle

Fang, Yi ; Zuck, Lenore D. / Improved Invariant Generation for Tvoc. In: Electronic Notes in Theoretical Computer Science. 2007 ; Vol. 176, No. 3 SPEC. ISS. pp. 21-35.
@article{70481811be86431b9fb039bdd4b666d7,
title = "Improved Invariant Generation for Tvoc",
abstract = "The NYU Tvoc project applies the method of translation validation to verify that optimized code is semantically equivalent to the unoptimized code, by establishing, for each run of the optimizing compiler, a set of verification conditions (VCs) whose validity implies the correctness of the optimized run. The core of Tvoc is Tvoc-sp, that handles structure preserving optimizations, i.e., optimizations that do not alter the inner loop structures. The underlying proof rule, Val, on whose soundness Tvoc-sp is based, requires, among other things, to generating invariants at each {"}cutpoint{"} of the control graph of both source and target codes. The current implementation of Tvoc-sp employs somewhat na{\"i}ve fix-point computations to obtain the invariants. In this paper, we propose an alternative method to compute invartiants which is based on simple data-flow analysis techniques.",
keywords = "data abstraction, data-flow analysis, invariant generation, Translation validation",
author = "Yi Fang and Zuck, {Lenore D.}",
year = "2007",
month = "7",
day = "19",
doi = "10.1016/j.entcs.2006.06.016",
language = "English (US)",
volume = "176",
pages = "21--35",
journal = "Electronic Notes in Theoretical Computer Science",
issn = "1571-0661",
publisher = "Elsevier",
number = "3 SPEC. ISS.",

}

TY - JOUR

T1 - Improved Invariant Generation for Tvoc

AU - Fang, Yi

AU - Zuck, Lenore D.

PY - 2007/7/19

Y1 - 2007/7/19

N2 - The NYU Tvoc project applies the method of translation validation to verify that optimized code is semantically equivalent to the unoptimized code, by establishing, for each run of the optimizing compiler, a set of verification conditions (VCs) whose validity implies the correctness of the optimized run. The core of Tvoc is Tvoc-sp, that handles structure preserving optimizations, i.e., optimizations that do not alter the inner loop structures. The underlying proof rule, Val, on whose soundness Tvoc-sp is based, requires, among other things, to generating invariants at each "cutpoint" of the control graph of both source and target codes. The current implementation of Tvoc-sp employs somewhat naïve fix-point computations to obtain the invariants. In this paper, we propose an alternative method to compute invartiants which is based on simple data-flow analysis techniques.

AB - The NYU Tvoc project applies the method of translation validation to verify that optimized code is semantically equivalent to the unoptimized code, by establishing, for each run of the optimizing compiler, a set of verification conditions (VCs) whose validity implies the correctness of the optimized run. The core of Tvoc is Tvoc-sp, that handles structure preserving optimizations, i.e., optimizations that do not alter the inner loop structures. The underlying proof rule, Val, on whose soundness Tvoc-sp is based, requires, among other things, to generating invariants at each "cutpoint" of the control graph of both source and target codes. The current implementation of Tvoc-sp employs somewhat naïve fix-point computations to obtain the invariants. In this paper, we propose an alternative method to compute invartiants which is based on simple data-flow analysis techniques.

KW - data abstraction

KW - data-flow analysis

KW - invariant generation

KW - Translation validation

UR - http://www.scopus.com/inward/record.url?scp=34447312836&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=34447312836&partnerID=8YFLogxK

U2 - 10.1016/j.entcs.2006.06.016

DO - 10.1016/j.entcs.2006.06.016

M3 - Article

VL - 176

SP - 21

EP - 35

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

SN - 1571-0661

IS - 3 SPEC. ISS.

ER -