• 用于 MLIR 中自动微分的声学与模块化活动分析

  摘要计算导数在多个领域中都至关重要，从训练神经网络到精确的气候模拟都离不开这一过程。虽然可以通过自动微分（AD）工具生成导数，但通常需要采取积极的优化措施以避免影响程序性能。其中一项核心优化工作是识别那些对目标偏导数没有贡献的“非活跃”操作。有多种工具可以为各种输入语言提供“活动性”分析功能，但这些工具通常仅提供非正式的正确性保证。本文正式定义了自动微分中的活动性分析方法，并证明了其正确性，同时将其实现了在MLIR编译器框架中。为了体现MLIR的通用性，本文首次对适用于自动微分的MLIR内部表示的一个子集进行了形式化描述。此外，本文还提出了一种基于函数摘要的全程序活动性分析的近似方法，并设计了

  来源：Proceedings of the ACM on Programming Languages

  时间：2025-11-07

• 调试 WebAssembly？用点强力工具吧！

  摘要调试和监控程序是软件工程及部署过程中的关键环节。动态分析方法通过源代码或中间表示（IR）注入、机器码或字节码重写、虚拟机API或直接硬件支持来监控应用程序。尽管这些技术在各自的领域内是可行的，但跨技术的通用工具却非常罕见，这导致了技能分散、重复劳动以及功能支持不一致的问题。我们在WebAssembly生态系统中通过Whamm来解决这一问题。Whamm是一个专为Wasm设计的仪器化框架，它利用引擎级别的探测机制，并提供字节码重写功能以提升代码的可移植性。Whamm解决了三个主要问题：1）工具的碎片化；2）通用框架带来的高昂仪器化开销；3）定制低级高性能机制的繁琐性。Whamm提供了完全可编程

  来源：Proceedings of the ACM on Programming Languages

  时间：2025-11-07

• 能力图：Rust所有权与借用保障机制的通用模型

  摘要由于Rust的类型系统在控制别名和可变性方面提供了丰富的保障，因此它成为了验证和程序分析工具的理想目标。然而，完全理解、提取和利用这些保障是非常微妙且具有挑战性的：现有的Rust类型检查模型要么支持一种与实际Rust代码脱节的简化语言，要么在精确建模Rust的借用操作、存储这些操作的复合类型、函数签名以及循环等方面存在严重限制。在本文中，我们提出了“位置能力图”（Place Capability Graphs）：这是一种新的Rust类型检查结果模型，它克服了上述限制，并且可以直接从Rust编译器自身的程序化表示和分析中计算得出。我们证明了该模型能够覆盖最流行的公共Rust库中97%以上的函

  来源：Proceedings of the ACM on Programming Languages

  时间：2025-11-07

• 用于交互式定理证明的策略库的自动化发现

  摘要为了利用交互式定理证明器（ITPs）推进形式化推理，实现更简洁、更模块化的证明至关重要。由于许多ITPs（如Rocq和Lean）采用策略式证明方法，因此学习高级自定义策略对于证明的模块化和自动化至关重要。本文提出了一种新颖的策略发现方法，该方法利用策略依赖图（TDGs）来识别多个证明中可重用的证明策略。TDGs能够捕捉策略应用之间的逻辑依赖关系，同时忽略无关的句法细节，从而既有助于发现新的策略，也有助于将现有证明重构为更模块化的形式。我们已在名为TacMineR的工具中实现了这一技术，并将其与基于反统一的方法（Peano）进行了对比。评估结果表明，TacMineR能够学习的策略数量是Pea

  来源：Proceedings of the ACM on Programming Languages

  时间：2025-11-07

• 利用逻辑关系对可达性类型进行建模：语义类型正确性、终止性、效果安全性及等式理论

  摘要可达性类型是一种近期提出的方法，旨在将Rust风格的关于内存属性的推理机制引入到更高级的语言中，重点关注高阶函数、参数化类型以及共享的可变状态——这些特性在当前Rust中使用的技术中仅得到了部分支持。虽然之前的研究已经利用常规的“进展”和“保持”等语法技术证明了可达性类型的关键类型正确性，但更强的元理论属性至今尚未被探索。本文提出了一种基于逻辑关系的可达性类型的替代语义模型，为研究以下关键属性提供了框架：（1）语义类型正确性，包括那些在语法上并不完全符合类型要求的代码片段；（2）终止性，特别是在存在高阶可变引用的情况下；（3）效果安全性，尤其是不存在可观察到的状态变化；最后是（4）程序等价

  来源：Proceedings of the ACM on Programming Languages

  时间：2025-11-07

