• MTP：一种用于人工智能集成编程的基于意义类型的语言抽象机制

  摘要软件开发正从传统的编程方式转向基于人工智能（AI）的应用程序，这些应用程序在运行时利用生成式AI和大型语言模型（LLMs）。然而，集成LLMs仍然非常复杂，开发者需要手动编写提示并处理输出结果。现有的工具试图辅助提示工程，但往往会增加额外的复杂性。本文提出了一种名为“Meaning-Typed Programming (MTP)”的新范式，它通过直观的语言级结构来抽象LLMs的集成过程。MTP利用代码固有的语义丰富性，自动完成提示生成和响应处理，无需开发者额外投入精力。我们介绍了以下关键技术：(1) by操作符，用于无缝调用LLMs；(2) MT-IR，一种基于语义的中间表示方法，用于提取

  来源：Proceedings of the ACM on Programming Languages

  时间：2025-11-07

• 用于机械化程序验证的结构时序逻辑

  摘要对于具有副作用和非确定性的无限程序，实现其活性属性的自动化验证具有挑战性。现有的时序推理框架主要在模型层面（如轨迹和自动机）进行操作。这些推理过程处于非常底层的层次，需要复杂的嵌套（协同）归纳证明技术以及对证明辅助工具（例如保护性检查器）的熟悉程度。此外，仅在模型层面进行推理而忽略程序结构本身，会导致验证过程中无法充分利用结构化程序逻辑（如Hoare逻辑）所具备的模块化和组合性优势。为了解决这一验证难题以及时序规范缺乏组合性证明技术的问题，我们提出了一种新的结构化时序逻辑——Ticl。通过使用Ticl，我们将复杂的（协同）归纳证明技术编码为结构化引理，并将推理重点放在程序的变体和不变量上。

  来源：Proceedings of the ACM on Programming Languages

  时间：2025-11-07

• 基于“天使假设”（Angelic Assumptions）的开源程序内存安全性验证

  摘要开源程序是指其完整源代码无法获取的程序，这在现实世界的程序验证中是普遍存在的现象。软件验证工具往往会对其未受限制的行为持最坏的假设，这可能导致针对开源程序产生大量虚假警告。对于任何严肃的验证工作，工程师都必须预先投入时间来构建缺失代码的合适模型（或模拟代码），而这既耗时又容易出错。模拟代码中的不准确之处可能会导致错误的验证结果。在本文中，我们展示了一种能够高精度区分开源程序中虚假阳性结果（误报）和实际错误以及潜在内存安全违规的技术。该技术的核心在于能够对缺失的代码做出合理的假设。为此，我们首先使用大型语言模型（LLM）从处理缓冲区的程序中提取一组惯用模式。然后通过一种形式化的合成策略对这些

  来源：Proceedings of the ACM on Programming Languages

  时间：2025-11-07

• RACER：避免加速型芯片多处理器中的端到端性能下降问题

  在当今的数据中心计算环境中，集成在CPU芯片上的硬件加速器正在成为一种重要的技术趋势。这些加速器与通用核心的近距离结合，使得它们能够高效地执行特定的固定功能内核，从而为系统带来显著的性能提升和能效优化。然而，这种技术并非在所有情况下都能带来预期的收益。有时，将计算任务转移到硬件加速器上反而会导致整体执行时间的增加，这种现象被称为“端到端的减速”。本文介绍了一种名为RACER的硬件架构和运行时系统，旨在规避这种风险，确保硬件加速不会导致性能下降，从而提升请求处理工作的效率。### 避免端到端性能损失的关键RACER的核心设计理念是通过多种优化手段来解决传统硬件加速方法中存在的问题。首先，它引入了

  来源：ACM Transactions on Architecture and Code Optimization

  时间：2025-11-07

• Mobile-3DCNN：一种用于在移动设备上超实时执行大型3D卷积神经网络（3D CNN）的加速框架

  ### 3D CNN在移动设备上的加速：Mobile-3DCNN框架解读近年来，3D卷积神经网络（3D CNN）在视频分析和动作识别等领域得到了广泛应用。然而，将3D CNN部署到移动设备上，尤其是在需要实时执行和高推理精度的情况下，面临诸多挑战。这是因为3D CNN的模型尺寸和结构通常比2D CNN更为庞大，导致其对计算和内存资源的需求显著增加。在移动平台上，这种高需求可能限制了模型的执行效率，使其难以满足实时处理的需求。为了应对这一挑战，本文提出了一种名为Mobile-3DCNN的端到端3D CNN加速框架，该框架通过结合权重剪枝和编译器优化，实现了对3D CNN的高效执行。具体而言，Mo

  来源：ACM Transactions on Architecture and Code Optimization

  时间：2025-11-07

