Verified Just-In-Time Compiler on x86

被引：5
|
作者：
Myreen, Magnus O. [1 ]
机构：
[1] Univ Cambridge, Comp Lab, Cambridge CB2 1TN, England
来源：
ACM SIGPLAN NOTICES | 2010年 / 45卷 / 01期
关键词：
Performance; Reliability; Verification; Compiler verification; just in time; self-modifying code;
D O I：
10.1145/1707801.1706313
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
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.
引用
收藏
页码：107 / 118
页数：12
相关论文
共 50 条
  • [31] Fast, effective code generation in a just-in-time Java']Java compiler
    Adl-Tabatabai, AR
    Cierniak, M
    Lueh, GY
    Parikh, VM
    Stichnoth, JM
    ACM SIGPLAN NOTICES, 1998, 33 (05) : 280 - 290
  • [32] An empirical study of method inlining for a Java']Java just-in-time compiler
    Suganuma, T
    Yasue, T
    Nakatani, T
    USENIX ASSOCIATION PROCEEDINGS OF THE 2ND JAVA(TM) VIRTUAL MACHINE RESEARCH AND TECHNOLOGY SYMPOSIUM, 2002, : 91 - 104
  • [33] X86 REVIVED
    SHANDLE, J
    ELECTRONIC DESIGN, 1995, 43 (17) : 14 - 14
  • [34] Evolution of a Java just-in-time compiler for IA-32 platforms
    Suganuma, Toshio
    Ogasawara, Takeshi
    Kawachiya, Kiyokuni
    Takeuchi, Mikio
    Ishizaki, Kazuaki
    Koseki, Akira
    Inagaki, Tatsushi
    Yasue, Toshiaki
    Kawahito, Motohiro
    Onodera, Tamiya
    Komatsu, Hideaki
    Nakatani, Toshio
    IBM Journal of Research and Development, 1600, 48 (5-6): : 767 - 795
  • [35] Automatically reducing repetitive synchronization with a just-in-time compiler for Java']Java
    Stoodley, M
    Sundaresan, V
    CGO 2005: INTERNATIONAL SYMPOSIUM ON CODE GENERATION AND OPTIMIZATION, 2005, : 27 - 36
  • [36] Digital Semiconductor is developing a just-in-time Java compiler for its StrongARM
    InfoWorld, 1997, 19 (27):
  • [37] Design, implementation, and evaluation of optimizations in a Java']Java™ Just-in-Time compiler
    Ishizaki, K
    Kawahito, M
    Yasue, T
    Takeuchi, M
    Ogasawara, T
    Suganuma, T
    Onodera, T
    Komatsu, H
    Nakatani, T
    CONCURRENCY-PRACTICE AND EXPERIENCE, 2000, 12 (06): : 457 - 475
  • [38] Design and evaluation of dynamic optimizations for a Java']Java Just-In-Time compiler
    Suganuma, T
    Yasue, T
    Kawahito, M
    Komatsu, H
    Nakatani, T
    ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 2005, 27 (04): : 732 - 785
  • [39] Code size and performance optimization for mobile JavaScript just-in-time compiler
    Lee, Seong-Won
    Moon, Soo-Mook
    Jung, Won-Ki
    Oh, Jin-Seok
    Oh, Hyeong-Seok
    Proceedings - Annual Workshop on Interaction between Compilers and Computer Architectures, INTERACT, 2010,
  • [40] Model checking x86 executables with CodeSurfer/x86 and WPDS++
    Balakrishnan, G
    Reps, T
    Kidd, N
    Lal, A
    Lim, J
    Melski, D
    Gruian, R
    Yong, S
    Chen, CH
    Teitelbaum, T
    COMPUTER AIDED VERIFICATION, PROCEEDINGS, 2005, 3576 : 158 - 163
12345