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 条
  • [1] Verified Just-In-Time Compiler on x86
    Myreen, Magnus O.
    POPL'10: PROCEEDINGS OF THE 37TH ANNUAL ACM SIGPLAN-SIGACT SYMPOSIUM ON PRINCIPLES OF PROGRAMMING LANGUAGES, 2010, : 107 - 118
  • [2] Compiler Mitigations for Time Attacks on Modern x86 Processors
    Van Cleemput, Jeroen
    Coppens, Bart
    De Sutter, Bjorn
    ACM TRANSACTIONS ON ARCHITECTURE AND CODE OPTIMIZATION, 2012, 8 (04)
  • [3] Automated Just-In-Time Compiler Tuning
    Hoste, Kenneth
    Georges, Andy
    Eeckhout, Lieven
    CGO 2010: THE EIGHTH INTERNATIONAL SYMPOSIUM ON CODE GENERATION AND OPTIMIZATION, PROCEEDINGS, 2010, : 62 - 72
  • [4] Verified LISP Implementations on ARM, x86 and PowerPC
    Myreen, Magnus O.
    Cordon, Michael J. C.
    THEOREM PROVING IN HIGHER ORDER LOGICS, PROCEEDINGS, 2009, 5674 : 359 - 374
  • [5] Design and Implementation of Java Just-in-Time Compiler
    丁宇新
    梅嘉
    程虎
    Journal of Computer Science and Technology, 2000, (06) : 584 - 590
  • [6] Design and implementation of Java just-in-time compiler
    Yuxin Ding
    Jia Mei
    Hu Cheng
    Journal of Computer Science and Technology, 2000, 15 : 584 - 590
  • [7] Evaluation of a Just-in-Time Compiler Retrofitted for PHP
    Tatsubori, Michiaki
    Tozawa, Akihiko
    Suzumura, Toyotaro
    Trent, Scott
    Onodera, Tamiya
    ACM SIGPLAN NOTICES, 2010, 45 (07) : 121 - 131
  • [8] A Just-in-Time compiler for a reconfigurable testing platform
    El-Kadri, Mohammad
    Groza, Voicu
    Abielmona, Rami
    Assaf, Mansour
    2006 IEEE INSTRUMENTATION AND MEASUREMENT TECHNOLOGY CONFERENCE PROCEEDINGS, VOLS 1-5, 2006, : 628 - +
  • [9] Just-in-time compiler for konohascript using LLVM
    Ide, Masahiro
    Kuramitsu, Kimio
    IPSJ Online Transactions, 2013, 6 (01) : 9 - 16
  • [10] Templates-based portable just-in-time compiler
    Iliasov, A
    ACM SIGPLAN NOTICES, 2003, 38 (08) : 37 - 43
12345