paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Probabilistic Concurrency Testing for Weak Memory Programs

面向弱内存程序的概率并发测试
ASPLOS Proceedings of the 28th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 22023匹配度 2/10 · 该论文研究弱内存模型下的概率并发测试，属于程序分析与测试/形式化方法，但不涉及用户核心关注的 LLM/Agent 与静态分析结合、浮点程序分析或贝叶斯程序分析。其问题驱动和理论保证虽有价值，但与当前研究画像交叉点很少。引用 8 inbox
Mingyu Gao, Soham Chakraborty, Burcu Kulahcioglu Ozkan
并发、并行与内存模型测试、调试与修复
crossref: 2026-09-12

AI 速览

一句话：提出适用于弱内存程序的概率并发测试，以在弱内存语义下保持并发缺陷检测的概率保证。

概率并发测试（PCT）算法能在顺序一致性语义下为检测并发缺陷提供理论概率保证，但该算法无法直接应用于弱内存程序。其根本原因在于 PCT 建立在顺序一致性的交错语义之上，而弱内存并发允许出现无法由任何交错执行产生的额外行为。本文针对弱内存程序研究概率并发测试，目标是在弱内存语义下重新建立并发缺陷检测的概率保证，从而覆盖超出传统交错语义的弱内存执行。摘要未给出具体方法与实验评估细节。

问题
现有 PCT 算法的理论保证依赖顺序一致性交错语义，不能适用于弱内存并发程序。
方法
论文面向弱内存程序提出概率并发测试方法，需要在弱内存语义下处理无法由交错执行产生的额外行为并重新建立检测概率保证。
评估
摘要未说明具体评估方式与实验结果。
原文摘要（Abstract）

The Probabilistic Concurrency Testing (PCT) algorithm that provides theoretical guarantees on the probability of detecting concurrency bugs does not apply to weak memory programs. The PCT algorithm builds on the interleaving semantics of sequential consistency, which does not hold for weak memory concurrency. It is because weak memory concurrency allows additional behaviors that cannot be produced by any interleaving execution.

链接与引用

DOI 原文 · PDF（开放获取） ·

BibTeX 
@inproceedings{paperbot10014,
  title = {Probabilistic Concurrency Testing for Weak Memory Programs},
  author = {Mingyu Gao and Soham Chakraborty and Burcu Kulahcioglu Ozkan},
  booktitle = {ASPLOS},
  year = {2023},
  doi = {10.1145/3575693.3575729}
}