• 合成声音与精确摘要变换器，用于非线性双曲偏微分方程求解器

  摘要偏微分方程（PDEs）在科学计算和工程领域中起着至关重要的作用。尽管数值方法使得求解PDEs变得可行，但这些数值求解器仍面临诸多问题，尤其是在处理双曲型PDEs时。这些问题源于多个方面：首先是PDE所描述的物理模型本身，它可能导致诸如冲击波形成等现象；其次是PDE求解器自身的近似方法，这些方法可能会引入虚假的数值误差。这些问题可能导致求解器程序崩溃（由于数值溢出），或者返回精度极低的结果（由于虚假振荡或能量耗散）。此外，许多PDE的非线性特性进一步加剧了这些挑战。另外，PDE求解器还必须遵守某些数值不变性，例如CFL条件。因此，迫切需要対PDE求解器进行程序分析，以确保这些问题不会发生，并

  来源：Proceedings of the ACM on Programming Languages

  时间：2025-11-07

• 追踪即时编译在效果处理和处理器中的应用

  摘要效果处理器（effect handlers）是一种近年来逐渐流行的编程语言特性。它们允许实现非局部但结构化的控制流，并涵盖了生成器（generators）、异常处理（exceptions）、异步性（asynchronicity）等特性。然而，目前的实现方式往往为了追求高效性而牺牲了一些功能。元追踪（meta-tracing）即时（JIT）编译器通过引入解释器的方式，有望提升编译器的性能。这些编译器会记录程序的执行过程，动态检测热点循环（hot loops），并利用运行时可获得的信息对这些循环进行优化。它们在优化动态控制流方面表现出色，而这正是效果处理器所引入的核心功能。我们首次针对效果处理

  来源：Proceedings of the ACM on Programming Languages

  时间：2025-11-07

• 静态分析R程序的数据流

  摘要R编程语言主要用于统计计算，主要由没有计算机科学背景的研究人员使用。R提供了许多动态特性和独特功能，这些特性很难通过静态分析来理解，例如动态作用域、惰性求值以及动态副作用等。同时，R生态系统缺乏能够帮助研究人员理解和改进代码的复杂分析工具。在本文中，我们提出了一种针对R编程语言的新型静态数据流分析框架，该框架能够处理R程序的动态特性，并生成给定R程序的数据流图。这种数据流图在多种分析中都非常有用，包括程序切片分析，我们通过一个概念验证来实现这一点。核心分析机制是对R程序抽象语法树的标准化版本进行状态化处理，跟踪（重新）定义、值、函数调用、副作用以及动态控制流，从而为每个程序生成一个数据流图

  来源：Proceedings of the ACM on Programming Languages

  时间：2025-11-07

• 激活函数的凸包近似

  摘要深度学习在安全关键领域的广泛应用促使人们需要正式验证神经网络的鲁棒性。这一努力中的一个关键挑战在于处理激活函数固有的非线性问题。激活函数的凸包作为一种有前景的解决方案应运而生，因为它能有效缩小变量范围并提供多神经元约束，从而提高验证精度。然而，由于构建精确的凸包在计算上非常昂贵，且在大多数情况下甚至不可行，现有研究主要集中在对其进行过度近似。针对ReLU和Sigmoid等特定函数，已经设计出了一些专门的方法。尽管如此，在开发适用于一般激活函数的方法方面仍存在较大差距。在这项工作中，我们提出了WraAct，这是一种高效构建激活函数凸包近似值的方法。其核心思想是通过引入线性约束来平滑目标函数中

  来源：Proceedings of the ACM on Programming Languages

  时间：2025-11-07

• Ephemera：通过利用内存文件系统加速I/O密集型无服务器工作负载的处理

  在当今快速发展的云计算环境中，服务器无状态计算（Serverless Computing）作为一种新兴的计算模式，正逐渐成为开发者和云服务提供商关注的焦点。它通过将服务器管理的复杂性从开发者转移到云服务提供商，为用户提供了更高效、更便捷的资源使用方式。然而，随着服务器无状态计算任务的多样化，如从简单的事件驱动任务到复杂的计算密集型任务，传统的文件系统在处理这些任务时暴露出了显著的性能瓶颈。特别是在I/O密集型任务中，文件输入输出（I/O）性能的优化成为提升整体系统效率的关键因素。### 1. 服务器无状态计算的发展与挑战服务器无状态计算的兴起可以追溯到AWS Lambda的推出，它改变了传统云

  来源：ACM Transactions on Architecture and Code Optimization

  时间：2025-11-07

