Efficient Data Race Detection of Async-Finish Programs Using Vector Clocks
现有的基于任务的程序的数据竞争检测器招致显著的运行时间和空间开销。开销的产生是因为频繁地在细粒度树数据结构中查找以检查两个访问是否可以并行发生。这项工作表明，如何有效地应用向量时钟的动态数据竞争检测的锁的完成程序。我们提出的技术，FastRacer，建立在FastTrack算法与每个任务和每个变量的优化，以减少向量时钟的大小。FastRacer利用了并行程序的结构化并行性，使用动态任务继承关系的粗粒度编码来限制多个并发读取器存在时的元数据。我们的评估表明，FastRacer大大提高了FastTrack的时间和空间开销，并与最先进的数据竞争检测器的锁完成程序。
2022-04-05 cs.PL
Optimal Prediction of Synchronization-Preserving Races
众所周知，并发程序很难正确编写，因为调度的不确定性引入了难以检测和重现的细微错误。最常见的并发错误是（数据）争用，当并发执行内存冲突操作时会发生这种错误。因此，已经做出了相当大的努力来开发用于种族检测的有效技术。最常见的方法是动态竞争预测：给定一个并发程序的观察到的、无竞争的跟踪$σ$，任务是决定$σ$的事件是否可以被正确地重新排序到一个跟踪$σ^*$，该跟踪见证了隐藏在$σ$中的竞争。在这项工作中，我们介绍了同步（hronization）保持种族的概念。当存在其中同步操作（例如，锁的获取和释放）以与$σ$中相同的顺序出现。这是一个广义的定义，严格包含了著名的“比赛前发生”的概念。我们的主要结果如下。首先，我们开发了一个健全的和完整的算法预测同步保持种族。对于中等值的参数（如线程数），算法在$\widetilde{O}(\mathcal{N})$时间和空间中运行，其中$\mathcal{N}$是跟踪$σ$的长度。其次，我们证明了该问题有一个$Ω(\mathcal{N}/\log^2 \mathcal{N})$空间下界，因此我们的算法本质上是时间和空间最优的。第三，我们表明，预测比赛，即使只是一个单一的逆转两个同步操作是$\operatorname{NP}$ -完整的，甚至$\operatorname{W}[1]$ -硬参数时，线程的数量。因此，同步保护的特点正是比赛预测的易处理边界…
2020-10-30 cs.PL
Computing Race Variants in Message-Passing Concurrent Programming with Selective Receives
消息传递并发性是一种流行的计算模型，它是几种程序设计语言的基础，Erlang、Akka，以及（在某种程度上）Go和Rust。特别是，我们考虑一个消息传递并发语言与动态进程产卵和选择性接收，即，其中消息只能在它们匹配特定约束时被目标进程消费（例如，Erlang的例子）。在这项工作中，我们引入了一个跟踪的概念，它可以被看作是一类因果等价执行的抽象（即，产生相同的结果）。然后，我们表明，执行跟踪可以用来识别消息竞争。我们提供了建设性的定义来计算消息竞赛以及产生所谓的竞赛变体，然后可以用来驱动新的执行，这些新的执行在因果关系上不等同于以前的执行。这是用于程序验证的状态空间探索技术的基本组成部分。
2022-10-06 cs.PL
A Practical Analysis of Rust's Concurrency Story
正确的并发程序很难编写;当多个线程改变共享数据时，它们可能会丢失写入、损坏数据或产生不稳定的程序行为。虽然并发性的许多数据竞争问题可以通过在代码中放置锁来避免，但这些问题通常会使程序执行串行化，并且会显着降低性能关键型应用程序的速度。程序员也会犯错误，并且经常忘记执行较少的代码路径中的锁，这导致程序仅在极少数情况下行为不当。Rust是Mozilla最近推出的一种程序设计语言，它试图通过在编译时检测数据竞争来解决这些相互交织的问题。Rust的类型系统编码了数据结构在类型系统中的线程之间共享的能力，这反过来允许编译器拒绝线程直接改变共享状态而没有锁或其他保护机制的程序。在这项工作中，我们研究了Rust类型系统的这一方面如何影响并发数据结构的开发和改进，以及它适应正确性由低级不变量保证的情况的能力（例如，在无锁算法中）不能直接在类型系统本身中表达。我们详细介绍了并发无锁散列表的实现，以描述Rust语言的这些特性。我们的代码可以在https://github.com/saligrama/concache上公开获得，并且是Rust语言中最快的并发散列表之一，这导致了并发程序中的瓶颈。
2019-04-27 cs.DC cs.PL
Dynamic Data-Race Detection through the Fine-Grained Lens
数据竞争是并发中最常见的错误之一。数据竞争检测的标准方法是通过动态分析，它在并发程序的执行上工作，而不是程序源代码。关于该主题的丰富文献已经创建了动态数据竞争的各种概念，已知当某些参数（例如，线程数）很小。然而，所有这些种族概念的\emph{fine-grained}复杂性仍然难以捉摸，使得不可能描述它们在精度和效率之间的权衡。在这项工作中，我们建立了几个细粒度的分离之间的许多流行的概念的动态数据竞争。输入是包含$N$事件、$T$线程和$L$锁的执行跟踪。我们的主要结果如下。首先，我们证明了在$O(N\cdot \min(T, L))$时间内可以检测到之前发生的（HB）种族，当$L=o(T)$结合时，其优于标准$O(N\cdot T)$。此外，我们表明，即使报告HB比赛，涉及读访问是很难为2-正交向量（2-OV）。这是第一次严格证明了检测HB竞赛的二次下界。其次，我们表明，最近推出的同步保持种族是很难检测到OV-3，因此有一个立方下界，当$T=Ω(N)$。这建立了一个复杂性分离HB种族是已知的表达较少。第三，我们表明，锁覆盖比赛是很难的2-OV，因此有一个二次下界，即使当$T=2$和$L = ω(\log N)$。锁集竞争的类似概念已知在$O(N\cdot L)$时间内是可检测的，因此我们实现了两者之间的复杂度分离。此外，我们表明，锁集种族成为击中集（HS）硬时，$L=Θ(N)$，…
2021-07-08 cs.CC cs.PL
Efficient and Reasonable Object-Oriented Concurrency
使线程程序安全且易于推理是现代编程的主要困难之一。这项工作提供了一个有效的执行模型SCOOP，并发的方法，不仅提供数据竞争的自由，但也前/后条件推理线程之间的保证。我们提出的扩展影响了底层语义，以增加可能的并发执行量，排除某些类别的死锁，并实现更高的性能。这些扩展被用作高效运行时和优化的基础，其性能比基线实现提高了15倍。SCOOP的这种新实现也比其他知名的安全并发语言快2倍。测量基于协调密集型和数据操作密集型基准，旨在提供混合工作负载。
2015-07-27 cs.DC cs.PL
DR.FIX: Automatically Fixing Data Races at Industry Scale
Uber Technologies（Uber技术公司）；Aarhus University（奥胡斯大学）
本文提出Dr.Fix工具，结合大语言模型与程序分析，在工业规模下自动修复Go语言数据竞争，经Uber实践验证，在404个竞争案例中成功生成224个补丁，其中86%被开发者接受。
2025-04-22 cs.AI cs.DC cs.LG
Gobra: Modular Specification and Verification of Go Programs (extended version)
Go是一种越来越流行的系统程序设计语言，特别是针对并发和分布式系统。Go语言与其他命令式语言的不同之处在于，它通过goroutine提供了结构化的子类型和轻量级的并发性以及消息传递通信。这些特性的组合为静态验证提出了有趣的挑战，最突出的是可变堆和高级并发原语的组合。我们提出Gobra，一个模块化的，演绎的程序验证器，证明内存安全，崩溃安全，数据竞争自由，和用户提供的规范。Gobra基于分离逻辑，支持Go语言的一个大子集。它的实现将带注释的Go程序转换为Viper中间验证语言，并使用现有的基于SMT的验证后端来计算和履行证明义务。
2021-05-28 cs.PL
ReLoC Reloaded: A Mechanized Relational Logic for Fine-Grained Concurrency and Logical Atomicity
本文提出ReLoC Reloaded，一种基于Iris框架的机械化关系分离逻辑，用于证明高阶状态与细粒度并发程序的精化关系，并扩展了逻辑原子关系规范，支持预言变量以增强实用性。
2021-07-20 cs.LO cs.PL
GPUMC: A Stateless Model Checker for GPU Weak Memory Concurrency
GPUMC是一种无状态模型检查器，用于在scoped-RC11弱内存模型下检查GPU共享内存并发程序，能探索所有执行以发现竞争、障碍发散和断言违反，并自动修复错误，在时间和内存上高效，优于现有工具。
2025-05-26 cs.LO cs.PL cs.SE
ActorScript(TM) extension of C sharp (TM), Java(TM), and Objective C(TM): iAdaptive(TM) concurrency for antiCloud(TM) privacy and security
ActorScript（TM）是一种通用程序设计语言，用于实现管理资源和需求的自主、自适应并发。它与以前的语言的区别在于：-通用性 * 指定Actor可以做什么的能力 * 指定硬件和软件之间的接口 * 语言中的一切都是使用消息传递完成的，包括ActorScript本身的定义 * 集成了函数式，命令式，逻辑和并发编程。* 并发动态适应可用资源和当前负载。* 程序不暴露低级别的实现机制，如线程，任务，锁，核心等。* 消息可以直接通信，而无需通过代理，通道，类层次结构，邮箱，管道，端口，队列等间接。* 消除了变量竞争。* 二进制XML和JSON是数据类型。* 提供了应用程序二进制接口，因此在运行时不需要查找标识符符号。- 安全和安全 * 程序是扩展不变的，即，扩展一个程序并不改变它的意义。* 应用程序不能直接相互伤害。- 性能 * 对Actor系统的实现不施加任何开销 * 消息传递的开销与过程调用和循环的开销基本相同。* 允许根据系统负载和容量（例如核心）动态调整执行 * 局部性，因为执行不受顺序全局内存模型的约束 * 固有并发性，因为执行不受通信顺序进程的约束 * 最大限度地减少关键路线上的延迟
2015-03-04 cs.DC cs.PL
VeriFast's separation logic: a logic without laters for modular verification of fine-grained concurrent programs
本文首次对VeriFast逻辑支持高阶幽灵代码以实现无需later模态的细粒度并发模块验证进行了形式化与可靠性证明，并与Iris等逻辑进行了比较。
2025-10-13 cs.PL
Fray: An Efficient General-Purpose Concurrency Testing Platform for the JVM (Extended Version)
Fray 是一个针对 JVM 的通用并发测试平台，通过影子锁定机制实现无需替换并发原语的受控线程交错，在基准测试中发现更多错误，并在真实项目中成功发现并发缺陷。
2025-08-27 cs.DC cs.PL cs.SE
Fine-grained Causal Reversibility for Asynchronous Channel-based Programming
Graduate School of Informatics, Nagoya University（名古屋大学情报学研究科）；Department of Computer Science, University of Oxford（牛津大学计算机科学系）；University of Bari Aldo Moro（巴里阿尔多·莫罗大学）
本文提出revGo，针对Go语言的无界异步通道，通过重排序队列中无因果关系的独立消息，实现最小性的回滚与重放，用于调试并发系统的并发错误。
2026-09-01 cs.PL
Sound Dynamic Deadlock Prediction in Linear Time
本文证明了可靠且完备的死锁预测难解性，提出“保持同步死锁”新概念，并设计了两种线性时间的可靠死锁预测算法，适用于离线与在线监控场景。
2023-06-25 cs.LO cs.PL
Compositional Non-Interference for Fine-Grained Concurrent Programs
非干扰性是一种程序属性，可确保不存在信息泄漏。在程序设计语言的上下文中，有两种常见的方法来建立非干扰：类型系统和程序逻辑。类型系统提供了强大的自动化（通过类型检查），但它们在它们支持的程序类型方面有固有的限制。程序逻辑支持具有挑战性的程序，但它们通常需要大量的人工帮助，并且不能处理模块或更高阶的程序。为了连接这两种方法，我们提出了SeLoC-一种非干扰的分离逻辑，在此基础上，我们使用逻辑关系技术建立了一个类型系统。通过在分离逻辑之上构建类型系统，我们可以组合地验证由类型化和非类型化部分组成的程序。前一部分通过型式检验进行验证，后一部分通过人工校对进行验证。SeLoC的核心技术贡献是最弱前提条件的关系形式，可以使用分离逻辑资源跟踪信息流。SeLoC是完全机器检查的，并且构建在Iris框架之上，用于Coq中的并发分离逻辑。与Iris的集成为细粒度并发提供了无缝支持，这是之前的类型系统和程序逻辑无法实现的无干扰性。
2020-03-06 cs.LO cs.PL
Program Execution on Reconfigurable Multicore Architectures
基于两个观察，即不同的应用程序在不同的多核架构上执行得更好，以及应用程序的不同阶段可能具有非常不同的资源需求，Jesus等人提出了一种用于执行多线程程序的新的可重构硬件方法。该体系结构不是将并发程序映射到固定的体系结构，而是自适应地重新配置自身以满足应用程序的并发性和通信要求，从而显著提高了性能。基于我们早期的抽象操作框架，多核执行与层次存储器结构，我们描述了多线程程序的可重构架构，支持各种集群配置的执行。由于可能引入由在不同核上运行的线程对共享存储器的并发访问引起的竞争条件，这种重新配置可能不保留程序的语义。我们提出了一个直观的偏序概念的集群配置，并表明，多线程程序的语义总是保留重新配置“向上”的顺序，而语义保存任意重新配置可以保证良好的同步程序。我们进一步表明，一个简单的近似概念的执行效率上的不同配置可以得到使用摊销互模拟的概念，并将其扩展到动态重新配置。
2016-06-20 cs.DC cs.PF cs.PL
An approach for modularly verifying the core of Rust's atomic reference counting algorithm against the (Y)C20 memory consistency model
提出一种模块化验证方法，通过交错操作语义连接 (Y)C20 公理模型与 Iris 等并发程序逻辑，以验证 Rust ARC 核心且不依赖程序序与 reads-from 并集无环假设。
2025-09-26 cs.PL
