Search engine for discovering works of Art, research articles, and books related to Art and Culture
Javascript must be enabled to continue!
Verified just-in-time compiler on x86
View through CrossRef
This paper presents a method for creating formally correct just-in-time (JIT) compilers. The tractability of our approach is demonstrated through, what we believe is the first, verification of a JIT compiler with respect to a realistic semantics of self-modifying x86 machine code. Our semantics includes a model of the instruction cache. Two versions of the verified JIT compiler are presented: one generates all of the machine code at once, the other one is incremental i.e. produces code on-demand. All proofs have been performed inside the HOL4 theorem prover.
Title: Verified just-in-time compiler on x86
Description:
This paper presents a method for creating formally correct just-in-time (JIT) compilers.
The tractability of our approach is demonstrated through, what we believe is the first, verification of a JIT compiler with respect to a realistic semantics of self-modifying x86 machine code.
Our semantics includes a model of the instruction cache.
Two versions of the verified JIT compiler are presented: one generates all of the machine code at once, the other one is incremental i.
e.
produces code on-demand.
All proofs have been performed inside the HOL4 theorem prover.
Related Results
The verified CakeML compiler backend
The verified CakeML compiler backend
AbstractThe CakeML compiler is, to the best of our knowledge, the most realistic verified compiler for a functional programming language to date. The architecture of the compiler, ...
Hardware-Accelerated Cross-Architecture Full-System Virtualization
Hardware-Accelerated Cross-Architecture Full-System Virtualization
Hardware virtualization solutions provide users with benefits ranging from application isolation through server consolidation to improved disaster recovery and faster server provis...
Application-level checkpointing for shared memory programs
Application-level checkpointing for shared memory programs
Trends in high-performance computing are making it necessary for long-running applications to tolerate hardware faults. The most commonly used approach is checkpoint and restart (C...
High-level compiler analysis for OpenMP
High-level compiler analysis for OpenMP
Nowadays, applications from dissimilar domains, such as high-performance computing and high-integrity systems, require levels of performance that can only be achieved by means of s...
Mapping Ada onto embedded systems: memory constraints
Mapping Ada onto embedded systems: memory constraints
Running Ada programs on a self-targeting system with "virtually" unlimited memory (such as a mainframe), is quite different from running Ada on an embedded target. On self-targetin...
Collective optimization
Collective optimization
Iterative optimization is a popular and efficient research approach to optimize programs using feedback-directed compilation. However, one of the key limitations that prevented wid...
Specification, Verification and Prototyping of an Optimized Compiler
Specification, Verification and Prototyping of an Optimized Compiler
Abstract
This paper generalizes an algebraic method for the design of a correct compiler to tackle specification and verification of an optimized compiler. The main optim...