• 为基础验证改进Verilog语义

  摘要在正式的硬件验证中，尤其是对于使用Verilog实现的寄存器传输级（RTL）设计，模型检验一直是主要的技术手段。然而，模型检验存在状态爆炸问题、表达能力有限以及需要较大的可信计算基础（TCB）等问题。演绎验证则具有更强的表达能力，并且能够在较小的TCB下完成基础性验证。尽管如此，Verilog的标准语义（其非确定性和全局调度特性）对其应用带来了重大挑战。为了解决这些问题，我们提出了一种新的Verilog语义，旨在促进演绎验证的进行。我们的新语义基于最小不动点理论，以实现周期级的功能评估和模块化推理。对于基础性验证，我们证明了这种新语义与可综合设计的标准调度语义等价。我们通过一个流水线RIS

  来源：Proceedings of the ACM on Programming Languages

  时间：2025-11-07

• 数据缓存分区在计算固态硬盘中的应用支持

  近年来，随着计算需求的不断增长，传统的存储设备如固态硬盘（SSD）的功能已经不再局限于数据存储。新型的计算型固态硬盘（CompSSD）逐渐成为研究热点，它不仅具备传统SSD的存储功能，还引入了计算能力，使得数据处理可以在存储设备内部完成，从而减轻主机与存储设备之间的数据传输负担。这种设计可以有效提升系统整体性能，特别是在处理大量数据时。然而，传统的缓存管理策略并未针对CompSSD的特性进行优化，导致在使用过程中缓存效率低下，影响了系统的I/O性能。为此，本文提出了一种新的缓存划分方法，以动态地将缓存空间划分为两部分，分别用于缓冲主机侧任务的输出数据和CompSSD侧任务的输入数据。CompS

  来源：ACM Transactions on Architecture and Code Optimization

  时间：2025-11-07

• 调度语言发展历程：过去、现在与未来

  在现代计算机科学领域，编译器和代码生成技术的发展一直是提升程序性能的重要手段。随着硬件架构的多样化和计算需求的复杂化，编译器的优化过程逐渐从传统的静态规则演进为一种更为灵活的调度语言机制。调度语言允许编译器或代码生成器以更结构化的方式表达一系列优化操作，为编译器的探索能力提供了更强大的接口。本文旨在探讨调度语言的历史演变、当前状态及未来发展方向，强调其在高性能计算中的关键作用，并指出当前存在的问题以及未来改进的方向。在过去的几十年中，编译器的优化策略主要依赖于启发式规则和固定算法，这在面对复杂的现代架构时显得力不从心。因此，研究者开始探索一种新的方法，即通过调度语言来表达优化策略，使编译器能够

  来源：ACM Transactions on Architecture and Code Optimization

  时间：2025-11-07

• EDAS：实现GPU无服务器计算中的快速数据加载

  在现代云计算环境中，GPU的集成正变得越来越重要，尤其是在需要高性能计算的任务中，例如深度学习推理和科学计算。这些任务通常需要快速访问大量数据，而GPU在执行计算任务时的高效性使得其成为处理这些任务的首选资源。然而，现有的GPU服务器端系统在数据加载方面存在显著的瓶颈，导致GPU的利用率低下。本文提出了一种名为EDAS的新系统，旨在解决这一问题，从而提升GPU在服务器端的性能表现。### 数据加载瓶颈与挑战现有的GPU服务器端系统，如阿里云的Function Compute和Azure Function，普遍采用固定大小的GPU资源分配模式（称为FixedGSL）。当一个GPU函数被触发时，系

  来源：ACM Transactions on Architecture and Code Optimization

  时间：2025-11-07

• 通过选择性扩展实现高效的抽象解释

  摘要抽象解释为静态分析提供了一个系统化的框架，在该框架中，扩展操作对于确保在分析无限高度格状结构上的程序时能够终止分析至关重要。当前的抽象解释器在所有被识别为需要扩展的变量（例如控制流循环头）上统一应用扩展操作和不动点检测，这导致了计算成本的增加。通过我们的实证研究，我们发现无限上升链通常仅源自参与值流循环的一部分变量，这为选择性扩展和有针对性的不动点检测提供了机会。本文介绍了一种通过基于值流分析的选择性扩展来优化非关系型域上的抽象解释的方法。我们开发了一种模块化且紧凑的值流图（MVFG），该图能够通过检测跨过程边界的值流循环来精确识别需要扩展的变量。我们的MVFG设计包含了高效的快捷边，这些

  来源：Proceedings of the ACM on Programming Languages

  时间：2025-11-07