• 概率程序的结构抽象与精炼

  摘要在本文中，我们提出了一种名为“结构抽象细化”的新框架，用于验证概率程序的阈值问题。我们的方法通过抽象掉语句的语义，将概率控制流自动机（PCFA）的结构表示为马尔可夫决策过程（MDP）。MDP的“最大可达性”自然地为违规概率提供了一个适当的上限，这个上限被称为“结构上限”。这种方法为PCFA和MDP之间的关系提供了一种新的“结构化”描述，与传统的“语义化”视角形成对比——在传统视角中，MDP反映了程序的语义。该方法的独特之处在于它清晰地分离了概率与计算语义之间的关注点：抽象层仅关注概率计算，而细化层仅处理语义方面；因此，无需修改即可使用非随机程序验证技术。基于这一特点，我们提出了一个通用的基

  来源：Proceedings of the ACM on Programming Languages

  时间：2025-11-07

• 舞蹈动作的快速变化：一类定位（集合）多态性

  摘要编舞编程是一种用于并发系统编程的有前景的新范式，开发者编写一个集中的程序，该程序会被编译成每个节点的单独程序。然而，现有的编舞语言缺乏现代系统所必需的关键特性，例如某个节点能够动态判断谁应该执行某个计算，并将这一决策发送给其他节点。本研究通过 λQC 来填补这一空白。λQC 是第一种支持“一类进程名称”以及对类型和（集合）位置进行多态化的类型化编舞语言。它还通过支持代数和递归数据类型以及多位置值，提升了编程的表达能力。我们在 Rocq 框架中对我们的结果进行了形式化定义和机械验证，包括标准的编舞编程保证——即无死锁特性。

  来源：Proceedings of the ACM on Programming Languages

  时间：2025-11-07

• 构建一个基于理论支撑且具有实用性的选择性对象敏感指针分析框架

  摘要上下文敏感性是指针分析中的基础技术，对于提高分析精度至关重要，但往往会导致显著的效率损失。最近的进展集中在选择性上下文敏感性分析上，即仅对程序中的部分元素（如方法或堆对象）进行上下文敏感性分析，而对其他元素则采用上下文不敏感性分析，以此在精度和效率之间取得平衡。然而，尽管这类方法越来越多，现有的方法通常是基于特定的代码模式来设计的，因此缺乏系统识别可以从上下文敏感性中受益的代码场景的全面理论基础。本文提出了一种新颖的基础理论，该理论能够准确估计出在上下文敏感性下真正能够提高精度的对象范围。所提出的理论将这种上限的识别问题重新表述为典型的指针流图（Pointer Flow Graph, PF

  来源：Proceedings of the ACM on Programming Languages

  时间：2025-11-07

• Tabby：一种用于高性能零知识证明电路的合成辅助编译器

  摘要零知识证明（ZKP）应用需要将高级程序转换为算术电路——这一过程既要求正确性，也要求效率。尽管最近的DSL（领域特定语言）提高了可用性，但它们生成的电路往往不够理想，而手工优化的实现仍然难以构建和验证。我们提出了Tabby，这是一种基于综合技术的编译器，能够自动从高级代码生成高性能的ZKP电路。Tabby引入了一种专为符号推理设计的领域特定中间表示，并应用基于草图的程序综合方法来生成优化的低级实现。通过将程序分解为可重用的组件，并通过基于SMT（符号模型检测）的推理来验证语义等价性，Tabby在确保正确性的同时显著提升了性能。我们在一系列实际ZKP应用中对Tabby进行了评估，发现与主流Z

  来源：Proceedings of the ACM on Programming Languages

  时间：2025-11-07

• 浮动自标记

  摘要动态和多态语言会将类型等信息附加到运行时对象上，因此需要调整内存布局以容纳这些信息。这使得高效实现IEEE754浮点数变得困难，因为该格式没有预留易于访问的空间来存储类型信息。目前常用的三种浮点数编码方式——带标签的指针、NaN装箱（NaN-boxing）和NuN装箱（NuN-boxing）都存在缺陷。带标签的指针会导致所有浮点对象都需要在堆（heap）上分配内存；而NaN装箱和NuN装箱则会增加类型检查及其他对象处理的运行时开销。本文介绍了一种新的对象标记方法——自标记（self-tagging），该方法利用可逆的位运算将浮点数映射到带有正确类型信息的标记值中，这些标记值将数值和类型信息

  来源：Proceedings of the ACM on Programming Languages

  时间：2025-11-07

