paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Robustness against the C/C++11 Memory Model

对 C/C++11 内存模型的鲁棒性
ISSTA Proceedings of the 33rd ACM SIGSOFT International Symposium on Software Testing and Analysis2024匹配度 3/10 · 论文关注 C/C++11 内存模型下的鲁棒性证明与程序验证，属于形式化验证/并发语义领域，但与用户核心方向 LLM/Agent 与静态分析、浮点程序分析或贝叶斯程序分析的交叉没有直接关系，仅泛相关。引用 0 inbox
Roy Margalit
并发、并行与内存模型程序验证
crossref: 2026-09-12

AI 速览

一句话：提出一种证明程序对 C/C++11 内存模型具有鲁棒性的方法，从而可在顺序一致性语义下推理且不牺牲性能。

并发程序正确性推理困难。顺序一致性（SC）语义便于推理，但同步开销高；C/C++11 内存模型试图在性能与推理之间取得平衡，却比预期复杂，连领域专家也难以掌握。本文提出一种方法，使程序员无需牺牲性能即可按 SC 语义推理程序正确性。其核心是证明程序相对于 C/C++11 内存模型的鲁棒性（robustness）：一旦程序被证明鲁棒，它只可能表现出 SC 行为，因此可以完全用 SC 语义进行推理。该方法为在弱内存模型下使用强语义推理提供了途径。

问题
在 C/C++11 弱内存模型下，并发程序的正确性推理非常复杂，而 SC 语义虽便于推理却带来高昂同步开销。
方法
提出通过证明程序对 C/C++11 内存模型的鲁棒性，使程序只表现出 SC 行为，从而可用 SC 语义推理并保留性能。
评估
摘要未报告具体实验、基准或机器化评估，只给出方法思路与鲁棒性证明带来的推理保证。
原文摘要（Abstract）

Concurrency is extremely useful, however reasoning about the correctness of concurrent programs is more difficult than ever. Sequential consistency (SC) semantics provide the ability to reason about correctness, however these come at a high synchronization cost. C11 introduced a memory model that was supposed to help with these problems, attempting to provide balance between performance and reasoning. However, this model was much more complicated than expected, proving to be a challenge even for domain experts. We propose a method that enables the programmer to reason about correctness with SC semantics without compromising performance. By proving robustness of a program it can only exhibit SC behaviors and can thus be reasoned about with SC semantics.

链接与引用

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

BibTeX 
@inproceedings{paperbot8501,
  title = {Robustness against the C/C++11 Memory Model},
  author = {Roy Margalit},
  booktitle = {ISSTA},
  year = {2024},
  doi = {10.1145/3650212.3685549}
}