Crellvm: Verified credible compilation for LLVM

Cited 9 time in webofscience Cited 7 time in scopus
  • Hit : 192
  • Download : 0
Production compilers such as GCC and LLVM are large complex software systems, for which achieving a high level of reliability is hard. Although testing is an effective method for finding bugs, it alone cannot guarantee a high level of reliability. To provide a higher level of reliability, many approaches that examine compilers' internal logics have been proposed. However, none of them have been successfully applied to major optimizations of production compilers. This paper presents Crellvm: a verified credible compilation framework for LLVM, which can be used as a systematic way of providing a high level of reliability for major optimizations in LLVM. Specifically, we augment an LLVM optimizer to generate translation results together with their correctness proofs, which can then be checked by a proof checker formally verified in Coq. As case studies, we applied our approach to two major optimizations of LLVM: register promotion (mem2reg) and global value numbering (gvn), having found four new miscompilation bugs (two in each).
Publisher
Association for Computing Machinery
Issue Date
2018-06-22
Language
English
Citation

39th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2018, pp.631 - 645

ISSN
0362-1340
DOI
10.1145/3192366.3192377
URI
http://hdl.handle.net/10203/269573
Appears in Collection
CS-Conference Papers(학술회의논문)
Files in This Item
There are no files associated with this item.
This item is cited by other documents in WoS
⊙ Detail Information in WoSⓡ Click to see webofscience_button
⊙ Cited 9 items in WoS Click to see citing articles in records_button

qr_code

  • mendeley

    citeulike


rss_1.0 rss_2.0 atom_1.0