Optimisation Validation
David Aspinall |
Lennart Beringer |
Alberto Momigliano
|
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.