We introduce the idea of optimisation validation, which is to formally establish that an instance of an optimising transformation indeed improves with respect to some resource measure. This is related to, but in contrast with, translation validation, which aims to establish that a particular instance of a transformation undertaken by an optimising compiler is semantics preserving. Our main setting is a program logic for a subset of Java bytecode, which is sound and complete for a resource-annotated operational semantics. The latter employs resource algebras for measuring dynamic costs such as time, space and more elaborate examples. We describe examples of optimisation validation that we have formally verified in Isabelle/HOL using the logic. We also introduce a type and effect system for measuring static costs such as code size, which is proved consistent with the operational semantics.

Optimisation Validation / D. Aspinall, L. Beringer, A. Momigliano. - In: ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE. - ISSN 1571-0661. - 176:3(2007 Jul), pp. 37-59. [10.1016/j.entcs.2006.06.017]

Optimisation Validation

A. Momigliano
Ultimo
2007

Abstract

We introduce the idea of optimisation validation, which is to formally establish that an instance of an optimising transformation indeed improves with respect to some resource measure. This is related to, but in contrast with, translation validation, which aims to establish that a particular instance of a transformation undertaken by an optimising compiler is semantics preserving. Our main setting is a program logic for a subset of Java bytecode, which is sound and complete for a resource-annotated operational semantics. The latter employs resource algebras for measuring dynamic costs such as time, space and more elaborate examples. We describe examples of optimisation validation that we have formally verified in Isabelle/HOL using the logic. We also introduce a type and effect system for measuring static costs such as code size, which is proved consistent with the operational semantics.
Compiler Optimisation; Cost Modelling; Java Virtual Machine Language; Lightweight Verification; Program Logic; Resource Algebras; Translation Validation
lug-2007
Article (author)
File in questo prodotto:
Non ci sono file associati a questo prodotto.
Pubblicazioni consigliate

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/2434/38308
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 14
  • ???jsp.display-item.citation.isi??? ND
social impact