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 条
  • [21] A study of devirtualization techniques for a Java']Java™ just-in-time compiler
    Ishizaki, K
    Kawahito, M
    Yasue, T
    Komatsu, H
    Nakatani, T
    ACM SIGPLAN NOTICES, 2000, 35 (10) : 294 - 310
  • [22] A dynamic optimization framework for a Java']Java Just-In-Time compiler
    Suganuma, T
    Yasue, T
    Kawahito, M
    Komatsu, H
    Nakatani, T
    ACM SIGPLAN NOTICES, 2001, 36 (11) : 180 - 194
  • [23] Dr.Jit: A Just-In-Time Compiler for Differentiable Rendering
    Jakob, Wenzel
    Speierer, Sebastien
    Roussel, Nicolas
    Vicini, Delio
    ACM TRANSACTIONS ON GRAPHICS, 2022, 41 (04):
  • [24] POSTER: Tango: An Optimizing Compiler for Just-In-Time RTL Simulation
    Tine, Blaise-Pascal
    Yalamanchili, Sudhakar
    Kim, Hyesoon
    Vetter, Jeff
    2019 28TH INTERNATIONAL CONFERENCE ON PARALLEL ARCHITECTURES AND COMPILATION TECHNIQUES (PACT 2019), 2019, : 480 - 481
  • [25] Just-in-Time Compiler Assisted Object Reclamation and Space Reuse
    Zhang, Yu
    Yuan, Lina
    Wu, Tingpeng
    Peng, Wen
    Li, Quanlong
    NETWORK AND PARALLEL COMPUTING, 2010, 6289 : 18 - 34
  • [26] HiPErJiT: A Profile-Driven Just-in-Time Compiler for Erlang
    Kallas, Konstantinos
    Sagonas, Konstantinos
    PROCEEDINGS OF THE 30TH SYMPOSIUM ON IMPLEMENTATION AND APPLICATION OF FUNCTIONAL LANGUAGES (IFL 2018), 2018, : 25 - 36
  • [27] CodeSurfer/x86 - A platform for analyzing x86 executables
    Balakrishnan, G
    Gruian, R
    Reps, T
    Teitelbaum, T
    COMPILER CONSTRUCTION, PROCEEDINGS, 2005, 3443 : 250 - 254
  • [28] CellMC-a multiplatform model compiler for the Cell Broadband Engine and x86
    Caulfield, Emmet
    Hellander, Andreas
    BIOINFORMATICS, 2010, 26 (03) : 426 - 428
  • [29] A novel just-in-time compiler on an embedded object-oriented processor
    Yau, CH
    Tan, YY
    Fong, AS
    Fifth International Conference on Computer and Information Technology - Proceedings, 2005, : 771 - 775
  • [30] A Just-In-Time compiler for memory constrained low-power devices
    Shaylor, N
    USENIX ASSOCIATION PROCEEDINGS OF THE 2ND JAVA(TM) VIRTUAL MACHINE RESEARCH AND TECHNOLOGY SYMPOSIUM, 2002, : 119 - 126
12345