Schedules Are Solvable Symbols: Tuning-Free Compilation of Tile Programs on Dataflow Architectures
School of Computing, National University of Singapore（新加坡国立大学计算机学院）
本文提出Loom，一种免调优符号编译框架，通过将瓦片程序编译视为硬件显式静态优化问题，在数据流架构上联合求解调度与块大小，匹配或超越供应商优化库。
2026-09-25 cs.PL
UNIT: Unifying Tensorized Instruction Compilation
University of California, Los Angeles（加利福尼亚大学洛杉矶分校）；Amazon Web Services（亚马逊网络服务）
由于DNN对计算的需求不断增加，研究人员开发了硬件和软件机制来减少计算和内存负担。一种广泛采用的方法是使用混合精度数据类型。然而，由于数据转换的开销，在没有硬件支持的情况下很难利用混合精度。硬件供应商提供用于混合精度张量运算的张量化指令，如Intel VNNI、Tensor Core和ARM-DOT。这些指令涉及一种计算习惯用法，它将多个低精度元素减少为一个高精度元素。缺乏编译技术使得很难利用这些指令：使用供应商提供的计算密集型内核库是不灵活的，并阻止进一步优化，手动编写硬件intrinsic容易出错，对程序员来说很困难。一些先前的作品通过为每个指令创建编译器来解决这个问题。当涉及到许多张量化指令时，这需要付出过多的努力。在这项工作中，我们开发了一个编译器框架来统一这些指令的编译-统一的语义抽象简化了新指令的集成，并重用分析和转换。来自不同平台的Tensorized指令可以通过UNIT进行编译，并具有良好的性能。给定一个张量化指令和一个张量操作，UNIT会自动检测适用性，转换操作的循环组织，并重写循环体以利用张量化指令。根据我们的评估，UNIT可以针对各种主流硬件平台。生成的端到端推理模型在x86 CPU上实现了Intel oneDNN的1.3倍加速，在NvidiaGPU上实现了Nvidia cuDNN的1.75倍加速，在ARM CPU上实现了精心调整的ARM DOT TVM解决方…
2021-03-28 cs.AR cs.LG cs.PF
Modularity and Separate Compilation in Logic Programming
以模块化方式编写代码的能力对于构建大型程序很重要。在逻辑编程环境中，希望通过基于逻辑的设备实现此类功能。我们在这里描述了一种实现此目的的方法。在我们的方案中，一个模块对应于一个代码块，其外部视图是由签名介导的。因此，签名强加了一种形式的隐藏，通过谓词，函数和常量名称的存在量化在逻辑上解释。模块通过累积机制进行交互，累积机制转化为连接其中的子句，同时尊重签名引入的存在量词的范围。我们表明，这种简单的静态结构化命名空间的设备足以实现与代码范围相关的功能，谓词定义的动态控制早先被认为是必要的。我们提出的模块功能以前已经通过累积模块的编译时内联实现。此方法不支持单独编译。我们纠正这种情况下，每个不同的模块可以单独编译和内联可以实现一个后来的，互补的，同样有效的链接阶段。
2023-03-18 cs.PL
TinyIREE: An ML Execution Environment for Embedded Systems from Compilation to Deployment
在过去十年中，用于训练和执行的机器学习模型部署一直是工业和学术研究的重要主题。大部分注意力都集中在开发特定的工具链来支持加速硬件。在本文中，我们提出了IREE，一个统一的编译器和运行时堆栈，其明确目标是将机器学习程序缩减到移动和边缘设备的最小占用空间，同时保持扩展到更大部署目标的能力。IREE采用基于编译器的方法，并通过使用MLIR编译器基础设施来优化异构硬件加速器，该基础设施提供了快速设计和实现多层编译器中间表示（IR）的方法。更具体地说，本文重点关注TinyIREE，这是IREE中的一组部署选项，可适应嵌入式系统和裸机平台中有限的内存和计算资源，同时还展示了IREE的直观工作流程，可通过LLVM为不同的ISA扩展和ABI生成工作负载。
2022-05-28 cs.PL
GRADE-RTL: Evaluating LLM-Generated RTL Beyond Compilation
Vellore Institute of Technology（维洛尔理工学院）；Queen’s University Belfast（贝尔法斯特女王大学）；Umm Al-Qura University（乌姆古拉大学）；University of Idaho（爱达荷大学）
本文提出GRADE-RTL框架，通过五项检查评估LLM生成的RTL代码，超越编译验证，区分结构、功能与实现质量，实验显示端到端成功率0%至70%，并揭示功能等价RTL在物理实现上的显著差异。
2026-09-23 cs.AR cs.PL
Strategy Preserving Compilation for Parallel Functional Code
图形处理单元（GPU）和其他并行设备是广泛可用的，并且具有加速广泛类别的算法的潜力。但是，需要专业的编程技能才能实现最佳性能。这些设备通过命令式编程接口暴露低级硬件细节，其中程序员显式地编码设备特定的优化策略。这不可避免地导致非性能可移植程序在其他设备上提供次优性能。函数式编程模型最近在系统社区中复兴，因为它们为解决性能可移植性挑战提供了可能的解决方案。最近的工作已经表明，如何自动选择高性能的并行化策略的广泛的硬件架构编码的功能表示。然而，这种功能表示到硬件接口所期望的命令式程序的转换通常是临时执行的，没有正确性保证，也没有保证保留预期的并行化策略。在本文中，我们提出了一个形式化的战略保持翻译从高层次的功能代码低层次的数据竞争免费并行命令式代码。这种翻译是制定和证明正确的语言，我们称之为数据并行理想化的Algol（DPIA），方言雷诺兹的理想化的Algol。GPU和多核CPU上的性能结果表明，形式化的翻译过程生成的低级代码的性能与ad hoc方法生成的代码相当。
2017-10-23 cs.DC cs.PL
QPanda3: A High-Performance Software-Hardware Collaborative Framework for Large-Scale Quantum-Classical Computing Integration
针对量子-经典融合应用中经典编译与通信耗时过长的瓶颈，研究团队推出高性能量子编程框架QPanda3，通过优化编译、OriginBIS指令流等技术实现多维度性能跃升，支撑多领域量子算法开发与产业落地。
2025-06-13 cs.PL
Towards a Fully Abstract Compiler Using Micro-Policies: Secure Compilation for Mutually Distrustful Components
安全编译可以防止对编译代码的所有低级攻击，并允许对源语言的安全性进行合理的推理。在这项工作中，我们提出了一个新的攻击者模型的安全编译，扩展了众所周知的概念，充分的抽象，以确保保护相互不信任的组件。我们设计了一个编译器链（编译器，链接器和加载器）和一个新的安全监视器，共同抵御这种强大的攻击模型。该监视器是使用最近提出的，通用的基于标签的保护框架，称为微策略，它配备了硬件支持高效缓存和形式化验证方法。我们的监视器保护抽象的一个简单的面向对象的语言-类隔离，方法调用的纪律，和类型安全-对任意低级别的攻击者。
2015-10-02 cs.CR cs.PL
A Compilation Target for Probabilistic Programming Languages
University of Oxford（牛津大学）
通过创造性地使用标准化的操作系统功能，包括进程、分叉、互斥和共享存储器，可以用任何程序设计语言来实现诸如用于概率编程的顺序蒙特卡罗和粒子马尔可夫链蒙特卡罗的前向推理技术。利用这一点，我们已经定义，开发和测试的概率程序设计语言中间表示语言，我们称之为概率C，它本身可以被编译成机器码的标准编译器和链接到操作系统库产生一个有效的，可扩展的，便携式的概率编程编译目标。这为优化概率编程系统开辟了一条新的硬件和系统研究路径。
2014-07-10 cs.AI cs.PL stat.ML
Modular Compilation of a Synchronous Language
同步语言依赖于形式化方法，以一种高效和可重用的方式简化应用程序的开发。形式化方法一直被提倡作为一种提高系统可靠性的手段，特别是那些安全或业务关键的系统。由于状态爆炸、不可判定性等限制，开发自动规格说明和验证工具仍然是困难的。在这项工作中，我们设计了一个新的规范模型的基础上反应同步的方法。然后，我们受益于一个正式的框架，非常适合执行编译和正式的系统验证。在实践中，我们设计并实现了一个专用语言（LE）和它的两个语义：抽象语义帮助我们定义一个程序的行为集，并避免在程序的解释歧义;执行等式语义允许模块化编译程序到软件和硬件目标（C代码，VHDL代码，FPGA综合，观察员）。考虑到关键现实应用程序的两个主要要求，我们的方法是相关的：模块化编译使我们能够处理大型系统，基于模型的方法为我们提供了正式的验证。
2008-01-24 cs.LO cs.PL
Quantum Gate Decomposition: A Study of Compilation Time vs. Execution Time Trade-offs
本研究在Ket平台上实现并分析最先进的多量子比特门分解算法，首次在单一平台内比较其编译时间与执行时间权衡，并提出两种分别优化编译时间和执行时间的编译配置文件。
2025-09-11 cs.PL quant-ph
Gemini: A Functional Programming Language for Hardware Description
本文介绍了双子座，功能程序设计语言的硬件描述，提供的功能，如参数多态性，递归数据库，高阶函数，和类型推断更高的表达能力相比，现代硬件描述语言。Gemini通过其独特的类型系统（由多个原子类型和依赖类型组成）演示了新颖的类型理论概念的理论和实现，该类型系统允许该语言安全地对软件和硬件构造进行建模，并通过多阶段编译执行类型推断。本文的主要技术成果包括形式化的双子座语法，类型规则，和评估规则，双子座的类型系统的安全性证明，和编译器的语义分析阶段的原型实现。
2019-11-10 cs.PL
SimuQ: A Framework for Programming Quantum Hamiltonian Simulation with Analog Compilation
SimuQ是首个支持哈密顿量编程和脉冲级编译的量子模拟框架，通过AAIS抽象和求解器编译，在IBM、QuEra和IonQ设备上实现异构模拟量子模拟器的统一编程与高效模拟。
2023-11-19 cs.PL quant-ph
CktFormalizer: Autoformalization of Natural Language into Circuit Representations
The University of Hong Kong（香港大学）
CktFormalizer通过依赖类型HDL在Lean 4中实现LLM生成硬件描述的自动形式化，解决Verilog中的宽度不匹配、组合环和不完整案例逻辑问题，提升后端实现率和仿真通过率。
2026-10-06 cs.CL cs.PL
Compilation Techniques for Graph Algorithms on GPUs
图形程序的性能在很大程度上取决于算法、输入图形的大小和结构以及底层硬件的特性。没有一组优化或一个硬件平台可以在所有设置中很好地工作。为了实现高性能，程序员必须仔细选择要使用哪组优化和硬件平台。GraphIt程序设计语言使程序员只需编写一次算法，并使用调度语言针对不同的输入进行优化。然而，GraphIt目前不支持为GPU生成高性能代码。为了在GPU上实现高性能，程序员必须采用一种具有完全不同的抽象和优化集的低级语言从头开始重新实现整个算法。我们提出GG，一个扩展的GraphIt编译器框架，实现高性能的CPU和GPU使用相同的算法规范。GG通过一种新的GPU调度语言和编译器显着扩展了GPU图形处理框架的优化空间，该语言和编译器支持为GPU组合图形优化。GG还引入了基于边缘的线程扭曲CTA负载均衡（ETWC）和边缘阻塞（EdgeBlocking）两种性能优化，为GPU拓展了优化空间。ETWC通过动态地将每个顶点的边划分为分配给线程、线程束和CTA以供执行的块来改进负载均衡。EdgeBlocking通过重新排序边和限制随机内存访问以适应L2缓存来提高程序的局部性。我们在Pascal和Volta两代NVIDIA GPU上对5种算法和9种输入图形进行了评估，结果表明，它在最先进的GPU图形处理框架上实现了高达5.11倍的加速比，并且在90个实验中的66个实验中是最快的。
2021-01-08 cs.DC cs.PL
Cyclotron: Compilation of Recurrences to Distributed and Systolic Architectures
Cyclotron是一个将递推方程表达的流数据流算法编译到分布式和脉动架构的框架与编译器，通过三层语言转换优化内存访问，支持用户定义调度实现流水线执行，在多硬件平台验证了可移植性，生成的分布式矩阵运算实现与ScaLAPACK竞争力相当。
2025-11-13 cs.PL
HELIX: Verified compilation of cyber-physical control systems to LLVM IR
University of Cambridge（剑桥大学）；INRIA（法国国家数字科学研究所）；Taras Shevchenko National University（塔拉斯·舍甫琴科国立大学）；Université Paris Cité（巴黎西岱大学）；University of Pennsylvania（宾夕法尼亚大学）
HELIX通过代数变换将高性能量算转换为LLVM IR，结合形式化验证确保代码正确性，展示从数学描述到高效实现的全过程。
2026-03-27 cs.PL
swTVM: Towards Optimized Tensor Code Generation for Deep Learning on Sunway Many-Core Processor
Beihang University（北京航空航天大学）；National University of Singapore（新加坡国立大学）；Tsinghua University（清华大学）
深度学习框架和硬件平台的蓬勃发展一直要求高效的编译器能够屏蔽软件和硬件的多样性，以提供应用程序的可移植性。在现有的深度学习编译器中，TVM以其在不同硬件设备上的代码生成和优化效率而闻名。与此同时，Sunway众核处理器凭借其在科学计算和深度学习工作负载方面的诱人计算能力，成为一个有竞争力的候选者。本文结合这两个方向的趋势。具体来说，我们提出了swTVM，扩展了原来的TVM，以支持提前编译的架构，需要交叉编译，如Sunway。此外，我们在编译过程中利用了架构特性，例如用于大规模并行的核心组，用于高带宽内存传输的DMA和用于数据局部性的本地设备内存，以便为Sunway上的深度学习工作负载生成高效的代码。实验结果表明，在六个有代表性的基准测试中，与Sunway上最先进的深度学习框架相比，swTVM生成的代码平均达到1.79倍。这项工作是第一次尝试从编译器的角度来弥合深度学习和Sunway处理器的差距，特别是考虑到生产力和效率。我们相信这项工作将鼓励更多的人接受深度学习和神威众核处理器的力量。
2022-07-11 cs.LG cs.PL stat.ML
