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 条
  • [41] X86 PROCESSORS
    Dipert, Brian
    EDN, 2010, 55 (03) : 19 - +
  • [42] Quality Criteria for Just-in-Time Requirements: Just Enough, Just-in-Time?
    Heck, Petra
    Zaidman, Andy
    1ST INTERNATIONAL WORKSHOP ON JUST-IN-TIME RE (JIT RE 2015), 2015, : 1 - 4
  • [43] A region-based compilation technique for a Java']Java just-in-time compiler
    Suganuma, T
    Yasue, T
    Nakatani, T
    ACM SIGPLAN NOTICES, 2003, 38 (05) : 312 - 323
  • [44] A Hybrid Just-In-Time Compiler for Android Comparing JIT Types and the Result of Cooperation
    Perez, Guillermo A.
    Kao, Chung-Min
    Chung, Yeh-Ching
    Hsu, Wei-Chung
    CASES'12: PROCEEDINGS OF THE 2012 ACM INTERNATIONAL CONFERENCE ON COMPILERS, ARCHITECTURES AND SYNTHESIS FOR EMBEDDED SYSTEMS, 2012, : 41 - 50
  • [45] Evolution of a Java']Java just-in-time compiler for IA-32 platforms
    Suganuma, T
    Ogasawara, T
    Kawachiya, K
    Takeuchi, M
    Ishizaki, K
    Koseki, A
    Inagaki, T
    Yasue, T
    Kawahito, M
    Onodera, T
    Komatsu, H
    Nakatani, T
    IBM JOURNAL OF RESEARCH AND DEVELOPMENT, 2004, 48 (5-6) : 767 - 795
  • [46] Dynamic path profile aided recompilation in a JAVA']JAVA just-in-time compiler
    Kumar, RV
    Narayanan, BL
    Govindarajan, R
    HIGH PERFORMANCE COMPUTING - HIPC 2002, PROCEEDINGS, 2002, 2552 : 495 - 505
  • [47] CACAO - A 64-bit Java']Java VM just-in-time compiler
    Krall, A
    Grafl, R
    CONCURRENCY-PRACTICE AND EXPERIENCE, 1997, 9 (11): : 1017 - 1030
  • [48] Effectiveness of cross-platform optimizations for a Java']Java Just-In-Time compiler
    Ishizaki, K
    Takeuchi, M
    Kawachiya, K
    Suganuma, T
    Gohda, O
    Inagaki, T
    Koseki, A
    Ogata, K
    Kawahito, M
    Yasue, T
    Ogasawara, T
    Onodera, T
    Komatsu, H
    Nakatani, T
    ACM SIGPLAN NOTICES, 2003, 38 (11) : 187 - 204
  • [49] LaTTe: A Java VM just-in-time compiler with fast and efficient register allocation
    Yang, Byung-Sun
    Moon, Soo-Mook
    Park, Seongbae
    Lee, Junpyo
    Lee, SeungIl
    Park, Jinpyo
    Chung, Yoo C.
    Kim, Suhyun
    Ebcioglu, Kemal
    Altman, Erik
    Parallel Architectures and Compilation Techniques - Conference Proceedings, PACT, 1999, : 128 - 138
  • [50] Just-in-time
    EP Electronic Production (London), 1997, 26 (05):
12345