Computer Science

Computer Science ›› 2024, Vol. 51 ›› Issue (11A): 240200115-9.doi: 10.11896/jsjkx.240200115

• Computer Software & Architecture • Previous Articles     Next Articles

Implementation of Retargeting CompCert Trusted Compiler for Loongson Processors

HU Shaoru, WANG Juanwei, WANG Shengyuan   

  1. Department of Computer Science and Technology,Tsinghua University,Beijing 100084,China
  • Online:2024-11-16 Published:2024-11-13
  • About author:HU Shaoru,born in 1999,B.S.His main research interests include formal verification and compiler,and so on.
    WANG Shengyuan,born in 1964,Ph.D,associate professor.His main research interests include programming languages and systems,compilers and formal methods.
  • Supported by:
    National Key R&D Program of China(2022YFB3305204).

PDF (PC)

173

Abstract: CompCert is a well-known trustworthy C-language compiler,which is highly credible and has been widely used in many research and development work in academia and industry in recent years.CompCert proves the property that the target assembly code it produces can keep the semantics of the source code,with Coq,an interactive proof assistant.The CompCert compiler now supports multiple target machine architectures,but there is currently a lack of versions specifically designed for domestically developed processors,such as the Loongson processor architecture(LoongArch).Retargetting CompCert to domestic processors such as Loongson is of great benefit to the development of safety-critical software in China.This paper analyzes the design and the structure of the CompCert compiler backend and the characteristics of Loongarch,revises the backend of the CompCert compiler to make it available to generate the assembly code suitable to run on the Loongson processor,and presents the work of the different modules.The revised CompCert compiler,which retargets to Loongson processors,has performance competitive with GCC at optimization level 1,and can meet the needs of various scenarios.

Key words: CompCert, Compiler, Compiler retargeting, Loongarch, Formally verified compilers, Coq

CLC Number: 

  • TP314