• MetaEC：一种基于分散内存的高效且具备容错能力的擦除编码键值存储系统

  在当今数据处理需求不断增长的背景下，键值（Key-Value, KV）存储系统作为分布式存储的重要组成部分，正在经历从传统单一服务器架构向分离式内存（Disaggregated Memory, DM）架构的迁移。这种迁移旨在提升资源利用率和系统的弹性，同时保持高性能。然而，传统的KV存储系统通常依赖于复制（Replication）机制来实现容错功能，这种方式虽然有效，但会带来较高的存储开销。因此，研究人员开始探索使用纠删码（Erasure Coding, EC）作为替代方案，以提高存储效率。然而，在DM架构中直接实现EC技术存在性能瓶颈，主要是由于EC元数据管理的复杂性和一致性校验过程的挑战。

  来源：ACM Transactions on Architecture and Code Optimization

  时间：2025-11-07

• 用于对称属性的霍尔逻辑（A Hoare Logic for Symmetry Properties）

  摘要许多自然程序正确性属性可以通过对称性来表述，但现有的形式化方法在推理这些属性方面支持甚少。我们研究了如何形式化验证用群作用表达的广泛对称性属性。为了指定这些属性，我们设计了一种群作用的语法，支持标准的构造和一种自然的蕴含概念。接着，我们开发了一种Hoare风格的逻辑来验证命令式程序的对称性属性，在这种逻辑中，群作用替代了典型的前置条件和后置条件断言。最后，我们开发了一个原型工具SymVerif，并使用它来验证一系列手工制作的基准测试案例中的对称性属性。我们的工具发现了一个由McLachlan和Quispel在[Acta Numerica 2002]中描述的动态系统模型中的错误。

  来源：Proceedings of the ACM on Programming Languages

  时间：2025-11-07

• 将大型语言模型交织用于编译器测试

  摘要使用人工智能模型（尤其是大型语言模型，LLMs）来测试编译器展现出了巨大的潜力。然而，当前的方法面临两个关键问题：为测试编译器生成的程序往往过于简单，而利用LLMs进行大规模测试在计算上成本高昂。在本文中，我们提出了一种新颖的编译器测试框架，将测试过程分为两个独立的阶段：离线阶段和在线阶段。在离线阶段，我们利用LLMs生成一系列规模较小但功能丰富的代码片段；在在线阶段，通过策略性地组合这些代码片段来构建高质量且有效的测试程序，进而用于测试编译器。我们将这一理念实现在一个名为LegoFuzz的工具中，用于测试C编译器。测试结果非常显著：我们在GCC和LLVM（最广泛使用的C编译器）中发现了6

  来源：Proceedings of the ACM on Programming Languages

  时间：2025-11-07

• 利用迭代应用程序来提高分布式系统上基于任务的编程模型的可扩展性

  分布式任务模型，如OmpSs-2@Cluster、StarPU-MPI和PaRSEC，通过显式的任务依赖关系将高性能计算（HPC）应用程序表示为任务图。这些模型提供了一种统一的方式来表达并行性，涵盖CPU核心、加速器和分布式内存节点，相较于传统的MPI + X模型，显著提升了程序员的生产力。大多数基于任务的模型采用顺序构建任务图的方式，这种方式提供了清晰且熟悉的编程模型，简化了代码的开发、维护和移植。然而，这种设计引入了任务创建和依赖管理的瓶颈，限制了性能和可扩展性。因此，除非任务粒度非常粗，当前的分布式顺序任务模型无法达到MPI + X模型的性能水平。许多科学应用具有迭代特性，每个时间步都会

  来源：ACM Transactions on Architecture and Code Optimization

  时间：2025-11-07

• 一种用于推理推理过程的领域特定概率编程语言（或：关于“memo”的备忘录）

  摘要人类思考自身思维的能力（即“心智理论”）是许多学科研究的基本对象。近几十年来，来自这些学科的研究人员逐渐形成了一种基于递归概率推理的丰富计算范式来建模心智理论。然而，实际应用中人们常常发现这种范式的编程具有挑战性：首先，对程序员来说，“思考自身思维”的概念较为复杂；其次，相关模型的运行速度较慢。本文介绍了一种新的领域特定概率编程语言 memo，它克服了这些难题：一方面，通过为心智理论提供专门的语法和语义；另一方面，采用了一种独特的推理方法，该方法通过数组编程能够在现代硬件上实现高效运行。memo 使开发者能够用更少的代码编写出运行速度更快的模型，并已被多个研究团队采纳。

  来源：Proceedings of the ACM on Programming Languages

  时间：2025-11-07

知名企业招聘：