RacerF: Lightweight Static Data Race Detection for C Code
本文提出RacerF，一种基于Frama-C平台的轻量级静态分析工具，通过上下近似方法实现线程模块化数据竞争检测，在保证高精度的同时提升检测速度。
2025-06-18 cs.PL cs.SE
A True Positives Theorem for a Static Race Detector - Extended Version
RacerD是一个静态竞争检测器，在工程实践中被证明是有效的：它已经看到了开发人员在进入生产之前修复的数千个数据竞争，并支持Facebook的Android应用渲染基础设施从单线程迁移到多线程架构。我们证明了一个真阳性定理，即在某些假设下，分析的理想化理论版本永远不会报告假阳性。我们还提供了一个实证评估的实施这种分析，与原来的RacerD。在第一种情况下，该定理的动机是希望了解RacerD为开发人员提供非常准确的信号的生产观察结果，然后该定理指导了进一步的分析仪设计决策。从技术上讲，我们的结果可以被看作是说，分析计算过近似的欠近似，这是静态分析中更常见的（过或欠）情况的相反。到目前为止，静态分析，在实践中是有效的，但不健全的往往被认为是特设的，相反，我们建议，在未来，这种品种的定理可能是普遍有用的理解，证明和设计有效的静态分析的错误捕捉。
2018-11-08 cs.PL
Instrumentation Optimization for Practical Dynamic Race Detection
National University of Singapore（新加坡国立大学）；Saint Petersburg Electrotechnical University "LETI"（圣彼得堡电气大学）
通过静态分析消除冗余仪器化，显著降低动态数据竞赛检测器的运行时开销，提升性能。
2026-10-20 cs.OS cs.PL cs.SE
Pointer Race Freedom
我们提出了一个新的概念指针竞争的并发程序操纵一个共享堆。指针竞争是对已释放的内存地址的访问，无论单元是否已重新分配，都不受访问者的控制。我们建立了两个结果。(1)在指针竞争自由的假设下，验证一个程序在显式存储管理下运行，就像它在垃圾回收下运行一样是合理的。(2)甚至指针竞争自由本身的要求也可以在垃圾收集语义下得到验证。然后，我们证明了类似的定理，一个更强的概念，指针种族需要处理性能关键的代码，故意使用活泼的比较，甚至活泼的指针引用。作为一个实际的贡献，我们应用我们的结果来优化显式存储管理下的线程模块化分析。我们的实验证实了高达两个数量级的加速。
2015-11-11 cs.PL
Dependence-Aware, Unbounded Sound Predictive Race Detection
数据竞争是并行软件的一个真正问题，但很难检测。可靠的预测分析会观察程序执行，并检测存在于其他未观察到的执行中的数据竞争。然而，现有的预测分析错过了比赛，因为它们不能扩展到完整的程序执行，或者没有精确地结合数据和控制依赖。本文介绍了两种新的，健全的预测方法，将数据和控制的依赖性，并处理完整的程序执行。使用真实的，大型的Java程序的评估表明，这些方法检测更多的数据竞争比最接近的相关方法，从而推进了最先进的声音预测竞争检测。
2021-06-28 cs.PL
Efficient Data Race Detection of Async-Finish Programs Using Vector Clocks
现有的基于任务的程序的数据竞争检测器招致显著的运行时间和空间开销。开销的产生是因为频繁地在细粒度树数据结构中查找以检查两个访问是否可以并行发生。这项工作表明，如何有效地应用向量时钟的动态数据竞争检测的锁的完成程序。我们提出的技术，FastRacer，建立在FastTrack算法与每个任务和每个变量的优化，以减少向量时钟的大小。FastRacer利用了并行程序的结构化并行性，使用动态任务继承关系的粗粒度编码来限制多个并发读取器存在时的元数据。我们的评估表明，FastRacer大大提高了FastTrack的时间和空间开销，并与最先进的数据竞争检测器的锁完成程序。
2022-04-05 cs.PL
Ready, set, Go! Data-race detection and the Go language
数据竞争经常在锁获取和释放的背景下讨论，竞争检测算法通常依赖于向量时钟作为捕获来自不同线程的事件的相对顺序的方法。在本文中，我们提出了一个数据竞争检测器的语言与通道通信作为其唯一的同步原语，并提供了一个语义直接绑定到之前发生的关系，从而锻造向量时钟的概念。
2020-01-15 cs.PL cs.SE
CPC: programming with a massive number of lightweight threads
线程是编写并发程序的一种方便和模块化的抽象，但通常相当昂贵。线程的标准替代方案，事件循环编程，允许更轻的并发单元，但导致代码难以编写，甚至更难理解。Continuation Passing C（CPC）是一个翻译器，可根据程序员的选择，将以线程风格编写的程序转换为使用事件和本机系统线程编写的程序。我们与两名本科生一起，通过编写Hekate自学了如何在CPC中编程，Hekate是一个大规模并发网络服务器，旨在有效地处理成千上万的同时连接的对等体。在本文中，我们描述了一些编程习惯用法，我们在写Hekate时学到的;虽然其中一些习惯用法是特定于CPC的，但许多应该适用于其他具有足够便宜的线程的编程系统。
2011-02-04 cs.PL
Efficient, Near Complete and Often Sound Hybrid Dynamic Data Race Prediction (extended version)
动态数据竞争预测的目标是基于由跟踪表示的单个程序运行来识别竞争。挑战是保持效率，同时尽可能健全和完整。高效意味着线性运行时间，否则该方法不可能用于现实世界的程序。我们介绍了一个有效的，接近完整的，通常是健全的动态数据竞争预测方法，结合锁集方法与几个改进的发生在该地区之前的方法。通过接近完成，我们的意思是该方法在理论上是完整的，但出于效率原因，实现应用了一些可能导致不完整性的优化。该方法可以被证明是两个线程的声音，但一般是不健全的。我们提供了大量的实验数据，表明我们的方法在实践中效果良好。
2022-05-18 cs.PL
Petrification: Software Model Checking for Programs with Dynamic Thread Management (Extended Version)
本文针对动态 fork/join 线程的并发程序验证，提出 petrification 转换，将其归约为基于 Petri 网的固定线程数形式化体系，并在支持 pthreads 的 C 程序模型检测工具中实现。
2023-11-02 cs.PL
Predicting All Data Race Pairs for a Specific Schedule (extended version)
我们考虑的问题，数据竞争预测程序的行为是由一个跟踪。跟踪是在程序执行期间记录的程序事件序列。我们采用可重复的发生之前的关系，以表征所有对的事件，在一个比赛中的时间表表现在跟踪。与经典的happens-before关系相比，可扩展的happens-before关系适当地处理了写-读依赖关系，从而避免了误报。挑战是有效地识别所有（可识别的）数据竞争对。我们提出了一个改进的线性时间向量时钟算法来预测许多可重复的数据竞争对。我们引入了二次时间后处理算法来预测所有剩余的数据竞争对。这提高了该领域的技术水平，我们的实验表明，我们的方法可以扩展到现实世界的例子。因此，用户可以系统地检查和修复在特定时间表的竞争中的所有节目位置。
2019-09-07 cs.PL
Lost in Abstraction: Monotonicity in Multi-Threaded Programs (Extended Technical Report)
并发系统中的单调性规定，在任何全局状态下，当新进程添加到该状态时，现存的系统操作仍然是可执行的。这个概念在多线程软件中不仅是自然和常见的，而且很有用：如果每个线程的内存是有限的，单调性通常保证安全属性验证的可判定性，即使在运行线程的数量未知的情况下。在本文中，我们表明，获得有限数据线程抽象的模型检验的行为可能与单调性不一致：谓词抽象某些广泛使用的单调软件的结果在非单调的多线程布尔程序的单调性是失去了抽象。其结果是，完善的健全和完整的安全检查算法变得不适用，事实上，安全检查原来是不可判定的无界线程布尔程序类。我们演示了如何将抽象程序修改为单调程序，而不影响非单调抽象的安全属性。这显着改进了早期通过过度逼近来强制单调性的方法。
2014-06-24 cs.PL
Predictive Data Race Detection for GPUs
GPU中的高度并行性和相对复杂的同步机制使得编写正确的内核变得困难。数据竞争造成了这样一个并发正确性的挑战，因此，需要检测尽可能多的数据竞争的有效方法。CPU程序的预测偏序关系旨在暴露动态执行过程中可能隐藏的数据竞争。由于编程模型的差异，现有的预测偏序不能简单地应用于分析GPU内核。这项工作提出了GWCP，预测偏序GPU内核的数据竞争检测。GWCP将多线程共享内存CPU程序中提出的一种合理而精确的关系称为弱因果优先关系（WCP）扩展到GPU内核。GWCP考虑了GPU线程层次结构和不同的同步语义，如屏障同步和作用域原子和锁。我们实现了一个名为PreDataR的工具，使用二进制仪表跟踪GWCP关系。PreDataR包括三个优化和一个新的矢量时钟压缩方案，这些方案很容易适用于其他基于偏序的分析。我们的评估与几个微基准测试和基准测试表明，PreDataR有更好的数据竞争覆盖率相比，以前的技术在实际运行时的开销。
2021-11-24 cs.PL
Model Checking Race-freedom When "Sequential Consistency for Data-race-free Programs" is Guaranteed
针对无数据竞争程序的顺序一致性保证下如何验证所有SC执行无竞争的问题，提出对模型检测做少量修改即可有效验证无竞争特性，并在OpenMP并行化的C程序集上进行了探索。
2023-07-20 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
Computing Race Variants in Message-Passing Concurrent Programming with Selective Receives
消息传递并发性是一种流行的计算模型，它是几种程序设计语言的基础，Erlang、Akka，以及（在某种程度上）Go和Rust。特别是，我们考虑一个消息传递并发语言与动态进程产卵和选择性接收，即，其中消息只能在它们匹配特定约束时被目标进程消费（例如，Erlang的例子）。在这项工作中，我们引入了一个跟踪的概念，它可以被看作是一类因果等价执行的抽象（即，产生相同的结果）。然后，我们表明，执行跟踪可以用来识别消息竞争。我们提供了建设性的定义来计算消息竞赛以及产生所谓的竞赛变体，然后可以用来驱动新的执行，这些新的执行在因果关系上不等同于以前的执行。这是用于程序验证的状态空间探索技术的基本组成部分。
2022-10-06 cs.PL
RacerF: Data Race Detection with Frama-C (Competition Contribution)
RacerF是基于Frama-C的静态分析插件，采用启发式方法结合欠/过逼近技术分析多线程C程序的数据竞争，在SV-COMP'25的NoDataRace-Main子类别中排名第二，仅产生4个误报。
2025-02-27 cs.PL cs.SE
A Partial Order Reduction Technique for Event-driven Multi-threaded Programs
事件驱动的多线程编程正在迅速成为开发高效和响应式应用程序的首选风格。在这种并发模型中，多个线程并发执行，通过共享对象进行通信，并发布按到达顺序执行的异步事件。在这项工作中，我们考虑事件驱动的多线程程序的部分降阶（POR）。现有的POR技术将与线程相关联的事件队列视为共享对象，从而对同一线程上处理的每对事件进行重新排序，即使重新排序它们不会导致不同的状态。我们不把事件队列作为共享对象，并提出了一种新的POR技术的基础上一种新的回溯集称为依赖覆盖集。由同一线程处理的事件仅在必要时才由POR技术重新排序。我们证明，探索依赖覆盖集足以检测所有的死锁周期和断言违反定义的局部变量。为了评估我们的POR方案的有效性，我们实现了一个动态算法来计算依赖覆盖集。从几个Android应用程序的执行轨迹，我们证明了我们的技术探索少得多的过渡-往往数量级少-相比，探索基于持久集，其中，事件队列被认为是共享对象。
2017-10-16 cs.PL
Degrees of Separation: A Flexible Type System for Data Race Prevention
提出捕获分离演算（System CSC），通过允许一般别名但在必要时跟踪控制别名，实现非侵入性的静态数据竞争防止，并验证其类型安全与合流性。
2023-09-14 cs.PL
From Single-thread to Multithreaded: An Efficient Static Analysis Algorithm
现在已经开发了各种各样的计算单线程程序安全性的静态分析。本文提出了一个系统的方法来扩展一类这样的静态分析，使他们处理程序与多个POSIX风格的线程。从语用操作语义学出发，我们建立了一个指称语义，表示推理的一个假设保证。最后的算法，然后通过抽象的解释。它依次分析每个线程，传播线程之间的干扰以及其他语义信息。组合爆炸，随之而来的明确考虑的所有交织，从而避免。与单线程情况相比，最坏情况的复杂度仅增加了n倍，其中n是程序中的指令数。我们已经实现了原型工具，证明了该方法的实用性。
2009-10-30 cs.PL
The Effect Race in Fine-Grained Concurrency
现有的大多数工作需要了解程序指令（或语句）的作用来分析和验证算法。本文通过揭示目标程序执行的一些发现，定义了两个基本概念--效果等价关系和效果竞争关系。进一步，我们证明了关于种族和历史的三个效应定理。其核心结论是：效应种族关系是捕捉内部步骤的精确关系，其中的优先顺序是导致混沌历史的原因。此外，将对象验证中广泛使用的线性化点概念形式化地定义为典型效应竞争关系。这些结果为分析复杂的细粒度执行提供了清晰的基础。我们进行了大量的实验，真实的对象算法，以显示这些定义在实践中的准确性和效率。并对这些算法提出了一种简单的定量分析方法。
2018-02-07 cs.PL
Modular Verification of Concurrent Programs via Sequential Model Checking
这项工作利用了过多的工作验证顺序程序的目的，验证并发程序。我们减少了一个并发程序的验证一系列的顺序程序的验证任务。我们的方法是模块化的，在这个意义上，每个顺序的验证任务大致对应于一个线程的验证，与一些额外的信息，它在其中运行的环境。根据需要，在算法运行期间收集关于环境的信息。虽然我们的方法是通用的，它专门针对线程层次结构的并发程序。这个想法是利用层次结构，以最大限度地减少需要在线程之间传输的信息量。为此，我们验证的线程之一，认为“主”，作为一个顺序程序。它的验证过程向它的“环境”（可能包含多个线程）发起查询。如果环境由单个线程组成，则通过顺序验证来回答这些查询，否则，通过在环境上应用相同的分层算法来回答这些查询。我们的技术是全自动的，并允许我们使用任何现成的顺序模型检查器。我们实现了我们的技术在一个工具，称为CoMuS和评估它对建立并发验证工具。我们的实验表明，它的工作特别好的层次结构的程序。
2021-06-01 cs.PL
Competitive Parallelism: Getting Your Priorities Right
多线程程序传统上分为两个领域：合作和竞争。这两个领域在传统上大多保持不相交，协作线程用于提高计算密集型应用程序（如科学工作负载）的吞吐量，而协作线程用于提高交互式应用程序（如GUI和游戏）的响应能力。随着多核硬件变得越来越主流，有必要将这两个不相交的世界连接起来，因为许多应用程序将交互和计算混合在一起，并且将从协作线程和竞争线程中受益。在本文中，我们提出了技术的并行交互式应用程序，可以使用合作和竞争线程的编程和推理。我们的技术使程序员编写丰富的并行交互式程序，创建和同步线程需要，并通过分配线程用户定义的和部分有序的优先级。为了确保重要的响应特性，我们提出了一个模态类型系统类似于S4模态逻辑，排除低优先级线程延迟高优先级线程，从而静态地防止一组关键的优先级反转错误。然后，我们提出了一个成本模型，允许推理良好类型的程序的响应和完成时间。成本模型扩展了传统的工作跨度模型的合作线程，以考虑到竞争的调度决策，以确保响应。最后，我们证明了我们提出的技术是现实的，通过将它们实现为标准ML语言的扩展。
2018-07-10 cs.PL
On the Value and Limits of Multi-level Energy Consumption Static Analysis for Deeply Embedded Single and Multi-threaded Programs
降低计算能耗的兴趣越来越大。能量透明是一个概念，它使程序的能量消耗从软件到硬件通过不同的系统层可见。这样的透明性可以在每一层和层之间实现能量优化，并且帮助程序员和操作系统两者做出能量感知决策。提取程序能耗的常用方法是直接测量目标硬件。这通常涉及大多数程序员不具备的专业设备和知识。在本文中，我们将研究如何利用现有的静态资源分析和能源建模方法来执行能源消耗静态分析（ECSA）的深度嵌入式程序。为了研究这一点，我们已经开发了ECSA技术，工作在指令集的水平和更高的水平，LLVM IR，通过一种新的映射技术。我们将ECSA应用于一组全面的主要工业基准测试，包括来自两种常用并发模式（任务农场和管道）的单线程和多线程嵌入式程序。我们比较我们的ECSA结果的硬件测量和预测的基础上获得的模拟痕迹。我们讨论了一些应用场景，ECSA的结果可以提供能源透明度，并得出结论，为今后的工作提出了一系列新的研究问题。
2015-10-24 cs.PL
Dynamic Robustness Verification Against Weak Memory (Extended Version)
针对标准动态竞态检测与弱内存模型不兼容的问题，提出基于位置时钟的动态鲁棒性验证算法，并在工具RSAN中实现，实现对弱内存的有效防御。
2025-04-21 cs.PL
WarpDRF: The Unwritten Contract of GPU Warp Programming
University of California at Santa Cruz（加州大学圣克鲁兹分校）；University of Massachusetts Boston（马萨诸塞大学波士顿分校）；Microsoft Research（微软研究院）
WarpDRF提出首个精确的抽象warp编程模型，定义数据竞争自由契约，通过形式化证明和模糊测试验证，并扩展静态分析器以检测GPU内核中的未知数据竞争。
2026-10-08 cs.PL
RaceFixer -- An Automated Data Race Fixer
提出自动化修复单变量原子性违规并发缺陷的工具 RaceFixer，结合 ThreadSanitizer 报告与静态分析生成并合并补丁，提升修复质量、性能与代码可读性。
2024-01-08 cs.PL cs.SE
Variable and Thread Bounding for Systematic Testing of Multithreaded Programs
以前的方法，系统的状态空间探索测试多线程程序提出了上下文绑定和深度绑定是有效的排名算法测试多线程程序。本文提出了两个新的指标来排名线程调度系统的状态空间探索。我们的指标基于使用v（表现错误所需的不同变量的最小数量）和t（表现错误所需的调度约束的不同线程的最小数量）对并发错误的描述。我们的算法是基于这样的假设，即在实践中，大多数并发错误具有低v（通常为1 - 2）和低t（通常为2 - 4）的特性。我们以v和t的递增顺序迭代地探索调度的搜索空间。我们定性和经验表明，我们的算法发现常见的错误，在较少的执行运行次数，与以前的方法相比。我们还表明，使用v和t提高了通过随机算法发现错误的概率的下限。系统地探索时间表需要对程序进行的每个变量访问进行检测，这可能非常昂贵，并且严重限制了这种方法的适用性。以前的工作[5，19]通过只在同步操作上插入（并忽略其他变量访问）来避免这个问题。我们证明，通过使用变量绑定（v）和静态不精确的别名分析，我们可以在所有变量访问（而不仅仅是同步操作）上进行同步，开销比以前的方法少10 - 100倍。
2013-02-05 cs.PL
Provable GPU Data-Races in Static Race Detection
我们扩展了Faial工具链背后的理论，该理论可以充分证明CUDA程序（又名内核）使用称为内存访问协议（MAP）的专门行为类型是无数据竞争的。在本文中，我们扩展理论的地图来表征内核的报警可以被识别为真正的报警。我们介绍了CUDA的核心演算，我们将其命名为BabyCUDA，以及它的行为类型系统。我们表明，如果可以为BabyCUDA程序分配MAP，那么Faial对此程序发出的任何警报都是真正的警报。
2022-03-24 cs.DC cs.PL
LLOV: A Fast Static Data-Race Checker for OpenMP Programs
在Exascale计算时代，编写高效的并行程序是必不可少的，同时，编写好的并行程序是非常困难的。与诸如OpenMP之类的框架的并行性是相对容易的，但是这些程序中的数据竞争是错误的重要来源。在本文中，我们提出了LLOV，一个快速，轻量级，语言无关，静态的数据竞争检查的基础上的LLVM编译器框架的OpenMP程序。我们比较LLOV与其他国家的最先进的数据竞赛检查各种完善的基准。我们表明，精度，准确性和F1得分的LLOV是可比的其他跳棋，而数量级更快。据我们所知，LLOV是最先进的数据竞争检查器中唯一可以验证C/C++或FORTRAN程序是否无数据竞争的工具。
2020-09-01 cs.LO cs.PL cs.SE
Static Race Detection and Mutex Safety and Liveness for Go Programs (extended version)
Go是一种流行的并发程序设计语言，这要归功于它能够有效地结合并发和系统编程。在Go程序中，许多并发错误可能是由数据竞争和通信问题引起的。在本文中，我们开发了一种基于行为类型的理论来静态检测Go程序中的数据竞争和死锁。我们首先使用Go内存模型中定义的happens-before关系，在Go程序模型上指定锁安全性、活动性和数据竞争属性。我们表示这些属性的程序中的$μ$演算模型的类型，并验证它们使用类型级别的模型检查。然后，我们扩展了框架，以考虑Go的通道，并实现了一个静态验证工具，可以检测并发错误。据我们所知，这是Go语言的第一个此类静态验证框架，统一分析了由共享内存访问和异步消息传递通信混合引起的并发错误。
2021-11-18 cs.LO cs.PL
Checking Race Freedom of Clocked X10 Programs
更好地利用并行性的许多方法之一（现在已经成为主流）是引入并行程序设计语言。然而，并行性本质上是不确定的，并且并非所有的并行错误都可以通过语言设计来避免。本文提出了一种方法，以保证没有数据竞争的多面体子集的时钟X10程序。X10中的时钟与barrier类似，但更加动态;参与同步的进程子集可以在运行时动态更改。我们构建的时钟X10程序的发生之前的关系，并表明，竞争检测的问题是不可判定的。然而，在许多实际情况下，现代工具能够找到解决方案或证明其不存在。我们提出了一套基准的分析是可能的，并有一个可接受的运行时间。
2013-11-18 cs.DC cs.PL
Flow-Sensitive Composition of Thread-Modular Abstract Interpretation
我们提出了一个基于约束的流敏感的静态分析并发程序通过迭代组成线程模块化的抽象解释器，通过使用一个系统的轻量级约束。我们的方法是组合的，因为它首先将顺序抽象解释器应用于各个线程，然后组合它们的结果。它是流敏感的，因为干扰的因果关系排序（从全局写入到读取的数据流）是由约束系统建模的。这些干扰约束是轻量级的，因为它们只涉及程序语句的执行顺序，而不是它们的数值属性：它们可以使用现成的数据库引擎有效地决定。我们的新方法的优势是更准确的比现有的，流不敏感的，静态分析，同时保持可扩展性，并提供预期的健全性和终止保证，即使是无限数据的程序。我们实现了我们的方法，并在大量的基准测试中进行了评估，证明了它在提高线程模块化抽象解释的准确性方面的有效性。
2017-09-28 cs.PL
Fast, Sound and Effectively Complete Dynamic Race Prediction
由于进程间通信的不确定性，编写并发程序非常容易出错。并发性中最可靠的错误指示器是数据竞争，即对可以连续执行的共享资源的访问。研究了基于锁的并发程序中的数据竞争预测问题。输入由并发跟踪$t$组成，任务是确定构成数据竞争的$t$的所有事件对。这一问题是同时核查的核心，三十多年来一直得到广泛研究。然而，现有的多项式时间声音技术是高度不完整的，可能会错过许多简单的比赛。在这项工作中，我们开发M2：一个新的多项式时间算法，这个问题，它没有误报。此外，我们的算法是完整的输入轨迹，包括两个过程，即，它可以检测到跟踪中的所有种族。我们还开发了充分条件动态检测完整性的情况下，两个以上的进程。我们的算法的一组标准的基准测试，从最近的文献中的主题进行了实验评估。我们的工具可以很好地报告数千场比赛，在整个基准测试集中最多错过一场比赛。此外，我们的技术检测基准集的所有活泼的内存位置。最后，它的运行时间是可比的，而且往往小于理论上最快的，但高度不完整的，现有的方法。据我们所知，M2是第一个在运行时间和所报告比赛的完整性上实现这种性能水平的可靠算法。
2019-11-05 cs.PL
Dynamic Choreographies - Safe Runtime Updates of Distributed Applications
编写没有通信死锁和竞争的分布式应用程序是复杂的。当应用程序在运行时更新时，保留这些属性就更难了。我们提出了DIOC，一种用于编程分布式应用程序的语言，该语言通过构造而免于死锁和竞争。DIOC程序将整个分布式应用程序描述为一个独特的实体（编排）。DIOC允许程序员指定应用程序的哪些部分可以更新。在运行时，这些部分可以被来自应用程序外部的新DIOC片段替换。DIOC程序是用一种称为DPOC的低级语言编译的，为每个站点生成代码。我们正式的DIOC和DPOC语义标记的过渡系统，并证明编译的正确性作为一个跟踪等价的结果。作为推论，DPOC应用程序没有通信死锁和竞争，即使在运行时更新的情况下也是如此。
2015-03-31 cs.PL
Continuation-Passing C: compiling threads to events through continuations
在本文中，我们介绍了连续传递C（CPC），一个程序设计语言的并发系统中，本地和合作线程是统一的，并提交给程序员作为一个单一的抽象。CPC编译器使用基于CPS转换的编译技术，可以生成高效的代码和极其轻量级的上下文表示。我们提供了一个证明我们的编译方案的正确性。我们表明，特别是，升降机，一种常见的编译技术的函数式语言，也是正确的，在一个命令式语言，如C，在某些条件下强制执行的CPC编译器。目前的CPC编译器已经足够成熟，可以编写大量的程序，比如Hekate，一个高度并发的BitTorrent种子程序。我们的基准测试结果表明，CPC是有效的，而使用显着更少的空间，作为最有效的线程库可用。
2012-07-05 cs.PL
Data Race Prediction for Inaccurate Traces
基于之前发生的数据竞争预测方法从事件的踪迹推断部分顺序以检查一个事件是否在另一个事件之前发生。如果两个两个写事件是无序的，那么它们处于竞争中。我们观察到，常见的跟踪方法不能保证跟踪顺序对应于实际的程序运行。追踪不准确的后果是报告的结果（种族）不准确。我们引入诊断方法来检查（1）一个种族是否保证是正确的，而不管任何潜在的不准确性，（2）可能是不正确的，由于不准确的跟踪。我们已经完全实现了这种方法，并提供了一个经验的比较与国家的最先进的发生之前，基于比赛的预测，如FastTrack和SHB。
2019-10-26 cs.PL
Proving Liveness of Parameterized Programs
多线程程序的正确性通常要求它们满足活性属性。例如，程序可能要求没有线程缺少共享资源，或者所有线程最终都同意一个值。本文提出了一种方法来证明这样的活性性质举行。在这项工作中解决的两个特殊挑战是：（1）正确性论证可能依赖于系统的全局行为（例如，正确性论证可以要求所有线程共同地朝着“好的事情”前进，而不是一个线程前进而其它线程不干扰），以及（2）这样的程序通常被设计成由任何数量的线程执行，并且所期望的活跃度属性必须保持，而不管程序中活动的线程的数量如何。
2016-05-08 cs.LO cs.PL
Effect Summaries for Thread-Modular Analysis
我们提出一种新的猜测和检查的原则，以提高无锁数据结构的线程模块验证的效率。我们建立在一个启发式的猜测候选人的无状态效果摘要的程序，通过搜索代码的实例的复制和检查编程习惯用法常见的无锁数据结构。这些候选摘要用于计算线性时间内线程间的干涉。由于候选摘要不需要是音效摘要，我们展示了如何完全自动地检查候选摘要的精度是否足够。因此，我们可以执行健全的验证，尽管依赖于不健全的启发式。我们已经实施了我们的方法，发现它比现有的方法快了两个数量级。
2017-05-10 cs.PL
Portability of Optimizations from SC to TSO
本文研究编译器优化跨并发内存模型的移植问题，提出从SC到TSO可移植优化的全局约束，并证明其与禁止引入三角竞争相关，同时关联到SRA模型的移植。
2025-04-24 cs.PL
Towards Bug-Free Distributed Go Programs
本文针对 Go 分布式程序中的通信竞争问题，提出基于扩展至有缓冲与无缓冲通道的 happens-before 顺序的静态验证框架，以证明程序不存在通信竞争。
2025-07-25 cs.LO cs.PL cs.SE
OpenMP aware MHP Analysis for Improved Static Data-Race Detection
数据竞争是并发程序中错误的一个主要来源，它会导致人力和时间的损失以及由于系统故障而导致的数据丢失。在HPC社区中使用的事实上的共享内存并行框架OpenMP也受到数据竞争的影响。为了检测OpenMP程序中的竞争条件并提高周转时间和/或开发人员的生产力，我们在LLVM编译器框架中提出了一种基于数据流分析的快速静态数据竞争检查器。我们的工具可以检测种族的存在或不存在显式的障碍，隐式或显式同步。此外，我们的工具有效地为OpenMP目标卸载结构，也支持常用的OpenMP结构。我们形式化并提供了一个数据流分析框架来执行OpenMP程序的相位间隔分析（PIA）。相位间隔，然后用于计算MHP（及其补充NHP）集的程序，这反过来又被用来检测数据竞争静态。我们评估我们的工作使用多个OpenMP竞争检测基准和现实世界中的应用程序。我们的实验表明，该检查器在各种性能指标方面与最先进的检查器相当，准确率约为90%，几乎完美的召回率，并且运行时间和内存占用量显着降低。
2021-11-08 cs.PL cs.SE
Delay-Bounded Scheduling Without Delay! (Extended Technical Report)
我们认为，在任意线程交织的异步并发程序的安全性分析的广泛问题。延迟有界的确定性调度，介绍了在以前的工作中，是一个有效的错误发现技术，以遏制与充分的调度不确定性的大成本。在本文中，我们首先提出了一种技术，以解除有限域变量程序的情况下的延迟界，从而增加了效率的错误检测的能力，证明安全的程序在任意线程交织。其次，我们展示了如何，结合谓词抽象，我们的技术可以反驳和验证安全属性的程序与无界的变量域，即使是无限的线程数。以前的工作已经建立，对于非平凡的并发例程，谓词抽象诱导一个高度复杂的抽象程序语义。然而，我们的技术，从来没有静态地构造一个抽象的参数化程序，它只需要一些抽象状态集在某些行动下被关闭，从而消除了对存在的抽象程序的验证算法的依赖。我们证明了我们的技术在以前的工作中使用的许多例子的效率，并展示其简单性相比，早期的方法在无限线程票锁协议。
2021-05-15 cs.PL
Data Race Detection on Compressed Traces
我们认为，已被压缩使用直线程序（SLP），这是特殊的上下文无关文法，正好产生一个字符串，即跟踪，他们表示的程序痕迹中的数据竞争检测的问题。我们考虑两种经典的方法来进行竞争检测-使用happens-before关系和锁集规则。我们提出了这两种方法的算法，运行的时间是线性的压缩，SLP表示的大小。典型的程序执行几乎总是表现出导致显著压缩的模式。因此，我们的算法预计会导致大的加速比相比，分析未压缩的痕迹。我们对这些新算法在标准基准上的实验评估证实了这一观察结果。
2018-07-23 cs.PL cs.SE
A Model of Cooperative Threads
我们开发了一个模型的并发命令式编程线程。我们专注于一个小的命令式语言与合作的线程，执行无中断，直到他们终止或显式地产生控制。我们定义并研究了这种语言的基于跟踪的指称语义，这种语义是完全抽象的，但数学上是初等的。我们还给出了一个方程理论的计算效果，基础的语言，包括线程产卵。然后，我们分析线程的自由代数单子这个理论。
2010-10-20 cs.PL
CUBA: Interprocedural Context-UnBounded Analysis of Concurrent Programs (Extended Manuscript)
Ramalingam关于同步敏感的过程间程序分析的一个经典结果表明，运行递归过程的并发线程的可达性是不可判定的。由Qadeer和Jesus of提出的一种技术，限制线程之间允许的上下文切换的数量，导致了一个不完整的解决方案，但是，相信在实践中可以捕获“大多数错误”。该技术是否也可以证明至少在某些情况下没有错误的问题在很大程度上仍然是开放的。在本文中，我们介绍了一个广泛的验证方法，观察资源参数的变化如何影响程序的行为的资源参数化的程序。应用于上下文无界分析问题（CUBA），该方法的结果在部分验证技术的过程并发程序。我们的解决方案可能不会终止，但能够反驳和证明并发递归线程的上下文无界安全。我们证明了我们的方法的有效性，使用各种各样的例子，其中的安全不能被证明是安全的早期，上下文有界的方法。
2018-04-13 cs.PL
A family of abstract interpretations for static analysis of concurrent higher-order programs
我们开发了一个框架，计算两个基本的分析并发高阶程序：（控制）流分析（CFA）和可能发生的并行分析（MHP）。我们特别关注的独特挑战所带来的不受限制的混合一流的延续和动态生成的线程。为了设置阶段，我们制定了一个具体的模型并发高阶程序：P（CEK*）S机。我们发现，这台机器的系统抽象的解释是能够计算流量和MHP分析。然而，仔细检查发现，MHP的精度很差。作为一种补救措施，我们采用了形状分析技术单例抽象动态产生的线程（而不是堆中的对象）。然后，我们表明，如果MHP分析是不感兴趣的，我们可以大大加快计算流分析单独崩溃线程交织与第二层的抽象。
2011-06-14 cs.PL
Thread-modular Analysis of Release-Acquire Concurrency
我们提出了一个线程模块化的抽象解释（TMAI）技术来验证程序下的释放获取（RA）的内存模型的安全属性侵犯。我们的工作的主要贡献是：我们捕获的程序语句的执行顺序作为一个抽象的域，并提出了一个健全的上近似在这个域有效地原因RA并发。所提出的域在其应用中是通用的，并且捕获了作为抽象解释理论中的第一类特征的排序关系。特别地，域将并发程序中全局变量的修改序列的集合表示为偏序集合。在这种近似下，全局变量的较旧的sequenced-before存储被遗忘，并且仅保留每个变量的最新存储。我们建立我们提出的抽象的合理性，并在一个原型抽象解释器PRIORI中实现它们。PRIORI对现有的和具有挑战性的RA基准的评估表明，所提出的技术不仅在反驳方面具有竞争力，而且在验证方面也具有竞争力。与最近最先进的RA并发工具相比，PRIORI显示出更高的精度和更快的分析运行时间。
2021-08-17 cs.PL
A Light-Weight Approach for Verifying Multi-Threaded Programs with CPAchecker
由于增加每个CPU插槽的处理单元数量的强烈趋势，因此多线程程序变得越来越重要。我们介绍了一种新的可配置的程序分析验证多线程程序的线程数有限。我们提出了一个简单而有效的实现现有的程序验证框架CPAchecker的组成部分。虽然CPAchecker已经在一个大型的基准集的顺序验证任务的竞争力，我们的扩展增强了框架的整体适用性。我们处理多线程的实现与数据流分析的抽象域是正交的，因此，可以与CPAcchecker中的几种现有分析相结合，如值分析，区间分析和BDD分析。新的分析是模块化的，可以用来，例如，验证可达性属性以及检测程序中的死锁。本文包括一些优化步骤的效益评估（例如，改变可达性算法的迭代顺序或应用偏序约简）以及与用于验证多线程程序的其它现有技术工具的比较。
2016-12-15 cs.LO cs.PL cs.SE
Thread and Memory-Safe Programming with CLASS
CLASS是一种基于线性逻辑的通用线性编程语言，通过类型系统自动保证线程与内存安全、无死锁及终止性，支持并发编程、惰性流和智能合约资产操作。
2025-05-27 cs.LO cs.PL
Static Analysis of Run-Time Errors in Embedded Real-Time Parallel C Programs
我们提出了一个静态分析的抽象解释检查运行时间错误的并行和多线程的C程序。在我们的工作Astrée，我们专注于嵌入式关键程序没有递归，也没有动态内存分配，但扩展到一个静态的线程集的分析，通过共享内存和显式地使用一组有限的互斥锁隐式通信，并根据实时的【形】调度策略和固定的优先级调度。我们的方法是线程模块化的。它是基于一个稍微修改的非平行分析，当分析一个线程，应用和丰富的一组抽象的线程冲突。然后迭代器依次重新分析每个线程，直到冲突稳定下来。我们证明了我们的方法的可靠性顺序一致性语义，但也相对于一个合理的弱一致的内存语义。我们还展示了如何考虑互斥和线程优先级，通过分区的抽象调度状态。我们展示了使用原型Thésée分析工业程序的初步实验结果，并展示了我们方法的可扩展性。
2012-03-22 cs.LO cs.PL
Correctness Witnesses for Concurrent Programs: Bridging the Semantic Divide with Ghosts (Extended Version)
本文提出一种基于幽灵的并发程序正确性见证格式，使交错语义与线程模块化语义下的见证有效性一致，并在SV-COMP基准上验证了其可行性。
2024-11-25 cs.PL
Reference Capabilities for Safe Parallel Array Programming
数组是一种基本的数据结构，它提供了一种有效的方法来存储和检索内存中连续的非稀疏数据。由于现代存储层次结构的设计，阵列对于许多内存密集型应用程序的性能非常重要：连续存储有助于空间局部性和预测访问模式，从而实现预取。大型数组上的操作通常很适合并行化，例如fork-join风格的分治排序算法。为了使阵列上的并行操作具有确定性，必须保证数据竞争自由。对于原始数据数组上的操作，通过协调访问来获得数据竞争自由，以便没有两个线程对相同的数组索引进行操作。然而，由于别名，这对于非原语数组是不够的：访问单独的数组元素可能会返回指向同一对象或重叠结构的指针。引用能力在过去已经成功地用于静态地保证面向对象程序中没有数据竞争。本文介绍了引用功能的第一个扩展--称为数组功能--它支持对原始值和非原始值的数组进行并发和并行操作。除了元素访问之外，数组功能还支持数组的抽象操作、将数组逻辑拆分为子数组以及合并子数组。这些操作允许表达广泛的数组用例。本文介绍了阵列能力设计空间，并展示了它如何应用于许多阵列用例。核心思想是形式化的，并在一个简单的微积分中得到了证明，同时证明了具有数组功能的良好类型的程序是没有数据竞争的。
2019-08-05 cs.PL
What Happens - After the First Race? Enhancing the Predictive Power of Happens - Before Based Dynamic Race Detection
动态竞争检测是确定所观察到的程序执行是否揭示程序中存在数据竞争的问题。解决这个问题的经典方法是检测是否有一对冲突的内存访问是无序的Lamport的happens-before（HB）关系。已知基于HB的种族检测不报告假阳性，即，它是健全的。然而，HB的可靠性保证仅承诺第一对无序的冲突事件是可消除的数据竞争。也就是说，可能存在作为不可并行竞争的HB无序冲突数据访问对，因为不存在对执行事件的重新排序，其中竞争中的事件可以在彼此之后立即执行。我们引入了一个新的偏序，称为可调度的发生之前（SHB），它准确地描述了可调度的数据竞赛对-每对由SHB识别的冲突数据访问都可以被调度，并且每一个可以被调度的HB竞赛都由SHB识别。因此，SHB偏序是真正合理的。我们提出了一个线性时间，矢量时钟算法来检测使用SHB可识别的种族。我们的实验表明，我们的算法的动态竞争检测的价值- SHB只会产生很小的性能开销，可以扩展到执行从现实世界的软件应用程序，而不损害健全性。
2018-08-01 cs.PL cs.SE