[1]YANG X J,CHEN Y,ERIC E,et al.Finding and understanding bugs in C compilers[C]//Proceedings of the 2011 ACM SIGPLAN Conference on Programming Language Design and Implementation(PLDI 2011).2011:283-294.
[2]ZHANG Q R,SUN C N,SU Z D.Skeletal Program Enume-ration for Rigorous Compiler Testing[C]//Proceedings of the 2017 ACM SIGPLAN Conference on Programming Language Design and Implementation(PLDI 2017).2017.
[3]MCCARTHY JPAINTER J.Correctness of a compiler for arithmetical expressions[C]//Mathematical Aspects of Computer Science,volume 19 of Proceedings of Symposia in Applied Ma-thematics.1967:33-41.
[4]MILNER R,WEYHRAUCH R.Proving compiler correctness in a mechanized logic[C]//Proceedings of 7th Annual Machine Intelligence Workshop,volume 7 of Machine Intelligence.1972:51-72.
[5]DAVE M A.Compiler verification:a bibliography[J].ACMSIGSOFT Software Engineering Notes,2003,28(6):2-2.
[6]LEROY X.Formal verification of a realistic compiler[C]//Communications of The ACM.2009:107-115.
[7]LEROY X.Formal certification of a compiler back-end or:pro-gramming a compiler with a proof assistant[C]//Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages.2006:42-54.
[8]PNUELI A,SIEGEL M,SINGERMAN E.Translation Valida-
tion[C]//Proceedings of TACAS'98,Lecture Notes in Compu-ter Science.1998:151-166.
[9]KÄSTNER D,LEROY X,BLAZY S,et al.Closing the gap－the formally verified optimizing compiler CompCert[C]//Developments in System Safety Engineering:Proceedings of the Twenty-fifth Safety-critical Systems Symposium(SSS'17).2017:163-180.
[10]LEROY X,BLAZY S.Formal verification of a C-like memory model and its uses for verifying program transformations[J].Journal of Automated Reasoning,2008,41(1):1-31.
[11]YANG P,WANG S Y.Analysis of Target Code GenerationMechanism of CompCert Compiler[J].Computer Science,2020,47(9):17-23.
[12]LEROY X.A formally verified compiler back-end[J].Journal of Automated Reasoning,2009,43(4):363-446.
[13]GEORGE L,APPEL A W.Iterated register coalescing[J].ACM Trans.Prog.Lang.Syst.,1996,18(3):300-324.
[14]RIDEAU S,LEROY X.Validating register allocation and spilling[C]//CC 2010.2010:224-243.
[15]BLAZY S,ROBILLARD B,APPEL A W.Formal verification of coalescing graph-coloring register allocation[C]//ESOP 2010.2010:145-164.
[16]龙芯中科.从必然王国到自由王国,龙芯重磅推出自主指令系统架构 LoongArch [EB/OL].[2021-05-10].https://www.loongson.cn/newsDetails/1913.
[17]龙芯中科.重磅发布｜基于龙芯架构的新一代处理器龙芯 3A5000 正式发布[EB/OL].[2021-09-03].https://www.loongson.cn/newsDetails/22.
[18]龙芯中科技术股份有限公司.龙芯架构参考手册[M].2021.
[19]胡伟武等.计算机体系结构基础[M].机械工业出版社,2021.
[20]Loongson Technology Corporation Limited.Loongarch elf abispecification[OL].https://loongson.github.io/LoongArch-Documentation/LoongArch-ELF-ABI-EN.html.
[21]LEROY X,BLAZY S,KÄSTNER D,et al.CompCert－A Formally Verified Optimizing Compiler [C]//ERTS 2016.2016..
[22]胡少儒.CompCert 编译器的龙芯处理器重定向[D].Beijing:Tsinghua University,2022.
[23]王隽伟.机器证明的CompCert编译器龙芯处理器后端[D].Beijing:Tsinghua University,2023.
[1] XU Jinlong, GUI Zhonghua, LI Jia'nan, LI Yingying, HAN Lin. FP8 Quantization and Inference Memory Optimization Based on MLIR [J]. Computer Science, 2024, 51(9): 112-120.
[2] YANG Heng, LIU Qinrang, FAN Wang, PEI Xue, WEI Shuai, WANG Xuan. Study on Deep Learning Automatic Scheduling Optimization Based on Feature Importance [J]. Computer Science, 2024, 51(7): 22-28.
[3] LIU Lei, ZHOU Zhide, LIU Xingxiang, CHE Haoyang, YAO Lei, JIANG He. Automatic Tensorization for TPU Coarse-grained Instructions [J]. Computer Science, 2024, 51(6): 52-60.
[4] WANG Zhen, NIE Kai, HAN Lin. Auto-vectorization Cost Model Based on Instruction MKS [J]. Computer Science, 2024, 51(4): 78-85.
[5] ZHU Pengzhe, YAO Yuan, LIU Zijing, XI Ruicheng. Compiler-supported Program Stack Space Layout Runtime Randomization Method [J]. Computer Science, 2023, 50(8): 314-320.
[6] SHEN Nan, CHEN Gang. Formalization of Inverse Matrix Operation Based on Coq [J]. Computer Science, 2023, 50(6A): 220400108-7.
[7] Peng XU, Jianxin ZHAO, Chi Harold LIU. Optimization and Deployment of Memory-Intensive Operations in Deep Learning Model on Edge [J]. Computer Science, 2023, 50(2): 3-12.
[8] LIANG Jiali, HUA Baojian, SU Shaobo. Tensor Instruction Generation Optimization Fusing with Loop Partitioning [J]. Computer Science, 2023, 50(2): 374-383.
[9] LU Hao-song, HU Yong-hua, WANG Shu-ying, ZHOU Xin-lian, LI Hui-xiang. Study on Hybrid Resource Heuristic Loop Unrolling Factor Selection Method Based on Vector DSP [J]. Computer Science, 2022, 49(6A): 777-783.
[10] GAO Xiu-wu, HUANG Liang-ming, JIANG Jun. Optimization Method of Streaming Storage Based on GCC Compiler [J]. Computer Science, 2022, 49(11): 76-82.
[11] CHI Hao-yu, CHEN Chang-bo. Survey on Automatic Tuning of Compilers by Machine Learning [J]. Computer Science, 2022, 49(1): 241-251.
[12] TANG Zhen, HU Yong-hua, LU Hao-song, WANG Shu-ying. Research on DSP Register Pairs Allocation Algorithm with Weak Assigning Constraints [J]. Computer Science, 2021, 48(6A): 587-595.
[13] HU Wei-fang, CHEN Yun, LI Ying-ying, SHANG Jian-dong. Loop Fusion Strategy Based on Data Reuse Analysis in Polyhedral Compilation [J]. Computer Science, 2021, 48(12): 49-58.
[14] SUN Xiao-xiang, CHEN Zhe. Study on Correctness of Memory Security Dynamic Detection Algorithm Based on Theorem Proving [J]. Computer Science, 2021, 48(1): 268-272.
[15] YANG Ping, WANG Sheng-yuan. Analysis of Target Code Generation Mechanism of CompCert Compiler [J]. Computer Science, 2020, 47(9): 17-23.
Viewed
Full text


Abstract

Cited
  Shared   
  Discussed   
No Suggested Reading articles found!
渝ICP备16013121号-4
Add:18# Honghu West Rd., Yubei ,Chongqing,China    Post Code: 401121
Tel: 023-63500828/023-67039612/023-67039623
E-mail: jsjkx12@163.com
Powered by Beijing Magtech Co., Ltd.