We introduce a reasoning infrastructure for proving statements about resource consumption in a fragment of the java virtual machine language (JVML). The infrastructure is based on a small hierarchy of program logics, ...
详细信息
We introduce a reasoning infrastructure for proving statements about resource consumption in a fragment of the java virtual machine language (JVML). The infrastructure is based on a small hierarchy of program logics, with increasing levels of abstraction: at the top there is a type system for a high-level language that encodes resource consumption. The infrastructure is designed to be used in a proof-carrying code (PCC) scenario, where mobile programs can be equipped with formal evidence that they have predictable resource behaviour. This article focuses on the core logic in our infrastructure, a VDM-style program logic for partial correctness, which can make statements about resource consumption alongside functional behaviour. We establish some important results for this logic, including soundness and completeness with respect to a resource-aware operational semantics for the JVML. We also present a second logic built on top of the core logic, which is used to express termination;it too is shown to be sound and complete. We then outline how high-level language type systems may be connected to these logics. The entire infrastructure has been formalized in Isabelle/HOL, both to enhance the confidence in our meta-theoretical results, and to provide a prototype implementation for PCC. We give examples to show the usefulness of this approach, including proofs of resource bounds on code resulting from compiling high-level functional programs. (c) 2007 Published by Elsevier B.V.
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 contr...
详细信息
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.
This paper proposes a run-time bytecode specialization (BCS) technique that analyzes programs and generates specialized programs at run-time in an intermediate language. By using an intermediate language for code gene...
详细信息
This paper proposes a run-time bytecode specialization (BCS) technique that analyzes programs and generates specialized programs at run-time in an intermediate language. By using an intermediate language for code generation, a back-end system can optimize the specialized programs after specialization. The system uses java virtual machine language (JVML) as the intermediate language, which allows the system to easily achieve practical portability and to use existing sophisticated just-in-time (JIT) compilers as its back-end. The binding-time analysis algorithm is based on a type system, and covers a non-object-oriented subset of JVML. The specializer generates programs on a per-instruction basis, and can perform method inlining at run-time. Our performance measurements show that a non-trivial application program specialized at run-time by BCS runs approximately 3-4 times faster than the unspecialized one. Despite the large overhead of JIT compilation of specialized code, we observed that the overall performance of the application can be improved.
暂无评论