• “通过构建保证正确性：通过神经网络训练实现认证个体公平性”

  摘要随着伦理问题的日益突出，机器学习中的公平性比以往任何时候都更加重要。个体公平性要求仅在敏感属性上存在差异的个体能够获得相同的结果。然而，常用的机器学习算法往往无法实现这种公平性。为了提高个体公平性，人们开发了各种训练方法，例如将公平性约束作为优化目标。尽管这些方法在实证上显示出有效性，但它们缺乏对公平性的正式保证。现有的旨在提供公平性保证的方法主要依赖于验证技术，而这些技术有时无法得出明确的结果。此外，仅靠验证并不能在训练过程中主动提升个体公平性。为了解决这一限制，我们提出了一个能够在整个训练过程中正式保证个体公平性的新框架。我们的方法包括两部分：（1）可证明公平的初始化过程，确保模型从公

  来源：Proceedings of the ACM on Programming Languages

  时间：2025-11-07

• 将线性运动G代码形式化，用于制造工具的不变性检测和差分测试

  摘要3D打印的计算制造流程类似于编译器：用户使用计算机辅助设计（CAD）工具设计模型，这些模型会被转换为多边形网格，最终由3D切片软件编译成机器代码。对于传统的编译器和编程语言，已经建立了检查程序不变性的技术。同样，差分测试等方法也常用于发现编译器本身的错误，从而提高其可靠性。制造流程也可以从类似的技术中受益，但传统方法并不直接适用于该领域使用的表示形式。与传统程序不同，3D模型既以几何对象（如CAD模型或多边形网格）的形式存在，也以最终在硬件上运行的机器代码的形式存在。与传统编译过程一样，机器代码受到许多因素的影响，例如模型本身、所使用的切片软件以及众多用户可配置的参数，这些参数控制着切片过

  来源：Proceedings of the ACM on Programming Languages

  时间：2025-11-07

• ABC：通过模型融合实现通用代码样式器

  摘要基于代码语言模型（code LMs）构建的代码风格转换模型取得了显著的成果。然而，这些模型通常专注于基础风格转换，即目标风格遵循单一标准，而在处理组合风格转换时往往面临困难，因为组合风格涉及多个标准。实际上，风格指南中包含多个标准，因此缺乏有效的组合风格转换能力成为这些模型在实际应用中的主要限制。在本文中，我们提出了“Absent-Basis-Combination”（简称ABC）这一新颖的代码风格转换框架，该框架显著提升了组合风格转换的性能，并克服了现有方法的局限性。我们实现了四种不同参数规模的ABC版本，分别为0.5B、1.3B、1.5B和3B，结果表明在所有模型规模下，ABC在基础风

  来源：Proceedings of the ACM on Programming Languages

  时间：2025-11-07

• 保持非干扰性的优化编译

  摘要为了保护安全关键型应用程序，安全编译器必须在编译过程中维护诸如“不干扰”之类的安全策略。维护安全策略超出了传统编译器正确性的概念范畴，后者仅要求保留源程序的语义。因此，一些标准的编译器优化操作可能会破坏这些安全策略。现有的安全编译方法在允许的编译器优化类型或支持的安全策略方面存在诸多限制，这主要是由于其形式化框架的概念性局限。在本文中，我们提出了“超属性模拟”（hyperproperty simulations）这一新颖的安全编译框架，该框架能够模拟编译过程中任意“k-超属性”（k-hyperproperties）的保持机制，并克服了现有方法的诸多局限性，特别是在表达能力和灵活性方面表现更

  来源：Proceedings of the ACM on Programming Languages

  时间：2025-11-07

• 现在：在保密计算中，减少信任，更多依赖验证机制

  摘要保密计算（Confidential Computing, CC）专为安全关键场景设计，利用远程认证机制来保证云服务器上代码的完整性。然而，仅靠保密计算本身无法确保代码具备高级别的安全特性（例如防止数据泄露）。在本文中，我们提出了一个名为Agora的新框架，该框架经过精心设计，旨在为保密计算提供一个可信且开放的验证平台。为了提升可信度，我们发现某些验证任务可以委托给不受信任的实体，而相应的（规模较小的）验证器则安全地部署在受信任的计算基础（Trusted Computing Base, TCB）内部。此外，通过基于区块链的奖励任务管理系统，Agora还利用众包机制来降低对复杂定理证明工具的依

  来源：Proceedings of the ACM on Programming Languages

  时间：2025-11-07

