面向龙芯处理器的一种CompCert可信编译器重定向实现

CompCert是著名的C语言可信编译器,它借助于交互式定理证明工具Coq实现,能够确保生成的目标汇编代码保持源代码的语义,具有极高的可信度,近年来被广泛应用于学术界和工业界的许多安全攸关任务的研发工作中。CompCert编译器的当前版本支持多种目标机结构,然而目前尚缺乏针对国内自主研发处理器的版本,如龙芯(Loongson)处理器体系结构(LoongArch)。将CompCert重定向到龙芯等国产处理器,对我国安全攸关软件领域的发展大有裨益。本文对CompCert编译器的设计理念、框架结构和龙芯架构的特点进行分析,改造CompCert编译器的后端,使其可以生成能在龙芯处理器上运行的汇编代码,并细致阐述不同模块的工作内容。重定向到龙芯处理器的CompCert编译器具有接近GCC-O1的性能,可满足许多场景的使用。

龙芯指令系统架构及其软件生态建设

构建独立于Wintel体系和AA体系的安全可控的信息技术体系是龙芯的发展目标。介绍龙芯自主指令系统架构LoongArch;并从构建LoongArch的基础软件体系、研发兼容及自主编程框架、通过二进制翻译实现与X86等主流架构的应用兼容、LoongArch开源社区建设等方面介绍龙芯软件生态建设进展及计划。

基于龙芯2K2000处理器的SATA驱动设计与实现

针对目前国产嵌入式龙芯系列芯片的设备接口驱动适配工作需要完善的现状,文章选取了SATA盘设备进行研究。为实现在龙芯系列处理器上适配SATA驱动和使用大容量外部存储设备的功能,通过分析龙芯2K2000处理器上SATA设备的工作原理,根据SATA接口采用的AHCI技术协议,提出了一种可以适配LoongArch架构和MIPS64架构的SATA驱动模型,在嵌入式操作系统上设计并实现了完整的SATA驱动程序。经过不同场景下的功能和可靠性测试,验证SATA驱动的读写一致性和读写速率等基本功能,测试结果显示所提出的SATA驱动程序满足龙芯系列2K20000处理器的基本功能需求,可以应用在嵌入式操作系统程序中。