• 理解并改进易出错的测试分类问题

  摘要回归测试是软件开发中不可或缺的一部分，但它存在“易变测试”（flaky tests）的问题——这类测试在相同代码上运行时结果不稳定，有时通过有时失败。这种不可预测的失败浪费了开发者的时间，且常常掩盖了真正的错误。先前的研究表明，经过微调的大型语言模型（LLMs）能够以非常高的准确率将易变测试分类到不同的类别中。然而，我们发现由于实验设计不当和数据集不真实，之前的方法高估了模型的准确率，从而使得易变测试分类问题看起来比实际更简单。在本文中，我们首先指出之前的易变测试分类器之所以高估预测准确率，原因在于：1）实验设计存在缺陷；2）它们所使用的数据集中易变测试（以及非易变测试）的真实分布被错误地

  来源：Proceedings of the ACM on Programming Languages

  时间：2025-11-07

• TianheGraph：一种具有拓扑感知能力的图处理框架

  在当今数据处理领域，随着图数据规模的不断扩大，对大规模图的高效处理成为一项关键挑战。图数据可以达到数十亿甚至数万亿条边，这种规模的数据对计算资源提出了极高的要求。传统的图处理引擎和方法在扩展性方面存在局限，通常无法有效支持超过几十个计算节点的并行处理，这主要归因于两方面的问题：一方面，它们在处理大规模图时需要大量的内存，导致存储和计算成本高；另一方面，它们未能充分考虑不同层级网络连接结构所带来的通信成本差异。为了克服这些挑战，本文提出了TianheGraph，一种专门设计用于提升大规模并行系统中图处理效率的软件方法。TianheGraph的核心在于其独特的空间-时间高效图压缩技术，以及其创新的

  来源：ACM Transactions on Architecture and Code Optimization

  时间：2025-11-07

• 具有布尔代数的合格类型

  摘要我们提出了基于布尔代数的类型限定符。传统的带有类型限定符的类型系统都是基于格（lattices）构建的，但格无法表达排他关系。我们认为，允许排他关系的布尔代数是作为类型限定符的实用且合适的数学基础。在本文中，我们提出了一个名为System F<:B的计算系统，该系统在布尔代数上扩展了原有的System F<:，并支持否定操作、限定符多态性以及子限定（subqualification）功能。我们展示了如何利用System F<:B来设计一个具有效果多态性（effect polymorphism）、子效果操作（subeffecting）以及多态效果排他性（polymorphic effect

  来源：Proceedings of the ACM on Programming Languages

  时间：2025-11-07

• Cppless：基于C++的单一源代码、高性能的无服务器编程

  ### Cppless：实现C++应用中高效服务器端函数的单源框架在现代计算环境中，服务器端函数（Serverless Functions）作为一种新兴的计算模型，为开发者提供了更灵活、更具弹性的计算资源管理方式。这种模型的核心理念是将计算任务从应用程序中分离出来，由云平台动态分配资源并执行，从而实现高效的计算任务并行处理。然而，对于C++应用程序而言，这一模式的集成仍然面临诸多挑战，包括复杂的部署流程、客户端与云环境之间的兼容性问题，以及输入和输出数据类型不一致导致的转换开销。为了克服这些障碍，我们提出了一种全新的解决方案——Cppless，一个专为C++设计的单源编程框架，它能够将应用程序

  来源：ACM Transactions on Architecture and Code Optimization

  时间：2025-11-07

• 致力于优化学习到的索引，以实现高性能、内存高效性以及对非统一内存架构（NUMA）的支持

  在数据存储领域，索引结构是提升数据访问效率的关键技术之一。传统索引，如Trie树和B+树，长期作为数据库、文件系统和搜索引擎的核心组件，为数据检索提供了基础支持。然而，随着数据量的指数级增长，这些经典索引在性能和空间效率方面逐渐显现出局限性。近年来，学习型索引（Learned Index）作为一种新兴的索引设计范式，通过引入机器学习模型来预测数据的位置，显著提升了索引的查询效率。尽管如此，现有的学习型索引仍然面临性能与空间消耗之间的权衡问题，以及在多NUMA节点环境下的扩展性挑战。为了解决这些问题，本文提出了一种名为DiffLex的学习型索引，它在保持高性能的同时，优化了内存使用效率，并引入了

  来源：ACM Transactions on Architecture and Code Optimization

  时间：2025-11-07

知名企业招聘：